English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Los programadores pueden afrontar la complejidad de escribir software concurrente con la ayuda de librerias de estructuras de datos concurrentes y, mas recientemente, memoria transaccional. Ambos enfoques facilitan el desarrollo de software proporcionando al programador garantias de correccion, que abstraen los detalles de la implementacion de librerias y memoria transaccional: el programador puede asumir que los metodos y transacciones se ejecutan atomicamente, aun cuando sus implementaciones en realidad sean concurrentes. Habitualmente, los investigadores, para justificar estas garantias de correcion, 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 logica modular y tecnicas de demostracion capaces de razonar sobre implementaciones de estructuras de datos concurrentes de grano fino, y sobre memoria transaccional. Tambien proporcionamos fundamentos formales para un modelo de programacion en el que se puede acceder a la memoria tanto desde dentro como desde fuera de una transaccion. Nuestra primera aportacion es una logica general para demostrar linearizabilidad, basada en la logica “Views framework” y puede ser instanciada con diferentes metodos de razonamiento composicional sobre la concurrencia, tales como la logica de separacion o la logica “rely-guarantee”. Independientemente de la eleccion que se haga acerca del metodo de razonamiento modular con respecto a un hilo, la logica generica aqui propuesta explica los principios de demostracion de la linearizabilidad, mediante el metodo de punto de linearizabilidad, habitualmente utilizado. Tambien demostramos la solidez de nuestra logica general. En nuestra segunda aportacion, proponemos un metodo de demostracion de la linearizabilidad de ciertas estructuras de datos sobre las que es complicado razonar usando el metodo de puntos de linearizabilidad (por ejemplo, la Herlihy- Wing queue y la Time-Stamped queue). La idea clave de nuestro metodo es la construccion incremental, no de un unico orden lineal de operaciones, sino de un orden parcial que describe multiples linearizaciones que satisfacen la especificacion secuencial. Esto permite retrasar las decisiones acerca del orden de las operaciones, imitando el comportamiento de la implementacion de las estructuras de datos. Formalizamos nuestro metodo como una logica basada en “rely-guarantee”, y demostramos su efectividad verificando diferentes estructuras de datos retadoras: las colas Herlihy-Wing y Time-Stamped, asi como el Optimistic set. Por ultimo, proponemos fundamentos para un modelo de programacion, donde el programador puede acceder los mismos datos tanto desde dentro como desde fuera de una transaccion. Idealmente, estos accesos se ejecutan con garantias atomicas fuertes. Desafortunadamente, muchas implementaciones de memoria transaccional que satisfacen el criterio de opacidad no proporcionan estas garantias, dado que en la practica son prohibitivamente caras. Diversos investigadores han propuesto garantizar atomicidad fuerte solo para ciertos programas libres de condiciones de carrera, y, en particular, para programas que realizan accesos no transaccionales siguiendo el estilo de privatizacion. Nuestra contribucion es proponer una definicion de condicion de carrera que de cabida a la privatizacion. 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 semantica de atomicidad fuerte. Mostramos que nuestra definicion de condicion de carrera permite al programador seguir los estilos de privatizacion. Tambien proponemos un metodo para demostrar nuestra generalizacion 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.

Proving consistency of concurrent data structures and transactional memory systems