cliff jones

Reasoning about shared-variable concurrency: interactions between research threads

One division of concurrency thinking is between shared-variable and communication-based approaches. This abstract sketches a DAG of connections (with [n] referring back to the nth list item) on the former topic (our planned research will cover the latter which intertwines with the points below; also Temporal Logic research is for future work).

Perhaps the root of the directed graph should be challenge problems because these have been extremely stimulating: Dijkstra was a master (e.g. “Dining Philosophers”); Owicki’s “Find”, Hoare’s “Sieve of Eratosthenes”, the “Fisher/Galler algorithm” and Simpson’s “Four-slot” deserve special mention.

1. Hoare’s 1969 Axiomatic Basis [Hoa69] established a clear approach to constructing proofs of sequential imperative programs.
2. Hoare’s Proof of FIND [Hoa71] pointed the way to a development method for such programs [Obviously 1]. For sequential programs, Apt’s [Apt81] looks at the first decade of Hoare’s logic and [Jon03] traces the move to development methods.
3. After his seminal 1969 paper on sequential programs [1] Hoare looked at extending the approach to parallel programs. In a 1971 paper [Hoa72] it is shown that it is possible to prove that a collection of parallel non- interfering threads satisfy specifications that are the conjunction of the pre/post conditions of its constituent threads. That paper treated the situation where all variables were stack variables.
4. There are many “inventions” of the idea of data abstraction and development by “reification” or “refinement” — initial examples were for sequential programs.
5. Susan Owicki’s 1975 thesis [Owi75] (and a joint paper with her PhD supervisor Gries [OG76]) made a key step in reasoning about shared-variable concurrent programs: the basic idea is to construct separate Hoare-style [1] proofs of all threads under the assumption that there is no interference and to follow this by showing, for each thread T_i, that the the sibling threads do not interfere with the proof of T_i. De Roever’s 2001 book classes [dR01], the Owicki/Gries approach [5] as non-compositional because failure to discharge their final “einmischugsfrei” proof obligation can result in needing to redo the development.
6. 1981 research on Rely/Guarantee (R/G) conditions [Jon81] offers a compositional development method for shared-variable concurrent programs by adding explicit rely and guarantee conditions to Hoare-like pre/post conditions. [1, 2]. It slowly emerged that data abstraction/reification [4] were intimately involved.
7. (Although material on Temporal Logic is planned future work, the 1984 paper by Barringer/Kuiper/Pnueli “Now You Can Compose Temporal Logic Specifications” is an intriguing link to [6]).
8. Reynolds’ Separation Logic in [Rey00] tackled the delicate issue of reasoning about (sequential) programs that use heap variables. [1]
9. In conjunction with others (there’s a nice history paper) O’Hearn developed Concurrent Separation Logic [O’H07] from [8] to reason about concurrent programs that share heap variables. CSL introduces a separating conjunction that, in a sense, carries forward the idea from Hoare’s approach [3]; although dealing with the trickier case of heap variables, separating conjunction formalises rules for when it is valid to conjoin pre and post conditions of separate threads. Another way of looking at CSL is that it is actually a logic of ownership which is important because the ownership of heap locations can pass between threads.
10. Vafeiadis’ RGSep [Vaf07, FFS07] and Feng’s SAGL are serious at- tempts to combine [6] and [9] formally. Furthermore, a friendly rivalry/cooperation exists between researchers working on R/G [6] and CSL [9] with five papers on Simpson’s algorithm alone — in fact, Bornat uses a combination of the ideas (plus “linearisability”).

Currently: research on Views promises a common way of showing property-oriented methods to be sound; recent developments on recasting R/G methods have led to pleasing and useful algebraic presentations. [Hay16, HJ18].

References

[Apt81] Krzysztof R. Apt. Ten years of Hoare’s logic: a survey—part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, October 1981.

[dR01] Willem-Paul de Roever. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, 2001.

[FFS07] Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP: Programming Languages and Systems, pages 173– 188. Springer, 2007.

[Hay16] I. J. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation. Formal Aspects of Computing, 28(6):1057–1078, November 2016.

[HJ18] I. J. Hayes and C. B. Jones. A guide to rely/guarantee thinking. In Jonathan Bowen, Zhiming Liu, and Zili Zhan, editors, Engineering Trustworthy Software Systems – Second International School, SETSS 2017, LNCS. Springer-Verlag, 2018.

[Hoa69] Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 1969.

[Hoa71] Charles Antony Richard Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39–45, January 1971.

[Hoa72] C. A. R. Hoare. Towards a theory of parallel programming. In Operating System Techniques, pages 61–71. Academic Press, 1972.

[Jon81] C. B. Jones. Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University, June 1981. Printed as: Programming Research Group, Technical Monograph 25.

[Jon03] Cliff B. Jones. The early search for tractable ways of reason- ing about programs. IEEE, Annals of the History of Computing, 25(2):26–49, 2003.

[OG76] S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319–340, 1976.

[O’H07] Peter O’Hearn. Resources, concurrency and local reasoning. (accepted for publication in) Theoretical Computer Science, 2007.

[Owi75] S. S. Owicki. Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Department of Computer Science, Cornell University, 1975. Hard copy - Published as technical report 75-251.

[Rey00] J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Jim Davies, Bill Roscoe, and Jim Woodcock, editors, Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.

[Vaf07] Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, 2007.