View-based Owicki-Gries reasoning for persistent x86-TSO
File(s)978-3-030-99336-8.pdf (10.79 MB)
Published version
Author(s)
Bila, Eleni
Dongol, Brijesh
Lahav, Ori
Raad, azalea
Wickerson, John
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
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 Issued
2022-03-29
Date Acceptance
2021-12-24
Citation
Lecture Notes in Computer Science, 2022, 13240, pp.234-261
ISSN
0302-9743
Publisher
Springer
Start Page
234
End Page
261
Journal / Book Title
Lecture Notes in Computer Science
Volume
13240
Copyright Statement
© The Editor(s) (if applicable) and The Author(s) 2022. This book is an open access publication.
Open Access This book is licensed under the terms of the Creative Commons Attribution 4.0 International
License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution
and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and
the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this book are included in the book’s Creative Commons license,
unless indicated otherwise in a credit line to the material. If material is not included in the book’s Creative
Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use,
you will need to obtain permission directly from the copyright holder.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication
does not imply, even in the absence of a specific statement, that such names are exempt from the relevant
protective laws and regulations and therefore free for general use.
The publisher, the authors and the editors are safe to assume that the advice and information in this book are
believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors
give a warranty, expressed or implied, with respect to the material contained herein or for any errors or
omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in
published maps and institutional affiliations.
Open Access This book is licensed under the terms of the Creative Commons Attribution 4.0 International
License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution
and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and
the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this book are included in the book’s Creative Commons license,
unless indicated otherwise in a credit line to the material. If material is not included in the book’s Creative
Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use,
you will need to obtain permission directly from the copyright holder.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication
does not imply, even in the absence of a specific statement, that such names are exempt from the relevant
protective laws and regulations and therefore free for general use.
The publisher, the authors and the editors are safe to assume that the advice and information in this book are
believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors
give a warranty, expressed or implied, with respect to the material contained herein or for any errors or
omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in
published maps and institutional affiliations.
License URL
Sponsor
Engineering & Physical Science Research Council (E
UK Research and Innovation
Identifier
http://link.springer.com/chapter/10.1007/978-3-030-99336-8_9
Grant Number
Ref: 542716
MR/V024299/1
Source
European Symposium on Programming (ESOP) 2020
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
Persistent memory
x86-TSO
Owicki-Gries
Isabelle/HOL
verification
SEMANTICS
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2022-04-02
Finish Date
2022-04-07
Coverage Spatial
Munich, Germany
Date Publish Online
2022-03-29