MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models

Abstract : With the wide expansion of multiprocessor architectures, the analysis and reasoning for programs under weak memory models has become an important concern. This work presents MMFilter, an original constraint solver for generating program behaviors respecting a particular memory model. It is implemented in Prolog using CHR (Constraint Handling Rules). The CHR formalism provides a convenient generic solution for specifying memory models. It benefits from the existing optimized implementations of CHR and can be easily extended to new models. We present MMFilter design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposed technique.
Type de document :
Article dans une revue
Computer Languages, Systems and Structures, Elsevier, In press
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01777123
Contributeur : Allan Blanchard <>
Soumis le : mardi 24 avril 2018 - 16:11:54
Dernière modification le : mercredi 3 octobre 2018 - 01:08:29
Document(s) archivé(s) le : mercredi 19 septembre 2018 - 22:36:28

Fichier

MMFilter.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01777123, version 1

Collections

Citation

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue. MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models. Computer Languages, Systems and Structures, Elsevier, In press. 〈hal-01777123〉

Partager

Métriques

Consultations de la notice

236

Téléchargements de fichiers

45