1.3.2 Simple buffer example

As a simple example, consider the specification that a process behaves like a one place buffer. This can be represented by the simple process COPY:

COPY left?x right!x COPY

A possible implementation might use separate sender and receiver processes, communication via a channel mid and an acknowledgement channel ack:

SEND	left?x mid!x ack SEND
REC	mid?x right!x ack REC
SYSTEM	(SEND REC) \ X,
	where X={|mid,ack|}

In this system, the process SEND sends the messages it receives on left to the channel mid (which is made internal to the SYSTEM by the use of hiding) and then waits for an acknowledgement, ack. In a rather similar way, REC receives these messages on the internal channel and passes them on to right. It then performs the acknowledgement ack, allowing the whole process to start again.

We may show that COPYSYSTEM confirming that the extra buffering introduced by having two communicating processes is eliminated by the use of an acknowledgement signal. In fact, SYSTEMCOPY is also true, so these two processes are actually equivalent. Other, weaker specifications that could be proved of either include

DF = a DF

which specifies that they are deadlock-free (this process may select any single event from the overall alphabet but can never get into a state where it can refuse all events).

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.