A semantics for ML concurrency primitives

ABSTRACT

We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such that the representation has the same behaviour as a direct definition. These proofs are the first steps towards integrating our semantics with the full definition of Standard ML.

REFERENCES

• BB90: Gerard Berry , Gerard Boudol, The chemical abstract machine, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-94, December 1989, San Francisco, California, United States [doi>10.1145/96709.96717]
• Ber89: B. Berthomieu. Implementing CCS, the LCS experiment. Technical Report 89425, LAAS- CNRS, 1989.
• Ber91a: Dave Berry. The Edinburgh SML library. LFCS Report Series ECS-LFCS-91-148, Laboratory for Foundations of Computer Science, University of Edinburgh, 1991.
• Ber91b: Dave Berry. Generating Program Animators from Programming Language Semantics. PhD thesis, University of Edinburgh, 1991.
• BS83: G. N. Buckley , Abraham Silberschatz, An Effective Implementation for the Generalized Input-Output Construct of CSP, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.223-235, April 1983 [doi>10.1145/69624.357208]
• CG89: Nicholas Carriero , David Gelernter, How to write parallel programs: a guide to the perplexed, ACM Computing Surveys (CSUR), v.21 n.3, p.323-357, Sep. 1989 [doi>10.1145/72551.72553]
• CM90: Eric C. Cooper and J. Gregory Morrisett. Adding threads to Standard ML. Technical Report CMU-CS-90-186, School of Computer Science, Carnegie Mellon University, 1990.
• GMP89: Alessandro Giacalone , Prateek Mishra , Sanjiva Prasad, Facile: a symmetric integration of concurrent and functional programming, International Journal of Parallel Programming, v.18 n.2, p.121-160, Apr. 1990 [doi>10.1007/BF01491213]
• Hen90: Matthew Hennessy, The semantics of programming languages: an elementary introduction using structural operational semantics, John Wiley & Sons, Inc., New York, NY, 1990
• Hol83: Shren Holstrhm. PFL: A functional language for parallel programming and its imp}{ementation. Report 83.03 R, Department of Computer Science, Chalmers University of Technology, 1983.
• Kna: F. Knabe. A distributed protocol for channelbased communication with choice. ECRC, Munich. In Preparation.
• Mat91: David Matthews. A distributed concurrent implementation of Standard ML. In EurOpen Autumn 1991 Conference, 1991. To appear.
• Mit86: Kevin Mitchell. implementations of Process Synchronisation and their Analysis. PhD thesis, Department of Computer Science, University of Edinburgh, Jul 1986.
• MTH90: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• Rep89: John H. Reppy, First-Class Synchronous Operations in Standard ML, Cornell University, Ithaca, NY, 1989
• Rep91a: John H. Reppy, CML: A higher concurrent language, ACM SIGPLAN Notices, v.26 n.6, p.293-305, June 1991
• Rep91b: J. H. Reppy. An operational semantics of first-class synchronous operations. Technical Report TR 91-1232, Dept. of Computer Science, Cornell University, Aug 1991.
• WF91: A. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Dept. of Computer Science, Rice University, Apr 1991.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Languages, Theory, Verification