Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Degrees of Separation: A Flexible Type System for Safe Concurrency
 
conference paper not in proceedings

Degrees of Separation: A Flexible Type System for Safe Concurrency

Xu, Yichen  
•
Boruch-Gruszecki, Aleksander Slawomir  
•
Odersky, Martin  
April 3, 2024
OOPSLA 2024

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

paper.pdf

Type

Postprint

Version

Access type

openaccess

License Condition

copyright

Size

946.88 KB

Format

Adobe PDF

Checksum (MD5)

5f061b06c870438ccf7a98f183fd5eeb

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés