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

ecoop-2017-papers
10:30 - 12:10: ECOOP Research Papers - Specification and Verification at Auditorium, Vertex Building
Chair(s): Doug LeaState University of New York, Oswego
ecoop-2017-papers10:30 - 10:55
Talk
Germán Andrés DelbiancoIMDEA Software Institute, Ilya SergeyUniversity College London, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
Link to publication Media Attached
ecoop-2017-papers10:55 - 11:20
Talk
Jens DietrichMassey University, David PearceVictoria University of Wellington, Kamil JezekUniversity of West Bohemia, Pilsen, CZ, Premek BradaUniversity of West Bohemia
Link to publication Pre-print Media Attached
ecoop-2017-papers11:20 - 11:45
Talk
Jan-Oliver KaiserMPI-SWS, Hoang-Hai DangMPI-SWS, Derek DreyerMPI-SWS, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Link to publication Media Attached
ecoop-2017-papers11:45 - 12:10
Talk
Anton PodkopaevSt. Petersburg University, JetBrains, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Link to publication Media Attached