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 paper 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 an intricate optimal snapshot algorithm due to Jayanti.