The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. It uses buffered states and an inductive definition of execution to assign an input-output meaning to pomsets. We show that our denotational account is sound and complete relative to the axiomatic account, that is, that it captures exactly the behaviours permitted by the axiomatic account. Our compositional approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.

John Reynolds (1935-2013) was a pioneer of programming languages research. In this paper we pay tribute to the man, his ideas, and his influence.

Abstract John Reynolds (1935-2013) was a pioneer of programming languages research. In this paper we pay tribute to the man, his ideas, and his influence.

We consider a parallel Algol-like language, combining the /spl lambda/-calculus with shared-variable parallelism. We provide a denotational semantics for this language, simultaneously adapting the possible worlds model of Reynolds and Oles (1981, 1982) to the parallel setting and generalizing the "transition traces" model to the procedural setting. This semantics supports reasoning about safety and liveness properties of parallel programs, and validates a number of natural laws of program equivalence based on noninterference properties of local variables. We also provide a relationally parametric semantics, to permit reasoning about relation-preserving properties of programs, and adapting work of O'Hearn and Tennent (1995) to the parallel setting. This semantics supports standard methods of reasoning about representational independence. The clean design of the programming language and its semantics supports the orthogonality of procedures and shared-variable parallelism.

We call language L1 intensionally more expressive than L2 if there are functions which can be computed faster in L1 than in L2. We study the intensional expressiveness of several languages: the Berry-Curien programming language of sequential algorithms, CDS0, a deterministic parallel extension to it, named CDSP, and various parallel extensions to the functional programming language PCF. The paper consists of two parts.

Gives a new denotational semantics for a shared variable parallel programming language and proves full abstraction. The semantics gives identical meanings to commands if and only if they induce the same partial correctness behavior in all program contexts. The meaning of a command is a set of transition traces, which record the ways in which a command may interact with and be affected by its environment. It is shown how to modify the semantics to incorporate new program constructs, to allow for different levels of granularity or atomicity, and to model fair infinite computation, in each case achieving full abstraction with respect to an appropriate notion of program behavior.>

A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated and proved. The possibilities of nondetermimsm are fully taken into account.

Two distinct models for the notion of communicating processes are introduced, developed and related. The first, called the possible-futures model, is a generalization to nondeterministic systems of the familiar derivative (Nerode equivalence class) construction. The second, called the acceptance-refusals model, is a slight strengthening of a model introduced by Hoare, Brookes, and Roscoe. The PF model can be mapped onto the AR model homomorphically, and the equivalence classes of this map can be characterized by imposing a very natural equivalence relation on the PF model. The resulting quotient algebra admits a complete partial order structure in which the algebraic operations are continuous.