Authors
Arthur Oliveira Vale
Yixuan Chen
Peixin You
Zhong Shao
Abstract
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.
Published
In
Proc. 2024 ACM SIGPLAN
International Conference on Object-Oriented Programming, Systems,
Languages, and Applications (OOPSLA'24), Pasadena, CA, October 2024.
Published as
Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number OOPSLA2, Article 352 (October 2024), 29 pages.