Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             Lundi 18 juin, 14h00

                               ----------------
                               Germán Delbianco
                               ----------------

                                     IRIF

                  =========================================
                  Concurrent Data Structures Linked in Time
                  =========================================

Arguments about linearizability of a concurrent data structure are typically
carried out by specifying the linearization points of the data structure's
procedures. Proofs that use such specifications are often cumbersome as the
linearization points' position in time can be dynamic, non-local and
non-regional: it can depend on the interference, run-time values and events
from the past, or even future, appear in procedures other than the one
considered, and might be only determined after the considered procedure has
terminated. In this talk we propose a new method, based on a Hoare-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 a
heap. We illustrate the method by verifying, in FCSL, an intricate optimal
snapshot algorithm by Jayanti.

(This is joint work with Aleks Nanevski, Ilya Sergey and Anindya Banerjee and
it was published in ECOOP'17.)