Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

The trend towards processors with more and more parallel cores is increasing the need for software that can take advantage of parallelism. The most widespread method for writing parallel software is to use explicit threads. Writing correct multithreaded programs, however, has proven to be quite challenging in practice. The key difficulty is non-determinism. The threads of a parallel application may be interleaved non-deterministically during execution. In a buggy program, non-deterministic scheduling will lead to non-deterministic results - some interleavings will produce the correct result while others will not.

We propose an assertion framework for specifying that regions of a parallel program behave deterministically despite non-deterministic thread interleaving. Our framework allows programmers to write assertions involving pairs of program states arising from different parallel schedules. We describe an implementation of our deterministic assertions as a library for Java, and evaluate the utility of our specifications on a number of parallel Java benchmarks. We found specifying deterministic behavior to be quite simple using our assertions. Further, in experiments with our assertions, we were able to identify two races as true parallelism errors that lead to incorrect non-deterministic behavior. These races were distinguished from a number of benign races in the benchmarks.

REFERENCES

• 1: Sarita V. Adve , Mark D. Hill , Barton P. Miller , Robert H. B. Netzer, Detecting data races on weak memory systems, Proceedings of the 18th annual international symposium on Computer architecture, p.234-243, May 27-30, 1991, Toronto, Ontario, Canada
• 2: 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]
• 3: Gul Agha, Actors: a model of concurrent computation in distributed systems, MIT Press, Cambridge, MA, 1986
• 4: Zachary Anderson , David Gay , Rob Ennals , Eric Brewer, SharC: checking data sharing strategies for multithreaded c, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 5: C. Artho, K. Havelund, and A. Biere. High-level data races. Software Testing Verification and Reliability, 13(4):207--227, 2003.
• 6: K. Asanovic, R. Bodik, J. Demmel, T. Keaveny, K. Keutzer, J. D. Kubiatowicz, E. A. Lee, N. Morgan, G. Necula, D. A. Patterson, K. Sen, J. Wawrzynek, D. Wessel, and K. A.Yelick. The parallel computing laboratory at U.C. berkeley: A research agenda based on the Berkeley view. Technical Report UCB/EECS-2008-23, EECS Department, University of California, Berkeley, Mar 2008.
• 7: Greg Barnes, A method for implementing lock-free shared-data structures, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.261-270, June 30-July 02, 1993, Velen, Germany [doi>10.1145/165231.165265]
• 8: Robert D. Blumofe , Christopher F. Joerg , Bradley C. Kuszmaul , Charles E. Leiserson , Keith H. Randall , Yuli Zhou, Cilk: an efficient multithreaded runtime system, Proceedings of the fifth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.207-216, July 19-21, 1995, Santa Barbara, California, United States
• 9: R. Bocchino, V. Adve, S. Adve, and M. Snir. Parallel programming must be deterministic by default. In First USENIX Workship on Hot Topics in Parallelism (HOTPAR 2009), March 2009.
• 10: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 11: 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
• 12: Leonardo Dagum , Ramesh Menon, OpenMP: An Industry-Standard API for Shared-Memory Programming, IEEE Computational Science & Engineering, v.5 n.1, p.46-55, January 1998 [doi>10.1109/99.660313]
• 13: Anne Dinning , Edith Schonberg, Detecting access anomalies in programs with critical sections, Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, p.85-96, May 20-21, 1991, Santa Cruz, California, United States
• 14: O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, and S. Ur. Multithreaded Java program test generation. IBM Systems Journal, 41(1):111--125, 2002.
• 15: Edinburgh Parallel Computing Centre. Java Grande Forum benchmark suite. www2.epcc.ed.ac.uk/computing/research_activities/java_grande/index_1.html.
• 16: 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
• 17: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 18: Cormac Flanagan , Stephen N. Freund, Detecting race conditions in large programs, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.90-96, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379687]
• 19: 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
• 20: Cormac Flanagan , Stephen N. Freund , Jaeheon Yi, Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 21: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 22: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 23: R. Floyd. Assigning meanings to programs. Mathematical aspects of computer science, 19(19--32):1, 1967.
• 24: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 25: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 26: IEEE. POSIX Part 1: System API- Amend. 1: Realtime Extension {C Language}. IEEE Std 1003.1b--1993, 1994.
• 27: Intel®. Threading Building Blocks for open source. http://threadingbuildingblocks.org/.
• 28: Wesley M. Johnston , J. R. Paul Hanna , Richard J. Millar, Advances in dataflow programming languages, ACM Computing Surveys (CSUR), v.36 n.1, p.1-34, March 2004 [doi>10.1145/1013208.1013209]
• 29: Pallavi Joshi , Chang-Seo Park , Koushik Sen , Mayur Naik, A randomized dynamic program analysis technique for detecting real deadlocks, Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, June 15-21, 2009, Dublin, Ireland
• 30: A. Kaminsky. Parallel Java: A Unified API for Shared Memory and Cluster Parallel Programming in 100% Java. In 21st IEEE International Parallel and Distributed Processing Symposium (IPDPS 2007), March 2007.
• 31: Edward A. Lee, The Problem with Threads, Computer, v.39 n.5, p.33-42, May 2006 [doi>10.1109/MC.2006.180]
• 32: H.-W. Loidl , F. Rubio , N. Scaife , K. Hammond , S. Horiguchi , U. Klusik , R. Loogen , G. J. Michaelson , R. Peña , S. Priebe , Á J. Rebón , P. W. Trinder, Comparing Parallel Functional Languages: Programming and Performance, Higher-Order and Symbolic Computation, v.16 n.3, p.203-251, September 2003 [doi>10.1023/A:1025641323400]
• 33: Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992 [doi>10.1109/2.161279]
• 34: 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
• 35: Robert O'Callahan , Jong-Deok Choi, Hybrid dynamic data race detection, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 36: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 37: Chang-Seo Park , Koushik Sen, Randomized active atomicity violation detection in concurrent programs, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia [doi>10.1145/1453101.1453121]
• 38: 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
• 39: David S. Rosenblum, Towards a method of programming with assertions, Proceedings of the 14th international conference on Software engineering, p.92-104, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143098]
• 40: Caitlin Sadowski , Stephen N. Freund , Cormac Flanagan, SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs, Proceedings of the 18th European Symposium on Programming Languages and Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, March 22-29, 2009, York, UK [doi>10.1007/978-3-642-00590-9_28]
• 41: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 42: Koushik Sen, Effective random testing of concurrent programs, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321679]
• 43: Koushik Sen, Race directed random testing of concurrent programs, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 44: Stephen F. Siegel , Anastasia Mironova , George S. Avrunin , Lori A. Clarke, Combining symbolic execution with model checking to verify parallel numerical programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-34, April 2008 [doi>10.1145/1348250.1348256]
• 45: N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97--106, 1993.
• 46: S. D. Stoller. Testing concurrent Java programs using randomized scheduling. In Workshop on Runtime Verification (RV'02), volume 70 of ENTCS, 2002.
• 47: W. Thies, M. Karczmarek, and S. Amarasinghe. StreamIt: A language for streaming applications. Lecture Notes in Computer Science, pages 179--196, 2002.
• 48: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 49: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Reliability, Verification

Keywords:
assertions, determinism, parallel programs