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 FebDisplayed 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:2025mTalk Verifying C11 Programs OperationallyMain ConferenceSimon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University, John Derrick University of Sheffield DOI 11:4525mTalk Checking Linearizability Using Hitting FamiliesMain ConferenceBurcu Kulahcioglu Ozkan MPI-SWS, Germany, Rupak Majumdar MPI-SWS, Germany, Filip Niksic University of Pennsylvania DOI 12:1025mTalk Transitive Joins: A Sound and Efficient Online Deadlock-Avoidance PolicyMain ConferenceCaleb Voss Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Rice University, USA DOI