AbstractThe Fork Calculus FC presents a theory of communicating systems in family with CCS, but it differs in the way that processes are put in parallel. In CCS there is a binary parallel operator |, and two processes p and q are put in parallel by p|q. In FC there is a unary fork operator, and a process p is activated to ``run in parallel with the rest of the program'' by fork(p). An operational semantics is defined, and a congruence relation between processes is suggested. In addition, a sound and complete axiomatisation of the congruence is provided. FC has been developed during an investigation of the programming language CML, an extension of ML with concurrency primitives, amongst them a fork operator.
Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages
Additional Key Words and Phrases: process calculi, process creation, bisimulation, axiomatisation
Selected references
- Dave Berry, Robin Milner, and David N. Turner. A semantics for ML concurrency primitives. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 119-129, Albequerque, New Mexico, January 1992.
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.