Abstract
In this paper we show how to compress efficiently the state-space of a concurrent system (here applied to a simple shared memory model, but this is no way limited to that model). The technology used here is based on research on geometric semantics by the authors and collaborators [1]. It has been implemented in a abstract interpretation based static analyzer (ALCOOL), and we show some preliminary results and benchmarks.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Fajstrup, L., Goubault, E., Haucourt, E., Raussen, M.: Components of the fundamental category. Applied Categorical Structures (2004)
Dijkstra, E.: Cooperating Sequential Processes. Academic Press, London (1968)
Nachbin, L.: Topology and Order. Van Nostrand, Princeton (1965)
Johnstone, P.T.: Stone Spaces. Cambridge University Press, Cambridge (1982)
Fajstrup, L., Goubault, E., Raussen, M.: Algebraic topology and concurrency. Submitted to Theoretical Computer Science, also technical report, Aalborg University (1999)
Goubault, E.: Some geometric perspectives in concurrency theory. Homology Homotopy and Applications (2003)
Goubault, E., Raussen, M.: Dihomotopy as a tool in state space analysis. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol. 2286, pp. 16โ37. Springer, Heidelberg (2002)
Gabriel, P., Zisman, M.: Calculus of fractions and homotopy theory. Ergebnisse der Mathematik und ihrer Grenzgebiete, vol. 35. Springer, Heidelberg (1967)
Haucourt, E.: A framework for component categories. ENTCS (2005) (to appear)
Mac Lane, S.: Categories for the working mathematician. Springer, Heidelberg (1971)
Gaucher, P., Goubault, E.: Topological deformation of higher dimensional automata. Technical report, arXiv:math.AT/010760, to appear in HHA (2001)
Godefroid, P., Peled, D., Staskauskas, M.: Using partial-order methods in the formal validation of industrial concurrent programs. IEEE Transactions on Software Engineering 22, 496โ507 (1996)
Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. In: Formal Methods and System Design, vol. 7, pp. 1โ15. Kluwer Academic Publishers, Dordrecht (1995)
Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531. Springer, Heidelberg (1991)
Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 89โ103. Springer, Heidelberg (1989)
Melzer, S., Roemer, S.: Deadlock checking using net unfoldings. In: Proc. of Computer Aided Verification. Springer, Heidelberg (1997)
Mazurkiewicz, A.: Basic notions of trace theory. Lecture notes for the REX summer school in temporal logic. Springer, Heidelberg (1988)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. Principles of Programming Languages 4, 238โ252 (1977)
Boigelot, B., Godefroid, P.: Model checking in practice: An analysis of the access bus protocol using spin. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 465โ478. Springer, Heidelberg (1996)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proc. of the Fifth Annual IEEE Symposium on Logic and Computer Science, pp. 428โ439. IEEE Press, Los Alamitos (1990)
Garavel, H., Jorgensen, M., Mateescu, R., Pecheur, C., Sighireanu, M., Vivien, B.: Cadp 1997 โ status, applications and perspectives. Technical report, Inria Alpes (1997)
Raussen, M.: Deadlocks and dihomotopy in mutual exclusion models. Technical report, Aalborg University (2005), Available at http://www.math.aau.dk/index_en.html
Carson, S., Reynolds, P.: The geometry of semaphore programs. ACM TOPLAS 9, 25โ53 (1987)
Gaucher, P.: A convenient category for the homotopy theory of concurrency preprint available at math. AT/0201252 (2002)
Grandis, M.: Directed homotopy theory, I. the fundamental category. Cahiers Top. Gom. Diff. Catg, to appear, Preliminary version: Dip. Mat. Univ. Genova, Preprint 443 (2001)
Spanier, E.J.: Algebraic Topology. McGraw-Hill, New York (1966)
Goubault, E.: Geometry and concurrency: A usersโ guide. Mathematical Structures in Computer Science (2000)
Goubault, E.: Cubical sets are generalized transition systems. Technical report, pre-proceedings of CMCIM 2002 (2001), also available at http://www.di.ens.fr/~goubault
Fahrenberg, U.: A category of higher-dimensional automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 187โ201. Springer, Heidelberg (2005) (to appear)
Boehm, H.: Bounding space usage of conservative garbage collector. In: Principles of Programing Language (2002), see http://www.hpl.hp.com/personal/Hans_Boehm/gc/
Holzmann, G.J.: SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley, Reading (2003)
Cousot, P., Cousot, R.: Comparison of the Galois connection and widening/ narrowing approaches to abstract interpretation. In: JTASPEFL 1991, Bordeaux, BIGRE, vol. 74, pp. 107โ110 (1991)
Demartini, C., Iosif, R., Sisto, R.: Modeling and validation of java multithreading applications using spin. In: SPIN Workshop (1998)
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. 417โ428. Springer, Heidelberg (1992)
Grandis, M.: The shape of a category up to directed homotopy. Technical Report preprint 509, Dip. Mat. Univ. Genova (2004), available at http://www.dima.unige.it/~grandis/rec.public_grandis.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
ยฉ 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goubault, E., Haucourt, E. (2005). A Practical Application of Geometric Semantics to Static Analysis of Concurrent Programs. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 โ Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_38
Download citation
DOI: https://doi.org/10.1007/11539452_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28309-6
Online ISBN: 978-3-540-31934-4
eBook Packages: Computer ScienceComputer Science (R0)