×

Causally consistent dynamic slicing. (English) Zbl 1392.68313

Desharnais, Josée (ed.) et al., 27th international conference on concurrency theory, CONCUR 2016, Québec City, Canada, August 23–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-017-0). LIPIcs – Leibniz International Proceedings in Informatics 59, Article 18, 15 p. (2016).
Summary: We offer a lattice-theoretic account of dynamic slicing for \(\pi\)-calculus, building on prior work in the sequential setting. For any run of a concurrent program, we exhibit a Galois connection relating forward slices of the start configurations to backward slices of the end configuration. We prove that, up to lattice isomorphism, the same Galois connection arises for any causally equivalent execution, allowing an efficient concurrent implementation of slicing via a standard interleaving semantics. Our approach has been formalised in the dependently-typed programming language Agda.
For the entire collection see [Zbl 1351.68014].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
06A15 Galois correspondences, closure operators (in relation to ordered sets)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv