Sciweavers

APLAS
2009
ACM

A Fresh Look at Separation Algebras and Share Accounting

13 years 10 months ago
A Fresh Look at Separation Algebras and Share Accounting
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.
Robert Dockins, Aquinas Hobor, Andrew W. Appel
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where APLAS
Authors Robert Dockins, Aquinas Hobor, Andrew W. Appel
Comments (0)