使用CPAchecker验证多线程死锁（哲学家就餐问题）的方法求助

我最近在尝试用CPAchecker来验证死锁问题，目标是搞定经典的“哲学家就餐问题”。不过在处理多线程相关的验证时踩了不少坑，有没有大佬能教教我怎么用CPAchecker检测死锁呀？

我还写了一段测试代码，想搞清楚CPAchecker是怎么处理锁的，但完全摸不着头绪，不知道该怎么用它来做锁的验证工作。

#include <pthread.h>
#include <stdio.h>

extern void __assert_fail(const char * assertion, const char * file, unsigned int line, const char * function) __attribute__ ((__noreturn__));
#define assert(expr) \
    ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))

pthread_mutex_t forks[5];

void *philosopher(void *arg) {
    int id = *(int *)arg;
    // 先拿左边的叉子
    pthread_mutex_lock(&forks[id]);
    // 再拿右边的叉子
    pthread_mutex_lock(&forks[(id + 1) % 5]);
    
    printf("Philosopher %d is eating\n", id);
    // 模拟就餐时间
    for (int i = 0; i < 1000000; i++);
    
    pthread_mutex_unlock(&forks[(id + 1) % 5]);
    pthread_mutex_unlock(&forks[id]);
    
    printf("Philosopher %d finished eating\n", id);
    return NULL;
}

int main() {
    pthread_t threads[5];
    int ids[5] = {0, 1, 2, 3, 4};
    
    for (int i = 0; i < 5; i++) {
        pthread_mutex_init(&forks[i], NULL);
    }
    
    for (int i = 0; i < 5; i++) {
        pthread_create(&threads[i], NULL, philosopher, &ids[i]);
    }
    
    for (int i = 0; i < 5; i++) {
        pthread_join(threads[i], NULL);
    }
    
    for (int i = 0; i < 5; i++) {
        pthread_mutex_destroy(&forks[i]);
    }
    
    return 0;
}

给你一些实操建议： #

• 先搞定配置：CPAchecker验证死锁需要启用对应的分析属性，你可以直接用它自带的死锁配置文件，不用自己从头写配置。
• 运行命令示例：切换到CPAchecker的安装目录，执行下面的命令：

  ./scripts/cpa.sh -config config/properties/deadlock.properties 你的代码文件路径.c
  

• 解读结果：如果代码里有死锁（比如你这段先左后右拿叉子的逻辑，本来就容易触发死锁），CPAchecker会在输出里明确告诉你死锁涉及的线程、锁，还有对应的调用栈信息；要是没检测到死锁，会提示验证通过。
• 遇到问题的小技巧：如果运行时出现超时或者内存不足，可以加-heap 4096M参数给程序分配更多内存，或者用-timelimit 3600s设置更长的超时时间（比如1小时）。

其实CPAchecker处理锁的逻辑是追踪每个线程的锁持有状态，分析线程之间的锁依赖关系，只要满足死锁的四个必要条件（互斥、持有并等待、不可剥夺、循环等待），它就能准确检测出来。你可以先拿这段代码试试上面的方法，应该能看到预期的死锁检测结果。

备注：内容来源于stack exchange，提问作者Robbb