hesela.devDurable linearizability
Durable linearizability requires a concurrent object's operation history to remain linearizable across system-wide crashes without losing completed operations.
The full-system model gives each era new abstract threads. A pending call may take effect before failure, be completed by later threads or have no effect, subject to a legal history. The condition does not require every interrupted call to resolve by the crash. [1]
Buffered durable linearizability can lose effects of completed calls. Retained portions of pre-crash eras must be happens-before-consistent cuts that remain linearizable when combined with subsequent execution. Unlike unbuffered durable linearizability, it is not generally compositional. [1]
Durability concerns abstract effects rather than every representation byte. A persistent set can recover links from durable membership information. In this proof framework, recovery must preserve the encoded abstract state even if recovery itself crashes. [2]
Relations
Advantages
- Recovery correctness and operation correctness can be verified separately using explicit durable and recovered representations. [2]
Limitations
- This safety condition alone gives no bound on recovery time or operation completion. [1]
Citations
- Izraelevitz, Mendes and Scott. Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. DISC 2016, sections 1-2 and 3.3.
- D'Osualdo, Raad and Vafeiadis. The Path to Durable Linearizability. POPL 2023, section 2 (pp. 8-9) and section 4.1.
Further reading
Sources & caveats
- DISC 2016 section 2, Definitions 1-4, supplies the full-system failure model and completed/pending-operation distinction; section 3.3 separates liveness conditions.
- The Path to Durable Linearizability was read in sections 2 and 4.1 for the link-free-set representation and sound-recovery argument.
- Source synthesis of a formal safety condition, not a hardware experiment or proof of a particular storage implementation.