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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
References
The SPIN Model-Checker, http://spinroot.com/
Berge, C.: Hypergraphs, vol. 445. North Holland Mathematical Library (1989)
Bonichon, R., Canet, G., Correnson, L., Goubault, E., Haucourt, E., Hirschowitz, M., Labbé, S., Mimram, S.: Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 85–98. Springer, Heidelberg (2011)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of Principles Of Programming Languages, pp. 269–282. ACM Press (1979)
Cousot, P., Cousot, R.: Abstract interpretation based program testing. In: Proc. of the SSGRR 2000 Computer & eBusiness International Conference (2000)
Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific (1995)
Dijkstra, E.: The Structure of the THE Operating System. Com. of the ACM 11(15) (1968)
Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1(2) (1971)
Fajstrup, L.: Trace spaces of directed tori with rectangular holes. Technical Report R-2011-08, Aalborg Univ. (2001)
Fajstrup, L., Goubault, É., Raußen, M.: Detecting Deadlocks in Concurrent Systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 332–347. Springer, Heidelberg (1998)
Fajstrup, L., Sokolowski, S.: Infinitely running concurrent processes with loops from a geometric viewpoint. ENTCS 39(2) (2000)
Fajstrup, L., Raußen, M., Goubault, E.: Algebraic topology and concurrency. Theor. Comput. Sci. 357(1-3), 241–278 (2006)
Fajstrup, L., Raußen, M., Goubault, E., Haucourt, E.: Components of the fundamental category. Appl. Cat. Struct. 12(1), 81–108 (2004)
Godefroid, P., Wolper, P.: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 332–342. Springer, Heidelberg (1992)
Goubault, É., Haucourt, E.: A Practical Application of Geometric Semantics to Static Analysis of Concurrent Programs. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 503–517. Springer, Heidelberg (2005)
Goubault, E., Haucourt, E.: Components of the fundamental category II. Applied Categorical Structures 15(4), 387–414 (2007)
Goubault, E., Mimram, S.: Formal relationships between geometrical and classical models for concurrency. CoRR, abs/1004.2818 (2010)
Grandis, M.: Directed Algebraic Topology, Models of Non-Reversible Worlds. New Mathematical Monographs, vol. 13. Cambridge University Press (2009)
Gunawardena, J.: Homotopy and concurrency. Bulletin of the EATCS 54, 184–193 (1994)
Kavvadias, D.J., Stavropoulos, E.C.: Evaluation of an Algorithm for the Transversal Hypergraph Problem. In: Vitter, J.S., Zaroliagis, C.D. (eds.) WAE 1999. LNCS, vol. 1668, pp. 72–84. Springer, Heidelberg (1999)
Kozlov, D.: Combinatorial Algebraic Topology. Springer, Heidelberg (2007)
Peltier, S., Fuchs, L., Lienhardt, P.: Simploidals sets: Definitions, Operations and Comparison with Simplicial Sets. Discrete Applied Math. 157, 542–557 (2009)
Raussen, M.: Simplicial models of trace spaces. Alg. & Geom. Top. 10, 1683–1714 (2010)
Valmari, A.: A Stubborn Attack on State Explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fajstrup, L., Goubault, É., Haucourt, E., Mimram, S., Raussen, M. (2012). Trace Spaces: An Efficient New Technique for State-Space Reduction. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)