Atomicity Checking in Linear Time using Vector Clocks
Atomicity Checking in Linear Time using Vector Clocks
复制标题
DOI：
10.1145/3373376.3378475
复制
发表时间：
2020-01
期刊：
影响因子：
--
通讯作者：
Umang Mathur;Mahesh Viswanathan
中科院分区：
文献类型：
--
作者：
Umang Mathur;Mahesh Viswanathan
多线程的程序很具有挑战性。开发人员通常需要对大量的线程交织来推理软件行为。通过确保任何执行等同于串行执行所有原子块的执行，诸如原子能之类的非交流属性可以减少此交织空间。我们考虑了动态检查原子性的冲突序列化的良好研究概念。现有算法通过检测在给定执行中观察到的交易图中检测周期来检测违反冲突序列化的行为。这种图中的边数可以随着迹线的长度而四倍地增长，从而使分析不可扩展。在本文中，我们提出了一种新颖的单个通过线性时间算法，该算法使用向量时钟来检测在线环境中违反冲突序列化的行为。实验表明，机场尺度到具有大量事件具有显着加速事件的痕迹。
Multi-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software. A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially. We consider the well studied notion of conflict serializability for dynamically checking atomicity. Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution. The number of edges in such a graph can grow quadratically with the length of the trace making the analysis not scalable. In this paper, we present AeroDrome, a novel single pass linear time algorithm that uses vector clocks to detect violations of conflict serializability in an online setting. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.