Trace Spaces: an Efficient New Technique for State-Space Reduction

Abstract : State-space reduction techniques, used primarily in model-checkers, all rely on the idea that some actions are independent, hence could be taken in any (respective) order while put in parallel, without changing the semantics. It is thus not necessary to consider all execution paths in the interleaving semantics of a concurrent program, but rather some equivalence classes. The purpose of this paper is to describe a new algorithm to compute such equivalence classes, and a representative per class, which is based on ideas originating in algebraic topology. We introduce a geometric semantics of concurrent languages, where programs are interpreted as directed topological spaces, and study its properties in order to devise an algorithm for computing dihomotopy classes of execution paths. In particular, our algorithm is able to compute a control-flow graph for concurrent programs, possibly containing loops, which is "as reduced as possible" in the sense that it generates traces modulo equivalence. A preliminary implementation was achieved, showing promising results towards efficient methods to analyze concurrent programs, with very promising results compared to partial-order reduction techniques.
Type de document :
Communication dans un congrès
Helmut Seidl. ESOP - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. Springer, 7211, pp.274-294, 2012, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/9q223737w333j551/〉. 〈10.1007/978-3-642-28869-2_14〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00684615
Contributeur : Samuel Mimram <>
Soumis le : lundi 2 avril 2012 - 16:12:20
Dernière modification le : mardi 24 avril 2018 - 16:16:02
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 19:53:10

Fichiers

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

Identifiants

Collections

CEA | DRT | LIST

Citation

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen. Trace Spaces: an Efficient New Technique for State-Space Reduction. Helmut Seidl. ESOP - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. Springer, 7211, pp.274-294, 2012, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/9q223737w333j551/〉. 〈10.1007/978-3-642-28869-2_14〉. 〈hal-00684615〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

111