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 DecDisplayed time zone: Auckland, Wellington change
13:30 - 15:00
|C4: verified transactional objects
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 PennsylvaniaDOI
|Veracity: Declarative Multicore Programming with Commutativity
Adam Chen Stevens Institute of Technology, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, Jared Pincus Stevens Institute of TechnologyDOI