Fine-grained Concurrency with Separation Logic

Research output: Contribution to journalArticle

Standard

Fine-grained Concurrency with Separation Logic. / Kapoor, K; Lodaya, K; Reddy, Uday.

In: Journal of Philosophical Logic, Vol. 40, No. 5, 01.10.2011, p. 583-632.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Kapoor, K ; Lodaya, K ; Reddy, Uday. / Fine-grained Concurrency with Separation Logic. In: Journal of Philosophical Logic. 2011 ; Vol. 40, No. 5. pp. 583-632.

Bibtex

@article{8dd6947b2e764420918f73bc89d6b8c7,
title = "Fine-grained Concurrency with Separation Logic",
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 = "Separation logic, Concurrent programs, Garbage collection, Program correctness, Resource logics, Heap storage",
author = "K Kapoor and K Lodaya and Uday Reddy",
year = "2011",
month = oct
day = "1",
doi = "10.1007/s10992-011-9195-1",
language = "English",
volume = "40",
pages = "583--632",
journal = "Journal of Philosophical Logic",
issn = "0022-3611",
publisher = "Springer",
number = "5",

}

RIS

TY - JOUR

T1 - Fine-grained Concurrency with Separation Logic

AU - Kapoor, K

AU - Lodaya, K

AU - Reddy, Uday

PY - 2011/10/1

Y1 - 2011/10/1

N2 - 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.

AB - 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.

KW - Separation logic

KW - Concurrent programs

KW - Garbage collection

KW - Program correctness

KW - Resource logics

KW - Heap storage

U2 - 10.1007/s10992-011-9195-1

DO - 10.1007/s10992-011-9195-1

M3 - Article

VL - 40

SP - 583

EP - 632

JO - Journal of Philosophical Logic

JF - Journal of Philosophical Logic

SN - 0022-3611

IS - 5

ER -