skip to main content
10.1145/1708016.1708019acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Effects for cooperable and serializable threads

Published: 23 January 2010 Publication History

Abstract

Reasoning about the correctness of multithreaded programs is complicated by the potential for unexpected interference between threads. Previous work on controlling thread interference focused on verifying race freedom and/or atomicity. Unfortunately, race freedom is insufficient to prevent unintended thread interference. The notion of atomic blocks provides more semantic guarantees, but offers limited benefits for non-atomic code and it requires bi-modal sequential/multithreaded reasoning (depending on whether code is inside or outside an atomic block).
This paper proposes an alternative strategy that uses yield annotations to control thread interference, and we present an effect system for verifying the correctness of these yield annotations. The effect system guarantees that for any preemptively-scheduled execution of a well-formed program, there is a corresponding cooperative execution with equivalent behavior in which context switches happen only at yield annotations. This effect system enables cooperative reasoning: the programmer can adopt the simplifying assumption of cooperative scheduling, even though the program still executes with preemptive scheduling and/or true concurrency on multicore processors. Unlike bimodal sequential/multithreaded reasoning, cooperative reasoning can be applied to all program code.

References

[1]
M. Abadi. Automatic mutual exclusion and atomicity checks. In Concurrency, Graphs and Models, volume 5065 of Lecture Notes in Computer Science, pages 510--526. Springer, 2008.
[2]
M. Abadi and G. Plotkin. A model of cooperative threads. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 29--40, New York, NY, USA, 2009. ACM.
[3]
M. Abadi, C. Flanagan, and S. N. Freund. Types for safe locking: Static race detection for Java. Transactions on Programming Languages and Systems (TOPLAS), 28(2):207--255, 2006.
[4]
A. Adya, J. Howell, M. Theimer, W. J. Bolosky, and J. R. Douceur. Cooperative task management without manual stack management. In ATEC '02: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, pages 289--302. USENIX Association, 2002.
[5]
R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 149--160, 2004.
[6]
R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized runtime race detection and atomicity checking using partial discovered types. In International Conference on Automated Software Engineering (ASE), pages 233--242, 2005.
[7]
R. M. Amadio and S. D. Zilio. Resource control for synchronous cooperative threads. In International Conference on Concurrency Theory (CONCUR), pages 68--82. Springer-Verlag, 2004.
[8]
R.-J. Back. A method for refining atomicity in parallel algorithms. In PARLE 89: Parallel Architectures and Languages Europe, volume 366 of Lecture Notes in Computer Science, pages 199--216, 1989.
[9]
G. Boudol. Fair cooperative multithreading. In International Conference on Concurrency Theory (CONCUR), pages 272--286, 2007.
[10]
C. Boyapati and M. Rinard. A parameterized type system for racefree Java programs. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 56--69, 2001.
[11]
C. Boyapati, R. Lee, and M. Rinard. A type system for preventing data races and deadlocks in Java programs. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 211--230, 2002.
[12]
J.-D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridhara. Efficient and precise datarace detection for multithreaded objectoriented programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 258--269, 2002.
[13]
X. Deng, M. Dwyer, J. Hatcliff, and M. Mizuno. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In International Conference on Software Engineering (ICSE), pages 442--452, 2002.
[14]
T. W. Doeppner, Jr. Parallel program correctness through refinement. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 155--169, 1977.
[15]
T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transaction-aware Java runtime. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 245--255, 2007.
[16]
D. R. Engler and K. Ashcraft. RacerX: Effective, static detection of race conditions and deadlocks. In ACM Symposium on Operating Systems Principles (SOSP), pages 237--252, 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), pages 219--232, 2000.
[18]
C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256--267, 2004.
[19]
C. Flanagan and S. Qadeer. A type and effect system for atomicity. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 338--349, 2003.
[20]
C. Flanagan and S. Qadeer. Types for atomicity. InWorkshop on Types in Language Design and Implementation, pages 1--12, 2003.
[21]
C. Flanagan, S. N. Freund, and M. Lifshin. Type inference for atomicity. In Workshop on Types in Language Design and Implementation (TLDI), pages 47--58, 2005.
[22]
C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. IEEE Transactions on Software Engineering, 31(4):275--291, 2005.
[23]
C. Flanagan, S. N. Freund, M. Lifshin, and S. Qadeer. Types for atomicity: Static checking and inference for Java. Transactions on Programming Languages and Systems (TOPLAS), 30(4), 2008.
[24]
P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems-An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, 1996.
[25]
D. Grossman. Type-safe multithreading in Cyclone. In Workshop on Types in Language Design and Implementation(TLDI), pages 13--25, 2003.
[26]
T. Harris and K. Fraser. Language support for lightweight transactions. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 388--402, 2003.
[27]
J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In International Conference on Verification, Model Checking, and Abstract Interpretation, 2004.
[28]
M. Hicks, J. S. Foster, and P. Pratikakis. Inferring locking for atomic sections. In Proceedings of the Workshop on Languages, Compilers, and Hardware Support for Transactional Computing, 2006.
[29]
M. Isard and A. Birrell. Automatic mutual exclusion. In HOTOS'07: Proceedings of the 11th USENIX workshop on hot topics in operating systems, pages 1--6, Berkeley, CA, USA, 2007. USENIX Association.
[30]
S. Jagannathan, J. Vitek, A. Welc, and A. Hosking. A transactional object calculus. Science of Computer Programming, 57(2):164--186, 2005.
[31]
L. Lamport and F. B. Schneider. Pretending atomicity. Research Report 44, DEC Systems Research Center, 1989.
[32]
R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975.
[33]
J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proceedings of the ACMConference on Lisp and Functional Programming, pages 47--57, 1988.
[34]
D. Marino and T. D. Millstein. A generic type-and-effect system. In Workshop on Types in Language Design and Implementation(TLDI), pages 39--50, 2009.
[35]
B. McCloskey, F. Zhou, D. Gay, and E. Brewer. Autolocker: synchronization inference for atomic sections. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 346--358, 2006.
[36]
M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 308--319, 2006.
[37]
H. Nishiyama. Detecting data races using dynamic escape analysis based on read barrier. In Virtual Machine Research and Technology Symposium, pages 127--138, 2004.
[38]
E. Pozniansky and A. Schuster. MultiRace: Efficient on-the-fly data race detection in multithreaded C++ programs. Concurrency and Computation: Practice and Experience, 19(3):327--340, 2007.
[39]
P. Pratikakis, J. S. Foster, and M. Hicks. Context-sensitive correlation analysis for detecting races. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 320--331, 2006.
[40]
A. Sasturkar, R. Agarwal, L.Wang, and S. D. Stoller. Automated typebased analysis of data races and atomicity. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 83--94, 2005.
[41]
S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems (TOCS), 15(4):391--411, 1997.
[42]
N. Shavit and D. Touitou. Software transactional memory. In ACM SIGACT--SIGOPS Symposium on Principles of Distributed Computing (PODC), pages 204--213, 1995.
[43]
J. Smorgun and J. Yi. An effect system for checking consistency of synchronization and yields. Technical Report UCSC-SOE-09-33, Department of Computer Science, University of California at Santa Cruz, 2009.
[44]
N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97--106, 1993.
[45]
M. Vaziri, F. Tip, and J. Dolby. Associating synchronization constraints with data in an object-oriented language. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 334--345, 2006.
[46]
C. von Praun and T. Gross. Object race detection. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 70--82, 2001.
[47]
C. von Praun and T. Gross. Static conflict analysis for multi-threaded object-oriented programs. In ACMSIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 115--128, 2003.
[48]
J. W. Voung, R. Jhala, and S. Lerner. Relay: static race detection on millions of lines of code. In ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pages 205--214, 2007.
[49]
L. Wang and S. D. Stoller. Static analysis of atomicity for programs with non-blocking synchronization. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 61--71, 2005.
[50]
L. Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 137--146, 2006.
[51]
L. Wang and S. D. Stoller. Runtime analysis of atomicity for multithreaded programs. IEEE Transactions on Software Engineering, 32: 93--110, Feb. 2006.
[52]
M. Xu, R. Bodík, and M. D. Hill. A serializability violation detector for shared-memory server programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 1--14, 2005.
[53]
Y. Yu, T. Rodeheffer, and W. Chen. RaceTrack: Efficient detection of data race conditions via adaptive tracking. In ACM Symposium on Operating Systems Principles (SOSP), pages 221--234, 2005.

Cited By

View all
  • (2017)From non-preemptive to preemptive scheduling using synchronization synthesisFormal Methods in System Design10.1007/s10703-016-0256-550:2-3(97-139)Online publication date: 1-Jun-2017
  • (2016)First-class effect reflection for effect-guided programmingACM SIGPLAN Notices10.1145/3022671.298403751:10(820-837)Online publication date: 19-Oct-2016
  • (2016)First-class effect reflection for effect-guided programmingProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2983990.2984037(820-837)Online publication date: 19-Oct-2016
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
TLDI '10: Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation
January 2010
108 pages
ISBN:9781605588919
DOI:10.1145/1708016
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2010

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. atomicity
  2. effect system
  3. race conditions
  4. yield

Qualifiers

  • Research-article

Conference

POPL '10
Sponsor:

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 22 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2017)From non-preemptive to preemptive scheduling using synchronization synthesisFormal Methods in System Design10.1007/s10703-016-0256-550:2-3(97-139)Online publication date: 1-Jun-2017
  • (2016)First-class effect reflection for effect-guided programmingACM SIGPLAN Notices10.1145/3022671.298403751:10(820-837)Online publication date: 19-Oct-2016
  • (2016)First-class effect reflection for effect-guided programmingProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2983990.2984037(820-837)Online publication date: 19-Oct-2016
  • (2012)CONCURRITProceedings of the 4th USENIX conference on Hot Topics in Parallelism10.5555/2342788.2342804(16-16)Online publication date: 7-Jun-2012
  • (2012)Cooperative types for controlling thread interference in JavaProceedings of the 2012 International Symposium on Software Testing and Analysis10.1145/2338965.2336781(232-242)Online publication date: 15-Jul-2012
  • (2011)Heuristic evaluation of programming language featuresProceedings of the 3rd ACM SIGPLAN workshop on Evaluation and usability of programming languages and tools10.1145/2089155.2089160(9-14)Online publication date: 24-Oct-2011
  • (2011)Cooperative reasoning for preemptive executionACM SIGPLAN Notices10.1145/2038037.194157546:8(147-156)Online publication date: 12-Feb-2011
  • (2011)Cooperative reasoning for preemptive executionProceedings of the 16th ACM symposium on Principles and practice of parallel programming10.1145/1941553.1941575(147-156)Online publication date: 12-Feb-2011
  • (2011)Cooperative concurrency for a multicore worldProceedings of the Second international conference on Runtime verification10.1007/978-3-642-29860-8_25(342-344)Online publication date: 27-Sep-2011
  • (2010)User evaluation of correctness conditionsEvaluation and Usability of Programming Languages and Tools10.1145/1937117.1937119(1-6)Online publication date: 17-Oct-2010

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media