Permission accounting in separation logic
Permission accounting in separation logic
复制标题
DOI：
10.1145/1047659.1040327
复制
发表时间：
2005-01-01
影响因子：
--
通讯作者：
Parkinson, M
中科院分区：
文献类型：
--
作者：
Bornat, R;Calcagno, C;Parkinson, M
本文基于访问权限的概念，描述了一种在并发线程之间实现无竞争堆存储共享的轻量级逻辑方法。线程间的权限转移；讨论了权限的细分和组合。该方法的根源在于Boyland的[3]演示，该演示演示了分数权限在指定并发线程之间的不干扰方面的实用性。我们增加了计数许可的概念；这反映了称为权限计数的编程技术。分数权限和计数权限都允许被动性，即允许程序访问堆单元但不允许修改堆单元的规范。描述了这两种机制的模型。为使用两种不同的机制进行辩护。一些有趣的问题被承认，以及未来发展的一些有趣的可能性；包括资源分配的概念，作为打字之外的一个步骤。
A light-weight 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.