®®®® SIIA Público

Título del libro: Proceedings Of The Annual Acm Symposium On Principles Of Distributed Computing
Título del capítulo: Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

Autores UNAM:
ARMANDO CASTAÑEDA ROJANO; GILDE VALERIA RODRIGUEZ JIMENEZ;
Autores externos:

Idioma:

Año de publicación:
2023
Palabras clave:

Concurrent algorithms; Distributed runtime; Distributed runtime verification; Enforcement; Linearizability; Lock freedoms; Run-time verification; Runtimes; Shared memory; Wait-freedom; Fault tolerance


Resumen:

This paper studies the problem of verifying linearizability at runtime, where one seeks for a concurrent algorithm for verifying that the current execution of a given concurrent shared object implementation is linearizable. It shows that it is impossible to runtime verify linearizability for some common sequential objects, regardless of the consensus power of base objects. Then, it argues that actually a stronger version of the problem can be solved, if linearizability is verified indirectly. Namely, it shows that (1) linearizability of a class of concurrent implementations can be strongly verified using only read/write base objects (i.e. without the need of consensus), and (2) any implementation can be transformed to its counterpart in the class (which implements the same object) using only read/write objects too. As far as we know, this is the first runtime verification algorithm for any correctness condition that is fully asynchronous and fault-tolerant. As a by-product, a simple and generic methodology for deriving self-enforced linearizable implementations is obtained. This type implementations produce outputs that are guaranteed linearizable, and are able to produce a certificate of it, which allows the design of concurrent systems in a modular manner with accountable and forensic guarantees. These results hold not only for linearizability but for a correctness condition that includes generalizations of it such as set-linearizability and interval-linearizability. © 2023 ACM.


Entidades citadas de la UNAM: