SPLASH 2021 (series) / Recent SIGPLAN Conference Paper Presentations /
Pomsets with Preconditions: A Simple Model of Relaxed Memory
Wed 20 Oct 2021 14:05 - 14:20 at Zurich G - OOPSLA and Onward! 2020 Papers 2 Chair(s): Michael Coblenz
Relaxed memory models must simultaneously achieve efficient implementability and thread-compositional reasoning. Is that why they have become so complicated? We argue that the answer is no: It is possible to achieve these goals by combining an idea from the 60s (preconditions) with an idea from the 80s (pomsets), at least for X64 and ARMv8. We show that the resulting model (1) supports compositional reasoning for temporal safety properties, (2) supports all reasonable sequential compiler optimizations, (3) satisfies the DRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without requiring extra fences on relaxed accesses.
Wed 20 OctDisplayed time zone: Central Time (US & Canada) change
Wed 20 Oct
Displayed time zone: Central Time (US & Canada) change
13:50 - 15:10 | OOPSLA and Onward! 2020 Papers 2SIGPLAN Papers at Zurich G Chair(s): Michael Coblenz University of Maryland at College Park | ||
13:50 15mTalk | Programming and Reasoning with Partial Observability SIGPLAN Papers Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology | ||
14:05 15mTalk | Pomsets with Preconditions: A Simple Model of Relaxed Memory SIGPLAN Papers | ||
14:20 15mTalk | Koord: a language for programming and verifying distributed robotics applications SIGPLAN Papers Ritwika Ghosh University of Illinois at Urbana-Champaign, Chiao Hsieh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign | ||
14:35 15mPaper | Demystifying Dependence SIGPLAN Papers Link to publication Pre-print | ||
14:50 20mLive Q&A | Discussion, Questions and Answers SIGPLAN Papers |