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

Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure’s procedures. Such arguments are often cumbersome as the linearization points’ position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated.

In this paper we propose a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure’s auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs. We name the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modeled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. We illustrate the method by verifying (mechanically in Coq) an intricate optimal snapshot algorithm due to Jayanti, as well as some clients.

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