Provable STM Properties: Leveraging Clock and Locks to Favor Commit and Early Abort

Damien Imbs 1 Michel Raynal 1
1 ASAP - As Scalable As Possible: foundations of large scale dynamic distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
Abstract : The aim of a Software Transactional Memory (STM) is to discharge the programmers from the management of synchronization in multiprocess programs that access concurrent objects. To that end, a STM system provides the programmer with the concept of a transaction: each sequential process is decomposed into transactions, where a transaction encapsulates a piece of code accessing concurrent objects. A transaction contains no explicit synchronization statement and appears as if it has been executed atomically. Due to the underlying concurrency management, a transaction commits or aborts. The major part of papers devoted to STM systems address mainly their efficiency. Differently, this paper focuses on an orthogonal issue, namely, the design and the statement of a safety property. The only safety property that is usually considered is a global property involving all the transactions (e.g., conflictserializability or opacity) that expresses the correction of the whole execution. Roughly speaking, these consistency properties do not prevent a STM system from aborting all the transactions. The proposed safety property, called obligation, is on each transaction taken individually. It specifies minimal circumstances in which a STM system must commit a transaction T. The paper proposes and investigates such an obligation property. Then, it presents a STM algorithm that implements it. This algorithm, which is based on a logical clock and associates a lock with each shared object, is formally proved correct.
Type de document :
Rapport
[Research Report] PI 1894, 2008, pp.20
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00281550
Contributeur : Anne Jaigu <>
Soumis le : vendredi 23 mai 2008 - 10:24:04
Dernière modification le : mardi 16 janvier 2018 - 15:54:13
Document(s) archivé(s) le : vendredi 28 mai 2010 - 17:58:27

Fichiers

PI-1894.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00281550, version 1

Citation

Damien Imbs, Michel Raynal. Provable STM Properties: Leveraging Clock and Locks to Favor Commit and Early Abort. [Research Report] PI 1894, 2008, pp.20. 〈inria-00281550〉

Partager

Métriques

Consultations de la notice

374

Téléchargements de fichiers

121