Concurrent library abstraction without information hiding

Abstract

The commonly accepted approach to specifying libraries of concurrent algorithms is a library abstraction. Its idea is to relate a library to another one that abstracts away from details of its implementation and is simpler to reason about. A library abstraction relation has to validate the Abstraction Theorem: while proving a property of the client of the concurrent library, the library can be soundly replaced with its abstract implementation. Typically a library abstraction relation, such as linearizability, assumes a complete information hiding between a library and its client, which disallows them to communicate by means of shared memory. However, such way of communication may be used in a program, and correctness of interactions
on a shared memory depends on the implicit contract between the library and the client.
In this work we approach library abstraction without any assumptions about information hiding. To be able to formulate the contract between components of the program, we augment machine states of the program with two abstract states, views, of the client and the library. It enables formalising the contract with the internal safety, which requires components to preserve each other's views whenever
their command is executed. We define the library a a correspondence between possible uses of a concrete and an abstract library. For our library abstraction relation and traces of a program, components of which follow their contract, we prove an Abstraction Theorem.
RESUMEN.
La técnica más aceptada actualmente para la especificación de librerías de algoritmos concurrentes es la abstracción de librerías (library abstraction). La idea subyacente
es relacionar la librería original con otra que abstrae los detalles de implementación y conóon que describa dicha
abstracción de librerías debe validar el Teorema de Abstracción: durante la prueba de la validez de una propiedad del cliente de la librería concurrente, el reemplazo de esta última por su implementación abstracta es lógicamente correcto. Usualmente, una relación de abstracción de librerías como la linearizabilidad (linearizability), tiene como premisa el ocultamiento de información entre el cliente y la librería (information hiding), es decir, que no se les permite comunicarse mediante la memoria compartida. Sin embargo, dicha comunicación ocurre en la práctica y la correctitud
de estas interacciones en una memoria compartida depende de un contrato implícito entre la librería y el cliente.
En este trabajo, se propone un nueva definición del concepto de abtracción de librerías que no presupone un ocultamiento de información entre la librería y el
cliente. Con el fin de establecer un contrato entre diferentes componentes de un programa, extendemos la máquina de estados subyacente con dos estados abstractos
que representan las vistas del cliente y la librería. Esto permite la formalización de la propiedad de seguridad interna (internal safety), que requiere que cada componente
preserva la vista del otro durante la ejecuci on de un comando. Consecuentemente, se define la relación de abstracción de librerías mediante una correspondencia entre
los usos posibles de una librería abstracta y una concreta. Finalmente, se prueba el Teorema de Abstracción para la relación de abstracción de librerías propuesta, para
cualquier traza de un programa y cualquier componente que satisface los contratos apropiados.