TLA+，概念初识

假设我们正在为银行构建一项电汇服务。用户可以向其他用户进行转账。作为要求，我们不允许任何可能使用户账户透支或余额降至零以下的转账。在高层次上，代码可能如下所示：

def transfer(from, to, amount)
  if (from.balance >= amount) # guard
		from.balance -= amount;  # withdraw
  	to.balance += amount;   # deposit

上面的代码可以满足要求：当你你试图转账超过你拥有的金额，该防护机制将阻止你。

现在考虑两个变化：

1. 用户可以同时发起多个转账。
2. 转账步骤是不可中断的。一个转账可以开始并（可能）完成，而另一个转账仍在进行中。

这两个改变单独来看都不会引起问题。但两者结合起来可能导致可能的竞争条件：

1. Alice 的账户有 6 美元，并向 Bob 发起了两笔转账。转账 X 金额为 3 美元，转账 Y 金额为 4 美元。
2. Guard(X) 运行。因为 3 < 6，我们继续执行 Withdraw(X)。
3. 在 Withdraw(X) 发生之前，Guard(Y) 运行。因为 4 < 6，我们继续执行 Withdraw(Y)。
4. 两次提款都执行了，从 Alice 的账户中取走了 7 美元，使她的余额变成 -1。

如果 Withdraw(X) 在 Guard(Y) 之前发生，那么就不会有问题；转账 Y 将会简单失败。这种竞争条件基本上很少出现：大多数情况下，程序会按预期行为并维护我们的属性。只有在特定事件顺序下才会出现 bug。这就是为什么并发错误很难发现。

这也是为什么它们难以修复。想象一下，如果我们添加了第三个功能，比如在正确的位置加锁来修复 bug。问题是否消失是因为我们解决了它，还是因为我们使它变得更少见了？如果不能探索设计的实际后果，我们就不能保证已经解决了任何问题。

因此，TLA+ 的目的是通过程序化探索这些设计问题。我们想要为工具提供一个系统和一个要求，它可以告诉我们是否违反了要求。如果可以，那么我们知道需要改变我们的设计。如果不能，我们就可以更有信心地认为我们是正确的。

TLA+ 的概念架构由三个部分组成.

首先, 我们需要去描述系统以及它可以做什么. 这被称之为规范(specification, spec).

我们的设计可能是这样的:

1. 我们有一组账户. 每个账户都有一个数字, 代码账户余额
2. 任何账户都可以尝试向其它任何账户转账任意金额的资金
3. 转账首先检查是否有足够的资金. 如果有, 金额将从第一个账户扣除, 并添加到第二个账户
4. 转账是不可中断的, 可以同时发生多笔转账

规范具有一组“行为”，或者说是可能的不同执行方式。对于规范的正确性，每个行为都必须满足我们系统的所有要求或属性。”没有账户可以透支” 就是一个属性示例，如果规范的某个行为在一个状态下存在账户余额为负数，就违反了这个属性。其他所有可能的行为没有透支是不重要的。我们正在寻找罕见的设计错误，所以只要有一个违反就足够了。

“任何账户都不能透支 “是一个不变的属性，是每个行为的每个状态都必须成立的属性。

一旦我们编写了规范和属性，就可以将它们输入 “模型检查器”(model checker)。模型检查器接收规范，生成每一种可能的行为，并查看它们是否都满足我们的所有属性。如果有一个不满足，它就会返回一个 “错误跟踪”，显示如何重现违规行为。TLA+ 有几种不同的模型检查器，但最常用的是 TLC，它与工具箱捆绑在一起。除非我另有说明，否则当我谈到模型检查器时，我指的就是 TLC。

现在，我们无法检查所有可能的行为。事实上，由于我们还可以在系统中添加更多账户和转账，因此这些行为的数量是无限的。因此，我们要检查某些限制条件下的所有行为，例如 “三个账户的所有行为，每个账户最多 10 美元，以及两次转账，每次转账最多 10 美元”。我们将这组运行时参数以及我们所做的所有其他模型检查配置称为模型。

这意味着通过模型并不能保证规格正确。也许只有在参数较大时才会出现错误。但根据经验，我们在规范中发现，大多数错误都出现在很小的范围内：如果一个系统能在 3 个 worker 的情况下工作，那么它也很可能能在 25 个worker的情况下工作。

那么，这一切在实践中是什么样的呢？让我们来介绍一下电汇的规范，首先是硬编码参数，然后是模型参数化参数。

---- MODULE wire ----
EXTENDS TLC, Integers

People == {"alice", "bob"}
Money == 1..10
NumTransfers == 2

(* --algorithm wire
variables
  acct \in [People -> Money];

define
  NoOverdrafts ==
    \A p \in People:
      acct[p] >= 0
end define;

process wire \in 1..NumTransfers
variable
  amnt \in 1..5;
  from \in People;
  to \in People
begin
  Check:
    if acct[from] >= amnt then
      Withdraw:
        acct[from] := acct[from] - amnt;
      Deposit:
        acct[to] := acct[to] + amnt;
    end if;
end process;
end algorithm; *)

====

解释下上面的代码：

• 定义使用 ==
• People 和 Money 是集合，是唯一且无序值的集合。编程语言大多使用数组和 map（分别是序列和结构），而集合在规范中的基础性更强。
• [People -> Money] 也是一个集合（这里是函数集合）。它代表了所有可能的人与钱的分配：Alice 有 5 美元，Bob 有 1 美元；Alice 有 10 美元，Bob 有 6 美元，等等。
• 变量 acct 并不是一个固定值，而是 100 个不同值中的一个，[People -> Money] 的每个元素都有一个。当我们对此进行建模检查时，TLC 将从这 100 个可能的初始值中的每一个开始，探索每一种可能的行为。
• NoOverdrafts 是一个量词(quantifier)。如果每个账户都 >= 0，则为 true，否则为 false。在 Python 中，这可能等同于 all([acct[p] >= 0 for p in People])。量词是 TLA+ 的一个非常强大的功能，可以轻松编写非常复杂的属性。
• 我们有多个转账进程同时运行。当 NumTransfers == 2 时，规格中有两个进程。但如果我们愿意，可以选择十个、一百个或一千个进程，限制因素只有我们的耐心和内存。
• 算法的每一步都属于一个单独的标签(label)。标签决定了哪些是原子发生的，哪些是可以被其他进程打断的。这样，我们就可以表示竞赛条件。

设计完成后，我们可以根据一些要求对其进行模型检查。我们可以建立一个模型，然后说 “NoOverdrafts “是一个不变量。然后，运行模型将检查系统演化的每一种可能方式。如果其中任何一种方式导致 NoOverdrafts 为 false，那么模型检查程序就会引发错误。

我们用两次转账进行了检查。但如果我们想用四次转印来检查呢？TLA+ 可以让我们轻松改变设计。我们可以设置任何参数值，然后让不同的模型使用不同的值进行检查。

---- MODULE wire ----
 EXTENDS TLC, Integers
-
-People == {"alice", "bob"}
-Money == 1..10
-NumTransfers == 2
+CONSTANTS People, Money, NumTransfers
 
 (* --algorithm wire
 variables

现在，我可以制作不同的模型，具有相同的不变量，但同时转账的次数不同。因此，我可以看到它在一次转账时工作正常，但在两次转账时就不正常了。