ABSTRACT
Concurrent programming errors arise when threads share data incorrectly. Programmers often avoid these errors by using synchronization to enforce a simple ownership policy: data is either owned exclusively by a thread that can read or write the data, or it is read owned by a set of threads that can read but not write the data. Unfortunately, incorrect synchronization often fails to enforce these policies and memory errors in languages like C and C++ can violate these policies even when synchronization is correct.
In this paper, we present a dynamic analysis for checking ownership policies in concurrent C and C++ programs despite memory errors. The analysis can be used to find errors in commodity multi-threaded programs and to prevent attacks that exploit these errors. We require programmers to write ownership assertions that describe the sharing policies used by different parts of the program. These policies may change over time, as may the policies' means of enforcement, whether it be locks, barriers, thread joins, etc. Our compiler inserts checks in the program that signal an error if these policies are violated at runtime. We evaluated our tool on several benchmark programs. The run-time overhead was reasonable: between 0 and 49% with an average of 26%. We also found the tool easy to use: the total number of ownership assertions is small, and the asserted specification and implementation can be debugged together by running the instrumented program and addressing the errors that arise. Our approach enjoys a pleasing modular soundness property: if a thread executes a sequence of statements on variables it owns, the statements are serializable within a valid execution, and thus their effects can be reasoned about in isolation from other threads in the program.
- P. Akritidis, C. Cadar, C. Raiciu, M. Costa, and M. Castro. Preventing memory error exploits with WIT. In IEEE Symposium on Security and Privacy, May 2008. Google ScholarDigital Library
- Z. Anderson, D. Gay, and M. Naik. Lightweight annotations for controlling sharing in concurrent data structures. In PLDI, 2009. Google ScholarDigital Library
- Z. Anderson, D. Gay, and M. Naik. Lightweight annotations for controlling sharing in concurrent data structures. In PLDI, 2009. Google ScholarDigital Library
- C. Cao Minh, J. Chung, C. Kozyrakis, and K. Olukotun. Stamp: Stanford transactional applications for multi-processing. In IISWC, 2008.Google Scholar
- M. Castro, M. Costa, J. Martin, M. Peinado, P. Akritidis, A. Donnelly, P. Barham, and R. Black. Fast byte-granularity software fault isolation. In SOSP, 2009. Google ScholarDigital Library
- Q. Chen, L. Wang, Z. Yang, and S. D. Stoller. HAVE: Detecting atomicity violations via integrated dynamic and static analysis. In FASE, 2009. Google ScholarDigital Library
- J. Condit, M. Harren, Z. Anderson, D. Gay, and G. Necula. Dependent types for low-level programming. In ESOP, 2007. Google ScholarDigital Library
- T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transaction-aware Java runtime. In PLDI, 2007. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. Sci. Comput. Program., 71(2):89--109, 2008. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. FastTrack: efficient and precise dynamic race detection. In PLDI, 2009. Google ScholarDigital Library
- C. Flanagan, S. N. Freund, and J. Yi. Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs. In PLDI, 2008. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In PLDI, 2003. Google ScholarDigital Library
- K. Glerum, K. Kinshumann, S. Greenberg, G. Aul, V. Orgovan, G. Nichols, D. Grant, G. Loihle, and G. Hunt. Debugging in the (very) large: Ten years of implementation and experience. In SOSP'09, 2009. Google ScholarDigital Library
- C. Hammer, J. Dolby, M. Vaziri, and F. Tip. Dynamic detection of atomic-set-serializability violations. In ICSE, 2008. Google ScholarDigital Library
- P. Joshi, M. Naik, C.-S. Park, and K. Sen. CalFuzzer: An extensible active testing framework for concurrent programs. In CAV, 2009. Google ScholarDigital Library
- R. J. Lipton. Reduction: a method of proving properties of parallel programs. Commun. ACM, 18(12):717--721, 1975. Google ScholarDigital Library
- M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI, 2008. Google ScholarDigital Library
- Phoenix. http://connect.microsoft.com/phoenix.Google Scholar
- P. Pratikakis, J. S. Foster, and M. Hicks. Context-sensitive correlation analysis for detecting races. In PLDI, 2006. Google ScholarDigital Library
- S. Rajamani, G. Ramalingam, V. P. Ranganath, and K. Vaswani. Isolator: dynamically ensuring isolation in comcurrent programs. In ASPLOS, 2009. Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst., 15(4):391--411, 1997. Google ScholarDigital Library
- L.Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In PPoPP, 2006. Google ScholarDigital Library
Index Terms
- Dynamically checking ownership policies in concurrent c/c++ programs
Recommendations
Dynamically checking ownership policies in concurrent c/c++ programs
POPL '10Concurrent programming errors arise when threads share data incorrectly. Programmers often avoid these errors by using synchronization to enforce a simple ownership policy: data is either owned exclusively by a thread that can read or write the data, ...
Randomized active atomicity violation detection in concurrent programs
SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineeringAtomicity is an important specification that enables programmers to understand atomic blocks of code in a multi-threaded program as if they are sequential. This significantly simplifies the programmer's job to reason about correctness. Several modern ...
Race directed random testing of concurrent programs
PLDI '08Bugs in multi-threaded programs often arise due to data races. Numerous static and dynamic program analysis techniques have been proposed to detect data races. We propose a novel randomized dynamic analysis technique that utilizes potential data race ...
Comments