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

Displayed time zone: Guadalajara, Mexico City, Monterrey change

11:20 - 12:35
Session 10: VerificationMain Conference at Salon 12/13
Chair(s): Michael Lam James Madison University
11:20
25m
Talk
Verifying C11 Programs Operationally
Main Conference
Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University, John Derrick University of Sheffield
DOI
11:45
25m
Talk
Checking Linearizability Using Hitting Families
Main Conference
Burcu Kulahcioglu Ozkan MPI-SWS, Germany, Rupak Majumdar MPI-SWS, Germany, Filip Niksic University of Pennsylvania
DOI
12:10
25m
Talk
Transitive Joins: A Sound and Efficient Online Deadlock-Avoidance Policy
Main Conference
Caleb Voss Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Rice University, USA
DOI