Toggle Main Menu Toggle Search


A Formal Semantics for Concurrent Systems

Lookup NU author(s):



Rigour, in the analysis of synchronisation mechanisms requires a firm mathematical milieu. This principle is applied to a study of the extended semaphore primitives (ESP's) of Agerwala. ESP's are provided with a formal semantics in terms of vector firing sequences (VSF's); objects for describing potential discrete concurrent behaviour, which may be manipulated in a clean algebraic manner. It is shown that any 'program' using ESP's as its only means of synchronisation and which is in some sense 'bounded' has equivalent descriptions in the COSY formalism. COSY is a notation for the abstract specification of discrete systems which has a semantic in terms of VFS's. It is demonstrated that a bounded ESP program may be represented as a COSY program, both of which have identical sets of VFS's. The report concludes with a discussion concerning extensions of this construction to the unbounded case, which essentially speculates on a 'completion' construction for the COSY formalism.

Publication metadata

Author(s): Shields MW, Lauer PE

Series Editor(s): Shaw B

Publication type: Report

Series Title: Computing Laboratory Technical Report Series

Year: 1979

Pages: 14

Source Publication Date: April 1979

Report Number: 132

Institution: Computing Laboratory, The University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne