Tesis:
Compositional Reasoning of Concurrency with the Visibility Method
- Autor: OHMAN, Joakim
- Título: Compositional Reasoning of Concurrency with the Visibility Method
- Fecha: 2024
- Materia:
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: SIN DEPARTAMENTO DEFINIDO
- Acceso electrónico: https://oa.upm.es/81182/
- Director/a 1º: NANEVSKI, Aleksandar
- Resumen: A challenge in concurrent programming has long been how to implement efficient concurrent programs while still being able to establish that the program is correct. Herlihy and Wing introduced the longstanding correctness criterion of linearizability, which states that a oncurrent program behaves equivalently to a sequential program.
Visibility reasoning have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent algorithms that obtains modular and reusable proofs. This is in contrast to the customary approach based on exhibiting the algorithm's linearization points.
In this dissertation, we apply visibility reasoning to develop modular proofs for four elegant concurrent snapshot algorithms, three of Jayanti and one of Afek et al. The proofs are divided by specifications into components of increasing level of abstraction; the components at higher abstraction levels are shared, i.e., they apply to all four algorithms simultaneously. Importantly, the interface properties mathematically capture Jayanti's original intuitions, which have previously only been given informally.
RESUMEN
Un reto en la programación concurrente ha sido durante mucho tiempo cómo implementar programas concurrentes eficientes sin dejar de ser capaz de establecer que el programa es correcto. Herlihy y Wing introdujeron el antiguo criterio de corrección de la linealidad, que establece que un programa concurrente se comporta de forma equivalente a un programa secuencial.
El razonamiento de visibilidad ha sido propuesto por Henzinger et al. como una abstracción para probar la linealidad de algoritmos concurrentes que obtiene pruebas modulares y reutilizables. Esto contrasta con el enfoque habitual basado en la exhibición de los puntos de linealización del algoritmo.
En esta tesis, aplicamos el razonamiento de visibilidad para desarrollar pruebas modulares para cuatro elegantes algoritmos de instantáneas concurrentes, tres de Jayanti y uno de Afek et al. Las pruebas se dividen por especificaciones en componentes de nivel de abstracción creciente; los componentes de niveles de abstracción superiores son compartidos, es decir, se aplican a los cuatro algoritmos simultáneamente. Es importante destacar que las propiedades de la interfaz recogen matemáticamente las intuiciones originales de Jayanti, que hasta ahora sólo se habían dado de manera informal.