hen*_*xin 4 concurrency correctness invariants tla+ tlaps
这是 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。该算法满足此属性，因为它保持归纳不变量。你知道那个不变量是什么吗？如果不是，那么你就没有完全理解为什么算法满足这个属性。
所以，
并发程序的归纳不变量是什么？
在TLA+语法中，该程序的归纳不变量是：
\n\n/\\ \\A i \\in 0..N-1 : (pc[i] \\in {"s2", "Done"} => x[i] = 1) \n/\\ (\\A i \\in 0..N-1 : pc[i] = "Done") => \\E i \\in 0..N-1 : y[i] = 1\n归纳不变量是满足以下两个\n条件的不变量：
\n\nInit => Inv\nInv /\\ Next => Inv\'\n在哪里：
\n\nInv是归纳不变量Init是描述初始状态的谓词Next是描述状态转换的谓词。请注意，归纳不变量仅与当前状态和下一个状态有关。它不引用执行历史记录，与系统过去的行为无关。
\n\n在并发系统原理和规范（通常称为TLA+ Hyperbook）的第 7.2.1 节中，Lamport 描述了为什么他更喜欢使用归纳不变量而不是行为证明（即那些引用执行历史记录的证明）。
\n\n\n\n\n行为证明可以变得更正式，但我不知道\xe2\x80\x99不知道任何实际的方法\n使它们完全正式\xe2\x80\x94也就是说，编写真实算法的可执行描述和正式的行为证明它们满足正确性属性。这就是为什么在超过 35 年的并发算法编写过程中，我发现行为推理对于更复杂的算法来说是不可靠的。我认为另一个原因是，对于足够复杂的算法，行为证明本质上比基于状态的证明更复杂。这导致人们为这些算法编写不太严格的行为证明\xe2\x80\x94，尤其是在没有完全正式的证明作为路标的情况下。
\n\n为了避免错误，我们必须根据状态来思考，\n 而不是执行...不过，行为推理提供了\n 思考算法的不同方式，并且思考总是有帮助的。\n 行为推理是仅当使用它代替基于状态的推理而不是补充它时才不好。
\n
我们有兴趣证明的属性是（以 TLA+ 语法）：
\n\n(\\A i \\in 0..N-1 : pc[i] = "Done") => \\E i \\in 0..N-1 : y[i] = 1\n在这里，我使用 PlusCal 约定，使用名为“pc”的变量（我将其视为“程序计数器”）来描述每个进程的控制状态。
\n\n该属性是一个不变量，但它不是归纳不变量，因为它不满足上述条件。
\n\n您可以通过编写如下所示的证明，使用归纳不变量来证明属性：
\n\n1. Init => Inv\n2. Inv /\\ Next => Inv\'\n3. Inv => DesiredProperty\n为了得出归纳不变量，我们需要为算法的每一步给出标签，我们称它们为“s1”、“s2”和“Done”，其中“Done”是\n的最终状态每个过程。
\n\ns1: x[self] := 1;\ns2: y[self] := x[(self-1) % N]\n考虑程序处于倒数第二个（倒数第二个）执行状态时的状态。\n
\n\n在最后的执行状态下，pc[i]="Done"对于 i 的所有值。在倒数第二个状态下，pc[i]="Done"对于除 1 之外的所有 i 值，我们将其称为\nj，其中pc[j]="s2"。
如果进程 i 处于“完成”状态，则 一定为真x[i]=1，因为该进程必须执行了语句“s1”。\n类似地，处于状态“s2”的进程 j 也必须执行\n语句“s1”，所以 一定是真的x[j]=1。
我们可以将其表示为一个不变量，它恰好是一个归纳\不变量。
\n\n\\A i \\in 0..N-1 : (pc[i] \\in {"s2", "Done"} => x[i] = 1)\n为了证明我们的不变量是归纳不变量，我们需要一个具有\nInit状态谓词和Next状态谓词的适当模型。
我们可以从描述PlusCal中的算法开始。这是一个非常简单的算法，所以我称之为“简单”。
\n\n--algorithm Simple\n\nvariables\n x = [i \\in 0..N-1 |->0];\n y = [i \\in 0..N-1 |->0];\n\nprocess Proc \\in 0..N-1 \nbegin\n s1: x[self] := 1;\n s2: y[self] := x[(self-1) % N]\nend process\n\nend algorithm\n我们可以将PlusCal模型转化为TLA+。这是我们将 PlusCal 转换为 TLA+ 时的样子（我省略了终止条件，因为我们这里不需要它）。
\n\n------------------------------- MODULE Simple -------------------------------\n\nEXTENDS Naturals\n\nCONSTANTS N\n\nVARIABLES x, y, pc\n\nvars == << x, y, pc >>\n\nProcSet == (0..N-1)\n\nInit == (* Global variables *)\n /\\ x = [i \\in 0..N-1 |->0]\n /\\ y = [i \\in 0..N-1 |->0]\n /\\ pc = [self \\in ProcSet |-> "s1"]\n\ns1(self) == /\\ pc[self] = "s1"\n /\\ x\' = [x EXCEPT ![self] = 1]\n /\\ pc\' = [pc EXCEPT ![self] = "s2"]\n /\\ y\' = y\n\ns2(self) == /\\ pc[self] = "s2"\n /\\ y\' = [y EXCEPT ![self] = x[(self-1) % N]]\n /\\ pc\' = [pc EXCEPT ![self] = "Done"]\n /\\ x\' = x\n\nProc(self) == s1(self) \\/ s2(self)\n\nNext == (\\E self \\in 0..N-1: Proc(self))\n \\/ (* Disjunct to prevent deadlock on termination *)\n ((\\A self \\in ProcSet: pc[self] = "Done") /\\ UNCHANGED vars)\n\nSpec == Init /\\ [][Next]_vars\n=============================================================================\n请注意它如何定义Init和 Next状态谓词。
我们现在可以指定我们想要证明的归纳不变量。我们还希望我们的归纳不变量能够暗示我们有兴趣证明的属性，因此我们将其添加为合取。
\n\nInv == /\\ \\A i \\in 0..N-1 : (pc[i] \\in {"s2", "Done"} => x[i] = 1)\n /\\ (\\A i \\in 0..N-1 : pc[i] = "Done") => \\E i \\in 0..N-1 : y[i] = 1\nInit => Inv为什么这是真的应该是显而易见的，因为Inv如果为真，则 中的前因都是假Init的。
Inv /\\ Next => Inv\'(\\A i \\in 0..N-1 : (pc[i] \\in {"s2", "Done"} => x[i] = 1))\'\n有趣的情况是对于某些 ipc[i]="s1"来说pc\'[i]="s2"。根据 的定义s1，应该清楚为什么这是真的。
((\\A i \\in 0..N-1 : pc[i] = "Done") => \\E i \\in 0..N-1 : y[i] = 1)\'\n有趣的情况是我们之前讨论的情况，其中pc[i]="Done"对于除 1 之外的所有 i 值，j，其中pc[j]="s2".
通过 Inv 的第一个合取，我们知道x[i]=1对于 i 的所有值。
经过s2，y\'[j]=1。
Inv => DesiredProperty在这里，我们想要的属性是
\n\n(\\A i \\in 0..N-1 : pc[i] = "Done") => \\E i \\in 0..N-1 : y[i] = 1\n请注意，我们刚刚将我们感兴趣的属性与变量进行了与运算，因此证明这一点很简单。
\n\n您可以使用TLA+ 证明系统(TLAPS) 编写\n正式证明，并可对其进行机械检查以确定其是否正确。
\n\n这是我使用 TLAPS 编写和验证的证明，该证明使用归纳不变量来证明所需的属性。（注意：这是我使用 TLAPS 编写的第一个证明，因此请记住这是由新手编写的）。
\n\nAtLeastOneYWhenDone == (\\A i \\in 0..N-1 : pc[i] = "Done") => \\E i \\in 0..N-1 : y[i] = 1\n\nTypeOK == /\\ x \\in [0..N-1 -> {0,1}]\n /\\ y \\in [0..N-1 -> {0,1}]\n /\\ pc \\in [ProcSet -> {"s1", "s2", "Done"}]\n\nInv == /\\ TypeOK\n /\\ \\A i \\in 0..N-1 : (pc[i] \\in {"s2", "Done"} => x[i] = 1)\n /\\ AtLeastOneYWhenDone\n\nASSUME NIsInNat == N \\in Nat \\ {0} \n\n\\* TLAPS doesn\'t know this property of modulus operator\nAXIOM ModInRange == \\A i \\in 0..N-1: (i-1) % N \\in 0..N-1\n\n\nTHEOREM Spec=>[]AtLeastOneYWhenDone\n<1> USE DEF ProcSet, Inv\n<1>1. Init => Inv\n BY NIsInNat DEF Init, Inv, TypeOK, AtLeastOneYWhenDone\n<1>2. Inv /\\ [Next]_vars => Inv\'\n <2> SUFFICES ASSUME Inv,\n [Next]_vars\n PROVE Inv\'\n OBVIOUS\n <2>1. CASE Next\n <3>1. CASE \\E self \\in 0..N-1: Proc(self)\n <4> SUFFICES ASSUME NEW self \\in 0..N-1,\n Proc(self)\n PROVE Inv\'\n BY <3>1 \n <4>1. CASE s1(self)\n BY <4>1, NIsInNat DEF s1, TypeOK, AtLeastOneYWhenDone\n <4>2. CASE s2(self)\n BY <4>2, NIsInNat, ModInRange DEF s2, TypeOK, AtLeastOneYWhenDone\n <4>3. QED\n BY <3>1, <4>1, <4>2 DEF Proc\n <3>2. CASE (\\A self \\in ProcSet: pc[self] = "Done") /\\ UNCHANGED vars\n BY <3>2 DEF TypeOK, vars, AtLeastOneYWhenDone\n <3>3. QED\n BY <2>1, <3>1, <3>2 DEF Next\n <2>2. CASE UNCHANGED vars\n BY <2>2 DEF TypeOK, vars, AtLeastOneYWhenDone\n <2>3. QED\n BY <2>1, <2>2\n<1>3. Inv => AtLeastOneYWhenDone\n OBVIOUS\n<1>4. QED\n BY <1>1, <1>2, <1>3, PTL DEF Spec \n请注意，在使用 TLAPS 的证明中，您需要有一个类型检查不变式（上面称为TypeOK），并且还需要处理没有变量发生变化的“口吃状态”，这就是我们[Next]_vars使用Next.
这是带有完整模型和证明的要点。
\n| 归档时间： |
|
| 查看次数： |
2300 次 |
| 最近记录： |