Staged concurrent program analysis
Staged concurrent program analysis
复制标题
DOI：
10.1145/1882291.1882301
复制
发表时间：
2010-11
期刊：
影响因子：
--
通讯作者：
Nishant Sinha;Chao Wang
中科院分区：
文献类型：
--
作者：
Nishant Sinha;Chao Wang
并发程序验证是具有挑战性的，因为它涉及探索大量可能的线程交织以及复杂的顺序推理。因此，并发程序验证器采取双模态推理，其在线程内（顺序）语义和线程间（并发）语义上的推理之间交替。这种推理通常涉及重复的线程内推理以探索每个交织（线程间推理），并且导致低效率。在本文中，我们提出了一个新的两阶段分析，完全分离内和线程间的推理。第一阶段使用顺序程序语义来获得每个线程在全局访问方面的精确摘要。第二阶段通过使用顺序一致性的概念组合这些线程模块化摘要来执行线程间推理。然后，在现成的SMT求解器的帮助下，在这个组合中检查断言违规和其他并发错误。我们已经实现了我们的方法在融合框架检查并发C程序表明，避免冗余的双峰推理，使分析更具可扩展性。
Concurrent program verification is challenging because it involves exploring a large number of possible thread interleavings together with complex sequential reasoning. As a result, concurrent program verifiers resort to bi-modal reasoning, which alternates between reasoning over intra-thread (sequential) semantics and inter-thread (concurrent) semantics. Such reasoning often involves repeated intra-thread reasoning for exploring each interleaving (inter-thread reasoning) and leads to inefficiency. In this paper, we present a new two-stage analysis which completely separates intra- and inter-thread reasoning. The first stage uses sequential program semantics to obtain a precise summary of each thread in terms of the global accesses made by the thread. The second stage performs inter-thread reasoning by composing these thread-modular summaries using the notion of sequential consistency. Assertion violations and other concurrency errors are then checked in this composition with the help of an off-the-shelf SMT solver. We have implemented our approach in the FUSION framework for checking concurrent C programs shows that avoiding redundant bi-modal reasoning makes the analysis more scalable.