Proving Correctness of Highly-Concurrent Linearisable ObjectsReportar como inadecuado




Proving Correctness of Highly-Concurrent Linearisable Objects - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 Regal - Large-Scale Distributed Systems and Applications LIP6 - Laboratoire d-Informatique de Paris 6, Inria Paris-Rocquencourt

Abstract : We study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical, coarse-grain synchronisation. Our examples are demonstrative of common design patterns such as lock coupling, optimistic, and lazy synchronisation. Although they are are highly concurrent, we prove that they are linearisable, safe, and they correctly implement a high-level abstraction. Our proofs illustrate the power and applicability of rely-guarantee reasoning, as well of some of its limitations. The examples of the paper establish a benchmark challenge for other reasoning techniques.

Keywords : SHARED-MEMORY CONCURRENCY FORMAL VERIFICATION LINEARISABILITY RELY-GUARANTEE REASONING CONCURRENT PROGRAMMING





Autor: Viktor Vafeiadis Maurice Herlihy Tony Hoare Marc Shapiro -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados