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

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