Fine-grained Concurrency with Separation Logic.
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 memor...
| Published in: | Journal of Philosophical Logic Vol. 40; no. 5; pp. 583 - 633 |
|---|---|
| Main Authors: | , , |
| Format: | Article |
| Published: |
Springer Nature
Oct2011
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=65548894&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 65548894 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00223611 JPH jtl: Journal of Philosophical Logic issn: 00223611 maglogo: N pubinfo: dt: Oct2011 vid: 40 iid: 5 pid: 237 pub: Springer Nature artinfo: ui: 65548894 10.1007/s10992-011-9195-1 ppf: 583 ppct: 50 formats: fmt: @attributes: type: P size: 711KB tig: atl: Fine-grained Concurrency with Separation Logic. aug: au: Kapoor, Kalpesh Lodaya, Kamal Reddy, Uday affil: Department of Mathematics, Indian Institute of Technology Guwahati, Guwahati 781 039 India The Institute of Mathematical Sciences, C.I.T. Campus Chennai 600 113 India School of Computer Sciences, University of Birmingham, Edgbaston Birmingham B15 2TT United Kingdom su: Hoare logic Parallel programs (Computer programs) Computer software correctness Distributed computing Synchronization Garbage collection (Computer science) Computer memory management sug: subj: Hoare logic Parallel programs (Computer programs) Computer software correctness Distributed computing Synchronization Garbage collection (Computer science) Computer memory management keyword: Concurrent programs Garbage collection Heap storage Program correctness Resource logics Separation logic 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. pubtype: Academic Journal doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y custom: Journal of Philosophical Logic is a copyright of Springer, 2011. All Rights Reserved. item: Journal of Philosophical Logic holder: Springer Nature dt: @attributes: year: 2011 holdings: @attributes: islocal: N |
|---|