SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 13:30 - 14:00 at Lecture Theatre 2 - Concurrency Chair(s): Suresh Jagannathan

Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability.

We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique of transactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers on interaction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studieswe mentioned only one above…? are mechanized in Coq.

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
ConcurrencyOOPSLA at Lecture Theatre 2
Chair(s): Suresh Jagannathan Purdue University
13:30
30m
Research paper
C4: verified transactional objects
OOPSLA
Mohsen Lesani University of California at Riverside, Li-yao Xia University of Pennsylvania, Anders Kaseorg Massachusetts Institute of Technology, Christian J. Bell MIT CSAIL, Adam Chlipala Massachusetts Institute of Technology, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI
14:00
30m
Talk
Concurrent Size
OOPSLA
Gal Sela Technion, Erez Petrank Technion
DOI
14:30
30m
Talk
Veracity: Declarative Multicore Programming with Commutativity
OOPSLA
Adam Chen Stevens Institute of Technology, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, Jared Pincus Stevens Institute of Technology
DOI