Causally Consistent Dynamic Slicing

DOI10.4230/LIPICS.CONCUR.2016.18MaRDI QIDQ4608670zbMATH OpenOpenAlexFDO

Authors Roly Perera, Deepak Garg, James Cheney

Publication date 21 March 2018

Full work available at URL https://arxiv.org/abs/1610.02327

zbMATH Keywords

\(\pi\)-calculuscausal equivalencedynamic slicingGalois connection

Mathematics Subject Classification ID

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

Abstract: 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 configuration 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 language Agda.

Recommendations

• Parametric and Sliced Causality
• scientific article; zbMATH DE number 148937
• Dynamic program slicing
• Dynamic slicing techniques for Petri nets
• An efficient method for computing dynamic program slices
• Theoretical foundations of dynamic program slicing

Cited in

(3)

• Causal-consistent replay reversible semantics for message passing concurrent programs
• Parametric and Sliced Causality
• Causal-consistent replay debugging for message passing programs

This page was built for publication: Causally Consistent Dynamic Slicing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4608670)