A Formal Semantics for Concurrent Systems

  1. Lookup NU author(s)
Author(s)Shields MW, Lauer PE
Series Editor(s)Shaw B
Publication type Report
Series TitleComputing Laboratory Technical Report Series
Year1979
DateApril 1979
Report Number132
Pages14
Full text is available for this publication:
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.
InstitutionComputing Laboratory, The University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
ActionsLink to this publication