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
    例如

    1
    RM <- {r1, r2, r3}

检查项目

在”What to Check”中:

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

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"

集合/元组/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. DOMAIN <<"a", "b", "c">>
    表示一个集合。Lamport说Math中的DOMAIN,对应于Progamming中的Index Set。

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

  8. “构造函数”{e: v \in S}
    对S中的元素应用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}
  9. “构造函数”{v \in S: P}
    类似一个filter。

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

    1
    2
    /\ x' = x
    /\ y' = y
  11. 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
    必须是一个布尔量的常量表达式
  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

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是子集的意思,这两句话实际就是在说tmPreparedmsgs中的值一定属于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 <- ye <- x + 2f <- 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

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+的讲解