A fresh look at separation algebras and share accounting

Robert Dockins, Aquinas Hobor, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

67 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 languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
Pages161-177
Number of pages17
DOIs
StatePublished - Dec 28 2009
Event7th Asian Symposium on Programming Languages and Systems, APLAS 2009 - Seoul, Korea, Republic of
Duration: Dec 14 2009Dec 16 2009

Publication series

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

Other

Other7th Asian Symposium on Programming Languages and Systems, APLAS 2009
CountryKorea, Republic of
CitySeoul
Period12/14/0912/16/09

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A fresh look at separation algebras and share accounting'. Together they form a unique fingerprint.

Cite this