Monitoring Refinement via Symbolic Reasoning
Monitoring Refinement via Symbolic Reasoning
复制标题
DOI：
10.1145/2813885.2737983
复制
发表时间：
2015-06-01
影响因子：
--
通讯作者：
Hamza, Jad
中科院分区：
文献类型：
--
作者：
Emmi, Michael;Enea, Constantin;Hamza, Jad
并发对象（如信号量、锁和原子集合）的有效实现对现代计算至关重要。编程这样的对象是容易出错的：在最大限度地减少并发对象调用之间的同步开销时，有可能与引用实现一致-或者用正式的术语来说，有可能违反观察细化。精确地测试这种细化，即使在一个单一的执行是棘手的，限制了现有的方法执行很少的对象invocations.We开发可扩展的和有效的算法检测细化违规。我们的算法是建立在增量，符号推理，并利用基本的见解细化检查问题。我们的方法是合理的，因为我们只检测实际的违规行为，并远远超出现有的违规检测算法的规模。根据经验，我们发现我们的方法实际上是完整的，因为我们发现了实际处决中出现的违法行为。
Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations - or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations.We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions.