Asserting and checking determinism for multithreaded programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Asserting and checking determinism for multithreaded programs

Full text

Pdf (416 KB)

Source

Foundations of Software Engineering archive
Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering on European software engineering conference and foundations of software engineering symposium table of contents

Amsterdam, The Netherlands

SESSION: Specifications and verification 1 table of contents

Pages 3-12

Year of Publication: 2009

ISBN:978-1-60558-001-2

Authors

Jacob Burnim	University of California, Berkeley, Berkeley, CA, USA
Koushik Sen	University of California, Berkeley, Berkeley, CA, USA

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 43, Downloads (12 Months): 103, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1595696.1595700 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	S. V. Adve, M. D. Hill, B. P. Miller, and R. H. B. Netzer. Detecting data races on weak memory systems. In 18th annual International Symposium on Computer architecture (ISCA), pages 234--243. ACM, 1991.
	2	R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. In 20th IEEE/ACM International Conference on Automated software engineering (ASE), pages 233--242. ACM, 2005.
	3	G. Agha. Actors: A Model of Concurrent Computation. MIT Press, 1986.
	4	Z. Anderson, D. Gay, R. Ennals, and E. Brewer. SharC: checking data sharing strategies for multithreaded C. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation (PLDI 2008), pages 149--158. ACM New York, NY, USA, 2008.
	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	G. Barnes. A method for implementing lock-free shared-datastructures. In Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, pages 261--270. ACM New York, NY, USA, 1993.
	8	R. Blumofe, C. Joerg, B. Kuszmaul, C. Leiserson, K. Randall, and Y. Zhou. Cilk: An efficient multithreaded runtime system. In Proceedings of the fifth ACM SIGPLAN symposium on Principles and practice of parallel programming (PPOPP), 1995.
	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	C. Boyapati and M. C. Rinard. A parameterized type system for race-free java programs. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA'01), pages 56--69, 2001.
	11	J. D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proc. of the ACMSIGPLAN Conference on Programming language design and implementation, pages 258--269, 2002.
	12	L. Dagum, R. Menon, and S. Inc. OpenMP: an industry standard API for shared-memory programming. IEEE Computational Science & Engineering, 5(1):46--55, 1998.
	13	A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. In Proc. of the ACM/ONR Workshop on Parallel and Distributed Debugging, 1991.
	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	D. R. Engler and K. Ashcraft. RacerX: effective, static detection of race conditions and deadlocks. In 19th ACM Symposium on Operating Systems Principles (SOSP), 2003.
	17	C. Flanagan and S. N. Freund. Type-based race detection for java. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00), 2000.
	18	C. Flanagan and S. N. Freund. Detecting race conditions in large programs. In Proc. of the Program Analysis for Software Tools and Engineering Conference, 2001.
	19	C. Flanagan and S. N. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256--267, 2004.
	20	C. Flanagan, S. N. Freund, and J. Yi. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In PLDI '08: Proceedings of the 2008 ACMSIGPLAN conference on Programming language design and implementation, pages 293--303. ACM, 2008.
	21	C. Flanagan and S. Qadeer. A type and effect system for atomicity. In ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, 2003.
	22	C. Flanagan and S. Qadeer. Types for atomicity. In TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, pages 1--12, New York, NY, USA, 2003. ACM.
	23	R. Floyd. Assigning meanings to programs. Mathematical aspects of computer science, 19(19--32):1, 1967.
	24	D. Gay, P. Levis, R. von Behren, M. Welsh, E. Brewer, and D. Culler. The nesC language: A holistic approach to networked embedded systems. In ACM SIGPLAN Conference on Programming language design and implementation, pages 1--11, 2003.
	25	C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576--580, 1969.
	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	W. M. Johnston, J. R. P. Hanna, and R. J. Millar. Advances in dataflow programming languages. ACM Comput. Surv., 36(1):1--34, 2004.
	29	P. Joshi, C.-S. Park, K. Sen, and M. Naik. A randomized dynamic program analysis technique for detecting real deadlocks. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'09), 2009.
	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	E. A. Lee. The problem with threads. Computer, 39(5):33--42, May 2006.
	32	H. Loidl, F. Rubio, N. Scaife, K. Hammond, S. Horiguchi, U. Klusik, R. Loogen, G. Michaelson, R. Pena, S. Priebe, et al. Comparing parallel functional languages: Programming and performance. Higher-Order and Symbolic Computation, 16(3):203--251, 2003.
	33	B. Meyer. Applying 'design by contract'. Computer, 25(10):40--51, 1992.
	34	M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 2006.
	35	R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In ACM SIGPLAN symposium on Principles and practice of parallel programming. ACM, 2003.
	36	S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Commun. ACM, 19(5):279--285, 1976.
	37	C.-S. Park and K. Sen. Randomized active atomicity violation detection in concurrent programs. In SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008.
	38	P. Pratikakis, J. S. Foster, and M. Hicks. LOCKSMITH: context-sensitive correlation analysis for race detection. In ACM SIGPLAN conference on Programming language design and implementation (PLDI). ACM, 2006.
	39	D. S. Rosenblum. Towards a method of programming with assertions. In ICSE '92: Proceedings of the 14th international conference on Software engineering, pages 92--104, New York, NY, USA, 1992. ACM.
	40	C. Sadowski, S. Freund, and C. Flanagan. SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs. In 18th European Symposium on Programming (ESOP), 2009.
	41	S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst., 15(4):391--411, 1997.
	42	K. Sen. Effective random testing of concurrent programs. In 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE'07), 2007.
	43	K. Sen. Race directed random testing of concurrent programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), 2008.
	44	S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Combining symbolic execution with model checking to verify parallel numerical programs. ACM Trans. Softw. Eng. Methodol., 17(2):1--34, 2008.
	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	W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engineering, 10(2):203--232, 2003.
	49	C. von Praun and T. R. Gross. Object race detection. In Proc. of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications (OOPSLA'01), pages 70--82, 2001.