Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation
Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation
复制标题
通过动态资源创建验证高阶并发程序
DOI：
10.1007/978-3-319-47958-3_18
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Takeshi Tsukada and Naoki Kobayashi
中科院分区：
文献类型：
--
作者：
Kazuhide Yasukata;Takeshi Tsukada and Naoki Kobayashi
我们提出了一个健全的和完整的静态验证方法（高阶）并发程序的动态创建资源，如锁和线程标识符。为了处理（可能是无限的）资源创建，我们准备了一组有限的抽象资源名称，并引入了范围安全的概念，作为避免映射到相同抽象名称的不同具体资源混淆的充分条件。如果在创建了具有相同抽象名称的另一个资源之后没有使用任何资源，则称程序是作用域安全的。证明了具有嵌套锁的作用域安全程序的成对可达性问题是可判定的。我们还提出了一种方法来检查给定的程序是范围安全的，并且具有嵌套锁定。
We propose a sound and complete static verification method for (higher-order) concurrent programs withdynamic creationof resources, such as locks and thread identifiers. To deal with (possibly infinite) resource creation, we prepare a finite set of abstract resource names and introduce the notion ofscope-safetyas a sufficient condition for avoiding the confusion of different concrete resources mapped to the same abstract name. We say that a program isscope-safeif no resource is used after the creation of another resource of the same abstract name. We prove that the pairwise-reachability problem is decidable for scope-safe programs with nested locking. We also propose a method for checking that a given program is scope-safe and with nested locking.