Modelling deterministic concurrent I/O

ABSTRACT

The problem of expressing I/O and side effects in functional languages is a well-established one. This paper addresses this problem from a general semantic viewpoint by giving a unified framework for describing shared state, I/O and deterministic concurrency. We develop a modified state transformer which lets us mathematically model the API, then investigate and machine verify some broad conditions under which confluence holds. This semantics is used as the basis for a small deterministic Haskell language extension called CURIO, which enforces determinism using runtime checks.Our confluence condition is first shown to hold for a variety of small components, such as individual shared variables, 1-to-1 communication channels, and I-structures. We then show how models of substantial APIs (like a modification of Haskell's file I/O API which permits inter-process communication) may be constructed from these smaller components using "combinators" in such a way that determinism is always preserved. We describe combinators for product, name-indexing and dynamic allocation, the last of which requires some small extensions to cater for process locality.

REFERENCES

• 1: Peter Achten and Rinus Plasmeijer. The Ins and Outs of Clean I/O. Journal of Functional Programming, 5(1):81--110, January 1995.
• 2: Arvind , Rishiyur S. Nikhil , Keshav K. Pingali, I-structures: data structures for parallel computing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.4, p.598-632, Oct. 1989 [doi>10.1145/69558.69562]
• 3: Erik Barendsen and Sjaak Smetsers. Uniqueness Typing for Functional Languages with Graph Rewriting Semantics. Mathematical Structures in Computer Science, 6(6):579--612, 1996.
• 4: John Boyland. Checking Interference with Fractional Permissions. In Radhia Cousot, editor, SAS, volume LNCS2694, pages 55--72. Springer, 2003.
• 5: Andrew Butterfield , Glenn Strong, Proving Correctness of Programs with IO - A Paradigm Comparison, Selected Papers from the 13th International Workshop on Implementation of Functional Languages, p.72-87, September 24-26, 2001
• 6: Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
• 7: Maarten de Mol , Marko C. J. D. van Eekelen , Marinus J. Plasmeijer, Theorem Proving for Functional Programmers, Selected Papers from the 13th International Workshop on Implementation of Functional Languages, p.55-71, September 24-26, 2001
• 8: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 9: Malcolm Dowse. A Semantic Framework for Deterministic Functional Input/Output. PhD thesis, Department of Computer Science, University of Dublin, 2006.
• 10: Malcolm Dowse, Andrew Butterfield, and Marko van Eekelen. Reasoning about Deterministic Concurrent Functional I/O. In Clemens Grelck and Frank Huch, editors, Proceedings of IFL 2004, volume LNCS3474, pages 177--194. Springer-Verlag, 2005.
• 11: Malcolm Dowse, Glenn Strong, and Andrew Butterfield. Proving "make" Correct - I/O Proofs in Haskell and Clean. In Ricardo Peña and Thomas Arts, editors, Proceedings of IFL 2002, volume LNCS2670, pages 68--83, 2002.
• 12: Andrew D. Gordon, Functional programming and input/output, Cambridge University Press, New York, NY, 1994
• 13: Andrew Gordon. Bisimilarity as a Theory of Functional Programming: Mini-course. Notes Series BRICS-NS-95-3, BRICS, Department of Computer Science, University of Aarhus, July 1995.
• 14: Cordelia Hall and Kevin Hammond. A Dynamic Semantics for Haskell (draft), May 20 1993.
• 15: Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, A principled approach to operating system construction in Haskell, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 16: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065952]
• 17: Ian Holyer , Eleni Spiliopoulou, Concurrent Monadic Interfacing, Selected Papers from the 10th International Workshop on 10th International Workshop, p.72-87, September 09-11, 1998
• 18: Mark Jones and Paul Hudak. Implicit and Explicit Parallel Programming in Haskell. Technical Report YALEU/DCS/RR-982, Department of Computer Science, Yale University, August 1993.
• 19: John Launchbury , Simon L. Peyton Jones, Lazy functional state threads, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.24-35, June 20-24, 1994, Orlando, Florida, United States
• 20: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 21: Flemming Nielson , Hanne Riis Nielson, Type and Effect Systems, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.114-136, January 1999
• 22: Simon Peyton Jones. Wearing the Hair Shirt: A retrospective on Haskell. Invited talk at POPL 2003.
• 23: Simon Peyton Jones. Tackling the Awkward Squad - monadic input/output, concurrency, exceptions, and foreign language calls in Haskell. In CAR Hoare, M Broy, and R Stein-brueggen, editors, Engineering theories of software construction, Marktoberdorf Summer School 2000, pages 47--96. IOS Press, 2001.
• 24: Simon Peyton Jones , Andrew Gordon , Sigbjorn Finne, Concurrent Haskell, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.295-308, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237794]
• 25: Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
• 26: Rinus Plasmeijer , Marko Van Eekelen, Functional Programming and Parallel Graph Rewriting, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1993
• 27: Peter Sewell, On Implementations and Semantics of a Concurrent Programming Language, Proceedings of the 8th International Conference on Concurrency Theory, p.391-405, July 01-04, 1997
• 28: Eleni Spiliopoulou. Concurrent and Distributed Functional Systems. PhD thesis, University of Bristol, Department of Computing Science, August 1999.
• 29: Tachio Terauchi , Alex Aiken, Witnessing side-effects, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 30: Simon Thompson. Interactive Functional Programs: a method and a formal semantics. Technical Report 48*, Computing Laboratory, University of Kent,, November 1987.
• 31: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613 ]
• 32: D Turner, An overview of Miranda, ACM SIGPLAN Notices, v.21 n.12, p.158-166, Dec. 1986 [doi>10.1145/15042.15053]
• 33: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Design, Languages, Theory

Keywords:
I/O, concurrency, determinism, effects, monads