Causally Consistent Dynamic Slicing

Authors Roly Perera, Deepak Garg, James Cheney

Thumbnail PDF


  • Filesize: 0.71 MB
  • 15 pages

Document Identifiers

Author Details

Roly Perera
Deepak Garg
James Cheney

Cite AsGet BibTex

Roly Perera, Deepak Garg, and James Cheney. Causally Consistent Dynamic Slicing. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


We offer a lattice-theoretic account of the problem of dynamic slicing for pi-calculus, building on prior work in the sequential setting. For any particular run of a concurrent program, we exhibit a Galois connection relating forward and backward slices of the initial and terminal configurations. 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.
  • pi-calculus; dynamic slicing; causal equivalence; Galois connection


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. U. A. Acar, A. Ahmed, J. Cheney, and R. Perera. A core calculus for provenance. Journal of Computer Security, 21:919-969, 2013. Full version of a POST 2012 paper. Google Scholar
  2. J. Cheng. Slicing concurrent programs: A graph-theoretical approach. In Automated and Algorithmic Debugging, number 749 in LNCS, pages 223-240. Springer-Verlag, 1993. Google Scholar
  3. I. Cristescu, J. Krivine, and D. Varacca. A compositional semantics for the reversible pi-calculus. In LICS, pages 388-397, June 2013. Google Scholar
  4. V. Danos and J. Krivine. Reversible communicating systems. In Concurrency Theory, 15th International Conference, CONCUR '04, LNCS, pages 292-307. Springer, 2004. Google Scholar
  5. N.G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5):381-392, 1972. Google Scholar
  6. M. Dezani-Ciancaglini, R. Horne, and V. Sassone. Tracing where and who provenance in linked data: A calculus. Theoretical Computer Science, 464:113-129, 2012. Google Scholar
  7. E. Duesterwald, R. Gupta, and M. L. Soffa. Distributed slicing and partial re-execution for distributed programs. In Proceedings of the 5th International Workshop on Languages and Compilers for Parallel Computing, pages 497-511. Springer, 1993. Google Scholar
  8. D. Goswami and R. Mall. Dynamic slicing of concurrent programs. In High Performance Computing - HiPC 2000, volume 1970 of LNCS, pages 15-26. Springer, 2000. Google Scholar
  9. D. Hirschkoff. Handling substitutions explicitly in the pi-calculus. In 2nd International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, 1999. Google Scholar
  10. I. Lanese, C. A. Mezzina, and J.-B. Stefani. Reversing higher-order π. In Concurrency Theory, 21st International Conference, CONCUR '10, pages 478-493. Springer, 2010. Google Scholar
  11. J.-J. Lévy. Optimal reductions in the lambda-calculus. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 159-191. Academic Press, New York, NY, USA, 1980. Google Scholar
  12. R. Milner. Communicating and mobile systems: the π calculus. Cambridge University Press, Cambridge, UK, 1999. Google Scholar
  13. D.P. Mohapatra, Rajib Mall, and Rajeev Kumar. An efficient technique for dynamic slicing of concurrent Java programs. In Applied Computing, volume 3285 of LNCS, pages 255-262. Springer, 2004. Google Scholar
  14. R. Perera, U. A. Acar, J. Cheney, and P. B. Levy. Functional programs that explain their work. In 17th ACM SIGPLAN International Conference on Functional Programming, ICFP '12, pages 365-376. ACM, 2012. Google Scholar
  15. R. Perera and J. Cheney. Proof-relevant pi-calculus, 2016. Submitted to Mathematical Structures in Computer Science. URL:
  16. I. Souilah, A. Francalanza, and V. Sassone. A formal model of provenance in distributed systems. In TAPP 2009, Berkeley, CA, USA, 2009. USENIX Association. Google Scholar
  17. S. Tallam, C. Tian, and R. Gupta. Dynamic slicing of multithreaded programs for race detection. In 24th IEEE International Conference on Software Maintenance (ICSM 2008), pages 97-106. IEEE, 2008. Google Scholar
  18. M. Weiser. Program slicing. In Proceedings of the 5th International Conference on Software Engineering, ICSE '81, pages 439-449, Piscataway, NJ, USA, 1981. IEEE Press. Google Scholar