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
المعرِّفات الرقمية للأشياء
حالة النشرنُشِر - 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, ألمانيا
المدة: ٥ أبريل ٢٠٢٢٧ أبريل ٢٠٢٢

سلسلة المنشورات

الاسمLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
مستوى الصوت13240 LNCS

!!Conference

!!Conference31st European Symposium on Programming, ESOP 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022
الدولة/الإقليمألمانيا
المدينةMunich
المدة٥/٠٤/٢٢٧/٠٤/٢٢

All Science Journal Classification (ASJC) codes

  • !!Theoretical Computer Science
  • !!General Computer Science

بصمة

أدرس بدقة موضوعات البحث “View-Based Owicki–Gries Reasoning for Persistent x86-TSO'. فهما يشكلان معًا بصمة فريدة.

قم بذكر هذا