Resources, Concurrency and Local Reasoning

 Peter O'Hearn, Queen Mary, University of London, UK

In the 1960s  Dijkstra suggested that, in order to limit the complexity of potential process interactions, concurrent programs should be designed so that different processes behave independently, except at rare moments of synchronization.  In the 1970s, Hoare and Brinch Hansen argued that debugging and reasoning about concurrent programs could be considerably simplified using compiler-enforceable syntactic constraints that preclude interference. Based on such restrictions Hoare described proof rules for shared-variable concurrency that were beautifully modular: one could reason locally about a process, and simple syntactic checks ensured that no other process could tamper with its state in a way that invalidated the local reasoning.

The major problem with Hoare and Brinch Hansen's proposal is that its scope-based approach to resource separation is too restrictive for many realistic programs.  It does not apply to flexible but unstructured  constructs such as semaphores, and the syntactic checks it relies on are insufficient to rule out interference in the presence of pointers and aliasing.

There is thus a mismatch, between the intuitive basis of concurrent programming with resources, where separation remains a vital design idea, and formal techniques for reasoning about such programs, where methods based on separation are severely limited.  The purpose of this work is to revisit these issues, using the recent formalism of separation logic: by using a logic of resources rather than syntactic constraints, we can overcome the limitations of scope-based approaches, while retaining their modular character.

We describe a variation on the proof rules of Hoare for conditional critical regions, using the ``separating conjunction'' connective to preclude pointer-based interference.  With the modified rules we can at once handle many examples where a linked data structure rather than, say, an array is used within a process or within a data abstraction that mediates interprocess interaction.