In this paper we present a new approach to verification of multi-threaded C/C++ programs. Our solution effectively chains the parallel and distributed-memory model checker DiVinE with CLang and the LLVM bitcode interpreter. This combination offers full LTL, distributed-memory model checking of virtually unmodified C/C++ source code and is supported by a newly introduced path-reduction technique. We demonstrate the efficiency of the reduction and also the capacity to produce human-readable counter-examples in two small case studies: a C implementation of the Peterson's mutual exclusion protocol and a C++ implementation of a shared-memory, lock-free FIFO data structure designed for fast inter-thread communication.
展开▼
机译:在本文中,我们提出了一种验证多线程C / C ++程序的新方法。我们的解决方案有效地将平行和分布式存储器模型检查程序与CLANG和LLVM BitCode解释器连接。此组合提供完整的LTL,分布式存储器模型检查几乎未修改的C / C ++源代码,并通过新引入的路径减少技术支持。我们展示了减少的效率以及在两个小写研究中产生人类可读的反击的能力:C彼得森的相互排除协议和C ++实现的C ++实现了一个共享内存,无锁FIFO数据结构专为快速的线程通信而设计。
展开▼