ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Mon 16 Nov 2020 07:20 - 07:40 at SPLASH-I - M-1 Chair(s): John Boyland, Peter Thiemann
Mon 16 Nov 2020 19:20 - 19:40 at SPLASH-I - M-1 Chair(s): Yu David Liu, Hidehiko Masuhara

Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous “out-of-thin-air” problem, and to enable efficient compilation to hardware. Nevertheless, this latter property—compilation correctness—has not yet been formally established. This paper closes this gap by establishing correctness in Coq of the intended compilation schemes from Weakestmo to a wide range of formal hardware memory models (x86, POWER, ARMv7, ARMv8). Our proof is the first that establishes correctness of compilation of an event-structure-based model that forbids “thin-air” behaviors, as well as the first mechanized compilation proof of a weak memory model supporting sequentially consistent accesses to such a range of hardware platforms. Our compilation proof goes via the recent Intermediate Memory Model (IMM), which we suitably extend with sequentially consistent accesses.

Mon 16 Nov

Displayed time zone: Central Time (US & Canada) change

07:00 - 08:20
M-1Research Papers at SPLASH-I +12h
Chair(s): John Boyland Univeristy of Wisconsin, Milwaukee, Peter Thiemann University of Freiburg, Germany
07:00
20m
Talk
A Semantics for the Essence of React
Research Papers
Magnus Madsen Aarhus University, Ondřej Lhoták University of Waterloo, Frank Tip Northeastern University
Link to publication DOI Media Attached
07:20
20m
Talk
Reconciling Event Structures with Modern Multiprocessors
Research Papers
Evgenii Moiseenko St. Petersburg University / JetBrains Research, Anton Podkopaev NRU HSE, JetBrains Research, Ori Lahav Tel Aviv University, Orestis Melkonian Utrecht University, Viktor Vafeiadis MPI-SWS
Link to publication DOI Media Attached
07:40
20m
Talk
A Framework for Resource Dependent EDSLs in a Dependently Typed Language
Research Papers
Jan de Muijnck-Hughes University of Glasgow, Wim Vanderbauwhede University of Glasgow, Edwin Brady University of St. Andrews
Link to publication DOI Media Attached
08:00
20m
Talk
Reshape your layouts, not your programs: A safe language extension for better cache localitySCICO Journal-First
Research Papers
Alexandros Tasos Imperial College London, Juliana Franco , Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
Link to publication DOI Media Attached
19:00 - 20:20
M-1Research Papers at SPLASH-I
Chair(s): Yu David Liu State University of New York (SUNY) Binghamton, Hidehiko Masuhara Tokyo Institute of Technology
19:00
20m
Talk
A Semantics for the Essence of React
Research Papers
Magnus Madsen Aarhus University, Ondřej Lhoták University of Waterloo, Frank Tip Northeastern University
Link to publication DOI Media Attached
19:20
20m
Talk
Reconciling Event Structures with Modern Multiprocessors
Research Papers
Evgenii Moiseenko St. Petersburg University / JetBrains Research, Anton Podkopaev NRU HSE, JetBrains Research, Ori Lahav Tel Aviv University, Orestis Melkonian Utrecht University, Viktor Vafeiadis MPI-SWS
Link to publication DOI Media Attached
19:40
20m
Talk
A Framework for Resource Dependent EDSLs in a Dependently Typed Language
Research Papers
Jan de Muijnck-Hughes University of Glasgow, Wim Vanderbauwhede University of Glasgow, Edwin Brady University of St. Andrews
Link to publication DOI Media Attached
20:00
20m
Talk
Reshape your layouts, not your programs: A safe language extension for better cache localitySCICO Journal-First
Research Papers
Alexandros Tasos Imperial College London, Juliana Franco , Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
Link to publication DOI Media Attached