GenMC 使用指南

GenMC (Generic Model Checking) 是一个用于 C 程序的无状态模型检查器，工作在 LLVM 中间表示（LLVM-IR）层面。它可以验证使用 C11 原子操作和 pthread 库的并发程序的安全性属性。

1. 简介

GenMC 是来自 MPI-SWS (Max Planck Institute for Software Systems) 的学术项目，采用 TruSt 算法进行动态偏序约简，能够高效检测并发程序中的各种问题。

主要功能

• 支持 SC、TSO、RA、RC11、IMM 等多种内存模型
• 检测竞态条件、内存错误
• 使用动态偏序约简技术
• 支持线性化检查
• 支持 Rust 代码分析

支持的内存模型

模型	说明	适用场景
SC	顺序一致性	理论分析基准
TSO	完全存储顺序	x86 架构
RA	释放-获取	简化验证
RC11	C11 松弛原子	默认模型
IMM	硬件内存模型	ARM/Power 架构

2. 安装与构建

2.1 依赖要求

• 编译器: C++20 兼容（推荐 g++ >= 14）
• LLVM 版本: 15.0.0 - 20.0.0
• 系统库:
  • cmake
  • clang
  • llvm
  • llvm-dev
  • libffi-dev
  • zlib1g-dev
  • libedit-dev

2.2 构建步骤

# 进入 GenMC 目录
cd /workspace/build/genmc

# 配置构建
cmake -DCMAKE_BUILD_TYPE=RelWithDebInfo -B RelWithDebInfo -S .

# 编译
cmake --build RelWithDebInfo

# 运行测试（可选）
cd RelWithDebInfo && ctest -R fast-driver

2.3 验证安装

# 检查版本
./RelWithDebInfo/genmc --version

# 查看帮助
./RelWithDebInfo/genmc --help

3. 基本使用

3.1 简单示例

创建文件 message_passing.c：

#include <stdlib.h>
#include <pthread.h>
#include <stdatomic.h>
#include <stdbool.h>
#include <assert.h>

atomic_int data;
atomic_bool ready;

void *thread_1(void *unused)
{
    atomic_store_explicit(&data, 42, memory_order_relaxed);
    atomic_store_explicit(&ready, true, memory_order_release);
    return NULL;
}

void *thread_2(void *unused)
{
    if (atomic_load_explicit(&ready, memory_order_acquire)) {
        int d = atomic_load_explicit(&data, memory_order_relaxed);
        assert(d == 42);
    }
    return NULL;
}

int main()
{
    pthread_t t1, t2;
    pthread_create(&t1, NULL, thread_1, NULL);
    pthread_create(&t2, NULL, thread_2, NULL);
    return 0;
}

运行验证：

./RelWithDebInfo/genmc message_passing.c

如果程序正确，GenMC 会显示：

GenMC: No errors found.

3.2 检测竞态条件

创建有竞态条件的程序 race.c：

#include <pthread.h>
#include <assert.h>

int counter = 0;

void *thread_func(void *arg)
{
    counter++;  // 非原子操作，存在竞态
    return NULL;
}

int main()
{
    pthread_t t1, t2;
    pthread_create(&t1, NULL, thread_func, NULL);
    pthread_create(&t2, NULL, thread_func, NULL);
    pthread_join(t1, NULL);
    pthread_join(t2, NULL);
    return 0;
}

运行验证：

./RelWithDebInfo/genmc race.c

输出示例：

GenMC: Found a bug!
GenMC: Thread '0' performs a data race with thread '1'.
GenMC: Location: counter
GenMC: Error trace: ...

4. GenMC 特殊 API

4.1 核心函数

// 假设语句 - 只有在条件为真时继续执行
void __VERIFIER_assume(int cond);

// 非确定性整数 - 为每个线程生成相同的伪随机序列
int __VERIFIER_nondet_int(void);

// 输出调试信息
void __VERIFIER_output(const char *msg);

使用示例：

int x = __VERIFIER_nondet_int();  // 非确定性值
__VERIFIER_assume(x >= 0);         // 约束 x 为非负

4.2 线程操作

// 线程类型
typedef unsigned long __VERIFIER_thread_t;

// 创建线程
__VERIFIER_thread_t __VERIFIER_spawn(void *(*func)(void *), void *arg);

// 创建对称线程（用于对称性约简）
__VERIFIER_thread_t __VERIFIER_spawn_symmetric(void *(*func)(void *), void *arg, __VERIFIER_thread_t th);

// 等待线程
void *__VERIFIER_join(__VERIFIER_thread_t th);

4.3 循环标记

// 标记循环开始
void __VERIFIER_loop_begin(void);

// 标记自旋循环开始
void __VERIFIER_spin_start(void);

// 标记自旋循环结束（cond 表示是否继续自旋）
void __VERIFIER_spin_end(bool cond);

使用示例：

void wait_for_flag(atomic_bool *flag) {
    __VERIFIER_spin_start();
    while (!atomic_load_explicit(flag, memory_order_acquire)) {
        // 自旋等待
    }
    __VERIFIER_spin_end(false);  // 条件为 false 表示自旋结束
}

4.4 写入标记

// 标记为局部写入（不会被其他线程观察）
#define __VERIFIER_local_write(s)

// 标记为最终写入（程序结束前的最后一次写入）
#define __VERIFIER_final_write(s)

4.5 CAS 帮助标记

用于无锁算法中的 CAS (Compare-And-Swap) 操作：

// 标记被帮助的 CAS
#define __VERIFIER_helped_CAS(c)

// 标记帮助 CAS
#define __VERIFIER_helping_CAS(c)

// 标记确认 CAS
#define __VERIFIER_confirming_CAS(c)

4.6 危险指针 API

// 分配危险指针槽
__VERIFIER_hp_t __VERIFIER_hp_alloc(void);

// 保护指针
void *__VERIFIER_hp_protect(__VERIFIER_hp_t hp, void *p);

// 清除保护
void __VERIFIER_hp_clear(__VERIFIER_hp_t hp);

// 释放危险指针槽
void __VERIFIER_hp_free(__VERIFIER_hp_t hp);

// 退役对象
void __VERIFIER_hp_retire(void *p);

5. 命令行选项

5.1 内存模型选择

-sc      # 顺序一致性模型
-tso     # TSO 内存模型（x86）
-ra      # RA 内存模型
-rc11    # RC11 内存模型（默认）
-imm     # IMM 内存模型

示例：

./genmc -tso program.c  # 使用 TSO 模型验证

5.2 验证选项

-nthreads=<N>           # 使用 N 个线程并发验证
-check-liveness         # 检查活性违规
-disable-race-detection # 禁用竞态检测
-disable-bam           # 禁用 BAM（Barrier-Aware Model-checking）
-disable-sr            # 禁用对称性约简
-unroll=<N>            # 循环最多执行 N 次
-bound=<N>             # 状态空间边界

示例：

./genmc -check-liveness -unroll=10 program.c

5.3 调试选项

-dump-error-graph=<file>   # 输出错误图到 DOT 文件
-print-error-trace         # 打印导致错误的源代码序列
-cache-instructions        # 缓存指令
-verbose                   # 详细输出

示例：

./genmc -dump-error-graph=error.dot -print-error-trace program.c

6. 实战案例

6.1 无锁队列（Treiber Stack）

创建 treiber_stack.c：

#include <stdatomic.h>
#include <stdlib.h>
#include <pthread.h>
#include <assert.h>

struct Node {
    int value;
    struct Node *next;
};

struct Stack {
    _Atomic(struct Node *) top;
};

void stack_init(struct Stack *s) {
    atomic_store_explicit(&s->top, NULL, memory_order_relaxed);
}

void stack_push(struct Stack *s, int value) {
    struct Node *node = malloc(sizeof(struct Node));
    node->value = value;
    node->next = atomic_load_explicit(&s->top, memory_order_relaxed);

    while (!atomic_compare_exchange_weak_explicit(
        &s->top, &node->next, node,
        memory_order_release,
        memory_order_relaxed)) {
        // CAS 失败，重试
    }
}

int stack_pop(struct Stack *s, int *value) {
    struct Node *old_top = atomic_load_explicit(&s->top, memory_order_acquire);
    while (old_top) {
        struct Node *new_top = old_top->next;
        if (atomic_compare_exchange_weak_explicit(
            &s->top, &old_top, new_top,
            memory_order_acquire,
            memory_order_acquire)) {
            *value = old_top->value;
            free(old_top);
            return 1;  // 成功
        }
    }
    return 0;  // 栈为空
}

atomic_int result;

void *pusher(void *arg) {
    struct Stack *s = (struct Stack *)arg;
    stack_push(s, 42);
    return NULL;
}

void *popper(void *arg) {
    struct Stack *s = (struct Stack *)arg;
    int value;
    if (stack_pop(s, &value)) {
        atomic_store(&result, value);
    }
    return NULL;
}

int main() {
    struct Stack stack;
    stack_init(&stack);
    atomic_init(&result, 0);

    pthread_t t1, t2;
    pthread_create(&t1, NULL, pusher, &stack);
    pthread_create(&t2, NULL, popper, &stack);
    pthread_join(t1, NULL);
    pthread_join(t2, NULL);

    assert(atomic_load(&result) == 42);
    return 0;
}

运行验证：

./RelWithDebInfo/genmc treiber_stack.c

6.2 互斥锁实现

创建 spinlock.c：

#include <stdatomic.h>
#include <pthread.h>
#include <assert.h>

typedef struct {
    atomic_flag flag;
} spinlock_t;

void spinlock_init(spinlock_t *lock) {
    atomic_flag_clear_explicit(&lock->flag, memory_order_relaxed);
}

void spinlock_lock(spinlock_t *lock) {
    while (atomic_flag_test_and_set_explicit(&lock->flag, memory_order_acquire)) {
        // 自旋等待
    }
}

void spinlock_unlock(spinlock_t *lock) {
    atomic_flag_clear_explicit(&lock->flag, memory_order_release);
}

int counter = 0;
spinlock_t lock;

void *thread_func(void *arg) {
    spinlock_lock(&lock);
    counter++;
    spinlock_unlock(&lock);
    return NULL;
}

int main() {
    spinlock_init(&lock);

    pthread_t t1, t2;
    pthread_create(&t1, NULL, thread_func, NULL);
    pthread_create(&t2, NULL, thread_func, NULL);
    pthread_join(t1, NULL);
    pthread_join(t2, NULL);

    assert(counter == 2);
    return 0;
}

7. 高级用法

7.1 活性检查

检查自旋循环是否可能永远不会终止：

./genmc -check-liveness spin_program.c

7.2 线性化检查

使用 Relinche 算法检查数据结构的线性化：

./genmc -check-linearization queue_program.c

7.3 状态空间约简

使用对称性约减少少状态空间：

./genmc -disable-sr=false program.c

7.4 循环展开限制

限制循环的最大迭代次数：

./genmc -unroll=5 program.c

8. 常见问题排查

8.1 编译错误

问题: 找不到 pthread.h 或 stdatomic.h

解决: 确保编译器支持 C11，并包含正确的头文件路径：

#include <pthread.h>
#include <stdatomic.h>

8.2 验证超时

问题: 程序验证时间过长

解决:

1. 使用状态空间边界：-bound=N
2. 限制循环展开：-unroll=N
3. 启用更多约简选项
4. 使用多线程验证：-nthreads=4

8.3 误报

问题: GenMC 报告错误，但程序实际正确

解决:

1. 检查内存模型是否正确（默认 RC11）
2. 使用 -unroll 增加循环展开次数
3. 检查是否需要使用 __VERIFIER_assume 约束非确定性值

8.4 遗漏错误

问题: GenMC 未报告已知的错误

解决:

1. 确保使用了正确的内存模型
2. 增加循环展开次数：-unroll=N
3. 检查是否禁用了某些检查选项

9. Rust 支持

GenMC 也支持 Rust 代码分析。使用 Rust 标准库：

// Cargo.toml
[dependencies]
genmc-std = { path = "/workspace/build/genmc/rust/genmc-std" }

// main.rs
use genmc_std::thread;

fn main() {
    let handle = thread::spawn(|| {
        // 线程代码
    });
    handle.join().unwrap();
}

验证：

cargo build
genmc target/debug/main

10. 测试框架

GenMC 提供了完整的测试框架：

10.1 运行测试

# 快速测试
cd /workspace/build/genmc
./scripts/fast-driver.sh

# 运行正确用例
./scripts/runcorrect.sh

# 运行错误用例
./scripts/runwrong.sh

10.2 测试分类

• correct: 验证通过的程序
• wrong: 应该检测到错误的程序
• cooking: 压力测试和基准测试

10.3 测试目录结构

tests/
├── correct/
│   ├── data-structures/    # 数据结构测试
│   ├── litmus/             # Litmus 测试
│   ├── liveness/           # 活性测试
│   └── relinche/           # 线性化测试
└── wrong/
    ├── racy/               # 竞态条件
    ├── memory/             # 内存错误
    └── safety/             # 安全违规

11. 最佳实践

11.1 编写可验证的代码

1. 使用 C11 原子操作而非非原子变量
2. 为循环添加适当的约束
3. 使用 __VERIFIER_assume 约束非确定性值
4. 标记自旋循环和局部写入

11.2 调试技巧

1. 使用 -print-error-trace 查看错误轨迹
2. 使用 -dump-error-graph 生成可视化图
3. 从简单的测试用例开始验证
4. 逐步增加程序复杂度

11.3 性能优化

1. 对称创建线程以利用对称性约简
2. 合理设置 -unroll 参数
3. 使用多线程验证
4. 对大型程序使用 -bound 限制状态空间

12. 资源与参考

12.1 官方资源

• GitHub: https://github.com/mc-imperial/genmc
• 论文: TruSt: Dynamic Partial Order Reduction for Relaxed Memory Models
• 文档: /workspace/build/genmc/doc/manual.md

12.2 学习资源

• 测试用例: /workspace/build/genmc/tests/
• 示例代码: /workspace/build/genmc/tests/correct/
• 开发文档: /workspace/build/genmc/doc/development.md

12.3 相关工具

• ThreadSanitizer (TSAN): 运行时数据竞争检测
• Helgrind: Valgrind 的线程检测工具
• CDSChecker: C/C++ 并发程序模型检查器

---

总结

GenMC 是一个强大的并发程序验证工具，特别适用于：

• 验证无锁数据结构
• 检测竞态条件
• 分析不同内存模型下的程序行为
• 教学和研究并发编程

遵循本文档的指南，您可以有效地使用 GenMC 来提高并发程序的正确性和可靠性。