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

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
Times are displayed in time zone: Central Time (US & Canada) change

07:00 - 08:20: M-1Research Papers at SPLASH-I +12h
Chair(s): Peter ThiemannUniversity of Freiburg, Germany, John BoylandUniveristy of Wisconsin, Milwaukee
07:00 - 07:20
Talk
Research Papers
Magnus MadsenAarhus University, Ondřej LhotákUniversity of Waterloo, Frank TipNortheastern University
Link to publication DOI Media Attached
07:20 - 07:40
Talk
Research Papers
Evgenii MoiseenkoSt. Petersburg University / JetBrains Research, Anton PodkopaevNRU HSE, JetBrains Research, Ori LahavTel Aviv University, Orestis MelkonianUtrecht University, Viktor VafeiadisMPI-SWS
Link to publication DOI Media Attached
07:40 - 08:00
Talk
Research Papers
Jan de Muijnck-HughesUniversity of Glasgow, Wim VanderbauwhedeUniversity of Glasgow, Edwin BradyUniversity of St. Andrews
Link to publication DOI Media Attached
08:00 - 08:20
Talk
Research Papers
Alexandros TasosImperial College London, Juliana Franco, Sophia DrossopoulouImperial College London, Tobias WrigstadUppsala University, Sweden, Susan EisenbachImperial College London
Link to publication DOI Media Attached
19:00 - 20:20: M-1Research Papers at SPLASH-I
Chair(s): Yu David LiuState University of New York (SUNY) Binghamton, Hidehiko MasuharaTokyo Institute of Technology
19:00 - 19:20
Talk
Research Papers
Magnus MadsenAarhus University, Ondřej LhotákUniversity of Waterloo, Frank TipNortheastern University
Link to publication DOI Media Attached
19:20 - 19:40
Talk
Research Papers
Evgenii MoiseenkoSt. Petersburg University / JetBrains Research, Anton PodkopaevNRU HSE, JetBrains Research, Ori LahavTel Aviv University, Orestis MelkonianUtrecht University, Viktor VafeiadisMPI-SWS
Link to publication DOI Media Attached
19:40 - 20:00
Talk
Research Papers
Jan de Muijnck-HughesUniversity of Glasgow, Wim VanderbauwhedeUniversity of Glasgow, Edwin BradyUniversity of St. Andrews
Link to publication DOI Media Attached
20:00 - 20:20
Talk
Research Papers
Alexandros TasosImperial College London, Juliana Franco, Sophia DrossopoulouImperial College London, Tobias WrigstadUppsala University, Sweden, Susan EisenbachImperial College London
Link to publication DOI Media Attached