Abstraction for Crash-Resilient Objects (Extended Version)

TL;DR

This paper introduces a new correctness criterion for crash-resilient concurrent objects in non-volatile memory, enabling formal reasoning about library behaviors and verification against specifications in NVM environments.

Contribution

It develops a sound library correctness criterion for NVM, extending the semantic foundation with specification constructs, and demonstrates its application on persistent object implementations.

Findings

First formal approach to compositional reasoning under NVM

Verified two persistent object implementations against specifications

Extended NVM model with specification constructs

Abstract

We study abstraction for crash-resilient concurrent objects using non-volatile memory (NVM). We develop a library correctness criterion that is sound for ensuring contextual refinement in this setting, thus allowing clients to reason about library behaviors in terms of their abstract specifications, and library developers to verify their implementations against the specifications abstracting away from particular client programs. As a semantic foundation we employ a recent NVM model, called Persistent Sequential Consistency, and extend its language and operational semantics with useful specification constructs. The proposed correctness criterion accounts for NVM-related interactions between client and library code due to explicit persist instructions, and for calling policies enforced by libraries. We illustrate our approach on two implementations and specifications of simple persistent objects with different prototypical durability guarantees. Our results provide the first approach to formal compositional reasoning under NVM.