SharC: checking data sharing strategies for multithreaded c

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%.

REFERENCES

• 1: Rahul Agarwal , Amit Sasturkar , Liqiang Wang , Scott D. Stoller, Optimized run-time race detection and atomicity checking using partial discovered types, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101944]
• 2: 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.
• 3: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 4: Guang-Ien Cheng , Mingdong Feng , Charles E. Leiserson , Keith H. Randall , Andrew F. Stark, Detecting data races in Cilk programs that use locks, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.298-309, June 28-July 02, 1998, Puerto Vallarta, Mexico [doi>10.1145/277651.277696]
• 5: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 6: Condit, J., Harren, M., Anderson, Z., Gay, D., and Necula, G. Dependent types for low-level programming. In ESOP?07.
• 7: Tayfun Elmas , Shaz Qadeer , Serdar Tasiran, Goldilocks: a race and transaction-aware java runtime, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 8: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 9: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 10: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 11: freedesktop.org. Gstreamer: Open source multimedia framework. http://gstreamer.freedesktop.org/.
• 12: Matteo Frigo, A fast Fourier transform compiler, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.169-180, May 01-04, 1999, Atlanta, Georgia, United States
• 13: David Gay , Rob Ennals , Eric Brewer, Safe manual memory management, Proceedings of the 6th international symposium on Memory management, October 21-22, 2007, Montreal, Quebec, Canada [doi>10.1145/1296907.1296911]
• 14: Grossman, D. Type-safe multithreading in Cyclone.
• 15: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Race checking by context inference, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 16: Yossi Levanoni , Erez Petrank, An on-the-fly reference-counting garbage collector for java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.1-69, January 2006 [doi>10.1145/1111596.1111597]
• 17: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 18: George C. Necula , Jeremy Condit , Matthew Harren , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy software, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.3, p.477-526, May 2005 [doi>10.1145/1065887.1065892]
• 19: Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 20: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 21: Amit Sasturkar , Rahul Agarwal , Liqiang Wang , Scott D. Stoller, Automated type-based analysis of data races and atomicity, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065956]
• 22: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multi-threaded programs, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.27-37, October 05-08, 1997, Saint Malo, France
• 23: 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.
• 24: US-CERT. Technical cyber security alerts. http://www.us-cert.gov/cas/techalerts/index.html.
• 25: Jan Wen Voung , Ranjit Jhala , Sorin Lerner, RELAY: static race detection on millions of lines of code, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287654]
• 26: Yuan Yu , Tom Rodeheffer , Wei Chen, RaceTrack: efficient detection of data race conditions via adaptive tracking, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

General Terms:
Languages

Keywords:
data-race