Document Open Access Logo

Data-Flow Analyses as Effects and Graded Monads

Authors Andrej Ivašković , Alan Mycroft , Dominic Orchard

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.15.pdf
  • Filesize: 0.75 MB
  • 23 pages

Document Identifiers

Author Details

Andrej Ivašković
  • Department of Computer Science and Technology, University of Cambridge, UK
Alan Mycroft
  • Department of Computer Science and Technology, University of Cambridge, UK
Dominic Orchard
  • School of Computing, University of Kent, UK

Funding

  • Ivašković, Andrej: funded by Trinity College, Cambridge (Internal Graduate Scholarship).
  • Orchard, Dominic: funded in part by EPSRC grant EP/T013516/1.

Cite AsGet BibTex

Andrej Ivašković, Alan Mycroft, and Dominic Orchard. Data-Flow Analyses as Effects and Graded Monads. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.15

Abstract

In static analysis, two frameworks have been studied extensively: monotone data-flow analysis and type-and-effect systems. Whilst both are seen as general analysis frameworks, their relationship has remained unclear. Here we show that monotone data-flow analyses can be encoded as effect systems in a uniform way, via algebras of transfer functions. This helps to answer questions about the most appropriate structure for general effect algebras, especially with regards capturing control-flow precisely. Via the perspective of capturing data-flow analyses, we show the recent suggestion of using effect quantales is not general enough as it excludes non-distributive analyses e.g., constant propagation. By rephrasing the McCarthy transformation, we then model monotone data-flow effects via graded monads. This provides a model of data-flow analyses that can be used to reason about analysis correctness at the semantic level, and to embed data-flow analyses into type systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • data-flow analysis
  • effect systems
  • graded monads
  • correctness

Metrics

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

Supplementary Materials

References

  1. Torben Amtoft, Hanne Riis Nielson, and Flemming Nielson. Type and effect systems - behaviours for concurrency. Imperial College Press, 1999. Google Scholar
  2. Nick Benton, Andrew Kennedy, Martin Hofmann, and Vivek Nigam. Counting successes: Effects and transformations for non-deterministic programs. In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella, editors, A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 56-72. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_3.
  3. Patrick Cousot and Radhia Cousot. Abstract interpretation frameworks. J. Log. Comput., 2(4):511-547, 1992. URL: https://doi.org/10.1093/logcom/2.4.511.
  4. Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès. Towards a Formal Theory of Graded Monads. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, volume 9634 of Lecture Notes in Computer Science, pages 513-530. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_30.
  5. David K. Gifford and John M. Lucassen. Integrating Functional and Imperative Programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP 1986, August 4-6, 1986, Cambridge, Massachusetts, USA., pages 28-38. ACM, 1986. URL: https://dl.acm.org/citation.cfm?id=319838.
  6. Colin S. Gordon. A Generic Approach to Flow-Sensitive Polymorphic Effects. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming (ECOOP 2017), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:31, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.13.
  7. Pierre Jouvelot and David K Gifford. Communication effects for message-based concurrency. Laboratory for Computer Science, Massachusetts Institute of Technology, 1989. Google Scholar
  8. John B. Kam and Jeffrey D. Ullman. Monotone Data Flow Analysis Frameworks. Acta Inf., 7:305-317, 1977. URL: https://doi.org/10.1007/BF00290339.
  9. Shin-ya Katsumata. Parametric Effect Monads and Semantics of Effect Systems. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 633-645. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535846.
  10. Uday P. Khedker, Amitabha Sanyal, and Bageshri Sathe. Data Flow Analysis - Theory and Practice. CRC Press, 2009. URL: http://www.crcpress.com/product/isbn/9780849328800.
  11. Peeter Laud, Tarmo Uustalu, and Varmo Vene. Type systems equivalent to data-flow analyses for imperative languages. Theoretical Computer Science, 364(3):292-310, 2006. Applied Semantics. URL: https://doi.org/10.1016/j.tcs.2006.08.013.
  12. John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part I. Commun. ACM, 3(4):184-195, 1960. URL: https://doi.org/10.1145/367177.367199.
  13. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  14. Steven Muchnick and Neil Jones. Program Flow Analysis: Theory and Applications. New York University, Courant Institute of Mathematical Sciences, Computer Science Department, January 1981. Google Scholar
  15. Alan Mycroft, Dominic A. Orchard, and Tomas Petricek. Effect Systems Revisited - Control-Flow Algebra and Semantics. In Christian W. Probst, Chris Hankin, and René Rydhof Hansen, editors, Semantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, volume 9560 of Lecture Notes in Computer Science, pages 1-32. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-27810-0_1.
  16. Flemming Nielson, Patrick Cousot, Mads Dam, Pierpaolo Degano, Pierre Jouvelot, Alan Mycroft, and Bent Thomsen. Logical and operational methods in the analysis of programs and systems. In LOMAPS workshop on Analysis and Verification of Multiple-Agent Languages, pages 1-21. Springer, 1996. URL: https://doi.org/10.1007/3-540-62503-8_1.
  17. Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program Analysis. Springer Publishing Company, Incorporated, 2010. Google Scholar
  18. Peter W. O'Hearn. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann, editors, Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 286-318. IOS Press, 2012. URL: https://doi.org/10.3233/978-1-61499-028-4-286.
  19. Dominic Orchard and Tomas Petricek. Embedding Effect Systems in Haskell. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, Haskell '14, pages 13-24, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2633357.2633368.
  20. Dominic A. Orchard, Tomas Petricek, and Alan Mycroft. The semantic marriage of monads and effects. CoRR, abs/1401.5391, 2014. URL: http://arxiv.org/abs/1401.5391.
  21. Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Ron K. Cytron and Peter Lee, editors, Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 49-61. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199462.
  22. Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis. In Steven Muchnick and Neil Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7. New York University, Courant Institute of Mathematical Sciences, Computer Science Department, January 1981. Google Scholar
  23. Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. Verifying higher-order programs with the Dijkstra monad. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 387-398. ACM, 2013. URL: https://doi.org/10.1145/2491956.2491978.
  24. Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and computation, 111(2):245-296, 1994. Google Scholar
  25. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. A new verified compiler backend for CakeMl. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 60-73, 2016. URL: https://doi.org/10.1145/2951913.2951924.
  26. Ross Tate. The Sequential Semantics of Producer Effect Systems. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 15-26, New York, NY, USA, 2013. ACM. URL: https://doi.org/10.1145/2429069.2429074.
  27. Philip Wadler. The essence of functional programming. In Ravi Sethi, editor, Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992, pages 1-14. ACM Press, 1992. URL: https://doi.org/10.1145/143165.143169.
  28. Philip Wadler and Peter Thiemann. The marriage of effects and monads. ACM Trans. Comput. Log., 4(1):1-32, 2003. URL: https://doi.org/10.1145/601775.601776.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact