Higher-order concurrent programs with finite communication topology (extended abstract)

ABSTRACT

Concurrent ML (CML) is an extension of the functional language Standard ML(SML) with primitives for the dynamic creation of processes and channels and for the communication of values over channels. Because of the powerful abstraction mechanisms the communication topology of a given program may be very complex and therefore an efficient implementation may be facilitated by knowledge of the topology. This paper presents an analysis for determining when a bounded number of processes and channels will be generated. The analysis proceeds in two stages. First we extend a polymorphic type system for SML to deduce not only the type of CML programs but also their communication behaviour expressed as terms in a new process algebra. Next we develop an analysis that given the communication behaviour predicts the number of processes and channels required during the execution of the CML program. The correctness of the analysis is proved using a subject reduction property for the type system.

REFERENCES

• 1: Dave Berry , Robin Milner , David N. Turner, A semantics for ML concurrency primitives, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-129, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143191]
• 2: A. Giacalone, P. Mishra, S. Prasad: Operational and Algebraic Semantics for Facile: A Syrmnetric Integration of Concurrent and Functional Programming. Proceedings of ICALP '90, SLNCS 443, 1990.
• 3: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 4: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 5: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 6: Flemming Nielson, The Typed lambda-Calculus with First-Class Processes, Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, p.357-373, June 12-16, 1989
• 7: Flemming Nielson , Hanne Riis Nielson, From CML to Process Algebras (Extended Abstract), Proceedings of the 4th International Conference on Concurrency Theory, p.493-508, August 23-26, 1993
• 8: John H. Reppy, CML: A higher concurrent language, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.293-305, June 24-28, 1991, Toronto, Ontario, Canada
• 9: John Hamilton Reppy, Higher-order concurrency, Cornell University, Ithaca, NY, 1992
• 10: J.-P. Talpin, P. Jouvelot: The Type and Effect Discipline. Proceedings of LICS'92, 1992.
• 11: B. Thomsen, A calculus of higher order communicating systems, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.143-154, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75290]
• 12: B. Thomsen: Polymorphic sorts and types for concurrent functional programs. Technical report ECRC-93-10, 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Concurrent, distributed, and parallel languages

General Terms:
Languages, Theory, Verification