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

There is an ongoing effort to provide programming abstractions that ease the burden of exploiting multicore hardware. Many programming abstractions
({\it e.g.}, concurrent objects, transactional memory, etc.) simplify matters, but still involve intricate engineering. We argue that some difficulty of multicore programming can be meliorated through a declarative programming style in which programmers directly express the independence of fragments of sequential programs.

In our proposed paradigm, programmers write programs in a familiar, sequential manner, with the added ability to explicitly express the conditions under which code fragments sequentially commute.
Putting such commutativity conditions into source code
offers a new entry point for a compiler to exploit the known connection between commutativity and parallelism. We give a semantics for the programmer's sequential perspective and, under a correctness condition, find that a compiler-transformed parallel execution is equivalent to the sequential semantics. Serializability/linearizability are not the right fit for this condition, so
we introduce scoped serializability and show how it can be enforced with lock synthesis techniques.

We next describe a technique for automatically verifying and synthesizing commute conditions via a new reduction from our commute blocks to logical specifications, upon which symbolic commutativity reasoning can be performed. We implemented our work in a new language called Veracity, implemented in Multicore OCaml. We show that commutativity conditions can be automatically generated
across a variety of new benchmark programs, confirm the expectation that concurrency speedups can be seen as the computation increases, and apply our work to a small in-memory filesystem and an adaptation of a crowdfund blockchain smart contract.

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
Hide past events