Proving consistency of concurrent data structures and transactional memory systems

Los programadores pueden afrontar la complejidad de escribir software concurrente con la ayuda de librerías de estructuras de datos concurrentes y, más recientemente, memoria transaccional. Ambos enfoques facilitan el desarrollo de software proporcionando al programador garantías de corrección, que abstraen los detalles de la implementación de librerías y memoria transaccional: el programador puede asumir que los métodos y transacciones se ejecutan atómicamente, aún cuando sus implementaciones en realidad sean concurrentes. Habitualmente, los investigadores, para justificar estas garantías de correción, demuestran ciertos requisitos de consistencia: linearizabilidad en el caso de estructuras de datos concurrentes, y opacidad en memoria transaccional. Esta tesis se centra en demostrar formalmente requisitos de consistencia. Proponemos una lógica modular y técnicas de demostración capaces de razonar sobre implementaciones de estructuras de datos concurrentes de grano fino, y sobre memoria transaccional. También proporcionamos fundamentos formales para un modelo de programación en el que se puede acceder a la memoria tanto desde dentro como desde fuera de una transacción. Nuestra primera aportación es una lógica general para demostrar linearizabilidad, basada en la lógica “Views framework” y puede ser instanciada con diferentes métodos de razonamiento composicional sobre la concurrencia, tales como la lógica de separación o la lógica “rely-guarantee”. Independientemente de la elección que se haga acerca del método de razonamiento modular con respecto a un hilo, la logica genérica aquí propuesta explica los principios de demostración de la linearizabilidad, mediante el método de punto de linearizabilidad, habitualmente utilizado. También demostramos la solidez de nuestra logica general. En nuestra segunda aportación, proponemos un método de demostración de la linearizabilidad de ciertas estructuras de datos sobre las que es complicado razonar usando el método de puntos de linearizabilidad (por ejemplo, la Herlihy- Wing queue y la Time-Stamped queue). La idea clave de nuestro método es la construcción incremental, no de un único orden lineal de operaciones, sino de un orden parcial que describe múltiples linearizaciones que satisfacen la especificación secuencial. Esto permite retrasar las decisiones acerca del orden de las operaciones, imitando el comportamiento de la implementación de las estructuras de datos. Formalizamos nuestro método como una lógica basada en “rely-guarantee”, y demostramos su efectividad verificando diferentes estructuras de datos retadoras: las colas Herlihy-Wing y Time-Stamped, así como el Optimistic set. Por último, proponemos fundamentos para un modelo de programación, donde el programador puede acceder los mismos datos tanto desde dentro como desde fuera de una transacción. Idealmente, éstos accesos se ejecutan con garantías atómicas fuertes. Desafortunadamente, muchas implementaciones de memoria transaccional que satisfacen el criterio de opacidad no proporcionan estas garantías, dado que en la práctica son prohibitivamente caras. Diversos investigadores han propuesto garantizar atomicidad fuerte sólo para ciertos programas libres de condiciones de carrera, y, en particular, para programas que realizan accesos no transaccionales siguiendo el estilo de privatización. Nuestra contribución es proponer una definición de condición de carrera que dé cabida a la privatización. Demostramos que si tenemos una memoria transaccional que satisface ciertos requisitos que generalizan la opacidad y un programa libres de condiciones de carrera asumiendo atomicidad fuerte, entonces dicho programa, en efecto, tiene una semántica de atomicidad fuerte. Mostramos que nuestra definición de condición de carrera permite al programador seguir los estilos de privatización. También proponemos un método para demostrar nuestra generalización de opacidad y aplicarlo a la memoria transaccional TL2. ----------ABSTRACT---------- Programmers can manage the complexity of constructing concurrent software with the help of libraries of concurrent data structures and, more recently, transactional memory. Both approaches facilitate software development by giving a programmer correctness guarantees that abstract from the implementation details of libraries and transactional memory: the programmer can expect that each library method or transaction execute atomically, even if in reality the implementation executes them concurrently. To justify these correctness guarantees, researchers typically prove certain consistency conditions: linearizability for concurrent data structures and opacity for transactional memory. This dissertation is dedicated to proving consistency conditions formally. We propose modular program logics and proof techniques capable of reasoning about sophisticated fine-grained concurrent implementations of data structures and transactional memory. We also provide formal foundations for the programming model in which memory can be accesses both inside and outside of transactions. Our first contribution is a generic logic for proving linearizability, which builds on the Views framework and can be instantiated with different means of compositional reasoning about concurrency, such as separation logic or relyguarantee. The proposed generic logic explicates principles of proving linearizability with commonly-used linearization-point method independently from a particular choice of an approach to thread-modular reasoning. We also prove our generic logic sound. In our second contribution, we propose a proof method for linearizability of data structures that are challenging to reason about using linearization points (e.g., the Herlihy-Wing queue and the Time-Stamped queue). The key idea of our method is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behavior of data structure implementations. We formalize our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the Time-Stamped queue and the Optimistic set. Finally, we provide foundations for a programming model where a programmer can access the same data both inside and outside of transactions. In this model programmers would like to have strong atomicity guarantees from TM. Unfortunately, many implementations satisfying opacity do not provide them, since it is prohibitively expensive in practice. Researchers have suggested guaranteeing strong atomicity only for certain data-race free (DRF) programs and, in particular, for programs performing non-transactional accesses according to the privatization idiom. Our contribution is to propose a notion of DRF that supports privatization. We prove that, if a TM satisfies a certain condition generalizing opacity and a program using it is DRF assuming strong atomicity, then the program indeed has strongly atomic semantics. We show that our DRF notion allows the programmer to use privatization idioms. We also propose a method for proving our generalization of opacity and apply it to the TL2 TM