Thu 16 Jun 2022 13:30 - 13:50 at Kon-Tiki - Concurrency Chair(s): Mike Dodds
Fri 17 Jun 2022 01:30 - 01:50 at Kon-Tiki - Concurrency

This paper proposes a new type system for concurrent programs, allowing threads to exchange complex, arbitrarily connected object graphs without risking destructive data races. While this goal is shared by a rich history of past work, existing solutions either rely on strictly enforced heap invariants that prohibit natural programming patterns or demand pervasive annotations that bring formidable formal overhead to the simplest programming tasks. As a result, past systems cannot express intuitively simple code without surprising and unnatural rewrites. Our work avoids these pitfalls through a novel type system that provides sound reasoning about separation in the heap while remaining amenable to whatever style of heap manipulations the programmer desires. This sweet spot is attained by tracking an invariant as strong as prior work, but allowing arbitrary violations to arise and persist across the program until recovery is needed. We present this system with large code examples demonstrating natural expression of patterns prior work balks at, a formal proof of correctness—that well-typed programs cannot encounter destructive data races at run time—and an efficient type checker implemented in Gallina and Ocaml.

Thu 16 Jun

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:50
ConcurrencyPLDI at Kon-Tiki +12h
Chair(s): Mike Dodds Galois, Inc.
13:30
20m
Talk
A Flexible Type System for Fearless Concurrency
PLDI
Mae Milano University of California, Berkeley, Julia Turcotti University of California, Berkeley, Andrew Myers Cornell University
DOI
13:50
20m
Talk
A Study of Real-world Data Races in Golang
PLDI
Milind Chabbi Uber Technologies Inc., Murali Krishna Ramanathan Uber Technologies Inc.
DOI
14:10
20m
Talk
Checking Robustness to Weak Persistency Models
PLDI
Hamed Gorjiara University of California, Irvine, Weiyu Luo University of California, Irvine, Alex Lee University of California, Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California, Irvine
DOI
14:30
20m
Talk
Sound Sequentialization for Concurrent Program Verification
PLDI
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg, Germany
DOI File Attached

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

01:30 - 02:50
ConcurrencyPLDI at Kon-Tiki
01:30
20m
Talk
A Flexible Type System for Fearless Concurrency
PLDI
Mae Milano University of California, Berkeley, Julia Turcotti University of California, Berkeley, Andrew Myers Cornell University
DOI
01:50
20m
Talk
A Study of Real-world Data Races in Golang
PLDI
Milind Chabbi Uber Technologies Inc., Murali Krishna Ramanathan Uber Technologies Inc.
DOI
02:10
20m
Talk
Checking Robustness to Weak Persistency Models
PLDI
Hamed Gorjiara University of California, Irvine, Weiyu Luo University of California, Irvine, Alex Lee University of California, Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California, Irvine
DOI
02:30
20m
Talk
Sound Sequentialization for Concurrent Program Verification
PLDI
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg, Germany
DOI File Attached