采用反证法证明含原子操作的C++多线程程序行为是否正确？

数据老陈

2026-6-2

关于C++原子操作程序行为的证明正确性疑问

示例代码

#include <thread>
#include <atomic>

int main(){
  std::atomic<int> val = 0;
  std::atomic<bool> flag = false;
  std::jthread t1([&](){
     if(val.load(std::memory_order::relaxed) == 1){ // #1
       flag.store(true, std::memory_order::release); // #2
     }
  });
  std::jthread t2([&](){
    while(!flag.load(std::memory_order::acquire)); // #3
    val.store(1,std::memory_order::relaxed); // #4
  });
}

反证法证明过程

我尝试通过反证法证明该程序的行为：

首先，假设反事实情况：#3处的循环退出。

基于该假设前提，推导如下逻辑语句：

#3处循环退出 ⟾ #3读取自#2
[stmt.while] p1：while语句中，子语句会重复执行，直到条件([stmt.pre])的值变为false。
#3读取自#2 ⟾ #2在程序生命周期内已执行
[intro.races] p10：原子对象M的取值（由求值B确定）是由某个修改M的未指定副作用A存储的值，且B不先于A发生。
#2在程序生命周期内已执行 ⟾ #1处if语句的条件为true
[stmt.if] p1：若条件([stmt.pre])为true，则执行第一个子语句；若存在else部分且条件为false，则执行第二个子语句。
#1处if语句的条件为true ⟾ #1读取自#4

应用假言三段论，可得出结论：