On Implementations and Semantics of a Concurrent
The concurrency theory literature contains many proposals for models
of process algebras. We consider an example application of
the pi-calculus, the programming language
Pict of Pierce and Turner,
primarily in order to see how far it is possible to argue, from facts about the
application, that some model is the most appropriate.
We discuss informally the sense in which the
semantics of Pict relates to the behaviour of actual implementations.
Based on this we give an operational model of the interactions between a Pict
implementation (considered as the abstract behaviour of a C program)
and its environment (modelling an operating system and user).
We then give a class of abstract machines and a definition of abstract machine
correctness, using an adapted notion of testing, and prove that a
abstract machine is indeed correct.
We briefly discuss the standard of correctness appropriate for program
transformations and the induced precongruence.
Many of the semantic choices do indeed turn out to be determined by
facts about Pict.
Back to my home page.