Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Wed 17 Jun 2020 11:40 - 12:00 at PLDI Research Papers live stream - Verification I Chair(s): Stephen Freund

Asynchronous programs are notoriously difficult to reason about because they spawn computation tasks which take effect asynchronously in a nondeterministic way. Devising inductive invariants for such programs requires understanding and stating complex relationships between an unbounded number of computation tasks in arbitrarily long executions. In this paper, we introduce \emph{inductive sequentialization}, a new proof rule that sidesteps this complexity via a \emph{sequential reduction}, a sequential program that captures every behavior of the original program up to reordering of coarse-grained commutative actions. A sequential reduction of a concurrent program is easy to reason about since it corresponds to a simple execution of the program in an idealized synchronous environment, where processes act in a fixed order and at the same speed. We have implemented and integrated our proof rule in the CIVL verifier, allowing us to provably derive fine-grained implementations of asynchronous programs. We have successfully applied our proof rule to a diverse set of message-passing protocols, including leader election protocols, two-phase commit, and Paxos.

Wed 17 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

pldi-2020-papers10:40 - 11:00
Siddharth KrishnaMicrosoft Research, Cambridge, Nisarg PatelNew York University, USA, Dennis ShashaNew York University, USA, Thomas WiesNew York University, USA
pldi-2020-papers11:00 - 11:20
Jacob R. LorchMicrosoft Research, USA, Yixuan ChenUniversity of Michigan, USA / Yale University, USA, Manos KapritsosUniversity of Michigan, USA, Bryan ParnoCarnegie Mellon University, USA, Shaz QadeerNovi, USA, Upamanyu SharmaUniversity of Michigan, USA, James R. WilcoxCertora, USA, Xueyuan ZhaoCarnegie Mellon University, USA
pldi-2020-papers11:20 - 11:40
Ori LahavTel Aviv University, Israel, Udi BokerIDC Herzliya, Israel
pldi-2020-papers11:40 - 12:00
Bernhard KraglIST Austria, Austria, Constantin EneaUniversity of Paris Diderot, France, Thomas A. HenzingerIST Austria, Austria, Suha Orhun MutluergilIRIF, France / University of Paris, France / CNRS, France, Shaz QadeerNovi, USA