arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1704.02432cs.PLcs.SE
收藏

线性时间中的动态竞争预测

Dynamic Race Prediction in Linear Time

Dileep Kini, Umang Mathur, Mahesh Viswanathan

摘要:

编写可靠的并发软件对于今天的程序员来说仍然是一个巨大的挑战。程序员很少通过显式地考虑代码执行的不同可能交织来推理代码。我们认为,在一个健全的方式从个人执行检测数据竞争的问题。解决这个问题的经典方法是使用Lamport的happens-before(HB)关系。到目前为止,HB仍然是唯一一种在线性时间内运行的方法。以前的努力,在改善HB,如因果先行(CP)和最大因果模型的不足,由于事实上,他们是不能有效地实现,因此不得不妥协的竞争检测能力,限制他们的技术,以有限大小的片段的执行。我们提出了一种新的弱因果关系(WCP),可以证明它比CP更好,能够检测到更多的种族,同时仍然保持健全。此外,它还允许一个线性时间算法,它可以在整个执行过程中工作,而不必将其分割。

英文摘要:

Writing reliable concurrent software remains a huge challenge for today's programmers. Programmers rarely reason about their code by explicitly considering different possible inter-leavings of its execution. We consider the problem of detecting data races from individual executions in a sound manner. The classical approach to solving this problem has been to use Lamport's happens-before (HB) relation. Until now HB remains the only approach that runs in linear time. Previous efforts in improving over HB such as causally-precedes (CP) and maximal causal models fall short due to the fact that they are not implementable efficiently and hence have to compromise on their race detecting ability by limiting their techniques to bounded sized fragments of the execution. We present a new relation weak-causally-precedes (WCP) that is provably better than CP in terms of being able to detect more races, while still remaining sound. Moreover it admits a linear time algorithm which works on the entire execution without having to fragment it.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑