A CHR-Based Solver for Weak Memory Behaviors

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 an original constraint solver for detecting 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, that benefits from the existing optimized implementations of CHR and can be easily extended to new models. We briefly present the solver design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposal.
Type de document :
Communication dans un congrès
7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA), Jul 2016, Saarbrücken, Germany. 2016
Liste complète des métadonnées

https://hal.inria.fr/hal-01318432
Contributeur : Frédéric Loulergue <>
Soumis le : jeudi 19 mai 2016 - 15:43:34
Dernière modification le : mercredi 14 février 2018 - 14:17:59

Identifiants

  • HAL Id : hal-01318432, version 1

Citation

Blanchard Allan, Nikolai Kosmatov, Frédéric Loulergue. A CHR-Based Solver for Weak Memory Behaviors. 7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA), Jul 2016, Saarbrücken, Germany. 2016. 〈hal-01318432〉

Partager

Métriques

Consultations de la notice

140