作者:JohnRegehr, Professor of Computer Science, University of Utah, USA
原文位址:http://blog.regehr.org/archives/140
【更新:本文沒有非常清楚地解釋底下的問題。我寫了一篇更好的新博】。
顯然,我不是認真的:編譯器不擅長解決高層次的數學問題,并且有很好的理由相信這個定理不能被反證。
不過我的話說得有點過了。最近——出于在這裡無關緊要的原因——我想寫一個無限循環的C代碼,但編譯器不了解這個循環是無限的。相反,如果我隻是寫
while (1) { }
或
for (;;) { }
大多數優化編譯器将看到這個循環不能退出,并生成相應的代碼。例如,給定這個C代碼:
void foo (void)
{
for (;;) { }
open_pod_bay_doors();
}
大多數編譯器将釋出像這樣的代碼:
foo:
L2: jmp L2
在這個情形裡,編譯器不會釋出對open_pod_bay_doors()的調用,也不會釋出最後的傳回指令,因為可證明兩者都不會得到執行。
也許很有趣,LLVM/Clang認識到這個稍模糊的無限循環永不退出:
unsigned int i = 0;
do {
i+=2;
} while (0==(i&1));
面對有點頭腦的一個循環優化器,我決定不再浪費時間,編寫一個能阻撓所有編譯器的終止分析的循環:
const int MAX = 1000;
int a=1,b=1,c=1;
while ((c*c*c) != ((a*a*a)+(b*b*b))) {
a++;
if (a>MAX) {
a=1;
b++;
}
if (b>MAX) {
b=1;
c++;
}
if (c>MAX) {
c=1;
}
}
這個循環僅當找到Fermat大定理一個特殊情形的一個反例。當然,Fermat大定理聲明對方程an+bn= cn,對正整數a,b與c,以及整數n>2,不存在解。這裡n=3且a,b,c在範圍[1..1000]。在一個使用32位整數的平台上,1000是一個合理的最大值,因為2*10003與231沒有太大差别。
結果是,當啟用優化時,幾個編譯器(LLVM/Clang 2.7,Open64-x864.2.3,SunCC 5.10與IntelCC 11.1.072)亟不可待地允許這個循環終止。特别地,當這個循環被包含在一個函數裡時,編譯器釋出看起來像這樣的x86彙編代碼:
fermat:
ret
當然,這意味着編譯器已經反證了Fermat大定理。面對這個令人難以置信的數學發現,我屏住呼吸,在該函數末尾添加了一行代碼來列印個反例:a,b,與c的值。不幸的是,它們的虛張聲勢以這個方式調用,所有的編譯器釋出實際執行所要求計算的代碼,它當然不會終止。我感覺這些工具——像Fermat本身——在空白處沒有足夠的空間來解釋它們的推理。
這裡真正發生的是編譯器優化以及終止分析長期不相稱。換而言之,如果編譯器對保留所翻譯代碼的終止屬性有責任,它們應該不能執行(或執行難度增加)某些它們用來建立高效代碼的優化。編譯器開發者做出的一個選擇——可能有意識的,雖然很難确定——速度優先于正确性。不過,都不是壞消息:WindRiver Diab C編譯器,以及GCC的幾個版本都做對了,沒有改變我嘗試例子的終止屬性。
5/1周六的更新:看來LLVM開發人員不久前一直着手這個問題,他們最新的SVN沒有包含這個錯誤。非常好!
5/1周六的更新:Reddit上的某人注意到(我的一個學生證明)Microsoft編譯器确實有終止錯誤。VisualStudio 2008與2010中的編譯器為Fermat函數生成代碼,但然後對這個函數的調用被丢棄了,因為它被認為沒有副作用(這也是LLVM在修複這個問題之前的行為)。
4/30周五的更新
我在這裡嘗試澄清在Reddit上及評論中出現的幾個問題。同樣我修正了Reddit上某人指出的,在Fermat大定理陳述中的一個錯誤。謝謝!
問:這真的重要嗎?
答:是的,但僅在開發嵌入式軟體時出現的非常特殊的情形裡。這裡描述了一個例子:發帖者希望main()退出時程式被模拟挂起。權宜之計是關閉優化編譯代碼。在一個嵌入式系統更新了固件,并等待看門狗時鐘将處理器重新開機到新版本時,出現另一個例子。Gcc與WindRiver C編譯器——兩者都被大量用于嵌入式領域——得到正确的結束不是巧合。
問:因為無限循環是不好的形式,編譯器終止它們不行嗎?人們不應該讓CPU睡眠,阻塞正在運作的線程嗎,還是怎麼着?
答:首先,不是所有的程式都有一個起作用的作業系統或甚至線程系統。嵌入式軟體通常運作在裸硬體上。其次,一個程式的含義由語言标準定義,形式與此無關。參考我之前的博文The compiler doesn’t care about yourintent。
問:C标準允許還是禁止編譯器終止無限循環?
答:在如何實作C程式上,編譯器被給予了相當大的自由,但其輸出的外部可見行為必須與程式在由标準描述的“C抽象機器”解釋的時相同。許多學識淵博的人(包括我)把這視為必須不能該程式的終止行為。顯然某些編譯器作者不同意,或者不相信它很重要。理性的人不同意這個解釋的事實,看起來意味着C标準是有缺陷的。相比之下,Java語言定義相當清晰,無限循環不會被JVM終止。
問:你是說編譯器應該進行終止分析嗎?稍加簡化為停機問題,那是不可能的。
答:終止分析完全不需要成為編譯器的一部分。不過,我(及其他人)聲明編譯器在删除任何無用的循環之前,應該執行一個終止分析。雖然一般問題是不可計算的,但許多特定的執行個體是很容易解決的。
問:在本博中的Fermat代碼會執行有符号整數溢出或其他未定義行為嗎?
答:我不認為。
5/1周六的更新
問:你不知道費馬大定理在1995年被證明了嗎?
答:我确實知道。因為我在1995年獲得了我的數學學位,對我來說錯過這件事幾乎不可能J。我開了個小玩笑,也是指出事實,證明,特别是複雜證明,會包含錯誤。實際上,正如有人會在注釋裡注意到,Wiles一開始的證明是錯的。也注意到n=3的特例早就在1770年被證明了。
問:如果真的希望一個C裡的無限循環,最好變通是什麼?
答:正如幾個人指出的,在一個volatile限定的變量上循環可能是最好的選擇。但記住,編譯器不總是遵守volatile……
5/1周六的另一個更新
這是一個有趣的完整程式,它比上面的代碼更令人信服,因為它顯式使用來自代碼“反證定理”分支的傳回值:
int fermat (void)
{
const int MAX = 1000;
int a=1,b=1,c=1;
while (1) {
if (((a*a*a) ==((b*b*b)+(c*c*c)))) return 1;
a++;
if (a>MAX) {
a=1;
b++;
}
if (b>MAX) {
b=1;
c++;
}
if (c>MAX) {
c=1;
}
}
return 0;
}
#include <stdio.h>
int main (void)
{
if (fermat()) {
printf ("Fermat'sLast Theorem has been disproved.\n");
} else {
printf("Fermat's Last Theorem has not been disproved.\n");
}
return 0;
}
這是Inte與Sun編譯器的輸出:
[email protected]:~$icc fermat2.c -o fermat2
[email protected]:~$./fermat2
Fermat's Last Theoremhas been disproved.
[email protected]:~$suncc -O fermat2.c -o fermat2
"fermat2.c",line 20: warning: statement not reached
[email protected]:~$./fermat2
Fermat's Last Theoremhas been disproved.
Open64-x86與LLVM/Clang 2.7具有相同的行為。雖然許多無關緊要的人不同意,看起來對我非常清楚:這是這些編譯器中一個嚴重的錯誤。我的意思是,為什麼傳回1?傳回0是更好還是更壞?沒有一個結果是合理的。