Permission Accounting in Separation Logic (Extended Abstract)

Separation logic began by describing total separation between the heap space used by separate parts of a program. It has moved on to consider how total and partial permissions to access heap elements can be transferred between concurrent threads. The roots of the new approach are in Boyland's [3] demonstration of the utility of fractional permissions in reasoning about programs. 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 are paraded