View-Based Owicki–Gries Reasoning for Persistent x86-TSO

Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson

פרסום מחקרי: פרק בספר / בדוח / בכנספרסום בספר כנסביקורת עמיתים

תקציר

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.

שפה מקוריתאנגלית
כותר פרסום המארחProgramming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
עורכיםIlya Sergey
מוציא לאורSpringer Science and Business Media Deutschland GmbH
עמודים234-261
מספר עמודים28
מסת"ב (מודפס)9783030993351
מזהי עצם דיגיטלי (DOIs)
סטטוס פרסוםפורסם - 2022
אירוע31st European Symposium on Programming, ESOP 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 - Munich, גרמניה
משך הזמן: 5 אפר׳ 20227 אפר׳ 2022

סדרות פרסומים

שםLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
כרך13240 LNCS

כנס

כנס31st European Symposium on Programming, ESOP 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022
מדינה/אזורגרמניה
עירMunich
תקופה5/04/227/04/22

ASJC Scopus subject areas

  • ???subjectarea.asjc.2600.2614???
  • ???subjectarea.asjc.1700.1700???

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'View-Based Owicki–Gries Reasoning for Persistent x86-TSO'. יחד הם יוצרים טביעת אצבע ייחודית.

פורמט ציטוט ביבליוגרפי