Abstract Jones and Plotkin give a general construction for forming a probabilistic powerdomain over any directed-complete partial order [Jon90, JoP89]. We apply their technique to the failures/divergences semantic model for Communicating Sequential Processes [Hoa85]. The resulting probabilistic model supports a new binary operator, probabilistic choice, and retains all operators of CSP including its two existing forms of choice. An advantage of using the general construction is that it is easy to see which CSP identities remain true in the probabilistic model. A surprising consequence however is that probabilistic choice distributes through all other operators; such algebraic mobility means that the syntactic position of the choice operator gives little information about when the choice actually must occur. That in turn leads to some interesting interaction between probability and nondeterminism. A simple communications protocol is used to illustrate the probabilistic algebra, and several suggestions are made for accommodating and controlling nondeterminism when probability is present.

Abstract In this paper we formalise three different views of a virtual shared memory system and show that they are equivalent. The formalisation starts with five basic component processes specified in the language of CSP [Hoa85], which can be adapted as necessary by two operations called labelling and clamping, and are combined in two basic ways: either they are chained, so that the output of one component becomes the input of the next, or they are put in parallel, so that their communications are arbitrarily interleaved. Using the laws of CSP we show that these basic processes and operators satisfy a number of algebraic equivalences, which enable us to prove equivalence of the different models of the memory system by reasoning entirely at the level of processes, instead of at the lower and more complicated level of events. As a result the proofs of equivalence of the different models are purely algebraic and very simple. The specification is intended to provide a general framework for any architecture using an interconnection network, such as the on-chip interconnect between macrocells or the networks of processor nodes connected by bit-serial interconnect which are described in [Jon93]. It addresses architecture independent design issues such as access transparency, connectivity, addressing models and serialisability. By structuring it as a hierarchy of models it is hoped that the treatment of these many issues is made as clear and tractable as possible, whilst the proofs of equivalence ensure consistency.

Probabilistic predicates generalize standard predicates over a state space; with probabilistic predicate transformers one thus reasons about imperative programs in terms of probabilistic pre- and postconditions. Probabilistic healthiness conditions generalize the standard ones, characterizing “real” probabilistic programs, and are based on a connection with an underlying relational model for probabilistic execution; in both contexts demonic nondeterminism coexists with probabilistic choice. With the healthiness conditions, the associated weakest-precondition calculus seems suitable for exploring the rigorous derivation of small probabilistic programs.