主要观点：GenMC 是用于验证并发 C/C++程序在不同内存模型下的开源先进模型检查器。
关键信息：

• 基于无状态模型检查算法，在内存模型选择上具参数性，算法可靠、完备且最优，仅探索符合模型的执行路径。
• 包含多种优化，如锁感知和屏障感知的偏序减少、对称性减少、自动自旋循环边界等。
  重要细节：
• 源分布：在 Github 上（https://www.github.com/mpi-sw...）。
• 形式证明：在 Coq 中的 TruSt 形式化（https://github.com/volodeyka/...）。
• 工具论文：有多篇相关论文，涵盖不同方面，如弱一致性库的模型检查、有效的锁处理等，各篇论文详细介绍相关研究成果，且多数有对应的 Zenodo 上的工件（Artifact），如 https://doi.org/10.5281/zenod... 等，表明工件可用且经过评估和功能验证。
• 相关人员：有 Michalis Kokologiannakis、Iason Marmanis、Azalea Raad、Viktor Vafeiadis 等（https://people.mpi-sws.org/~m... 等）。
• 相关项目：有 RCMC 用于 RC11 模型检查，Repairing sequential consistency in C/C++11 定义 RC11 模型，PerSeVerE 用于在 Linux ext4 下的模型检查等。