We present the SER modeling language for automatically verifying serializability of concurrent programs, i.e., whether every concurrent execution of the program is equivalent to some serial execution. SER programs are suitably restricted to make this problem decidable, while still allowing for an unbounded number of concurrent threads of execution, each potentially running for an unbounded number of steps. Building on prior theoretical results, we give the first automated end-to-end decision procedure that either proves serializability by producing a checkable certificate, or refutes it by producing a counterexample trace. We also present a network-system abstraction to which SER programs compile. Our decision procedure then reduces serializability in this setting to a Petri net reachability query. Furthermore, in order to scale, we curtail the search space via multiple optimizations, including Petri net slicing, semilinear-set compression, and Presburger-formula manipulation. We extensively evaluate our framework and show that, despite the theoretical hardness of the problem, it can successfully handle various models of real-world programs, including stateful firewalls, BGP routers, and more.

翻译：我们提出SER建模语言，用于自动验证并发程序的可串行化，即程序的每个并发执行是否等价于某个串行执行。SER程序经过适当限制以使该问题可判定，同时仍允许无限数量的并发执行线程，每个线程可能运行无限步数。基于先前的理论结果，我们给出了首个自动化端到端判定程序，该程序要么通过生成可验证证书来证明可串行化，要么通过生成反例轨迹来证伪。我们还提出了SER程序编译所面向的网络系统抽象模型。在此设置下，我们的判定程序将可串行化问题归约为Petri网可达性查询。此外，为提升可扩展性，我们通过多种优化技术缩减搜索空间，包括Petri网切片、半线性集压缩和Presburger公式操作。我们对框架进行了全面评估，结果表明尽管该问题在理论上具有高复杂度，我们的方法仍能成功处理各类现实程序模型，包括有状态防火墙、BGP路由器等。