看这个例子：

#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 退出。
因此，基于这个假设前提，第一条逻辑陈述是：

1. #3 处的循环结束 ⟾ #3 从 #2 读取

[stmt.while] p1: 在while语句中，子语句会被重复执行，直到条件的值（[stmt.pre]）变为false。

1. #3 从 #2 读取 ⟾ #2 在程序的整个生命周期中某处被执行

[intro.races] p10: 由评估B 决定的原子对象M 的值，是被某个未指明的、修改M 的副作用A 存储的值，其中B 并非在A 之前发生。

1. #2 在程序的整个生命周期中的某处被执行 ⟾ 位于 #1 的 if 的条件为真

[stmt.if] p1: 如果条件 ([stmt.pre]) 为真，则执行第一条子语句。若选择语句存在else部分且条件为假，则执行第二条子语句。

1. 位于 #1 的 if 的条件为真 ⟾ #1 从 #4 读取

应用 hypothetical syllogism，我们可以得到结论：

1. #3 处的循环结束 ⟾ #1 从 #4 读取

此外，#3 从 #2 读取意味着 #2 发生在 #3 之前，这意味着 #1 发生在 #4 之前，进而意味着 #1 不从 #4 读取。所以，我们可以推断出

1. #3 从 #2 读取 ⟾ ¬(#1 从 #4 读取)

再次，将第一条推理和第六条推理应用于假设三段论，结果是：

1. #3 处的循环结束 ⟾ ¬(#1 从 #4 读取)

把 5 与 7 的推论联系起来，我们得到一个矛盾：

#3 处的循环结束 ⟾ ¬(#1 从 #4 读取) ∧ (#1 从 #4 读取)

也就是说

#3 处的循环结束 ⟾ False

注：符号 ⟾ 表示逻辑蕴含

因此，矛盾意味着假设前提是错误的。该程序中的循环在 #3 处不能退出。

这是一种正确的形式化证明方法吗？

解决方案

是的，这是一个正确的证明（在若干隐含前提，如“flag 为 true 意味着#2会被执行，因为没有其他表达式能让它获得该值”），而且这也是对多线程C/C++程序正确性的正确证明类型。

尽管它是以实现符合性的术语来表述，[intro.races]/16通过谈论“原子加载与它们观察到的修改之间的关联”和“精心选择的修改顺序”来指向这个模型。作为程序员，你的目标是证明在标准允许范围内的任意关联和顺序都会产生期望的结果；等价地说，你要证明任何其他结果都会意味着对这些规则的违反。