Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8
Thu 24 Jun 2021 21:05 - 21:10 at PLDI-B - Talks 3B: Architectures and Systems
Non-volatile memory (NVM) is a cutting-edge storage technology that promises the performance of DRAM with the durability of SSD.
Recent work has proposed several \emph{persistency models} for mainstream architectures such as Intel-x86 and Armv8, describing the order in which writes are propagated to NVM.
However, these models have several limitations; most notably, they either lack operational models or do not support persistent synchronization patterns.
We close this gap by revamping the existing persistency models.
First, inspired by the recent work on promising semantics, we propose a \emph{unified operational style} for describing persistency using \emph{views}, and develop view-based operational persistency models for Intel-x86 and Armv8, thus presenting the \emph{first} operational model for Armv8 persistency.
Next, we propose a \emph{unified axiomatic style} for describing hardware persistency, allowing us to recast and repair the existing axiomatic models of Intel-x86 and Armv8 persistency.
We prove that our axiomatic models are equivalent to the authoritative semantics reviewed by Intel and Arm engineers.
We further prove that each axiomatic hardware persistency model is equivalent to its operational counterpart.
Finally, we develop a persistent model checking algorithm and tool, and use it to verify several representative examples.
Thu 24 JunDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 09:40 | |||
09:00 5mTalk | Reticle: A Virtual Machine for Programming Modern FPGAs PLDI Luis Vega University of Washington, Joseph McMahan University of Washington, Adrian Sampson Cornell University, Dan Grossman University of Washington, Luis Ceze University of Washington DOI | ||
09:05 5mTalk | Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8 PLDI Kyeongmin Cho KAIST, Sung-Hwan Lee Seoul National University, Azalea Raad Imperial College London, Jeehoon Kang KAIST DOI | ||
09:10 5mTalk | Developer and User-Transparent Compiler Optimization for Interactive Applications PLDI Paschalis Mpeis University of Edinburgh, Pavlos Petoumenos University of Manchester, Kim Hazelwood Facebook AI Research, Hugh Leather Facebook Link to publication DOI Media Attached | ||
09:15 5mTalk | Perceus: Garbage Free Reference Counting with Reuse PLDI Alex Reinking Microsoft Research, Ningning Xie University of Toronto, Leonardo de Moura Microsoft Research, Daan Leijen Microsoft Research DOI | ||
09:20 5mTalk | Filling Typed Holes with Live GUIs PLDI Cyrus Omar University of Michigan, David Moon University of Michigan, Andrew Blinn University of Michigan, Ian Voysey Carnegie Mellon University, Nick Collins University of Chicago, Ravi Chugh University of Chicago DOI Pre-print | ||
09:25 5mTalk | Boosting SMT Solver Performance on Mixed-Bitwise-Arithmetic Expressions PLDI Dongpeng Xu University of New Hampshire, Binbin Liu University of New Hampshire; University of Science and Technology of China, Weijie Feng University of Science and Technology of China, Jiang Ming University of Texas at Arlington, Qilong Zheng University of Science and Technology of China, Jing Li University of Science and Technology of China, Qiaoyan Yu University of New Hampshire DOI | ||
09:30 5mTalk | Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems PLDI Milijana Surbatovich Carnegie Mellon University, Limin Jia Carnegie Mellon University, Brandon Lucia Carnegie Mellon University DOI | ||
09:35 5mTalk | Bliss: Auto-tuning Complex Applications using a Pool of Diverse Lightweight Learning Models PLDI Rohan Basu Roy Northeastern University, Tirthak Patel Northeastern University, Vijay Gadepally MIT Lincoln Laboratory, Devesh Tiwari Northeastern University DOI |
21:00 - 21:40 | |||
21:00 5mTalk | Reticle: A Virtual Machine for Programming Modern FPGAs PLDI Luis Vega University of Washington, Joseph McMahan University of Washington, Adrian Sampson Cornell University, Dan Grossman University of Washington, Luis Ceze University of Washington DOI | ||
21:05 5mTalk | Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8 PLDI Kyeongmin Cho KAIST, Sung-Hwan Lee Seoul National University, Azalea Raad Imperial College London, Jeehoon Kang KAIST DOI | ||
21:10 5mTalk | Developer and User-Transparent Compiler Optimization for Interactive Applications PLDI Paschalis Mpeis University of Edinburgh, Pavlos Petoumenos University of Manchester, Kim Hazelwood Facebook AI Research, Hugh Leather Facebook Link to publication DOI Media Attached | ||
21:15 5mTalk | Perceus: Garbage Free Reference Counting with Reuse PLDI Alex Reinking Microsoft Research, Ningning Xie University of Toronto, Leonardo de Moura Microsoft Research, Daan Leijen Microsoft Research DOI | ||
21:20 5mTalk | Filling Typed Holes with Live GUIs PLDI Cyrus Omar University of Michigan, David Moon University of Michigan, Andrew Blinn University of Michigan, Ian Voysey Carnegie Mellon University, Nick Collins University of Chicago, Ravi Chugh University of Chicago DOI Pre-print | ||
21:25 5mTalk | Boosting SMT Solver Performance on Mixed-Bitwise-Arithmetic Expressions PLDI Dongpeng Xu University of New Hampshire, Binbin Liu University of New Hampshire; University of Science and Technology of China, Weijie Feng University of Science and Technology of China, Jiang Ming University of Texas at Arlington, Qilong Zheng University of Science and Technology of China, Jing Li University of Science and Technology of China, Qiaoyan Yu University of New Hampshire DOI | ||
21:30 5mTalk | Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems PLDI Milijana Surbatovich Carnegie Mellon University, Limin Jia Carnegie Mellon University, Brandon Lucia Carnegie Mellon University DOI | ||
21:35 5mTalk | Bliss: Auto-tuning Complex Applications using a Pool of Diverse Lightweight Learning Models PLDI Rohan Basu Roy Northeastern University, Tirthak Patel Northeastern University, Vijay Gadepally MIT Lincoln Laboratory, Devesh Tiwari Northeastern University DOI |