Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References
Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References
复制标题
DOI：
10.1007/978-3-540-89330-1_12
复制
发表时间：
2008-12
期刊：
影响因子：
--
通讯作者：
Kohei Suenaga
中科院分区：
文献类型：
--
作者：
Kohei Suenaga
我们提出了一个基于类型的无死锁验证的并发程序与非块结构的锁原语和可变引用。虽然这两个特征经常使用，但以前的核查方法没有充分处理这两个特征。我们的类型系统使用了锁级别、义务和权限的新颖组合。锁级别用于保证以特定的顺序获取锁。义务和所有权保证获取的锁只被释放一次。
We present a type-based deadlock-freedom verification for concurrent programs with non-block-structured lock primitives and mutable references. Though those two features are frequently used, they are not dealt with in a sufficient manner by previous verification methods. Our type system uses a novel combination oflock levels, obligationsandownerships. Lock levels are used to guarantee that locks are acquired in a specific order. Obligations and ownerships guarantee that an acquired lock is released exactly once.