Modularising Opacity Verification for Hybrid Transactional Memory

Abstract : Transactional memory (TM) manages thread synchronisation to provide an illusion of atomicity for arbitrary blocks of code. There are various implementations of TM, including hardware (HTM) and software (STM). HTMs provide high performance, but are inherently limited by hardware restrictions; STMs avoid these limitations but suffer from unpredictable performance. To solve these problems, hybrid TM (HyTM) algorithms have been introduced which provide reliable software fallback mechanisms for hardware transactions. The key safety property for TM is opacity, however a naive combination of an opaque STM and an opaque HTM does not necessarily result in an opaque HyTM. Therefore, HyTM algorithms must be specially designed to satisfy opacity. In this paper we introduce a modular method for verifying opacity of HyTM implementations. Our method provides conditions under which opacity proofs of HTM and STM components can be combined into a single proof of an overall hybrid algorithm. The proof method has been fully mechanised in Isabelle, and used to verify a novel hybrid version of a transactional mutex lock.
Type de document :
Communication dans un congrès
Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.33-49, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_3〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01658416
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 décembre 2017 - 15:48:50
Dernière modification le : jeudi 7 décembre 2017 - 15:50:48

Fichier

 Accès restreint
Fichier visible le : 2020-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Alasdair Armstrong, Brijesh Dongol. Modularising Opacity Verification for Hybrid Transactional Memory. Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.33-49, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_3〉. 〈hal-01658416〉

Partager

Métriques

Consultations de la notice

45