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.

In  POPL

Details