Visibility and Separability for Declarative Proofs of Linearizability

Resumen

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).