Visibility and Separability for Declarative Proofs of Linearizability
Authors:   , Dom�nguez S�nchez Jes�s H�ctor 
Published: May 2024

Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms linearization points. However, linearization points often hinder abstraction, and for some algorithms it is unclear how to even identify their linearization points. This dissertation shows how to develop declarative proofs of linearizability by foregoing linearization points and instead employing axiomatization of so-called visibility relations. While visibility relations have been considered before for some of the data structures explored in this dissertation, the results in this document are the first to show how to derive concurrent axiomatizations systematically and intuitively from the atomic specification of the data structure. The main contribution of this dissertation is the extension of the visibility relations technique with a novel relation, called separability, that emerges to generalize real-time precedence of procedure invocation. It is the separability relation that enables the systematic derivation of concurrent axiomatizations from atomic specifications. The visibility and separability relations have natural definitions for the algorithms considered in this dissertation. This provides strong evidence that visibility and separability are useful abstractions for building declarative proofs of linearizability. In particular, this dissertation applies visibility and separability to build novel linearizability proofs for the Timestamped stack of Dodds et al. and several descriptor-based algorithms of Harris et al. (RDCSS, MCAS, and optimizations). RESUMEN La linealizabilidad es un criterio est�ndar de correcci�n para algoritmos concurrentes que t�picamente se demuestra mediante la localizaci�n de los puntos de linealizaci�n del algoritmo. Sin embargo, el uso de puntos de linealizaci�n obstaculiza la construcci�n de abstracciones, y para algunos algoritmos, ni siquiera es claro el c�mo identificar sus puntos de linealizaci�n. Esta disertaci�n muestra c�mo desarrollar demostraciones declarativas de linealizabilidad que se centran en la axiomatizaci�n de relaciones de visibilidad, en lugar de la identificaci�n de puntos de linealizaci�n. Aunque las relaciones de visibilidad han sido usadas antes en algunas de las estructuras de datos que se exploran en esta disertaci�n, los resultados en este documento son los primeros en mostrar c�mo derivar, sistem�tica e intuitivamente, axiomatizaciones concurrentes a partir de la especificaci�n at�mica de la estructura de datos. La principal contribuci�n de esta disertaci�n es la extensi�n de la t�cnica de relaciones de visibilidad con una nueva relaci�n, llamada separabilidad, que emerge de la generalizaci�n de la precedencia en tiempo real entre invocaci�n de procedimientos. La relaci�n de separabilidad es la que permite la derivaci�n sistem�tica de axiomatizaciones concurrentes a partir de especificaciones at�micas. Las relaciones de visibilidad y separabilidad tienen definiciones naturales en los algoritmos considerados en esta disertaci�n. Esta es fuerte evidencia de que visibilidad y separabilidad son abstracciones �tiles en la construcci�n de demostraciones declarativas de linealizabilidad. En particular, esta disertaci�n usa visibilidad y separabilidad para construir novedosas demostraciones de linealizabilidad para la pila con marcas de tiempo de Dodds et al. y varios algoritmos basados en descriptores de Harris et al. (RDCSS, MCAS, y optimizaciones).