Completeness and Nondeterminism in Model Checking Transactional Memories

Rachid Guerraoui, Vasu Singh
2008
Article de conférence

Abstract. Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first deterministic specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a complete verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is nondeterministic and establishes correctness for all possible contention management schemes.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés

Chargement

Publications associées

Chargement

Rachid Guerraoui, Vasu Singh
2008
Article de conférence

Résumé

Official source

https://infoscience.epfl.ch/record/125895?ln=fr

À propos de ce résultat

Concepts associés (6)

Concepts associés

Chargement

Publications associées (3)

Chargement

Publications associées

Chargement

Programmation concurrente

La programmation concurrente est un paradigme de programmation tenant compte, dans un programme, de l'existence de plusieurs piles sémantiques qui peuvent être appelées threads, processus ou tâches. E

Transactional memory

In computer science and engineering, transactional memory attempts to simplify concurrent programming by allowing a group of load and store instructions to execute in an atomic way. It is a concurrenc

Serializability

In concurrency control of databases, transaction processing (transaction management), and various transactional applications (e.g., transactional memory and software transactional memory), both cent

Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first \emph{deterministic} specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a \emph{complete} verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is \emph{nondeterministic} and establishes correctness for all possible contention management schemes.

Springer2008

Chargement

Opacity: A Correctness Condition for Transactional Memory

Rachid Guerraoui, Michal Kapalka

Transactional memory is perceived as an appealing alternative to critical sections for general purpose concurrent programming. Despite the large amount of recent work on transactional memory implementations, however, its actual specification has never been precisely defined. This paper presents \emph{opacity}, a new correctness criterion for transactional memory systems. Opacity extends the notion of strict serializability, itself a strong form of the classical serializability property, with the requirement that even \emph{non-committed} transactions are prevented from accessing inconsistent state. Yet opacity does not preclude versioning, invisible reads and lazy updates, often used by modern TM implementations. In fact, most transactional memory systems we know of ensure opacity. We prove a tight bound on the inherent cost of implementing opacity. The bound highlights a trade-off that explains some of the differences between current transactional memory systems, and also draws a sharp complexity line between opacity on one hand, and the combination of strict serializability and strict recoverability on the other hand.

2007

Chargement

Safety, Liveness and Parallelism in Concurrent Computing

Victor Bushkov

The correctness of a shared object, which can be accessed by several processes concurrently, is specified through two different kinds of properties - safety and liveness. When implementing a shared object it is important to specify its correctness in a such way that it should be feasible under given assumptions. In this work we study the question of implementability of shared objects that satisfy certain safety and liveness properties under certain assumptions. In particular, we study implementability of liveness properties of transactional memory (TM) shared objects with strict serializability, a strong safety property. TM allows a programmer to encapsulate pieces of sequential code within transactions that run concurrently and it ensures that transactions run in some consistent manner by committing or aborting them. First, we give a formal definition of a liveness property in the TM context. Then, we proceed to show that certain classes of liveness properties of TM can not be implemented with strict serializability in a system in which processes are prone to failures. We also show that, in general, we cannot find a weakest non-implementable (resp. strongest implementable) liveness of TM when we require some common safety property like strict serializability. Moreover, we generalize this result to other shared object types and give a characterization of safety properties for which we can find weakest non-implementable (resp. strongest implementable) liveness. In addition to correctness properties we study the limitations of parallelism which affects performance and scalability of implementations. Specifically, we show that we cannot implement a TM which guarantees disjoint-access parallelism, which say that transactions do not need to synchronize unless they access the same application objects, while guaranteeing very weak safety and the weakest non-blocking liveness.

EPFL2015

Chargement