TLA用法

发表于 |

介绍TLA+用法。
TLA全称为Temporal Logic of Actions，相比传统数学，更着重研究时序逻辑。
TLC是TLA+的模型检验工具。

模型

Module，是写TLA+ Specification的地方。
Model，是用TLC检验TLA+ Module的地方。

Model Value

在”What is the model?”中。

模型(Model)行为

在”What is the behavior spec?”中。

  1. Ordinary assignment
    例如

    1
    RM <- {"r1", "r2", "r3"}

  2. Model value

  3. Set of model values
    需要输入一组 model-value 名。

    1
    RM <- {r1, r2, r3}

    注意，model value 是有类型的，例如如果输入的是 {2, a, b}，并且选择 type 为 t，则生成的 model value 为 {t_2, t_a, t_b}。

检查项目

在”What to Check”中：

  1. Invariants
    例如各种Spec
  2. Properties
    例如Termination

Deadlock

Deadlock 指的是在一个 state 中，对应的 next-state 关系指明没有后续的 state 了。
Termination 是一个 deadlock，但不被认为是错误。如果我们的 spec 中是允许 Termination 的，那么就需要关掉 deadlock option。
注意如果是使用 PlusCal 算法翻译的 TLA，则不需要这么做，因为它的 next-state 关系的写法不会把 Termination 看成 deadlock。

如何将 Termination 和 deadlock 区分

learntla 中列出了一种方式。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
VARIABLES counter, pc

vars == << counter, pc >>

ProcSet == (Threads)

Init == (* Global variables *)
        /\ counter = 0
        /\ pc = [self \in ProcSet |-> "IncCounter"]

IncCounter(self) == /\ pc[self] = "IncCounter"
                    /\ counter' = counter + 1
                    /\ pc' = [pc EXCEPT ![self] = "Done"]

thread(self) == IncCounter(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in Threads: thread(self))
           \/ Terminating

Spec == Init /\ [][Next]_vars

我理解大概就是实现如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Terminating == /\ done = TRUE
               /\ UNCHANGED vars
               /\ UNCHANGED done

doneChecker ==
    /\ done = FALSE
    /\ 一些判定条件
    /\ done' = TRUE
    /\ UNCHANGED vars

Next == 
    \/ 一些 step
    \/ doneChecker
    \/ Terminating

TLC Option

如何调试

创建一个Spec，写入我们要计算的函数。
新建一个Module，设置”What is the behavior spec?”为”No Behavior Spec”。
在”Evaluate Constant Expression”中，对我们要计算的函数带入具体值。

从命令行执行

1
java tlc2.TLC -config .\TESpecSafetyTest.cfg -workers 4 -dfid 10 .\TESpecTest.tla

语法

逻辑部分

  1. \/
    表示or。
  2. /\
    表示and。
  3. \A x \in S: P(x)
    对于任意的S中的x，满足P(x)。
  4. \E x \in S: P(x)
    S中存在某个x，满足P(x)。
    注意，一般会用\E来表示选择任意一个元素进行操作的语义。如下所示，我们在AtoB中移除任意一个位置的元素。因此我们进一步能看到，TLA并不是命令式的，而是描述式的。 
    1
    \E i \in 1..Len(AtoB): AtoB' = Remove(i, AtoB)

函数/映射部分

这一部分可以查看Specify System中的第300页开始。
函数通常用中括号括起来。

  1. F == [x \in S |-> e]
    对S中的元素应用e，类似于mapper。
    函数的执行结果是一个tuple，例如下面函数的结果是<<2, 3>>

    1
    [i \in 1..2 |-> i+1]

  2. F[x \in S] == e

  3. [S -> T]
    表示了从S到T的一系列函数。
    例如，对于People中的p和Animals中的a，p对a可能like或者hate，我们可以写成下面的形式

    1
    2
    3
    Pref == [People -> [Animals -> {"like", "hate"}]]
    Pref == [[person: People, animal: Animals] -> {"like", "hate"}]
    Pref == [People \X Animals -> {"like", "hate"}]

    需要区别|->和->，前者表示是从DOMAIN到某个特定的RANGE的一个函数，后者表示从DOMAIN到RANGE的一系列函数。

  4. [S EXCEPT ![x] = v]
    这个语句通常用来表示返回整个集合，但是对集合中的某个特定元素的值进行变化。
    如果S是一个集合，表示返回S，除了x等于v。
    如果S是一个Record（类似于C里面的struct），表示返回S，除了x等于v。例如

    1
    [f EXCEPT !.prof = "RED"]

  5. @@和:>
    这两个符号用来定义函数。例如函数定义域是{1,2}，我们可以这么定义f

    1
    1 :> "ab" @@ 2 :> "cd"

  6. @
    f' = [f EXCEPT ![e1] = f[e1] + 1中，我们就可以写成f' = [f EXCEPT ![e1] = @ + 1]

  7. 直接在集合间映射
    例如

    1
    2
    CONSTANTS People, Animals
    Pref == [person: People]

    打印出来是

    1
    {[person |-> calvin], [person |-> neo]}

    又例如

    1
    Pref == [People -> People]

    打印出来是

    1
    2
    3
    4
    { (calvin :> calvin @@ neo :> calvin),
     (calvin :> calvin @@ neo :> neo),
     (calvin :> neo @@ neo :> calvin),
     (calvin :> neo @@ neo :> neo) }

    又例如

    1
    Pref == [message: {"Hello"}, src:People, dst:People]

    打印出来是

    1
    2
    3
    4
    { [src |-> calvin, dst |-> calvin, message |-> "Hello"],
     [src |-> calvin, dst |-> neo, message |-> "Hello"],
     [src |-> neo, dst |-> calvin, message |-> "Hello"],
     [src |-> neo, dst |-> neo, message |-> "Hello"] }

集合/元组/Record部分

这一部分可以查看Specify System中的第300页开始。
此外，在第339页开始会介绍标准模块，如Sequences、Bags等。

  1. Record
    Record类似于C++里面的struct。
    如何表示一个Record的实例？

    1
    [type |-> "Prepared", rm |-> r]

  2. <<"a", 42, {1,2}>>
    表示一个tuple，在P09a中也被Lamport称为Finite sequence。
    tuple从1编号。

  3. {1,2,3}
    表示一个Set。

  4. Tuple简单运算符
    Head和Tail类似于car和cdr。
    \o表示concat。如果seq /= <<>>，有seq = <<Head(seq)>> \o Tail(seq)。
    Append(tuple,elem)表示将elem放到tuple的末尾。
    Len，返回长度。
    Remove(i, seq)表示从seq移除i位置的元素之后的新seq。
    \X表示计算笛卡尔积。
    Seq表示所有由这个tuple中元素构成的序列。例如Seq({2})是{<<>>,<<3>>, <<3,3>>, <<3,3,3>>, ...}。我们可以进行下面的实验

    1
    2
    <<0,0,1>> \in Seq({0,1})
    <<2>> \in Seq({0,1})

  5. Set运算符
    SUBSET(S)求出所有子集，例如SUBSET( {1,2,3} )返回

    1
    { { }, {1}, {2}, {3}, {1, 2}, {1, 3}, {2, 3}, {1, 2, 3} }

    Cardinality(S)计算一个集合的大小。
    IsFiniteSet(S)计算一个集合是不是有限集。

  6. UNION
    合并多个集合
    S(n) == UNION {[0..m -> 0..m] : m \in 0..n}，则S(1)为

    1
    2
    3
    4
    5
    { (0 :> 0),
     (0 :> 0 @@ 1 :> 0),
     (0 :> 0 @@ 1 :> 1),
     (0 :> 1 @@ 1 :> 0),
     (0 :> 1 @@ 1 :> 1) }

    这是因为中括号里面是一个集合，然后m取不同的值又是一个集合。

  7. DOMAIN <<"a", "b", "c">>
    表示一个集合。Lamport说Math中的DOMAIN，对应于Progamming中的Index Set。

  8. <<"a", "b", "c">>[2]
    表示集合中的第2个元素，即"b"。

  9. “构造函数”{e: v \in S}
    对 S 中的元素应用 e，其中 e 是个表达式，类似于 mapper。
    需要区别|->和:：

    1
    2
    3
    EXTENDS Integers, Sequences
    Rem(i, seq) == [j \in 1..Len(seq)-1 |-> IF j<i THEN seq[j] ELSE seq[j+1]]
    RemSet(i, seq) == {(IF j<i THEN seq[j] ELSE seq[j+1]) : j \in 1..Len(seq)-1}

  10. “构造函数”{v \in S: P}
    类似一个filter。
    注意这里不能有 \A

    1
    2
    3
    4
    {\A key2 \in {1, 2}: key2 + 10000 # 10001}
    \* 结果为 {FALSE}
    {key2 \in {1, 2}: key2 + 10000 # 10001}
    \* 结果为 {2}

  11. UNCHANGED <<x,y>>
    是一个语法糖，可以理解为

    1
    2
    /\ x' = x
    /\ y' = y

  12. CHOOSE v \in S: P
    在S中满足P的元素中任选一个v。注意这个CHOOSE是没有随机性的，我们比较

    1
    2
    \E i \in 1..99 : x' = i
    x' = CHOOSE i \in 1..99 : TRUE

    上面的式子允许x'下一个状态的值是1..99之间任意一个数。
    下面的式子允许x'下一个状态的值是1..99之间某个特定的数。
    CHOOSE主要用法是：S中只有一个v满足P，比如最大值最小值等，我们将这个v取出来。所以一般CHOOSE和TRUE这个Predicate不会连用。
    下面通过CHOOSE计算在一段区间中的最大质数。可以在模型中执行LargestPrime(1..1000)，得到结果997。

    1
    2
    3
    4
    5
    6
    EXTENDS Integers, Sequences
    IsPrime(x) == x > 1 /\ ~\E d \in 2..(x-1) : x % d = 0
    LargestPrime(S) == CHOOSE x \in S:
                        /\ IsPrime(x)
                        /\ \A y \in S:
                            IsPrime(y) => y <= x

    这里用来表示最大的语句中用了 =>，可以学习下这种写法。

Expression/Spec部分

  1. IF-THEN-ELSE

  2. Enabling condition
    这是一个概念，例如下面式子中，第一个式子就是enabling condition，因为它并没有涉及下一个状态rmState'

    1
    2
    DecideC(r) == /\ rmState[r] = "prepared"
                  /\ rmState' = [rmState EXCEPT ![r] = "committed"]

    如果在state s时满足了这些Enabling条件，则A被enabled，且s->t是一个A step。

  3. Constant expression

  4. State expression
    能够包含所有Constant expression能够包含的元素。此外，还能包含声明了的变量。
    需要注意的还是，在P08b里面，Lamport说一个State表示给variable进行赋值。这里的variable表示所有可能的variable，而不是被定义出来的variable。我觉得实际在说在一个formula里面，如果没有提到其他变量，并不代表不存在其他变量。
    State的值取决于变量的值。

  5. Action expression
    能够包含所有State expression能够包含的元素。此外，还能包含'和UNCHANGED。
    一个State expression是一个Action expression，它在一个steps->t上具有一个值，这个值只取决于s。
    这里step表示一对状态之间的切换。例如，state s是p <- 42，state t是q <- 24，那么p-q'在steps->t上具有值42-24。

  6. THEOREM
    对于一个Temporal formula，THEOREM TF表示TF在每个可能行为下，都是true。
    例如下面的THEOREM表示对于每一个behavior，如果TPSpec是true（也就是这个behavior满足TPSpec的条件），那么[]TPTypeOK也是true（也就是对于这个bahavior下的每个state都是true）。

    1
    THEOREM TPSpec => []TPTypeOK

    进一步理解为，TPTypeOK是关于TpSpec的不变量。
    还可以说TPSpec实现(implement)了[]TPTypeOK。
    为了检查这个THEOREM，有两种方案：

    1. 将[]TPTypeOK/TPSpec加入”What to check?“下面的Properties中。
    2. 将TPTypeOK加入”What to check?“下面的Invariants中。

  7. Behavior

  8. Temporal(时序的) formula
    一般写成Spec == Init /\ []Next。
    在学习TCommit的时候，我们都是在Module标签页里面”Initial predicate and next-state relation”这个标签里面指定Init和Next的，现在可以直接在Temporal formula标签里面直接填我们的Spec了。

  9. Stuttering steps
    在Temporal formula中，会见到下面的写法，在TCNext周围包围了中括号：

    1
    [][TCNext]_rmState

    它等价于下面的形式，也就是说满足TCNext，或者保持rmState不变。后者称为stuttering steps。

    1
    TCNext \/ (UNCHANGED rmState)

    因此，一个常见的Temporal formula写法可以是

    1
    Spec == Init /\ [][Next]_<<...>>

  10. Stuttering steps和Termination
    一个有无限长的Stuttering steps作为结尾的behavior是一个Terminating execution。
    这个是容易理解的，在我们的系统停止之后，地球还是照转不误的。所以所有的behavior都是无限长的state构成的序列。

  11. May和Must
    我觉得这是一个贯穿的思想，也就是Lamport反复强调TLA+是一个数学的，而不是命令的东西。
    Spec中的主体部分都是May部分，规定了系统可能做什么，而不是必须做什么。可以加入L，作为Must部分

    1
    Spec == Init /\ [][Next]_<<...>> /\ L

    一个Safety Formula断言May发生的事件。
    一个Liveness Formula断言Must发生的事件。这表示在任何时候都不能违反的条件。

  12. []和~>
    对于顺序执行的程序来说，只需要满足能够最终终止就行了。这里最终表示为<>。关于<>，有下面的关系

    1
    <>P == ~[]~P

    ~>表示lead to。对于ABSpec来说，它的Liveness property是

    1
    (AVar = <<"hi",0>>) ~> (BVar = <<"hi",0>>)

  13. Fairness
    Weak Fairness指，如果Action A持续(continuouesly) enabled（enabled定义见下面），那么一个A step会最终发生。也就是说，下图中的绿色部分一定会发生一个A step。

    Weak Fairness使用下面的格式，其中vars是这个Spec中涉及的所有变量。

    1
    WF_vars(A)

    容易看出，Weak Fairness是一个Liveness property。因为它在A step或者A没有被enabled的时候，都是true。
    对应的，还有Strong Fairness，如果Action A重复地(repeatedly) enabled，那么一个A step会最终发生。
    因此，我们可以总结得到具有Liveness的Spec的格式。其中Fairness是WF_vars(A)和SF_vars(A)的组合，其中A是Next的之动作。

    1
    Spec == Init /\ [][Next]_<<...>> /\ Fairness

    即

    1
    Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

    在检查Liveness条件时，不能使用symmetry set。

  14. 精化(refinement)关系
    为了使用TLC检验在精化映射φ下，ImplSpec到AbsSpec的精化关系，我们在模块ImplModule中添加定义和THEAOREM

    1
    2
    AbsSub == INSTANCE AbsModule
    THEOREM ImplSpec => AbsSub!AbsSpec

尚未归类

  1. ASSUME
    必须是一个布尔量的常量表达式。
    TLA+会检查ASSUME中列出的条件是否满足。
  2. CONSTANTS
    定义了一系列常量，这些常量都可以理解为是集合。
    根据Lamport的P10a，传统数学中的变量，类似于TLA+中的CONSTANT。传统数学中没有和TLA+中的VARIABLE对应的概念，这个概念属于Temporal Logic(时序逻辑)。
  3. VARIABLE/VARIABLES
    以TCommit为例，我们定义了CONSTANT RM，还定义了VARIABLE rmState。
    如何区分VARIABLE和CONSTANTS呢？我们可以理解为rmState是一个数组，这个数组的indexer是我们定义的RM集合，而这个集合是一个常量。
  4. []TPNext
    表示TPNext始终成立。
  5. EXTENDS
    类似于C++里面的#include
  6. INSTANCE
    下面的语句表示我们现在的Module实现了TCommit，于是我们将TCommit中的所有定义import到我们当前Module中。 
    1
    INSTANCE TCommit

常见写法

  1. 求 Sub Sequence
    Sequence 中有 SubSeq

  2. Sequence 转为 Set

    1
    ToSet(seq) == {seq[i]: i \in DOMAIN seq}

  3. 实现类似 { f(x) for x in S if p(x) }
    我觉得一种方法是组合使用 {e: v \in S} 和 {v \in S: P}。也就是

    1
    { f(x) : x \in { v \in S : p(v) } }

DieHard

在TLA中，需要在等式==右边指定全部状态。

TCommit

对应Lamport的第5节课。
TCommit主要定义了事务的提交模型。如下图所示，每个Resource Manager(RM)节点，可以理解为2PC里面的参与者节点，具有working、prepared、committed、aborted四种状态。在这个提交模型中，我们不考虑协调者，也就是只考虑怎么样，不考虑如何做。后者会在下一章中考虑。

下面定义TypeOK对么？肯定是不对的，因为rmState是RM的集合。我们并不是希望这个集合属于这四个值，而是希望每个rmState[r]属于这四个值之中

1
TCTypeOK == rmState \in {"working", "prepared", "committed", "aborted"}

所以我们需要

1
TCTypeOK == rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]

其实我觉得应该也可以这么写

1
TCTypeOK == \A r \in RM: rmState[r] \in {"working", "prepared", "committed", "aborted"}

在Module中不检查Deadlock，但检查TCConsistent和TCTypeOK。

注意，源码里面有一些诸如TCSpec的，并不会在这篇文章里面讲解。

TwoPhase

首先介绍一下消息：

  1. Prepared
    RM->TM，表示某个RM已经Prepared了。
  2. Commit
    TM->RM
  3. Abort
    TM->RM

然后介绍下动作：

  1. TMRcvPrepared
    TM收到了某个RM的Prepared消息。
  2. TMCommit
    TM决定commit事务。
    此时TM必须在initial态，并且所有的RM都已经发送了Prepared消息。
  3. TMAbort
    TM自发地abort事务。
  4. RMPrepare
    某个RM决定prepare。
  5. RMChooseToAbort
    某个RM决定abort。
    注意，此时RM不会发送任何消息。这个是正常的，例如我宕机了，那还怎么发送消息。
  6. RMRcvCommitMsg
    某个RM收到了来自TM的Commit消息。
  7. RMRcvAbortMsg
    某个RM收到了来自TM的Abort消息。

下面介绍状态：

  1. rmState
    包含{"working", "prepared", "committed", "aborted"}。
  2. tmState
    包含{"init", "done"}。
    done表示TM进行了Commit或者Abort操作。
  3. tmPrepared
    TM接受到了哪些RM的准备消息。
  4. msgs
    是一个表示所有已经发送的消息的集合。

这里面涉及到定义类型，有点类似于Haskell的ADT。

1
Messages == [type: {"Prepared"}, rm: RM] \union [type: {"Commit", "Abort"}]

这里\subseteq是子集的意思，这两句话实际就是在说tmPrepared和msgs中的值一定属于RM或者Message。

1
2
TPTypeOK == /\ tmPrepared \subseteq RM
            /\ msgs \subseteq Messages

PaxosCommit (P07)

通过2PC，我们通过协调者TM去处理事务的提交。但如果TM宕掉怎么办呢？一个通常的实践是在主TM宕机后切换到备份的TM。这个操作的问题是，可能主TM决定Commit后分区/暂停了，但是备份TM决定Abort。但当它发送这个消息后，主TM恢复，并且发送Commit消息。这可能导致某些RM会Commit，另一些会Abort。

需要检查：

  1. PCTypeOK
  2. TCConsistent

Lamport强调，随着模型的线性增大，运行时间会以指数增大。

P08a+P08b

这一章节中的大部分内容被归纳到Expression/Spec章节。

Implication

介绍蕴含关系(implication)，也就是=>

1
p => Q

等同

1
IF P THEN Q ELSE TRUE

我们知道原命题的逆否命题成立，即

1
~Q => ~P

其中~也可以表示为\lnot或者\neg

在口语中，implication通常断言因果。但是在数学中，只断言相关性。

Module-closed expression

一个module-closed formula是一个不二良的module-closed expression。例如

1
(x \in 1..42) /\ (y' = x + 1)

P09a

这一章节中的大部分内容被归纳到Expression/Spec章节。

介绍了ABSpec，即AlteringBits这个协议。

我们需要进行Liveness检查，分为以下步骤

  1. 选择Temporal Formula为FairSpec
  2. 设置”What is the model?”为”Set of model values”，但是关闭”Symmetry sets”选项。
  3. 在**”What to check?”下面的“Properties”**中填入下面的检查 
    1
    \A v \in Data \X {0,1}: (AVar = <<"hi",0>>) ~> (BVar = <<"hi",0>>)

P09b

这一章节介绍AB，也就是AlteringBits这个协议的具体实现。

这个协议如下所示，A向B同步信息。开始，A和B都是<<"",0>>。接着A开始发送<<"Mary",1>>，会不断重传。当B收到<<"Mary",1>>后，就更新自己的值，并且开始不断向A发送1，而不是0。

在实现完AB之后，需要进行Safety检查。但不能直接检查Spec。这是因为A和B可以不断地给彼此发送消息，并且发送的速度远远比丢包或者对端接收要快，这样的话会导致有无数的可到达状态，我们的TCL程序可能永远不会结束！
此时需要打开”Additional Spec Options”标签，在”State Constraint”中设置。这样我们就限制了消息的最大长度。

1
2
/\ Len(AtoB) =< 3
/\ Len(BtoA) =< 3

此外，我们还要在”What to check?”下面的”Properties”中填入ABS!Spec，表示我们要检查ABSpec里面的Spec。

下面进行Liveness检查，也就是添加Fairness条件，从而imply消息能够持续被发送以及接收。
此时Weak Fairness是不够的。因为这实际上允许了B一直向A发送1，如下如所示。【Q】为什么呢？稍后解释

因此我们得使用下面的

1
2
FairSpec == Spec  /\  SF_vars(ARcv) /\ SF_vars(BRcv) /\
                      WF_vars(ASnd) /\ WF_vars(BSnd)

【Q】能不能改成全是WF呢，如下所示

1
2
FairSpec == Spec  /\  WF_vars(ARcv) /\ WF_vars(BRcv) /\
                      WF_vars(ASnd) /\ WF_vars(BSnd)

尝试一下，可以发现下面的错误：

它的路径如下，容易发现形成了循环。

  1. BSnd: 1
  2. ASnd: <<a, 1>>
  3. LoseMsg: BtoA from <<1>> to <<>>
  4. BRcv: AtoB from <<<<a, 1>>>> to <<>>
    回到了状态1

Why？这是因为WF_var(ASnd)和WF_var(BSnd)是true，因为ASnd和BSnd一直在发生。
现在考虑WF_vars(ARcv)。在Init状态，它没有enable，因为BtoA是空的。在B发送消息之后，它enable了，但是如果发生了LostMsg，那么它又不enable了。容易看出，WF_vars(ARcv)也是true，因为ARcv并不能continuouesly enable。
所以，我们满足了FairSpec，但并不满足ABS!FailSpec，所以下面的THEOREM也不成立了

1
THEOREM FairSpec => ABS!FailSpec

因此，我们要引入Strong Fairness。

P10a

递归

实现RemoveX，用来移除一个Tuple中的所有"X"。我们需要一个前置声明。

1
2
3
4
RECURSIVE RemoveX(_)
RemoveX(l) == IF l = <<>> THEN l
                ELSE IF Head(l) = "X" THEN RemoveX(Tail(l))
                     ELSE <<Head(l)>> \o RemoveX(Tail(l))

代入(Substitution)

考虑传统数学中的代入逻辑，即把e导入到f(v)中

1
(v = e) => (f = (f WITH v <- e))

其中WITH是Lamport定义的描述性的语句，其作用如下

1
(y^3-y) WITH y <- x+2 = (x+2)^3-(x+2)

因为TLA关注时序的逻辑，我们不能在写TLA+的时候这么进行代换，我们考虑下面的代入：v <- y、e <- x + 2、f <- y'，其实未必是一直成立的

1
THEOREM (y = x + 2) => (y' = (x + 2)')

因此，我们使用Temporal Substitution Law

1
[] (v = e) => (f = (f WITH v <- e))

即写成下面的形式

1
THEOREM [] (y = x + 2) => (y' = (x + 2)')

AB2

这个协议旨在处理出现消息损坏(Corrupted)的情况。
为此，我们引入了一个新消息Bad。并且Bad一定不等于所有的其他消息。我们用ASSUME来描述这个性质。

1
ASSUME Bad \notin (Data \X {0,1}) \cup {0,1}

此外在运行Module的时候，需要给Bad赋一个不同于所有其他消息的值，一个Idea是用字符串”Bad”来代表。但这会遇到错误”Attempted to check equality of interger 0 with non-integer: “Bad””。所以，实际上我们可以直接用Model Value，即我们给Bad的值就是Bad。

我们需要保证消息需要在他们Corrupted之前被Receive，这个靠目前的Fairness条件是不够的，我们需要修改Safety条件。
首先，我们加入了AtoBgood和BtoAgood用来表示某条信息是不是肯定不会Corrupt。
然后，如果我们将AtoB2里面的Bad消息去掉，就可以得到一个等价的AtoB，因此我们得到了SpecH。去掉可以通过RemoveBad，类似于之前提到的RemoveX。

1
2
3
SpecH == /\ AB2!Spec
         /\ [] /\ AtoB = RemoveBad(AtoB2)
               /\ BtoA = RemoveBad(BtoA2)

我们的目标是，但此时我们的SpecH并不符合TLA+的Safety检查的格式，即Init /\ [][Next]_vars。

1
THEOREM SpecH => AB!Spec

为此，我们引入了SpecHH

1
2
SpecHH == InitH /\ [][NextH]_varsH
THEOREM SpecHH <=> SpecH

其中<=>的作用等价于

1
2
/\ SpecHH => SpecH
/\ SpecH  => SpecHH

PlusCal Manual

2 Getting Started

欧几里得算法

可以用 TLC Options -> Checking Mode 中选择 Simulation mode 来随机模拟可能的情况。
也可以用 Model-checking mode 去检验所有的情况。
注意这里 Debug 的时候，Print 的顺序未必是按照代码序的，因为 TLC 不是顺序执行代码，而是一个 BFS 搜索所有状态。

1
2
3
4
5
6
7
8
9
10
11
12
variables
    u = 24,
    v \in 1..N,
    ori_v = v;
begin
    while u /= 0 do
        if u < v then u := v || v := u ;
        end if ;
        u := u - v;
    end while ;
print <<"have gcd", u, ori_v, v, gcd(24, ori_v)>> ;
assert v = gcd(24, ori_v)

Fast Mutation 算法

在 process 里面定义的 variable 是 “thread local” 的。
self 表示这个 process 自己，也就是1..N中的某个数。
一个原子的操作，也就是一个 step，表示从一个 label 到另一个 label 的执行过程。比如，label l2 处的 y /= 0 是原子的，并在到达 label l3 或 l4 时结束。

只有当 await exp 中的 exp 是 true 的时候，对应 step 里面的操作才会被执行。如果 exp 是 false，那么就不会产生任何修改，会稍后再尝试执行这个 step。await 和 when 互为 alias。
下面的代码比较有意思，它实际上是用集合的表示实现了for (i = 1; i < N; i++) 这个循环条件。

1
2
3
4
5
6
j := 1.. N ;
l8: while j /= {} do
    with p \in j do await ~b[p] ;
        j := j \ {p} ;
    end with ;
end while ;

上面的这个 with，表示在 j 里面随机选择一个 p。当然在 model checking mode 中，TLC 会检查所有可能的选项。
如果把 p \in j 替换成 p = exp，则导致 p 是当前 exp 的值。

process Name = e表示一个 id 为 e 的线程，它的名字是 Name。不同的 process 有不同的 id。

Fast Mutex 的安全性条件是同一时间，最多只有一个 process 能够进入 critical section。PlusCal 通过原子的 skip 表示 nocritical 和 critical section。那么形式化来说，我们可以定义一个 Invariant，即没有两个 process 可以同时在 cs 这个 label 处。
那么如何检验这一点呢？首先，TLA+ translation 会引入一个 pc，表示下一个被执行的 statement。以 Fast Mutex 为例，当且仅当 pc[i] 为 l5 时，process[i] 下一个执行 l5。对于多进程来说，pc 是一个定义域为 process id 的函数。对于单进程来说，pc 是一个等于下一个要执行的 label 的字符串。对于每个 process，有一个隐式的 label 即 Done，标记该 process 的结束。因为 Fast Mutex 不会结束，所以 pc[i] 永远不会为Done。
容易想到下面的 Mutex

1
Mutex == \A i,k \in 1..N : (i /= k) => \neg ((pc[i] = "cs") /\ (pc[k] = "cs"))

我们可以将 Mutex 添加到 What to check 中，也可以用它来替换 cs 中的 skip

1
cs: assert \A i \in 1..N : (i /= self) => (pc[i] /= "cs")

Label 的规则

  1. 每个 process 必须从一个 label 开始
  2. while 必须被 label
  3. do+with 中不能包含任何 label
    因此，with 中不能包含 while
  4. 如果一个 if 包含 label，那么在 if 后面一定跟着一个 label
  5. 从一个 label 到下一个 label 的过程中，不能有对于一个变量的两次分别的赋值。即使这个赋值是对于一个数组中的多个元素
    但当然，允许 single multiple assignment，即 
    1
    x[1] := 1 || x[2] := 2

通过 -label 可以让 translator 加 label，通过 -reportLabels 可以让 translator 同时告诉你它在哪里加了 label。对于一个单线程的算法，-label 作为默认选项，如果我们不手动添加任何的 label。

备注：关于 Fast Mutex 算法的解释

Michael Fischer 提出了下面的 Mutex 算法。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(*--algorithm mut
variables lock = 0;
process Proc \in 1..N
begin
    ncs: while TRUE do
            skip;
            l1: while lock /= self do
                    l2: await lock = 0;
                    l3: lock := self;
                    /* Delay
                end while;
     cs:    skip;
         end while;
end process
end algorithm; *)

算法存在缺点。考虑进程 j，它在进程 i 执行完 lock := i 之前，读取到 await lock = 0，那么 j 会已经完成 lock := j。可以发现随后的 delay 是不必要的。

i j
await lock = 0
lock := j
delay
lock := i

3 The language

Either

会随机选择一个可以执行的 clause 并执行。

1
2
3
4
5
either clause1
    or clause2
    ...
    or clausen
end either ;

如果有 clause 包含 call、return、goto，则 either 需要有一个 label。
if 和 either 之间存在关系

1
2
3
if test then t
        else e
end if ;

可以被写成

1
2
3
either await      test ; t
    or await \neg test ; e
end either ;

While

1
2
lb: while test do body end while ;
lb: if test then body ; goto lb ; end if ;

Await and When

下面两个等价

1
2
3
a : x := y + 1 ;            a : await y + 1 > 0 ;
    await x > 0 ;               x := y + 1
b : ...                     b : ...

Definition

Reference

  1. https://www.jianshu.com/p/12fda75ddf9e
    介绍TLA+的语法
  2. http://lamport.azurewebsites.net/video/videos.html
    Lamport的视频教学
    这里面有课件，以及视频教程里面的代码，这些在https://github.com/tlaplus/Examples并没有。
  3. https://github.com/parlarjb/tla_workshop
    Lamport的代码的整理
  4. https://learntla.com/tla/
    一个TLA+学习的网站
  5. https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
    Specifying Systems这本书，这是终极版本的讲义
  6. http://lamport.azurewebsites.net/tla/newmodule.html
    TLA中的module的相关说明，包含了很多语法相关的讲解
  7. http://lamport.azurewebsites.net/tla/book-21-07-04.pdf
    Specifying Systems这本书的新版本？
  8. https://lamport.azurewebsites.net/tla/tla2-guide.pdf
    TLA2
  9. https://www.bilibili.com/video/BV1X54y1U7LU?from=search&seid=1851114600685541822
    教学视频，包含P10
  10. https://www.bilibili.com/video/BV1yW411s7Hg?from=search&seid=1851114600685541822
    教学视频，不包含P10，但是赠送了对Paxos的讲解
  11. https://github.com/BinyuHuang-nju/raft-tla/blob/master/2021-JoS-PRaft.pdf
  12. https://github.com/tlaplus/DrTLAPlus
  13. https://www.youtube.com/watch?v=6Kwx8zfGW0Y
    从1.07开始有个简单的对Raft的TLA+的讲解
  14. https://lamport.azurewebsites.net/pubs/pluscal.pdf
    对PlusCal的介绍
  15. https://lamport.azurewebsites.net/tla/p-manual.pdf
    PlusCal手册
  16. https://github.com/belaban/pluscal/
    PlusCal源码实例
  17. https://www.ics.uci.edu/~cs230/reading/Lamport%20Fast%20Mutual%20Exclusion%20Algorithm.pdf
    Lamport 的 FastMut 算法论文
  18. https://www.hillelwayne.com/post/list-of-tla-examples/
    各种 tla 系统