Journal of Philosophical Logic 40 (5):583-632 (2011)

Abstract
Reasoning about concurrent programs involves representing the information that concurrent processes manipulate disjoint portions of memory. In sophisticated applications, the division of memory between processes is not static. Through operations, processes can exchange the implied ownership of memory cells. In addition, processes can also share ownership of cells in a controlled fashion as long as they perform operations that do not interfere, e.g., they can concurrently read shared cells. Thus the traditional paradigm of distributed computing based on locations is replaced by a paradigm of concurrent computing which is more tightly based on program structure. Concurrent Separation Logic with Permissions, developed by O’Hearn, Bornat et al., is able to represent sophisticated transfer of ownership and permissions between processes. We demonstrate how these ideas can be used to reason about fine-grained concurrent programs which do not employ explicit synchronization operations to control interference but cooperatively manipulate memory cells so that interference is avoided. Reasoning about such programs is challenging and appropriate logical tools are necessary to carry out the reasoning in a reliable fashion. We argue that Concurrent Separation Logic with Permissions provides such tools. We illustrate the logical techniques by presenting the proof of a concurrent garbage collector originally studied by Dijkstra et al., and extended by Lamport to handle multiple user processes.
Keywords Resource logics  Separation logic  Program correctness  Concurrent programs  Garbage collection  Heap storage
Categories (categorize this paper)
ISBN(s)
DOI 10.1007/s10992-011-9195-1
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 54,568
Through your library

References found in this work BETA

The Logic of Bunched Implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Assertions.[author unknown] - 2006 - International Studies in Philosophy Monograph Series:167-170.

View all 6 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

AI as Complex Information Processing.Hideyuki Nakashima - 1999 - Minds and Machines 9 (1):57-80.
Semantics of Information as Interactive Computation.Gordana Dodig-Crnkovic - 2008 - Proceedings of the Fifth International Workshop on Philosophy and Informatics 2008.
Reasoning Processes in Propositional Logic.Claes Strannegård, Simon Ulfsbäcker, David Hedqvist & Tommy Gärling - 2010 - Journal of Logic, Language and Information 19 (3):283-314.
Definability and the Structure of Logical Paradoxes.Haixia Zhong - 2012 - Australasian Journal of Philosophy 90 (4):779 - 788.
Concurrent Processing of Saccades.Robert M. McPeek, Edward L. Keller & Ken Nakayama - 1999 - Behavioral and Brain Sciences 22 (4):691-692.

Analytics

Added to PP index
2011-10-18

Total views
33 ( #304,560 of 2,385,661 )

Recent downloads (6 months)
1 ( #560,301 of 2,385,661 )

How can I increase my downloads?

Downloads

My notes