MCSP: compiling CSP-like expressions

The new occam-pi compiler now supports compilation of a simple CSP-like langauge. It's not quite the standard machine-readable CSP (CSP-M), but fairly close.

[ status | language ]

Current Status

Fairly basic MCSP programs compile and work ok -- no support for any kind of separate compilation yet. Other things that don't work include "sub-events" and interleaving on events. Fixpoints work as long as they're tail-recursive. Also, scoping is forward only (can't do mutual recursion on "procedures" or things like that).

The MCSP Language

A typical program (and one that currently works!) could be:

    # test MCSP program
    SYSTEM ::= ((x -> SKIP) || (y -> SKIP))
		

This sets up two parallel processes, one that synchronises on x and another on y. To compile this program successfully, the --unbound-events flag must be given to the compiler. This (and it's MCSP specific) causes any free events in a process definition to be incorporated into its parameters. At some point during compilation (front-end transform) the above would be turned into:

    # test MCSP program
    SYSTEM (x, y) ::= ((x -> SKIP) || (y -> SKIP))
		

which we could have written in the first place if desired.

A top-level process such as SYSTEM is not particularly compatible with what KRoC normally expects. As one of the stages in the front-end transforms the compiler inserts an "environment" process, that alternates on all free events in SYSTEM (its parameters after unbound events are taken care of), printing the event name on KRoC's "screen" channel when triggered.

Events are either bound in formal parameters or by CSP's normal hiding operator, the latter hiding the event from the rest of the system. For example:

    FOO (x) ::= csp -> x -> SKIP
    BAR (y) ::= y -> rocks -> SKIP

    SYSTEM ::= (FOO (z) || BAR (z)) \ {z}
		

The compiler automatically works out which variables are shared in a PAR (not very hard as parallel is a binary operator). At the moment, interleaving is not supported (sorry!) -- that is interleaving in the sense of the intersection of events; disjoint event interleaving is fine (e.g. non-synchronising parallel processes). But when it is, it would look something like:

    SYSTEM ::= (x -> x -> SKIP) || ((x -> y -> SKIP) ||| (z -> x -> SKIP))
		

Alternation (choice) is supported -- both internal and external; for example:

    SYSTEM1 ::= (a -> SKIP) [] (b -> SKIP)
    SYSTEM2 ::= (a -> SKIP) |~| (b -> SKIP)

    SYSTEM ::= SYSTEM1 || SYSTEM2
		

Programs spend most of their time in loops. In this MCSP implementation these are realised through the fixpoint operator:

    SYSTEM ::= @X.(csp -> rules -> X)