View article

A survey is given of work performed by the authors in recent years concerning the semantics of imperative concurrency. Four sample languages are presented for which a number of operational and denotational semantic models are developed. All languages have parallel execution through interleaving, and the last three have as well a form of synchronization. Three languages are uniform, i.e., they have uninterpreted elementary actions; the fourth is nonuniform and has assignment, tests and value-passing communication. The operational models build on Hennessy-Plotkin transition systems; as denotational structures both metric spaces and cpo domains are employed. Two forms of nondeterminacy are distinguished, viz. the local and global variety. As associated model-theoretic distinction that of linear time versus branching time is investigated. In the former we use streams, i.e. finite or infinite sequences …