Verifying Lock-free Search Structure Templates
We present and verify template algorithms for lock-free concurrent search structures that cover a broad range of existing implementations based on lists and skiplists. Our linearizability proofs are fully mechanized in the concurrent separation logic Iris. The proofs are modular and cover the broader design space of the underlying algorithms by parameterizing the verification over aspects such as the low-level representation of nodes and the style of data structure maintenance. As a further technical contribution, we present a mechanization of a recently proposed method for reasoning about future-dependent linearization points using hindsight arguments. The mechanization builds on Iris’ support for prophecy reasoning and user-defined ghost resources. We demonstrate that the method can help to reduce the proof effort compared to direct prophecy-based proofs.
Wed 18 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | VerificationTechnical Papers at EI 2 Pichelmayer Chair(s): João Costa Seco NOVA-LINCS; Nova University of Lisbon | ||
13:30 15mTalk | A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson Technical Papers Barnabas Arvay University of Freiburg, Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany | ||
13:45 15mTalk | Qafny: A Quantum-Program Verifier Technical Papers Liyi Li Iowa State University, Mingwei Zhu University of Maryland, College Park, Rance Cleaveland University of Maryland, Alexander Nicolellis Iowa State University, Yi Lee University of Maryland, College Park, Le Chang University of Maryland, College Park, Xiaodi Wu University of Maryland | ||
14:00 15mTalk | Verifying Lock-free Search Structure Templates Technical Papers Nisarg Patel New York University, Dennis Shasha New York University, Thomas Wies New York University | ||
14:15 15mTalk | Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning Technical Papers | ||
14:30 15mTalk | Compositional Symbolic Execution for Correctness and Incorrectness Reasoning Technical Papers Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Caroline Cronjäger Ruhr-Universität Bochum, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London | ||
14:45 15mTalk | Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations Technical Papers Jie Qiu Duolingo, Colin Cai University of California, Berkeley, Sahil Bhatia University of California, Berkeley, Niranjan Hasabnis Code Metal, Sanjit Seshia UC Berkeley, Alvin Cheung University of California at Berkeley | ||