Permission accounting in separation logic

R Bornat, C Calcagno, P O'Hearn… - Proceedings of the 32nd …, 2005 - dl.acm.org
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of …, 2005dl.acm.org
A lightweight logical approach to race-free sharing of heap storage between concurrent
threads is described, based on the notion of permission to access. Transfer of permission
between threads, subdivision and combination of permission is discussed. The roots of the
approach are in Boyland's [3] demonstration of the utility of fractional permissions in
specifying non-interference between concurrent threads. We add the notion of counting
permission, which mirrors the programming technique called permission counting. Both …
A lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion of permission to access. Transfer of permission between threads, subdivision and combination of permission is discussed. The roots of the approach are in Boyland's [3] demonstration of the utility of fractional permissions in specifying non-interference between concurrent threads. We add the notion of counting permission, which mirrors the programming technique called permission counting. Both fractional and counting permissions permit passivity, the specification that a program can be permitted to access a heap cell yet prevented from altering it. Models of both mechanisms are described. The use of two different mechanisms is defended. Some interesting problems are acknowledged and some intriguing possibilities for future development, including the notion of resourcing as a step beyond typing, are paraded.
ACM Digital Library