Permission accounting in separation logic

摘要: A lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion permission access. Transfer threads, subdivision and combination discussed. The roots are in Boyland's [3] demonstration utility fractional permissions specifying non-interference threads. We add counting permission, which mirrors programming technique called counting. Both permit passivity, specification that a program can be permitted access cell yet prevented from altering it. Models both mechanisms described. use two different defended. Some interesting problems acknowledged some intriguing possibilities for future development, including resourcing as step beyond typing, paraded.