Write a Blog >>
Thu 22 Jun 2017 11:45 - 12:10 at Auditorium, Vertex Building - Specification and Verification Chair(s): Doug Lea

We prove the correctness of compilation of relaxed memory accesses and release-acquire fences from the “promising”’ semantics of [Kang et al.~POPL’17] to the ARMv8 POP machine of [Flur et al.~POPL’16]. The proof is highly non-trivial because both the ARMv8 POP and the promising semantics provide some extremely weak consistency guarantees for normal memory accesses; however, they do so in rather different ways. Our proof of compilation correctness to ARMv8 POP strengthens the results of the Kang et al., who only proved the correctness of compilation to x86-TSO and Power, which are much simpler in comparison to ARMv8 POP.

Thu 22 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Specification and VerificationECOOP Research Papers at Auditorium, Vertex Building
Chair(s): Doug Lea State University of New York, Oswego
10:30
25m
Talk
Concurrent Data Structures Linked in Time
ECOOP Research Papers
Germán Andrés Delbianco IMDEA Software Institute, Ilya Sergey University College London, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute
Link to publication Media Attached
10:55
25m
Talk
Contracts in the Wild: A Study of Java Programs
ECOOP Research Papers
Jens Dietrich Massey University, David J. Pearce Victoria University of Wellington, Kamil Jezek University of West Bohemia, Pilsen, CZ, Premek Brada University of West Bohemia
Link to publication Pre-print Media Attached
11:20
25m
Talk
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
ECOOP Research Papers
Jan-Oliver Kaiser MPI-SWS, Hoang-Hai Dang MPI-SWS, Derek Dreyer MPI-SWS, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Link to publication Media Attached
11:45
25m
Talk
Promising Compilation to ARMv8 POP
ECOOP Research Papers
Anton Podkopaev St. Petersburg University, JetBrains, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Link to publication Media Attached