Fencing Programs with Self-Invalidation and Self-Downgrade

Abstract : Cache coherence protocols using self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors that are often not intended by the programmer. We propose a novel formal model that captures the semantics of programs running under such protocols, and employs a set of fences that interact with the coherence layer. Using the model, we perfform a reachability analysis that can check whether a program satisfies a given safety property with the current set of fences. Based on an algorithm in [19], we describe a method for insertion of optimal sets of fences that ensure correctness of the program under such protocols. The method relies on a counter-example guided fence insertion procedure. One feature of our method is that it can handle a variety of fences (with different costs). This diversity makes optimization more difficult since one has to optimize the total cost of the inserted fences, rather than just their number. To demonstrate the strength of our approach, we have implemented a prototype and run it on a wide range of examples and benchmarks. We have also, using simulation, evaluated the performance of the resulting fenced programs.
Type de document :
Communication dans un congrès
Elvira Albert; Ivan Lanese. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. Lecture Notes in Computer Science, LNCS-9688, pp.19-35, 2016, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-39570-8_2〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01432925
Contributeur : Hal Ifip <>
Soumis le : jeudi 12 janvier 2017 - 11:34:41
Dernière modification le : jeudi 12 janvier 2017 - 11:38:42
Document(s) archivé(s) le : vendredi 14 avril 2017 - 16:22:44

Fichier

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

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

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Parosh Abdulla, Mohamed Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, et al.. Fencing Programs with Self-Invalidation and Self-Downgrade. Elvira Albert; Ivan Lanese. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. Lecture Notes in Computer Science, LNCS-9688, pp.19-35, 2016, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-39570-8_2〉. 〈hal-01432925〉

Partager

Métriques

Consultations de la notice

150