引子

在讨论 TiKV Transaction 之前，我们先聊聊 Percolator。TiKV 的事务是参考 Google [Percolator] （后面我们使用 Percolator 来表示 Percolator 的事务）实现的，然后做了些许优化，所以这里，我们先实现 Percolator 的 TLA+，然后再去实现 TiKV 的。

介绍

Percolator 是建立在 Google BigTable 上面的，而 BigTable 只能支持单行事务，所以 Percolator 需要在 BigTable 上面封装一套事务机制来实现分布式事务。

Percolator 仍然使用的是 MVCC 机制，用来提供 Snapshot Isolation。Percolator 并不像其他传统的 DBMS 一样，直接内置 lock 来进行并发控制。Percolator 只能通过 client 来操作 BitTable，所以需要自己实现 lock，加上 Percolator 任何节点都可以发起请求，并没有传统 2 PC 里面一个协调者的概念，所以 Percolator 的整个事务其实是实现的非常巧妙和高效的。

我们先介绍下 Percolator 的几个主要 Column 定义：

• lock：任何的未提交的事务都会写 lock。Lock 分为 primary lock 和 secondary key，如果是 secondary lock，则会包含 primary lock 的位置信息。
• write：用来表示数据已经提交，里面会存放数据的 timestamp。
• data：实际的数据

Percolator 还有一个 notify 和 ack 的 Column，主要是用在通知上面，但因为我们没有用到，所以这里就不做说明了。

流程

在 Percolator 论文里面对事务已经有详细的伪码实现，这里简单的用通俗的语言介绍一下。Percolator 使用的是乐观锁机制，当事务开始的时候，首先会拿一个 start timestamp，然后用这个 timestamp 去获取感兴趣的数据，然后再提交的时候进行加锁处理。

Get

首先我们来看 Get， 事务会先用 start timestamp 去拿对应 key 的数据，首先看这个 key 上面是不是有 lock，如果有 lock，可能几种情况：

1. 另一个事务正在提交数据，这个 key 被 lock 住了，所以我需要在等待一段时间再重试。
2. 如果很长一段时间，这个 key 还是被 lock 住的，有可能对应发起事务的 client 已经挂掉了，这时候就要做清锁处理。
3. 这个 lock 其实是一个残留的 lock，这种情况多数发生在 一个事务 primary key 已经提交成功并清理了 primary key，但 secondary key 没有提交成功，secondary key 残留的情况，这时候其实就可以安全的对 secondary key 进行清锁处理。

当没有 lock 的时候，这时候就可以找到在 [0, start_ts] 区间里面最新的一个 committed write 的，如果没有，那就是这个 key 还没有任何数据，如果找到了，则通过 committed write 里面对应的 start timestamp 的值，找到对应的 data。

Pre-write

当事务拿完所有的数据，并处理之后，就要将更新提交了，提交分为两步，首先就是 pre-write，对于任何 key，会先判断在 [start_ts, +] 范围内是不是有一个新的 write 写入，如果有，表明另一个事务已经写入了新的数据，那么当前事务就要结束回滚了。也需要判断 key 的 lock 是不是已经被锁住，如果有，也需要结束回滚了。

当发现没有任何新的写入，锁也没有被占用的时候，我们就可以写入自己的 lock 以及对应的 data。

Commit

当事务所有的 key 都完成了 pre-write，我们就可以最终进行 commit，commit 会先提交 primary key，首先会判断 primary key 对应的 lock 还在不在，如果不在了，标明其他的事务已经把当你给清掉了，所以我们只能失败回滚。如果发现 lock 还在，则可以写入 committed write，以及将 lock 给清掉。

当 primary key 提交成功之后，我们就认为事务已经完成了，secondary key 就可以异步提交，主要就是写入 committed write 和清掉 lock。即使 secondary key 提交失败了，下一个事务如果读到了这个 key 的 lock，发现该 lock 对应的 primary key 已经清掉，就自动帮之前的事务写入 committed write 和清锁，然后在继续处理自己的事务数据了。

例子

我们来看一个简单的例子，初始的时候，Bob 是 10 块钱，而 Job 是 2 块钱，Bob 要给 Joe 转 7 块钱，那么最终结果就是 Bob 后面只有 3 块钱，Job 有 9 块钱。

我们开启一个事务，起始 timestamp 是 7。因为 Bob 和 Joe 之前的数据都是提交的，提交 timestamp 是 6，所以我们就能读到 6 对应的实际数据，也就是 timestamp 5 的 data - 10 和 2。

因为这个事务涉及到了两个 key，也就有两个 lock，我们设置 primary lock 是 Bob ，而 secondary key 则是 Job。首先对 Bob 进行 prewrite 操作，在 timestamp 7 写入 primary lock 以及对应的 data，也就是 3 块钱。

然后对 Joe 进行 Prewrite 操作，写入 secondary key，里面的值就是对应的 Job 的 primary key，顺带写入新的 data，也就是 8 块钱。

当两个 lock 都写入成功之后，我们就需要先提交 primary key 了，这里就是 Bob，我们使用新的提交 timestamp 8，写入 write，值就是 data 对应的 timestamp，也就是 7，同时将自己的 primary lock 给清掉。

只有 primary key 提交成功，那么整个事务就是成功了，即使 secondary key 没有被清理成功，后面也会被其他事务给正常清理掉。但这里我们还是说一下正常流程，提交 secondary key，也就是 Joe 会写入 write，里面的值就是对应的 data 的 timestamp，就是 7，顺便清掉自己的 lock。

进行完上面的步骤，这次事务就结束了。当然这里为了简单，我们并没有冲突，或者异常的情况。

TLA+

上面我们详细讨论了 Percolator 的算法以及一个简单的例子，剩下的就是开始使用 TLA+ 来详细的实现了。完整的 Percolator TLA+ 可以参考 [Percolator.tla]，这里我只是简单的介绍一下。

常量和变量

首先我们引入两个常量 KEY 和 CLIENT，KEY 表示的就是要操作的 key 的集合，大家可以在 TLA+ Toolbox 里面设置，譬如 {"k1", "k2", "k3"}。然后就是 CLIENT，可以认为是要发起事务的客户端集合，我们可以设置为 {"c1", "c2", "c3"}。然后我们定义一个 next_ts 用来获取当前的 timestamp，因为 Percolator 能通过一个 Oracle 服务来保证 timestamp 单调递增，所以这里我们也约定不同事务的 timestamp 一定是不同，单调递增的。

对于一个实际发起事务的 client，它可能会处于多种状态，譬如 “init”，”working”，”committed”，”aborted” 等，这里我们使用变量 client_state 来表示。每个 client 会保存自己事务的 timestamp，我们使用 client_ts 来存储，里面是一个 record， 譬如 [start_ts |-> 1, commit_ts |-> 2]。然后对于一个 Percolator 事务来说，它有一个 primary key，剩下的就是 secondary key，我们使用一个 record，譬如 [primary |-> "k1", secondary |-> {"k2", "k3"}]。

对于实际的 key，我们有一个 key_lock，它是一个 lock record （譬如 [start_ts |-> 1, primary |-> "k1"]） 集合，用来保存事务的 lock，还有一个 key_data，用来保存实际事务的数据，因为每个事务的 start timestamp 是唯一的，所以我们这里就使用 start timestamp 来当做 data，也就是 key_data 是一个 start timestamp 的集合。然后就是 key_write，用来保存这个 key 在不同的 timestamp 的提交，因为 write 一定是有序写入的，所以 key_write 是一个 write record（譬如 [start_ts |-> 1, commit_ts |-> 2]）的 sequence。

关键流程

之前我们说过，写 TLA+，在确定好变量之后，最重要的就是需要注意：

1. 变量的初始化
2. 从一个状态转换到另一个状态，变量之前的关系

首先我们来看初始化，如下：

Init == 
    /\ next_ts = 0
    /\ client_state = [c \in CLIENT |-> "init"]
    /\ client_ts = [c \in CLIENT |-> [start_ts |-> 0, commit_ts |-> 0]]
    /\ client_key = [c \in CLIENT |-> [primary |-> "", secondary |-> {}]]
    /\ key_lock = [k \in KEY |-> {}]
    /\ key_write = [k \in KEY |-> <<>>]
    /\ key_data = [k \in KEY |-> {}]

在上面的 Init 函数中，我们对所有的变量进行了初始化处理，将 client 的 state 全部设置成了 “init” 状态。Client 的事务 start 和 commit timestamp 都是 0，而 primary 和 secondary key 都还没有。在 KEY 这边当然就没有任何的数据。

然后就是 Next 函数：

Next == 
    \E c \in CLIENT:
        Start(c) \/ Get(c) \/ Prewrite(c) \/ Commit(c)

对于任意的 client，我们都有可能进入 Start，Get，Prewrite，Commit 等阶段，这些其实就是对应的 Percolator 算法的具体流程了。譬如对于 Commit，实现如下：

Commit(c) ==
    /\ client_state[c] = "committing"
    /\ IF canCommitPrimary(c)
       THEN
            /\ commitPrimary(c)
            /\ client_state' = [client_state EXCEPT ![c] = "committed"] 
            /\ UNCHANGED <<key_data, client_txn_vars, next_ts>>
            \* If we commit primary successfully, we can think the transaction is committed
            \* TODO: use async message to commit second keys
       ELSE
            /\ client_state' = [client_state EXCEPT ![c] = "aborted"]      
            /\ UNCHANGED <<key_vars, client_txn_vars, next_ts>>

这里简单介绍一下，首先 client 的 state 要处于 “committing” 状态，我们才会继续处理 commit，然后 canCommitPrimary 必须要为 TRUE，这样我们就可以实际的去 commitPrimary，顺带将自己的 state 改成 “committed”，也就是事务提交成功了。这里我并没有提交 secondary，因为 Percolator 算法会保证它被后面的事务给正确提交。不过不排除我面我加上 Message Bag 来处理。如果 canCommitPrimary 不为 TRUE，那么事务就变成 “aborted” 了。

当然，写完了算法，我们还需要证明算法是可靠的，这里我写了两个 Consistency 验证，一个是 WriteConsistency，它会去验证 key_write 一定是按照 commit timestamp 有序排列的。另一个就是 CommittedConsistency，如果一个 client 处于 “committed” 状态了，那就表明这个事务提交成功了，那么它的 primary key lock 一定被清掉，write 里面一定有 commit timestamp，但 secondary key lock 不一定会被清掉，如果还有 secondary key lock，那么 key_lock 一定没有其他的 lock，同时 key_write 里面最后一次的 commit timestamp 一定要小于 lock 的 start timestamp。当然，我可能后面还会加入更多的 Consistency 验证。

具体的算法实现大家可以参考源码，因为这算是我第一次写 TLA+ 难免，可能有些地方没有写好，欢迎大家提出修改意见。

小结

当我们设计一个算法的时候，都可以使用 TLA+ 先来证明我们算法的正确性，如果算法都不确定，后面如何实现都是枉然的。当然，这里需要注意，即使 TLA+ 证明出来我们设计的算法没问题，但并代表自己实现的算法没有问题，毕竟理论论证是一回事，工程实践又是另一回事。