Abstract
The advent of non-volatile memory technologies has spurred intensive research
interest in correctness and programmability. This paper addresses both by
developing and verifying a durable (aka persistent) transactional memory (TM)
algorithm, dTMLPx86. Correctness of dTMLPx86 is judged in terms of durable
opacity, which ensures both failure atomicity (ensuring memory consistency after
a crash) and opacity (ensuring thread safety). We assume a realistic execution
model, Px86, which represents Intel’s persistent memory model and extends the
Total Store Order memory model with instructions that control persistency. Our
TM algorithm, dTMLPx86, is an adaptation of an existing software transactional
mutex lock, but with additional synchronisation mechanisms to cope with Px86.
Our correctness proof is operational and comprises two distinct types of proofs:
(1) proofs of invariants of dTMLPx86 and (2) a proof of refinement against an
operational specification that guarantees durable opacity. To achieve (1), we build on
recent Owicki-Gries logics for Px86, and for (2) we use a simulation-based
proof technique, which, as far as we are aware, is the first application of simulation-based
proofs for Px86 programs. Our entire development has been mechanised in
the Isabelle/HOL proof assistant.