Persistent owicki-gries reasoning: a program logic for reasoning about persistent programs on Intel-x86

File Description SizeFormat 
3428219.pdfPublished version460.09 kBAdobe PDFView/Open
Title: Persistent owicki-gries reasoning: a program logic for reasoning about persistent programs on Intel-x86
Authors: Raad, A
Lahav, O
Vafeiadis, V
Item Type: Journal Article
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.
Issue Date: 13-Nov-2020
Date of Acceptance: 1-Nov-2020
URI: http://hdl.handle.net/10044/1/97398
DOI: 10.1145/3428219
ISSN: 2475-1421
Publisher: Association for Computing Machinery (ACM)
Start Page: 1
End Page: 28
Journal / Book Title: Proceedings of the ACM on Programming Languages
Volume: 4
Issue: OOPSLA
Replaces: http://hdl.handle.net/10044/1/84612
10044/1/84612
Copyright Statement: © 2020 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.
Publication Status: Published
Online Publication Date: 2020-11-01
Appears in Collections:Computing



This item is licensed under a Creative Commons License Creative Commons