Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Brinch Hansen, P.: Operating System Principles. Prentice-Hall, Englewood Cliffs (1973)
Brookes, S.D.: A semantics for concurrent separation logic. Draft of 7/25/03 (2003)
Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43–112. Academic Press, London (1968)
Hoare, C.A.R.: Towards a theory of parallel programming. In: Hoare, Perrot (eds.) Operating Systems Techniques. Academic Press, London (1972)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Conference (1983)
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: 31st POPL, Venice, January 2004, pp. 268–280 (2004)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica (19), 319–340 (1976)
Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13(1), 45–60 (1981)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Invited Paper, LICS 2002 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
O’Hearn, P.W. (2004). Resources, Concurrency, and Local Reasoning. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive