PPoPP 2019
Sat 16 - Wed 20 February 2019 Washington, DC, United States
Wed 20 Feb 2019 11:45 - 12:10 at Salon 12/13 - Session 10: Verification Chair(s): Michael Lam

Linearizability is a key correctness property for concurrent data types. Linearizability requires that the behavior of concurrently invoked operations of the data type be equivalent to the behavior in an execution where each operation takes effect at an instantaneous point of time between its invocation and return. Given an execution trace of operations, the problem of verifying its linearizability is NP-complete, and current exhaustive search tools scale poorly.

In this work, we empirically show that linearizability of an execution trace is often witnessed by a schedule that orders only a small number of operations (the ``linearizability depth'') in a specific way, independently of other operations. Accordingly, one can structure the search for linearizability witnesses by exploring schedules of low linearizability depth first. We provide such an algorithm. Key to our algorithm is a procedure to generate a \emph{strong $d$-hitting family} of schedules, which is guaranteed to cover all linearizability witnesses of depth $d$. A strong $d$-hitting family of schedules of an execution trace consists of a set of schedules, such that for each tuple of $d$ operations in the trace, there is a schedule in the family that (i) executes these operations in the order they appear in the tuple, and (ii) as late as possible in the execution.

We show that most linearizable execution traces from existing benchmarks can be witnessed by strongly $d$-hitting schedules for $d\leq 5$. Our result suggests a practical and automated method for showing linearizability of a trace based on a prioritization of schedules parameterized by the linearizability depth.

Wed 20 Feb

11:20 - 12:35: Main Conference - Session 10: Verification at Salon 12/13
Chair(s): Michael LamJames Madison University
PPoPP-2019-papers11:20 - 11:45
Simon DohertyUniversity of Sheffield, Brijesh DongolUniversity of Surrey, Heike WehrheimPaderborn University, John DerrickUniversity of Sheffield
PPoPP-2019-papers11:45 - 12:10
Burcu Kulahcioglu OzkanMPI-SWS, Germany, Rupak MajumdarMPI-SWS, Germany, Filip NiksicUniversity of Pennsylvania
PPoPP-2019-papers12:10 - 12:35
Caleb VossGeorgia Institute of Technology, Tiago CogumbreiroUniversity of Massachusetts Boston, Vivek SarkarRice University, USA