前面对 TLA+ 有了一个大概的介绍，但我相信大家可能仍然是一头雾水，我们如何使用 TLA+ 去验证系统原型设计的正确性呢？我觉得我们可以先从一些简单的例子入手，然后再逐渐理解，最后再用 TLA+ 来验证我们自己的系统。
DieHard
第一个简单的例子就是 DieHard，不过我没看过这部电影。电影里面主角需要用一个 3 加仑的水壶和一个 5 加仑的水壶得到 4 加仑的水，怎么做呢？
当然，这个问题比较简单，大家可以在脑袋里面自行分析流程，这里我们通过 TLA+ 来得到结果。
首先我们定义两个变量，big 和 small，用来表示 5 和 3 加仑的水壶。定义是 VARIABLES big, small。在前面我们介绍过，TLA+ 其实就是一个状态机，它有一个初始状态，然后就开始不停的迭代循环到下一个状态。
首先我们来看初始状态，也就是 big 和 small 都为 0，如下：
Init ==
/\ big = 0
/\ small = 0
然后我们再看 Next 状态，我们可以做如下事情：
- 给 3 加仑水壶灌满水
- 给 5 加仑水壶灌满水
- 清空 3 加仑水壶
- 清空 5 加仑水壶
- 将 3 加仑水壶的水倒到 5 加仑水壶
- 将 5 加仑水壶的水倒到 3 加仑水壶
对应的 TLA+ 为：
Next ==
\/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall
我们首先来看 FillSmall，我们可以写 FillSmall == small' = 3，但这样其实是不对的。因为这里我们并没有处理 big 的情况，在之前的文章里面我们说过，Next 表示的其实就是在当前状态下变量的值以及在下一个状态下这些变量的可能的值之间的关系，所以上面的语句我们只处理了 small，但 big 可能就是任意值了，实际上 big 的值是不变的，所以真正的 FillSmall 为：
FillSmall ==
/\ small' = 3
/\ big' = big
注意，这里在说明一下，TLA+ 里面会用 ' 来表示下一个状态。
自然的 EmptySmall 为：
EmptySmall ==
/\ small' = 0
/\ big' = big
然后我们再来看看 SmallToBig，它有几种情况：
- small + big <= 5，那么我们就能将 small 的水全部倒到 big 里面
- small + big > 5，我们只能从 small 这边倒 5 - big 的水
上面两种情况，其实都可以写成 Min(big + small, 5) - big，首先我们定义 Min：
Min(m, n) == IF m < n THEN m ELSE n
如果公式 m 小于 n 为 TRUE，那么就使用公式 m，否则就使用公式 n。
然后我们实现 SmallToBig：
SmallToBig ==
LET poured == Min(big + small, 5) - big
IN
/\ big' = big + poured
/\ small' = small - poured
当然，我们可以很容易的写出其他的公式，详细可以参考 DieHard.tla。
实现了 Init 和 Next 之后，下一步就是如何去验证了。我们要得到 4 加仑的水，所以如果我们发现，在某一个状态的时候，big 里面有 4 加仑的水，那么直接报错，TLA+ 会输出迭代到 4 加仑水这个状态时候所有的步骤，我们自然就能知道如何得到 4 加仑水了。所以我们先定义 NotSolved == big /= 4，并加入到 TLC model 的 Invariants 里面，然后执行 model，会发现 TLC 会报错了。关于 TLA+ toolbox 的使用，大家可以自行下载尝试，后面有机会我也会在说明一下。
Transaction Commit
上面的 DieHard 只是一个比较简单的例子，我们下面来说说事务。说到事务，就不得不用结婚的例子来说明了。一个婚礼的大概流程如下：
- 神父对新郎说：『你准备好了吗？』
- 新郎回复：『准备好了。』
- 神父对新娘说：『你准备好了吗？』
- 新娘回复：『准备好了。』
- 神父对新郎新娘说：『恭喜你们。』
上面假设 2 和 4 的时候任意一方说『不愿意』，那么神父就会取消婚礼。所以对于一次婚礼来说，要不就是新郎新娘结为夫妇，要不就是散伙，绝对不会出现新郎认为结婚了，但新娘认为没结婚这样的状态，反之亦然。
对应到事务上面，新郎新娘就是 Resource Manager（RM），而神父就是 Transaction Manager（TM）。对于所有 RM，它们最终只可能是 committed，或者 aborted 状态，不可能一些是 committed，一些是 aborted。最开始 RM 是 working 状态，然后会变成 prepared 状态，当一个 RM 是 prepared 了，它就可能变成 committed 或者 aborted，RM 也可以直接从 working 变成 aborted。
这里，我们首先用 TLA+ 来描述下事务提交的规格，这里，我们只会关注 RM，而不会关注 TM，因为 TM 是用来执行事务的，也就是 How 的过程，而并不是 What。后面我们会实际的用 2 PC 再来讲解 How。
首先我们先定义常亮 RM，使用 CONSTANTS RM，RM 是一个集合，在 TLC model 里面我们会给它赋值，譬如叫 {"r1", "r2", "r3"} 这种的。然后我们定义变量 VARIABLES rmState 用来表示 RM 的状态。
初始我们会将所有的 rmState 设置为 working，也就是 TCInit == rmState = [r \in RM |-> "working"]。
对于任意一个 RM，它的 Next 可能是准备事务，也可能是觉得是否提交或者终止事务。所以 Next 定义为 TCNext == \E rm \in RM : Prepare(rm) \/ Decide(rm)，这里我们注意下 \E rm \in RM : Prepare(rm) \/ Decide(rm)，假设 RM 是 {"r1", "r2"}，那么它就等价于 Prepare("r1") \/ Decide("r1") /\ Prepare("r2") \/ Decide("r2")。
我们先来看 Prepare，定义如下：
Prepare(rm) == /\ rmState[rm] = "working"
/\ rmState' = [rmState EXCEPT ![rm] = "prepared"]
这里我们会注意到 function 的 EXCEPT 用法，对于 rmState 为 working 的，Prepare 会将其设置为 prepared 状态，其他的 rmState 不变。
再来看看 Decide，如下：
canCommit == \A rm \in RM : rmState[rm] \in {"prepared", "committed"}
notCommitted == \A rm \in RM : rmState[rm] /= "committed"
Decide(rm) == \/ /\ rmState[rm] = "prepared"
/\ canCommit
/\ rmState' = [rmState EXCEPT ![rm] = "committed"]
\/ /\ rmState[rm] \in {"working", "prepared"}
/\ notCommitted
/\ rmState' = [rmState EXCEPT ![rm] = "aborted"]
我们可以先看 Decide 的第一个公式，如果 RM 的状态为 prepared，并且所有的 RM 状态都是 prepared 或者 committed，并且下一个状态可以设置 RM 为 committed，那么这个公式就是 TRUE 的。这里不再分析第二个公式。
前面说到，我们不可能出现一个 RM 是 committed，而另一个是 aborted 的情况，所以定义：
TCConsistent == \A rm1, rm2 \in RM : ~ /\ rmState[rm1] = "aborted"
/\ rmState[rm2] = "committed"
然后将 TCConsistent 将入到 TLC 的 Invariants 里面，运行。如果 TLC 没有报错，那么就证明我们的 Transaction Commit 规格设计的是对的。实际例子大家可以参考 TCommit.tla。
Two Phase
上面说完了 Transaction Commit，这里我们在继续说说 Two Phase，也就是我们经常说的 2 PC，2 PC 是实现分布式事务的一种传统方式，这里我们会引入一个新的角色：TM，也就是 Transaction Manager，用来操作不同的 RM。
我们仍然定义 RM 常量，这里不再说明。然后定义变量 VARIABLES rmState, tmState, tmPrepared, msgs，tmState 就是 TM 的状态，tmPrepared 是一个 prepared RM 的集合，msgs 则是 TM 和 RM 之间发送的消息。
我们定义消息集合 Messages == [type: {"Prepared"}, rm: RM] \union [type: {"Commit", "Abort"}]，这里，我们使用了 TLA+ 里面一种特殊的 function - record，record 其实就可以认为是 C 里面的 struct。上面的 Messages 定义包含两类 record，一个是给某个 RM 发送的 Prepared 消息，而另一个就是给所有 RM 发送 Commit 或者 Abort 消息。
初始状态为：
TPInit ==
/\ rmState = [r \in RM |-> "working"]
/\ tmState = "init"
/\ tmPrepared = {}
/\ msgs = {}
所有 RM 初始状态为 working，TM 为 init，tmPrepared 和 msgs 都是空的。我们下面来开始处理 Next，先考虑 prepared，TM 会先跟 RM 发送 prepared 消息，然后 TM 会将 RM 加入到 tmPrepared 集合里面，如下：
RMPrepare(r) ==
/\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
/\ msgs' = msgs \union {[type |-> "Prepared", rm |-> r]}
/\ UNCHANGED <<tmState, tmPrepared>>
上面的 RMPrepare 里面，如果 RM 的状态为 working，我们将其设置为 prepared，将 [type |-> "Prepared", rm |-> r] record 添加到 msgs 里面。这里我们注意下 UNCHANGED，它等同于 /\ tmState' = tmState /\ tmPrepared' = tmPrepared。
在看 TMRcvPrepare，如下：
TMRcvPrepared(r) ==
/\ tmState = "init"
/\ [type |-> "Prepared", rm |-> r] \in msgs
/\ tmPrepared' = tmPrepared \union {r}
/\ UNCHANGED <<rmState, tmState, msgs>>
TM 的状态需要为 init，并且 msgs 里面已经有了对应 RM 的 prepared 消息，那么就将 RM 加入到 tmPrepared 里面。
我们再来看看 commit：
RMRcvCommitMsg(r) ==
/\ [type |-> "Commit"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
TMCommit ==
/\ tmState = "init"
/\ tmPrepared = RM
/\ tmState' = "committed"
/\ msgs' = msgs \union {[type |-> "Commit"]}
/\ UNCHANGED <<rmState, tmPrepared>>
如果 Commit 在 msgs 里面，就将 RM 的状态设置为 committed。对于 TM 来说，则是需要确保所有的 RM 都已经在 tmPrepared 里面，才会将 Commit 加入到 msgs 里面。
对于 Abort，这里不再解释，所以 Next 就是：
TPNext ==
\/ TMCommit \/ TMAbort
\/ \E r \in RM:
TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r)
\/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r)
具体可以参考 TwoPhase.tla。
小结
上面只是 TLA+ 的几个简单例子，写多了大家可能就会发现，用 TLA+ 来设计系统无非几个关键地方：
- 提取该系统的变量
- 在 Init 初始化变量
- 考虑 Next 都可能有哪一些状态组合，这些状态下面，需要保证那些条件为 TRUE，变量是如何变化的
- 考虑 Invariants，也就是变量一定不会有某些情况
当然，虽然上面看起来比较容易，但真正开始写大型项目，还是会有很多坑等着我们去踩。后面，我就会详细解释下 Raft，以及尝试先将 TLA+ 应用到我们实际的 TiKV Transaction 中。
网友评论