一句话：通过内存模型静态分析计算关系边界，并优化 SMT 编码，加速有界模型检测。
本文旨在提升内存模型模块化有界模型检测器的效率。第一个贡献是作为预处理的内存模型静态分析，它计算事件对之间可能或必然存在的关系边界，并将这些边界相对于事件执行进行相对化，从而首次不仅能得到上界，也能得到有意义的下界；分析还可导入外部验证实例信息以提高精度。第二个贡献是新的 SMT 编码优化，特别是利用下界简化无环性约束。作者在有界模型检测器中实现了分析与优化，并在挑战性基准上评估。结果显示，包含分析时间在内，验证时间最多减少 40%，并能高效检查 Linux 内核代码的安全性、活性与数据竞争自由。
The goal of this work is to improve the efficiency of bounded model checkers that are modular in the memory model. Our first contribution is a static analysis for the given memory model that is performed as a preprocessing step and helps us significantly reduce the encoding size. Memory model make use of relations to judge whether an execution is consistent. The analysis computes bounds on these relations: which pairs of events may or must be related. What is new is that the bounds are relativized to the execution of events. This makes it possible to derive, for the first time, not only upper but also meaningful lower bounds. Another important feature is that the analysis can import information about the verification instance from external sources to improve its precision. Our second contribution are new optimizations for the SMT encoding. Notably, the lower bounds allow us to simplify the encoding of acyclicity constraints. We implemented our analysis and optimizations within a bounded model checker and evaluated it on challenging benchmarks. The evaluation shows up-to 40% reduction in verification time (including the analysis) over previous encodings. Our optimizations allow us to efficiently check safety, liveness, and data race freedom in Linux kernel code.
@article{paperbot1828,
title = {Static Analysis of Memory Models for SMT Encodings},
author = {Thomas Haas and René Maseli and Roland Meyer and Hernán Ponce de León},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622855}
}