Decidable models of integer-manipulating programs with recursive parallelism
Decidable models of integer-manipulating programs with recursive parallelism
复制标题
具有递归并行性的整数操作程序的可判定模型
DOI：
10.1016/j.tcs.2018.04.050
复制
发表时间：
2018
影响因子：
1.1
通讯作者：
Hague M
中科院分区：
文献类型：
--
作者：
Hague M
我们研究了具有递归并行性（即无限线程创建和递归）以及无限整数变量的多线程程序的安全性验证。由于每个程序配置中的线程都是以分层的方式构建的，因此我们的模型是状态扩展的地面树重写系统，该系统配备了共享的无界整数计数器，可以递增，递减，并与整数常数进行比较。由于模型是图灵完备的，我们提出了一个可判定的欠近似。首先，使用类似于上下文绑定的限制，我们通过弱全局控制（即可能具有自循环的DAG）欠近似全局控制，从而限制不同线程之间的同步数量。其次，我们限制了计数器的非递减和非递增模式之间的反转次数。在此限制下，我们证明了可达性成为NP完全。事实上，它是多时间可简化的，以满足存在的Presburger公式，这允许人们利用高度优化的SMT求解器。我们的可判定近似严格概括了已知的可判定模型，包括（i）弱同步地面树重写系统，（ii）同步/反向有界并发下推系统计数器。最后，我们表明，当配备有反向有界计数器，放松弱控制限制的概念，衰老的结果在不可判定性。
We study safety verification for multithreaded programs with recursive parallelism (i.e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is state-extended ground-tree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turing-complete, we propose a decidable underapproximation. First, using a restriction similar to context-bounding, we underapproximate the global control by a weak global control (i.e. DAGs possibly with self-loops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between non-decrementing and non-incrementing modes of the counters. Under this restriction, we show that reachability becomes NP-complete. In fact, it is poly-time reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weakly-synchronised ground-tree rewrite systems, and (ii) synchronisation/reversal-bounded concurrent pushdown systems with counters. Finally, we show that, when equipped with reversal-bounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.