A fresh look at separation algebras and share accounting

Robert Dockins; Aquinas Hobor; Andrew W. Appel

doi:10.1007/978-3-642-10672-9_13

A fresh look at separation algebras and share accounting

Robert Dockins, Aquinas Hobor, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

79 Scopus citations

Abstract

Separation Algebras serve as models of Separation Logics; Share Accounting allows reasoning about concurrent-read/exclusive- write resources in Separation Logic. In designing a Concurrent Separation Logic and in mechanizing proofs of its soundness, we found previous axiomatizations of separation algebras and previous systems of share accounting to be useful but imperfect. We adjust the axioms of separation algebras; we demonstrate an operator calculus for constructing new separation algebras; we present a more powerful system of share accounting with a new, simple model; and we provide a reusable Coq development.

Original language	English (US)
Title of host publication	Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
Pages	161-177
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-642-10672-9_13
State	Published - 2009
Event	7th Asian Symposium on Programming Languages and Systems, APLAS 2009 - Seoul, Korea, Republic of Duration: Dec 14 2009 → Dec 16 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5904 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	7th Asian Symposium on Programming Languages and Systems, APLAS 2009
Country/Territory	Korea, Republic of
City	Seoul
Period	12/14/09 → 12/16/09

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-10672-9_13

Cite this

Dockins, R., Hobor, A., & Appel, A. W. (2009). A fresh look at separation algebras and share accounting. In Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings (pp. 161-177). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5904 LNCS). https://doi.org/10.1007/978-3-642-10672-9_13

@inproceedings{6afb75335d9241d0ac90bc1712ec9d8e,

title = "A fresh look at separation algebras and share accounting",

abstract = "Separation Algebras serve as models of Separation Logics; Share Accounting allows reasoning about concurrent-read/exclusive- write resources in Separation Logic. In designing a Concurrent Separation Logic and in mechanizing proofs of its soundness, we found previous axiomatizations of separation algebras and previous systems of share accounting to be useful but imperfect. We adjust the axioms of separation algebras; we demonstrate an operator calculus for constructing new separation algebras; we present a more powerful system of share accounting with a new, simple model; and we provide a reusable Coq development.",

author = "Robert Dockins and Aquinas Hobor and Appel, {Andrew W.}",

year = "2009",

doi = "10.1007/978-3-642-10672-9_13",

language = "English (US)",

isbn = "3642106714",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "161--177",

booktitle = "Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings",

note = "7th Asian Symposium on Programming Languages and Systems, APLAS 2009 ; Conference date: 14-12-2009 Through 16-12-2009",

}

Dockins, R, Hobor, A & Appel, AW 2009, A fresh look at separation algebras and share accounting. in Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5904 LNCS, pp. 161-177, 7th Asian Symposium on Programming Languages and Systems, APLAS 2009, Seoul, Korea, Republic of, 12/14/09. https://doi.org/10.1007/978-3-642-10672-9_13

A fresh look at separation algebras and share accounting. / Dockins, Robert; Hobor, Aquinas; Appel, Andrew W.
Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. 2009. p. 161-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5904 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A fresh look at separation algebras and share accounting

AU - Dockins, Robert

AU - Hobor, Aquinas

AU - Appel, Andrew W.

PY - 2009

Y1 - 2009

N2 - Separation Algebras serve as models of Separation Logics; Share Accounting allows reasoning about concurrent-read/exclusive- write resources in Separation Logic. In designing a Concurrent Separation Logic and in mechanizing proofs of its soundness, we found previous axiomatizations of separation algebras and previous systems of share accounting to be useful but imperfect. We adjust the axioms of separation algebras; we demonstrate an operator calculus for constructing new separation algebras; we present a more powerful system of share accounting with a new, simple model; and we provide a reusable Coq development.

AB - Separation Algebras serve as models of Separation Logics; Share Accounting allows reasoning about concurrent-read/exclusive- write resources in Separation Logic. In designing a Concurrent Separation Logic and in mechanizing proofs of its soundness, we found previous axiomatizations of separation algebras and previous systems of share accounting to be useful but imperfect. We adjust the axioms of separation algebras; we demonstrate an operator calculus for constructing new separation algebras; we present a more powerful system of share accounting with a new, simple model; and we provide a reusable Coq development.

UR - http://www.scopus.com/inward/record.url?scp=72449130855&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=72449130855&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-10672-9_13

DO - 10.1007/978-3-642-10672-9_13

M3 - Conference contribution

AN - SCOPUS:72449130855

SN - 3642106714

SN - 9783642106712

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 161

EP - 177

BT - Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings

T2 - 7th Asian Symposium on Programming Languages and Systems, APLAS 2009

Y2 - 14 December 2009 through 16 December 2009

ER -

A fresh look at separation algebras and share accounting

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this