The Complexity of Predicting Atomicity Violations
The Complexity of Predicting Atomicity Violations
复制标题
预测原子性违规的复杂性
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
P. Madhusudan
中科院分区：
文献类型：
--
作者：
Azadeh Farzan;P. Madhusudan
我们研究了违反单一运行或并发程序的常规或下降模型的跑步预测。当预测忽略所有同步时，我们可以在时间O（n + k .c k）中求解从单个运行（或常规模型）中的预测，其中n是运行的长度（或常规模型的大小）， k是螺纹的数量，C是常数。这与简单的$ o（n^kcdot 2^{k^2}）$算法相比，这是由构建全局自动机和监视它产生的。我们还表明，令人惊讶的是，对于不同步而无需同步的递归并发程序，问题是可决定的。我们的结果使用了一个新颖的轮廓概念：我们从本地和组合中提取曲线，并在构图上结合其效果以预测违反原子性。
对于使用一组锁$ MATHCAL {l} $同步的线程，我们表明可以从运行和常规模型进行预测，可以在时间$ o（n^kcdot 2^{| Mathcal {l} | CDOT log k+k+{k^k^k^ 2}}）$。请注意，在这种情况下，我们无法从n指数上删除因子k。但是，我们表明，更快的算法不太可能：更确切地说，我们证明，常规程序的预测不太可能在参数$（k，| Mathcal {l} |）中进行固定参数，证明是W [ 1] - hard。我们还毫不奇怪地表明，对使用锁进行交流的递归模型的原子性违规预测是不可确定的。
We study the prediction of runs that violate atomicity from a single run, or from a regular or pushdown model of a concurrent program. When prediction ignores all synchronization, we show predicting from a single run (or from a regular model) is solvable in time O (n + k .c k ) where n is the length of the run (or the size of the regular model), k is the number of threads, and c is a constant. This is a significant improvement from the simple $O(n^kcdot 2^{k^2})$ algorithm that results from building a global automaton and monitoring it. We also show that, surprisingly, the problem is decidable for model-checking recursive concurrent programs without synchronizations. Our results use a novel notion of a profile : we extract profiles from each thread locally and compositionally combine their effects to predict atomicity violations.
For threads synchronizing using a set of locks $mathcal{L}$, we show that prediction from runs and regular models can be done in time $O(n^kcdot 2^{|mathcal{L}|cdot log k+{k^2}})$. Notice that we are unable to remove the factor k from the exponent on n in this case. However, we show that a faster algorithm is unlikely : more precisely, we show that prediction for regular programs is unlikely to be fixed-parameter tractable in the parameters $(k,|mathcal{L}|)$ by proving it is W [1]-hard. We also show, not surprisingly, that prediction of atomicity violations on recursive models communicating using locks is undecidable.