SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
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 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
15m
Talk
Programming and Reasoning with Partial Observability
SIGPLAN Papers
Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
14:05
15m
Talk
Pomsets with Preconditions: A Simple Model of Relaxed Memory
SIGPLAN Papers
Radha Jagadeesan DePaul University, Alan Jeffrey Roblox, James Riely DePaul University
14:20
15m
Talk
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
15m
Paper
Demystifying Dependence
SIGPLAN Papers
James Koppel Massachusetts Institute of Technology, USA, Daniel Jackson MIT
Link to publication Pre-print
14:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers