一句话：提出 Mixer——面向混合大小访问程序的最优 DPOR 算法，并在 GenMC 中实现，首次自动验证此类 C/C++ 并发代码。
采用动态偏序归约（DPOR）的先进模型检测器已能在 SC、TSO、RA 以及修复后的 C11 内存模型（RC11）等多种内存模型下，以最优且节省内存的方式验证并发程序。然而，当程序存在混合大小访问（MSA）——即原子指令访问同一字内不同（集合的）字节——时，这些 DPOR 技术无法保持最优性。这类模式在含 C/C++ union 类型的真实代码中自然出现，甚至被用于并发场景。为此，本文提出 Mixer，一种面向 MSA 程序的最优 DPOR 算法，它允许（多字节）读被多个写共同重访。作者将 Mixer 实现于 GenMC 模型检测器，首次实现了对含混合大小访问的 C/C++ 代码的自动验证。该结果还可推广到更一般的事务程序情形，前提是事务的读访问集合能在事务开始时被动态过近似。
State-of-the-art model checkers employing dynamic partial order reduction (DPOR) can verify concurrent programs under a wide range of memory models such as sequential consistency (SC), total store order (TSO), release-acquire (RA), and the repaired C11 memory model (RC11) in an optimal and memory-efficient fashion. Unfortunately, these DPOR techniques cannot be applied in an optimal fashion to programs with mixed-sized accesses (MSA), where atomic instructions access different (sets of) bytes belonging to the same word. Such patterns naturally arise in real life code with C/C++ union types, and are even used in a concurrent setting. In this paper, we introduce Mixer , an optimal DPOR algorithm for MSA programs that allows (multi-byte) reads to be revisited by multiple writes together. We have implemented Mixer in the GenMC model checker, enabling (for the first time) the automatic verification of C/C++ code with mixed-size accesses. Our results also extend to the more general case of transactional programs provided that the set of read accesses performed by a transaction can be dynamically overapproximated at the beginning of the transaction.
@article{MarmanisKV25,
title = {Model Checking C/C++ with Mixed-Size Accesses},
author = {Iason Marmanis and Michalis Kokologiannakis and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704911}
}