Contrasting themes in the semantics of imperative concurrency

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 of actions; in the latter the (metrically based) notion of process is introduced. We furthermore study a model with only finite observations. Ready sets also appear, used as technical tool to compare various semantics. Altogether, ten models for the four languages are described, and precise statements on (the majority of) their interrelationships are made. The paper supplies no proofs; for these references to technical papers by the authors are provided.