Compositionality and Observational Refinement for Linearizability with Crashes
This program is tentative and subject to change.
Crash-safety is an important property of real systems, as the main functionality of some systems is resilience to crashes. Toward a compositional verification approach for crash-safety under full-system crashes, one observes that crashes propagate instantaneously to all components across all levels of abstraction, even to unspecified components, hindering compositionality. Furthermore, in the presence of concurrency, a correctness criterion that addresses both crashes and concurrency proves necessary. For this, several adaptations of linearizability have been suggested, each featuring different trade-offs between complexity and expressiveness. The recently proposed compositional linearizability framework shows that to achieve compositionality with linearizability both a locality and observational refinement property are necessary. Despite that, no linearizability criterion with crashes has been proven to support an observational refinement property.
In this paper, we define a compositional model of concurrent computation with full-system crashes. We use this model to develop a compositional theory of linearizability with crashes, which reveals a criterion, crash-aware linearizability, as its inherent notion of linearizability and supports both locality and observational refinement. We then show that strict linearizability and durable linearizability factor through crash-aware linearizability as two different ways of translating between concurrent computation with and without crashes, enabling simple proofs of locality and observational refinement for a generalization of these two criteria. Then, we show how the theory can be connected with a program logic for durable and crash-aware linearizability, which gives the first program logic that shows some form of linearizability with crashes. We showcase the advantages of compositionality by verifying a library facilitating programming persistent data structures and a fragment of a transactional interface for a file system.
This program is tentative and subject to change.
Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change
13:50 - 15:30 | |||
13:50 20mTalk | Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of Programs OOPSLA 2024 Shaan Nagy University of Wisconsin-Madison, Jinwoo Kim Seoul National University, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison | ||
14:10 20mTalk | Compositionality and Observational Refinement for Linearizability with Crashes OOPSLA 2024 Arthur Oliveira Vale Yale University, Zhongye Wang Shanghai Jiao Tong University, Yixuan Chen Yale University, Peixin You Yale University, Zhong Shao Yale University | ||
14:30 20mTalk | Hypra: A Deductive Program Verifier for Hyper Hoare Logic OOPSLA 2024 | ||
14:50 20mTalk | SMT2Test: From SMT Formulas to Effective Test Cases OOPSLA 2024 | ||
15:10 20mTalk | Validating SMT Solvers for Correctness and Performance via Grammar-based Enumeration OOPSLA 2024 |