Concurrent Processes

Abstract

This chapter expands the process language by an operation of concurrent composition of processes. The operation considered is called synchronisation merge because it allows processes to synchronise on particular actions, while others can be performed independently of another. This operation is then applied in several examples to model concurrent processes in computing systems. Counters of bounded capacity are implemented as concurrent compositions of counters of capacity one. A simple controller for a railway level crossing is design, with the system modelled as the concurrent composition of the road, the rail and the controller; safety and liveness properties of the controller are considered in detail. Various mutual exclusion algorithms are considered, including for the dining philosophers problem and Peterson’s algorithm for two processes attempting to access a shared critical section. Simple sender-receiver protocols are also presented, including a version of the alternating bit protocol.