C++的forward progress guarantee:震惊,哥德巴赫猜想竟被程序找出反例(不是)

为了学习C++内存模型读了cpp reference page,发现了一个有意思的东西:forward progress guarantee。它是说,对于一个合法的C++程序,它的每个线程(或者说每个控制流)最终需要至少做下面四件事中的一个:

  • 终止
  • 调用IO库函数
  • 访问volatile变量
  • 做一个原子操作或者使用其他的同步操作

从直观上来说,它的意思是说一个控制流不能永远运行下去,而不对“外部”产生任何影响。因为一个永远不终止也不产生任何可观测效应的控制流并没有什么用,所以禁止这样的代码来给编译器优化更强的assumption。

这里的和“外部”交互包括和程序的外部环境交互,或者是和其他线程交互,总之就是任何让这个线程“有用”的事情。对volatile变量的访问被视为是有副作用的,因此这算是产生了影响。而线程间同步操作则会影响其他线程的执行,所以也算是产生了影响。至于原子操作为什么是同步操作,之后写内存模型的博客时会介绍。

“最终”(原文是eventually)这个词的语义其实有点模糊,比如说我先随便做点IO,然后进入一个啥也不干的死循环,这违反这条规则吗?cpp reference上还具体解释了一下:一个没有可观测效应的死循环(或者无限递归,形式不重要,反正就是永不结束的控制流)是ub。这似乎意味着“最终”这个词的意思是说,在控制流正在运行的任何一个时间点向之后看,之后至少要发生这四件事中的一个。但这只是我个人的理解,如果有误请指出。

这给了编译器优化很强的assumption:如果一个循环里没有产生任何可观测效应,就可以假定这个循环不是死循环。进一步,如果这个循环对之后的执行也不产生影响(之后的语句不依赖这个循环里算出来的东西),那么这个循环可以被直接去掉。这带来了一些很有趣的编译优化结果。

首先当然是直接写一个死循环程序

1
2
3
int main() {
while (true) ;
}

godbolt试了下clang 14.0.0 -O2,发现它直接生成了一个空的main函数,连ret都没有。在本地运行它会直接结束。至于连ret都没有为啥能正常结束我就不懂了,可能跟linker安排的内存布局,或者libc的实现有关。我猜测这里的优化思路是,编译器发现这真的是个无副作用的死循环,是ub,而进入main函数就会进入这个循环,所以它认为main函数是不可达的,直接不给它生成代码了。

然后来整点花活,写个程序在unsigned int范围内找哥德巴赫猜想的反例,如果找到就退出,输出消息,找不到就会一直在循环里找。当然这时候编译器看不出来它是死循环了,所以假定它不是死循环,就移除了循环,直接输出消息告诉我们哥德巴赫猜想错了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
#include <cstdio>

using uint = unsigned int;
bool isprime(uint n) {
if (n < 2) {
return false;
}
for (uint i = 2; i * i <= n; ++i) {
if (n % i == 0) {
return false;
}
}
return true;
}

int main() {
for (uint i = 0; ; ++i) {
if (i >= 4 && i % 2 == 0) {
bool found = false;
for (uint j = 2; j < i; ++j) {
if (isprime(j) && isprime(i - j)) {
found = true;
break;
}
}
if (!found) {
break;
}
}
}
puts("Goldbach is wrong!");
}

在godbolt上看clang 14生成的代码,发现它果然移除了循环,main函数里只做了调用puts一件事。因为我对risc-v比较熟,就放risc-v汇编了。

1
2
3
4
5
6
7
8
9
10
11
12
main:                                   # @main
addi sp, sp, -16
sw ra, 12(sp) # 4-byte Folded Spill
lui a0, %hi(.L.str)
addi a0, a0, %lo(.L.str)
call puts
li a0, 0
lw ra, 12(sp) # 4-byte Folded Reload
addi sp, sp, 16
ret
.L.str:
.asciz "Goldbach is wrong!"

这样的激进优化我只在clang上观察到了(版本是14.0.0和14.0.1),gcc 9.3.0老实地生成了循环。此外,在C的对应页面上并没有看到相似的假定,也就是说无副作用的死循环在C中并非ub(很有趣,这样的代码是合法的C程序,却不是合法的C++程序)。如果把上面两个代码改写为C代码,那么即便用clang 14编译,也会得到正常的死循环,印证了这一点。这也算是让C实际上并非C++子集的又一个小区别。