Resources, Concurrency, and Local Reasoning (Abstract)

t) Peter W. O’Hearn Queen Mary, University of London 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 [3]. Then, 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 [4, 1]; scope restrictions were described which had the effect that all process interaction was mediated by a critical region or monitor. Based on such restrictions Hoare described proof rules for shared-variable concurrency that were beautifully modular [4]: 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 ...

• Type: Conference
• Year: 2004
• Where: ESOP
• Authors: Peter W. O'Hearn
• Keywords: Concurrent Programs, ESOP 2004, Process Interaction, Programming Languages, Syntactic Checks