Zachary Anderson
David Gay
Eric Brewer
ABSTRACT
Unintended or unmediated data sharing is a frequent cause of insidious bugs in multithreaded programs. We present a tool called SharC (short for Sharing Checker) that allows a user to write lightweight annotations to declare how they believe objects are being shared between threads in their program. SharC uses a combination of static and dynamic analyses to check that the program conforms to this specification.
SharC allows any type to have one of five "sharing modes" -- private to the current thread, read-only, shared under the control of a specified lock, intentionally racy, or checked dynamically. The dynamic mode uses run-time checking to verify that objects are either read-only, or only accessed by one thread. This allows us to check programs that would be difficult to check with a purely static system. If the user does not give a type an explicit annotation, then SharC uses a static type-qualifier analysis to infer that it is either private or should be checked dynamically.
SharC allows objects to move between different sharing modes at runtime by using reference counting to check that there are no other references to the objects when they change mode.
SharC's baseline dynamic analysis can check any C program, but is slow, and will generate false warnings about intentional data sharing. As the user adds more annotations, false warnings are reduced, and performance improves.We have found in practice that very few annotations are needed to describe all sharing and give reasonable performance. We ran SharC on 6 legacy C programs, summing to over 600k lines of code, and found that a total of only 60 simple annotations were needed to remove all false positives and to reduce performance overhead to only 2-14%.
- Agarwal, R., Sasturkar, A.,Wang, L., and Stoller, S. D. Optimized run-time race detection and atomicity checking using partial discovered types. In ASE?05. Google Scholar
Digital Library
- Anderson, Z. R., Gay, D., Ennals, R., and Brewer, E. SharC: Checking data sharing strategies for multithreaded C. Tech. Rep. UCB/EECS-2008-25, EECS Department, University of California, Berkeley, Mar 2008.Google ScholarDigital Library
- Boyapati, C., Lee, R., and Rinard, M. Ownership types for safe programming: preventing data races and deadlocks. In OOPSLA?02, pp. 211--230. Google ScholarDigital Library
- Cheng, G.-I., Feng, M., Leiserson, C. E.,Randall, K. H., and Stark, A. F. Detecting data races in Cilk programs that use locks. In SPAA?98, pp. 298--309. Google ScholarDigital Library
- Choi, J.-D., Lee, K., Loginov, A., O?Callahan, R., Sarkar, V., and Sridharan, M. Efficient and precise datarace detection for multithreaded object-oriented programs. In PLDI?02, pp. 258--269. Google ScholarDigital Library
- Condit, J., Harren, M., Anderson, Z., Gay, D., and Necula, G. Dependent types for low-level programming. In ESOP?07. Google ScholarDigital Library
- Elmas, T., Qadeer, S., and Tasiran, S. Goldilocks: a race and transaction-aware Java runtime. In PLDI?07, pp. 245--255. Google ScholarDigital Library
- Engler, D., and Ashcraft, K. RacerX: effective, static detection of race conditions and deadlocks. In SOSP?03, pp. 237--252. Google ScholarDigital Library
- Flanagan, C., and Freund, S. N. Atomizer: a dynamic atomicity checker for multithreaded programs. In POPL?04, pp. 256--267. Google ScholarDigital Library
- Foster, J. S., Fahndrich, M., and Aiken, A. A theory of type qualifiers. In PLDI?99, pp. 192--203. Google ScholarDigital Library
- freedesktop.org. Gstreamer: Open source multimedia framework. http://gstreamer.freedesktop.org/.Google Scholar
- Frigo, M. A fast Fourier transform compiler. In PLDI?99, pp. 169--180. Google ScholarDigital Library
- Gay, D., Ennals, R., and Brewer, E. Safe manual memory management. In ISMM?07 (New York, NY, USA, 2007), ACM, pp. 2--14. Google ScholarDigital Library
- Grossman, D. Type-safe multithreading in Cyclone.Google Scholar
- Henzinger, T. A., Jhala, R., and Majumdar, R. Race checking by context inference. In PLDI?04, pp. 1--13. Google ScholarDigital Library
- Levanoni, Y., and Petrank, E. An on-the-fly reference-counting garbage collector for Java. ACM Transactions on Programming Languages and Systems 28, 1 (2006), 1--69. Google ScholarDigital Library
- Naik, M., Aiken, A., and Whaley, J. Effective static race detection for Java. In PLDI?06, pp. 308--319. Google ScholarDigital Library
- Necula, G. C., Condit, J., Harren, M.,McPeak, S., and Weimer, W. CCured: Type-safe retrofitting of legacy software. ACM Transactions on Programming Languages and Systems 27, 3 (May 2005). Google ScholarDigital Library
- Pratikakis, P., Foster, J. S., and Hicks, M. Locksmith: contextsensitive correlation analysis for race detection. In PLDI?06, pp. 320--331. Google ScholarDigital Library
- Qadeer, S., and Wu, D. KISS: keep it simple and sequential. In PLDI?04, pp. 14--24. Google ScholarDigital Library
- Sasturkar, A.,Agarwal, R.,Wang, L., and Stoller, S. D. Automated type-based analysis of data races and atomicity. In PPoPP?05, pp. 83--94. Google ScholarDigital Library
- Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., and Anderson, T. Eraser: a dynamic data race detector for multi-threaded programs. In SOSP?97, pp. 27--37. Google ScholarDigital Library
- Sen, K., and Agha, G. A race-detection and flipping algorithm for automated testing of multi-threaded programs. In Haifa Verification Conference (2006), pp. 166--182. Google ScholarDigital Library
- US-CERT. Technical cyber security alerts. http://www.us-cert.gov/cas/techalerts/index.html.Google Scholar
- Voung, J. W., Jhala, R., and Lerner, S. RELAY: static race detection on millions of lines of code. In ESEC-FSE?07, pp. 205--214. Google ScholarDigital Library
- Yu, Y., Rodeheffer, T., and Chen,W. Racetrack: efficient detection of data race conditions via adaptive tracking. In SOSP?05, pp. 221--234. Google ScholarDigital Library
Index Terms
- SharC: checking data sharing strategies for multithreaded c
Recommendations
SharC: checking data sharing strategies for multithreaded c
PLDI '08Unintended or unmediated data sharing is a frequent cause of insidious bugs in multithreaded programs. We present a tool called SharC (short for Sharing Checker) that allows a user to write lightweight annotations to declare how they believe objects are ...
Sharc: Managing CPU and Network Bandwidth in Shared Clusters
Abstract--In this paper, we argue the need for effective resource management mechanisms for sharing resources in commodity clusters. To address this issue, we present the design of Sharc--a system that enables resource sharing among applications in such ...
Model-checking task-parallel programs for data-race
AbstractMany of the correctness properties afforded by task-parallel programming models such as OpenMP, Cilk, X10, Chapel, Habanero, etc. rely on data-race freedom. The research in this paper studies data-race in the context of these models with the ...
Comments