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

The field of concurrent separation logics (CSLs) has recently undergone two exciting developments: (1) the \emph{Iris framework} for encoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for \emph{weak memory models}, notably C11’s release-acquire (RA) consistency. Unfortunately, these developments are seemingly incompatible, since Iris only applies to languages with an operational interleaving semantics, while C11 is defined by a declarative (axiomatic) semantics. In this paper, we show that, on the contrary, it is useful and feasible to marry these developments together. Our first step is to provide a novel operational characterization of RA+NA, the fragment of C11 containing RA accesses and ``non-atomic'' (normal data) accesses. Instantiating Iris with this semantics, we then derive higher-order variants of two prominent RA+NA logics, GPS and RSL. Finally, we deploy these derived logics in order to perform the first mechanical verifications (in Coq) of several interesting case studies of RA+NA programming. In a nutshell, we provide the first foundationally verified framework for proving programs correct under C11’s weak-memory semantics.

Thu 22 Jun
Times are displayed in 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 LeaState University of New York, Oswego
10:30 - 10:55
Talk
Concurrent Data Structures Linked in Time
ECOOP Research Papers
Germán Andrés DelbiancoIMDEA Software Institute, Ilya SergeyUniversity College London, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
Link to publication Media Attached
10:55 - 11:20
Talk
Contracts in the Wild: A Study of Java Programs
ECOOP Research Papers
Jens DietrichMassey University, David J. PearceVictoria University of Wellington, Kamil JezekUniversity of West Bohemia, Pilsen, CZ, Premek BradaUniversity of West Bohemia
Link to publication Pre-print Media Attached
11:20 - 11:45
Talk
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
ECOOP Research Papers
Jan-Oliver KaiserMPI-SWS, Hoang-Hai DangMPI-SWS, Derek DreyerMPI-SWS, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Link to publication Media Attached
11:45 - 12:10
Talk
Promising Compilation to ARMv8 POP
ECOOP Research Papers
Anton PodkopaevSt. Petersburg University, JetBrains, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Link to publication Media Attached