Cited By
View all- Georges APeters BElbeheiry LWhite LDolan SEisenberg RCasinghino CPottier FDreyer D(2025)Data Race Freedom à la ModeProceedings of the ACM on Programming Languages10.1145/37048599:POPL(656-686)Online publication date: 9-Jan-2025
Degrees of Separation: A Flexible Type System for Safe Concurrency
Article No.: 136, Pages 1181 - 1207
Abstract
Data races have long been a notorious problem in concurrent programming. They are hard to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress has been made in this area, and these type systems are increasingly usable and practical. However, their adoption in mainstream programming languages is still limited, which is largely attributed to their strict alias prevention principles that obstruct the usage of existing programming patterns. This is a deterrent to the migration of existing code bases. To tackle this problem, we propose Capture Separation Calculus (System CSC), a calculus that models fork-join parallelism and statically prevents data races while being compatible with established programming patterns. It follows a control-as-you-need philosophy: by default, aliases are allowed, but they are tracked in the type system. When data races are a concern, the tracked aliases are controlled to prevent data-race-prone patterns. We study the formal properties of System CSC. Type soundness is proven via the standard progress and preservation theorems. Additionally, we formally verify the data race freedom property of System CSC by proving that the reduction of a well-typed program is confluent.
Supplementary Material
The appendix of the paper. It contains the full proof.
- Download
- 1.60 MB
References
[1]
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World.
[2]
Yuyan Bao, Guannan Wei, Oliver Bracevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf. 2021. Reachability types: tracking aliasing and separation in higher-order functional programs. Proceedings of the ACM on Programming Languages, 5 (2021), 1 – 32.
[3]
Erik Barendsen and Sjaak Smetsers. 1996. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6 (1996), 579 – 612.
[4]
Chandrasekhar Boyapati and Martin C. Rinard. 2001. A Parameterized Type System for Race-Free Java Programs. In OOPSLA. 56–69.
[5]
John Tang Boyland. 2001. Alias burying: Unique variables without destructive reads. Software: Practice and Experience, 31 (2001).
[6]
John Tang Boyland. 2010. Semantics of fractional permissions with nesting. ACM Trans. Program. Lang. Syst., 32 (2010), 22:1–22:33.
[7]
Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as capabilities: effect handlers and lightweight effect polymorphism. Proceedings of the ACM on Programming Languages, 4 (2020), 1 – 30.
[8]
Elias Castegren and Tobias Wrigstad. 2016. Reference Capabilities for Concurrency Control. In European Conference on Object-Oriented Programming.
[9]
Alonzo Church and J. Barkley Rosser. 1936. Some properties of conversion. Trans. Amer. Math. Soc., 39 (1936), 472–482.
[10]
Dave Clarke and Tobias Wrigstad. 2003. External Uniqueness Is Unique Enough. In European Conference on Object-Oriented Programming.
[11]
David G. Clarke, John Potter, and James Noble. 1998. Ownership Types for Flexible Alias Protection. In OOPSLA. 48–64.
[12]
Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015. Deny capabilities for safe, fast actors. Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control.
[13]
Karl Crary, David Walker, and Greg Morrisett. 1999. Typed memory management in a calculus of capabilities. In ACM-SIGACT Symposium on Principles of Programming Languages.
[14]
Manuel Fähndrich and Robert A Deline. 2002. Adoption and focus: practical linear types for imperative programming. In ACM-SIGPLAN Symposium on Programming Language Design and Implementation.
[15]
Kasra Ferdowsi. 2023. The Usability of Advanced Type Systems: Rust as a Case Study. ArXiv, abs/2301.02308 (2023).
[16]
Ian Goodfellow, Yoshua Bengio, and Aaron Courville. 2016. Deep Learning. The MIT Press. isbn:0262035618
[17]
Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. 2012. Uniqueness and Reference Immutability for Safe Parallelism. In OOPSLA. 21–40.
[18]
J. Hogg. 1991. Islands: aliasing protection in object-oriented languages. In Conference on Object-Oriented Programming Systems, Languages, and Applications.
[19]
Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press, USA. isbn:1593278284
[20]
Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages.
[21]
Amit Levy, Michael P. Andersen, Bradford Campbell, David Culler, Prabal Dutta, Branden Ghena, Philip Levis, and Pat Pannuto. 2015. Ownership Is Theft: Experiences Building an Embedded OS in Rust. In Proceedings of the 8th Workshop on Programming Languages and Operating Systems. ACM, Monterey California. 21–26. isbn:978-1-4503-3942-1 https://doi.org/10.1145/2818302.2818306
[22]
Daniel Marshall, Michael Vollmer, and Dominic A. Orchard. 2022. Linearity and Uniqueness: An Entente Cordiale. In European Symposium on Programming.
[23]
Mae Milano, Joshua Turcotti, and Andrew C. Myers. 2022. A flexible type system for fearless concurrency. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation.
[24]
Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. USA. AAI3245526
[25]
James Noble, Julian Mackay, and Tobias Wrigstad. 2022. Rusty Links in Local Chains. ArXiv, abs/2205.00795 (2022).
[26]
Martin Odersky. 1992. Observers for Linear Types. In European Symposium on Programming.
[27]
Martin Odersky, Aleksander Boruch-Gruszecki, Edward Lee, Jonathan Immanuel Brachthäuser, and Ondrej Lhoták. 2022. Scoped Capabilities for Polymorphic Effects. ArXiv, abs/2207.03402 (2022).
[28]
Peter W. O’Hearn, John Power, Robert D. Tennent, and Makoto Takeyama. 1999. Syntactic control of interference revisited. In Mathematical Foundations of Programming Semantics.
[29]
Dimitri Racordon, Denys Shabalin, Daniel Zheng, Dave Abrahams, and Brennan Saeta. 2022. Implementation Strategies for Mutable Value Semantics. J. Object Technol., 21 (2022), 2:1–11.
[30]
Marianna Rapoport and Ondrej Lhoták. 2019. A path to DOT: formalizing fully path-dependent types. Proceedings of the ACM on Programming Languages, 3 (2019), 1 – 29.
[31]
John C. Reynolds. 1978. Syntactic control of interference. Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages.
[32]
Scala. 2022. The Scala 3 compiler, also known as Dotty. https://dotty.epfl.ch
[33]
Marco Servetto, David J. Pearce, Lindsay J. Groves, and Alex Potanin. 2013. Balloon Types for Safe Parallelisation over Arbitrary Object Graphs.
[34]
Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods.
[35]
Guannan Wei, Oliver Bracevac, Songlin Jia, Yuyan Bao, and Tiark Rompf. 2023. Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. ArXiv, abs/2307.13844 (2023).
[36]
Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal J. Ahmed. 2019. Oxide: The Essence of Rust. ArXiv, abs/1903.00982 (2019).
[37]
Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput., 115 (1994), 38–94.
Index Terms
- Degrees of Separation: A Flexible Type System for Safe Concurrency
Recommendations
Type-based safe resource deallocation for shared-memory concurrency
OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applicationsWe propose a type system to guarantee safe resource deallocation for shared-memory concurrent programs by extending the previous type system based on fractional ownerships. Here, safe resource deallocation means that memory cells, locks, or threads are ...
Type-based safe resource deallocation for shared-memory concurrency
OOPSLA '12We propose a type system to guarantee safe resource deallocation for shared-memory concurrent programs by extending the previous type system based on fractional ownerships. Here, safe resource deallocation means that memory cells, locks, or threads are ...
The tasks with effects model for safe concurrency
PPoPP '13Today's widely-used concurrent programming models either provide weak safety guarantees, making it easy to write code with subtle errors, or are limited in the class of programs that they can express. We propose a new concurrent programming model based ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2024
1492 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 29 April 2024
Published in PACMPL Volume 8, Issue OOPSLA1
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- FNSNF
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 510Total Downloads
- Downloads (Last 12 months)510
- Downloads (Last 6 weeks)57
Reflects downloads up to 28 Jan 2025
Other Metrics
Citations
Cited By
View all- Georges APeters BElbeheiry LWhite LDolan SEisenberg RCasinghino CPottier FDreyer D(2025)Data Race Freedom à la ModeProceedings of the ACM on Programming Languages10.1145/37048599:POPL(656-686)Online publication date: 9-Jan-2025
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in