IRUS Total

View-based Owicki-Gries reasoning for persistent x86-TSO

File Description SizeFormat 
2201.05860.pdfFile embargoed until 01 January 10000411.53 kBAdobe PDF
Title: View-based Owicki-Gries reasoning for persistent x86-TSO
Authors: Bila, E
Dongol, B
Lahav, O
Raad, A
Wickerson, J
Item Type: Conference Paper
Abstract: The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about x86 code that uses low-level operations such as memory accesses and fences, as well as persistency primitives such as flushes. Our logic, Pierogi, benefits from a simple underlying operational semantics based on views, is able to handle optimised flush operations, and is mechanised in the Isabelle/HOL proof assistant. We detail the proof rules of Pierogi and prove them sound. We also show how Pierogi can be used to reason about a range of challenging single- and multi-threaded persistent programs
Date of Acceptance: 24-Dec-2021
URI: http://hdl.handle.net/10044/1/95468
ISSN: 0302-9743
Publisher: Springer
Journal / Book Title: Lecture Notes in Computer Science
Copyright Statement: This paper is embargoed until publication.
Sponsor/Funder: Engineering & Physical Science Research Council (E
UK Research and Innovation
Funder's Grant Number: Ref: 542716
Conference Name: European Symposium on Programming (ESOP) 2020
Keywords: Artificial Intelligence & Image Processing
Publication Status: Accepted
Start Date: 2022-04-02
Finish Date: 2022-04-07
Conference Place: Munich, Germany
Embargo Date: publication subject to indefinite embargo
Open Access location: https://arxiv.org/pdf/2201.05860.pdf
Appears in Collections:Electrical and Electronic Engineering