What a process may share

A subject the papers are about. The loosest grouping, and the one to reach for last.

What processes may share, and what keeps the sharing honest. First as language constructs -- semaphores, monitors, then message passing, which shares nothing -- and afterwards as proof rules for the same question, where what a process owns becomes what the logic tracks.

The construct half is nearly complete as a sequence: Dijkstra's 1965 mutual exclusion solution and the THE system, Brinch Hansen's structured multiprogramming, Hoare's monitors, then the two 1978 answers that go the other way -- distributed processes and CSP, where the discipline is that nothing is shared at all. Lampson and Redell's Mesa paper is the one that reports what monitors cost once real programs use them, and Brinch Hansen on reproducible testing is the admission that a construct which prevents races does not make them observable.

The proof half contains a genuine disagreement rather than a progression. Owicki and Gries discharge interference by proving that no assertion in one process invalidates one in another -- which works and does not compose, because the obligations grow with the product of the processes. Jones's rely/guarantee is the compositional answer to exactly that. O'Hearn's concurrent separation logic is the third answer: make ownership the thing the logic tracks, so disjointness is structural rather than checked pairwise. Brookes surveys where that ended up, and Views and Nanevski are attempts to give the competing accounts one framework.

Chandy and Lamport sit slightly apart, asking not what may be shared but what a global state even means when nobody can observe one.

Iorga is the set's sharpest late entry, and belongs to the chip material as much as here: it works out the semantics of shared memory in Intel CPU/FPGA systems -- that is, what the hardware actually provides underneath every logic above.

Three Owicki records are held: a 1975 technical report and two 1976 papers, in CACM and Acta Informatica. Their relationship is flagged on the links and not settled; the Acta paper is titled 'I' and the corpus holds no part II.