Thu 11 Jan 2018 10:30 - 10:55 at Bunker Hill - Consistency Chair(s): Xinyu Feng

While many program properties like the validity of assertions and in-bounds array accesses admit nearly-trivial monitoring algorithms, the standard correctness criterion for concurrent data structures does not. Given an implementation of an arbitrary abstract data type, checking whether the operations invoked in one single concurrent execution are linearizable, i.e., indistinguishable from an execution where the same operations are invoked atomically, requires exponential time in the number of operations.

In this work we identify a class of collection abstract data types which admit polynomial-time linearizability monitors. Collections capture the majority of concurrent data structures available in practice, including stacks, queues, sets, and maps. Although monitoring executions of arbitrary abstract data types requires enumerating exponentially-many possible linearizations, collections enjoy combinatorial properties which avoid the enumeration. We leverage these properties to reduce linearizability to Horn satisfiability. As far as we know, ours is the first sound, complete, and tractable algorithm for monitoring linearizability for types beyond single-value registers.

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
ConsistencyResearch Papers at Bunker Hill
Chair(s): Xinyu Feng University of Science and Technology of China
10:30
25m
Talk
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Research Papers
Michael Emmi Nokia Bell Labs, Constantin Enea Université Paris Diderot
10:55
25m
Talk
Reducing Liveness to Safety in First-Order Logic
Research Papers
Oded Padon Tel Aviv University, Jochen Hoenicke Universität Freiburg, Giuliano Losa University of California at Los Angeles, USA, Andreas Podelski University of Freiburg, Germany, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
11:20
25m
Talk
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Research Papers
Gowtham Kaki Purdue University, Kartik Nagar Purdue University, Mahsa Najafzadeh Purdue University, Suresh Jagannathan Purdue University
11:45
25m
Talk
Programming and Proving with Distributed Protocols
Research Papers
Ilya Sergey University College London, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle
DOI Pre-print