An Observational Approach to Defining Linearizability on Weak Memory Models

Abstract : In this paper we present a framework for defining linearizability on weak memory models. The purpose of the framework is to be able to define the correctness of concurrent algorithms in a uniform way across a variety of memory models. To do so linearizability is defined within the framework in terms of memory order as opposed to program order. Such a generalisation of the original definition of linearizability enables it to be applied to non-sequentially consistent architectures. It also allows the definition to be given in terms of observable effects rather than being dependent on an understanding of the weak memory model architecture. We illustrate the framework on the TSO (Total Store Order) weak memory model, and show that it respects existing definitions of linearizability on TSO.
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.108-123, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_8〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01658421
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 décembre 2017 - 15:49:00
Dernière modification le : mercredi 31 janvier 2018 - 15:14:02

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

John Derrick, Graeme Smith. An Observational Approach to Defining Linearizability on Weak Memory Models. 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.108-123, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_8〉. 〈hal-01658421〉

Partager

Métriques

Consultations de la notice

54