Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC, a new SMC algorithm that uses a novel \emph{reads-value-from (RVF)} partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and "reads-from" partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.
翻译:无国籍模式检查( SMC ) 是核查同时程序的标准方法之一 。 由于排期不确定性会创造出巨大的线状交错空间, SMC 试图将这个空间分割成等效类, 并只探索每个类的少数代表。 这种方法的效率取决于两个因素 :(a) 分区的粗糙性, 以及 (b) 在每个类中产生代表的时间。 因此, 寻找高效可探索的粗分割区比最近基于 Mazurkiewiz 和“ 解析” 的分隔方法要容易发现复杂。 我们的实验性评估显示, RVF 与快速分析的快速分析相比, 快速分析通常能产生非常有效的平衡。