Formal semantics for LIPS (Language for Implementing Parallel/distributed Systems)

This thesis presents operational semantics and an abstract machine for a point-to-point asynchronous message passing language called LIPS (Language for Implementing Parallel/ distributed Systems). One of the distinctive features of LIPS is its capability to handle computation and communication independently. Taking advantage of this capability, a two steps strategy has been adopted to define the operational semantics. The two steps are as follows:
• A big-step semantics with single-step re-writes is used to relate the expressions and their evaluated results (computational part of LIPS).
• The developed big-step semantics has been extended with Structural Operational Semantics (SOS) to describe the asynchronous message passing of LIPS (communication part of LIPS).
The communication in LIPS has been implemented using Asynchronous Message Passing System (AMPS). It makes use of very simple data structures and avoids the use of buffers.
While operational semantics is used to specify the meaning of programs, abstract machines are used to provide intermediate representation of the language's implementation. LIPS Abstract Machine (LAM) is defined to execute LIPS programs. The correctness of the execution of the LIPS program/expression written using the operational semantics is verified by comparing it with its equivalent code generated using the abstract machine.
Specification of Asynchronous Communicating Systems (SACS) is a process algebra developed to specify the communication in LIPS programs. It is an asynchronous variant of Synchronous Calculus of Communicating Systems (SCCS). This research presents the SOS for SACS and looks at the bisimulation equivalence properties for SACS which can be used to verify the behaviour of a specified process.
An implementation is said to be complete when it is equivalent to its specifications. SACS has been used for the high level specification of the communication part of LIPS programs and is implemented using AMPS. This research proves that SACS and AMPS are equivalent by defining a weak bisimulation equivalence relation between the SOS of both SACS and AMPS.

A thesis submitted to Middlesex University in partial fulfilment of the requirements for the degree of Doctor of Philosophy.