Persistent Owicki-Gries Reasoning

Abstract

The advent of non-volatile memory (NVM) technologies is expected to transform how software systems are structured fundamentally, making the task of correct programming significantly harder. This is because ensuring that memory stores persist in the correct order is challenging, and requires low-level programming to flush the cache at appropriate points. This has in turn resulted in a noticeable verification gap.

To address this, we study the verification of NVM programs, and present Persistent Owicki-Gries (POG), the first program logic for reasoning about such programs. We prove the soundness of POG over the recent Intel-x86 model, which formalises the out-of-order persistence of memory stores and the semantics of the Intel cache line flush instructions. We then use POG to verify several programs that interact with NVM.

Paper

• Azalea Raad, Ori Lahav, and Viktor Vafeiadis.
  Persistent Owicki-Gries reasoning: A program logic for reasoning about persistent programs on Intel-x86.
  Proc. ACM Program. Lang. 4, OOPSLA, Article 151 (November 2020)
  [Paper] [@ACM]

People

• Azalea Raad (MPI-SWS & Imperial College London)
• Ori Lahav (Tel Aviv University)
• Viktor Vafeiadis (MPI-SWS)

See also

• More papers about persistent memory.