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
Type
conference paper not in proceedings
Author(s)
Xu, Yichen  
Boruch-Gruszecki, Aleksander Slawomir  
Odersky, Martin  
Date Issued

2024-04-03

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LAMP1  
Event nameEvent placeEvent date
OOPSLA 2024

Pasadena, California, United States

20 - 25 October 2024

Available on Infoscience
April 3, 2024
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/207003
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