这是 Leslie Lamport 的《教学并发》一文中的一个简单并发程序。
考虑N编号从 0 到N-1每个进程i执行的进程
x[i] := 1
y[i] := x[(i - 1) % N]
并停止，其中每个x[i]初始值都等于 0。（假设每个的读取和写入x[i]都是原子的。）
该算法满足以下性质：每个进程停止后，y[i]至少有一个进程等于1 i。很容易验证：最后i写入的进程y[i]必须将其设置为1。
然后，兰波特评论说
但该进程并未设置
y[i]为 1，因为它是最后一个写入的进程y。该算法满足此属性，因为它保持归纳不变量。你知道那个不变量是什么吗？如果不是，那么你就没有完全理解为什么算法满足这个属性。
所以，
并发程序的归纳不变量是什么？