Los tipos de datos concurrentes básicamente son implementaciones concurrentes de abstracciones de datos clásicas, diseñados específicamente para aprovechar el gran paralelismo disponible en arquitecturas multiprocesador y multinúcleo. La corrección de los tipos de datos concurrentes resulta esencial para demostrar la corrección de sistemas concurrentes en su conjunto. En este trabajo estudiamos el problema de asistir en la automatización de la verificación de propiedades temporales en tipos de datos concurrentes.udLa principal dificultad en el razonamiento sobre estos tipos de datos proviene de la interacción entre la alta concurrencia que éstos poseen y la necesidad de manipular al mismo tiempo la memoria dinámica.udLa mayoría de los enfoques utilizados hasta el momento para la verificación de tipos de datos concurrentes intentan enriquecer separation logic para poder hacer frente a la concurrencia, valiéndose del éxito alcanzado por separation logic en el razonamiento de algoritmos secuenciales y que manipulan el heap.udEste trabajo contiene dos contribuciones. En primer lugar, presentamos un enfoque complementario para la verificación de estructuras de datos concurrentes: partimos de verificación temporal deductiva, una poderosa técnica para razonar sobre sistemas concurrentes, y la enriquecemos para poder lidiar con memoria dinámica. El proceso de verificación utiliza diagramas de verificación y anotación explícita de regiones. Al final, cada prueba se descompone en una secuencia de condiciones de verificación. Losudliterales que forman parte de cada una de estas condiciones de verificación dependen casi exclusivamente de las estructuras de datos que vayan a ser verificadas.udLa segunda, y principal, contribución consiste en dos procedimientos de decisión para tipos de datos específicos: listas concurrentes simplemente enlazadas con cerrojos en cadena y listas concurrentes con saltos. Estos procedimientos de decisión son capaces de razonar sobre regiones, punteros, listas del estilo de Lisp o listas ordenadas, permitiendo la verificación automática de las condiciones de verificación generadas previamente.udAquí demostramos cómo, utilizando nuestra técnica, resulta posible demostrar no solo propiedades de seguridad, sino también viveza sobre una versión de listas concurrentes, además de la preservación de la forma de listas con saltos por parte de una estructura de datos. Así mismo, el enfoque presentado puede ser fácilmente extendido para razonar sobre un amplio espectro de tipos de datos concurrentes,udincluyendo tablas hash y grafos.ud[ABSTRACT]udConcurrent datatypes are concurrent implementation of classical data abstractions, specifically designedudto exploit the great deal of parallelism available in multiprocessor and multicore architectures.udThe correctness of concurrent datatypes is essential for the overall correctness of the system. In this work we study the problem of aiding in the automation of temporal verification of concurrent datatypes.udThe main diculty to reason about these datatypes comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. Most previous approaches to verification of concurrent datatypes try to enrich separation logic to deal with concurrency, leveraging on the success of separation logic in reasoning about sequential heap algorithms.udThis work contains two contributions. First, we present a complementary approach to the verification of concurrent data structures: we start from deductive temporal verification, a very powerful technique to reason about concurrent systems, and enrich it to cope with dynamic memory. The verification process uses verification diagrams and explicit region annotations. In the end, each proof is decomposed into a sequence of verification conditions. The literals involved in these verification conditions dependudmainly on the data structured being verified. The second, and main, contribution consists in two decision procedures for specific data-types: concurrent lock-coupling singly-linked lists and concurrent skiplists.udThese decision procedures are capable of reasoning about regions, pointers, lisp-like lists and ordered lists allowing automatic verification of generated verification conditions.udWe show how using our technique we are able to prove not only safety but also liveness properties of a version of concurrent lists and express the preservation of skiplist shape by a data structure. Moreover, the approach we present can be easily extended for using it in the verification of a wide range of similar concurrent datatypes including hash maps and graphs.
展开▼
