A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Recently we have seen a renewed interest in programming languages that tame the complexity of state and concurrency through refined type systems with more fine-grained control over effects. In addition to simplifying reasoning and eliminating whole classes of bugs, statically tracking effects opens the door to advanced compiler optimizations.
In this paper we present a relational model of a type-and-effect system for a higher-order, concurrent program- ming language. The model precisely captures the semantic invariants expressed by the effect annotations. We demonstrate that these invariants are strong enough to prove advanced program transformations, including automatic parallelization of expressions with suitably disjoint effects. The model also supports refinement proofs between abstract data types implementations with different internal data representations, including proofs that fine-grained concurrent algorithms refine their coarse-grained counterparts. This is the first model for such an expressive language that supports both effect-based optimizations and data abstraction.
The logical relation is defined in Iris, a state-of-the-art higher-order concurrent separation logic. This greatly simplifies proving well-definedness of the logical relation and also provides us with a powerful logic for reasoning in the model.
Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:20 - 16:00
|A Promising Semantics for Relaxed-Memory Concurrency|
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWSLink to publication Pre-print Media Attached
|Automatically Comparing Memory Consistency Models|
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UKPre-print Media Attached File Attached
|Interactive Proofs in Higher-Order Concurrent Separation Logic|
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus UniversityDOI Pre-print Media Attached
|A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic|