Contrasting Themes in the Semantics of Imperative Concurrency

摘要

Four sample languages for which operational and denotational semantic models are developed are presented. All languages have parallel execution through interleaving, and three have 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, the local and global variety. Linear time versus branching time is investigated. In the former, streams, i.e., finite or infinite sequences of actions; in the latter the (metrically based) notion of process is introduced. Ready sets are used to compare semantics.