Degrees of Separation: A Flexible Type System for Safe Concurrency
Data races have long been a notorious problem in concurrent programming. They are subtle 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), which statically prevents data races while being compatible with established programming patterns. It follows a \emph{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.
Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change
13:50 - 15:30 | Types and Gradual Typing 2OOPSLA 2024 at Pasadena Chair(s): Fabian Muehlboeck Australian National University | ||
13:50 20mTalk | Degrees of Separation: A Flexible Type System for Safe Concurrency OOPSLA 2024 DOI | ||
14:10 20mTalk | Full Iso-recursive Types OOPSLA 2024 Litao Zhou University of Hong Kong, Qianyong Wan The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
14:30 20mTalk | Gradually Typed Languages Should Be Vigilant! OOPSLA 2024 Olek Gierczak Northeastern University, Lucy Menon Northeastern University, Christos Dimoulas Northwestern University, Amal Ahmed Northeastern University, USA DOI | ||
14:50 20mTalk | Merging Gradual Typing OOPSLA 2024 Wenjia Ye National University of Singapore, Bruno C. d. S. Oliveira University of Hong Kong, MatÃas Toro University of Chile DOI | ||
15:10 20mTalk | Persimmon: Nested Family Polymorphism with Extensible Variant Types OOPSLA 2024 Anastasiya Kravchuk-Kirilyuk Harvard University, Gary Feng University of Waterloo, Jonas Iskander Harvard University, Yizhou Zhang University of Waterloo, Nada Amin Harvard University DOI |