一句话：提出带崩溃的并发计算组合模型和 crash-aware linearizability，并给出首个验证崩溃下线性一致性的程序逻辑。
崩溃安全是真实系统的关键需求，但全系统崩溃会瞬时传播到所有抽象层级乃至未指定组件，破坏组合性；并发下还需准则同时处理崩溃与并发。本文定义带全系统崩溃的并发计算组合模型，发展带崩溃的线性一致性理论，提出内在准则 crash-aware linearizability，并证明其满足局部性与观测精化。进一步表明 strict 与 durable linearizability 可经两种翻译归约到该准则，从而简化其局部性与观测精化证明。最后连接程序逻辑，得到首个验证带崩溃线性一致性的程序逻辑，并验证持久数据结构库与文件系统事务接口片段。
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 verifies a 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.
@article{ValeW0YS24,
title = {Compositionality and Observational Refinement for Linearizability with Crashes},
author = {Arthur Oliveira Vale and Zhongye Wang and Yixuan Chen and Peixin You and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689792}
}