概念概述

To justify the value of TLA+, let’s talk about how it’s useful, and how it’s different from programming languages. 为了安利TLA+，我们来谈一谈它的实用性，以及它与编程语言有何不同。

Imagine we’re building a wire transfer service for a bank. Users can make transfers to other users. As a requirement, we don’t allow any wires that would overdraft the user’s account, or make it go below zero dollars. At a high level, the could would look like this: 需求是为银行写一个电子转账服务。用户可以给其他用户转账。需求之一是不允许任何用户的账户透支，账户余额也不能为负数。那么这个方法的实现可能长这样：

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

This would satisfy the requirement: if you try to transfer more than you have, the guard prevents you. 这个实现是满足需求的：当你试图超支，保护语句会把你拦下。

Now consider two changes: 考虑两个新场景：

  1. Users can start more than one transfer at a time. 用户同一时间有可能发起多笔转账。

  2. Transfer steps are nonatomic. One transfer can start and (potentially) finish while another transfer is ongoing. 转账步骤没有原子性。一笔转账还没完成，另一笔转账可能发起，甚至可能已经完成了。

Neither change by itself causes a problem. But both of them together leads to a possible race condition: 以上两个场景，单拎出来没啥问题，不过同时出现的话就会出现竞争条件（race condition）问题：

  1. Alice has 6 dollars in her account, and makes two transfers to Bob. Transfer X is for 3 dollars, and transfer Y is for 4 dollars. Alice账户中有6美元，对Bob发起了两笔转账，其中转账X额度为3美元，转账Y额度为4美元。

  2. Guard(X) runs. Because 3 < 6, we go on to Withdraw(X). Guard(X) 语句生效，由于3 < 6，分支走向Withdraw(X)。

  3. Before Withdraw(X) happens, Guard(Y) runs. Because 4 < 6, we go on to Withdraw(Y). 在Withdraw(X)落地之前，Guard(X) 语句生效，由于4 < 6，分支走向Withdraw(Y)。

  4. Both withdrawals run, taking 7 dollars out of Alice’s account and leaving her with -1. 于是两个Withdraw操作都生效了，Alice共计给Bob转账7美元，最终账户余额为-1美元。

If Withdraw(X) happens before Guard(Y), then there’s no problem; transfer Y will simply fail. Race conditions like this are fundamentally rare: most of the time, the program will behave as expected and maintain our properties. It’s only in very particular orderings of events that we have a bug. That’s why concurrency errors are so far hard to find. 如果Withdraw(X)在Guard(Y)开始之前执行完毕落地了，就没有问题；转账Y会直接失败。这种竞争条件基本很罕见：在大多数情况下，程序会按预期的方式执行，从而保护了我们的属性（指的是账户余额）。但是当事件的顺序变得诡异了，就会出现缺陷。这就是并发错误很难找到的原因。

That’s also why they’re hard to fix. Imagine if we added a third feature, say a lock in the right place, to fix the bug. Does the issue go away because we’ve solved it, or because we’ve made it rarer? Without being able to explore the actual consequences of the designs, we can’t guarantee we’ve solved anything. 这也是并发错误很难修复的原因。设想我们在上述的程序中某个地方引入一个锁，试图修复竞争条件的问题，这样刚才的问题确实得到了修复，但是这么做真的完全修复了吗？也许仅仅是让竞争条件更难以复现而已。若无法探寻设计产生的所有实际结果，我们无法保证程序是没有缺陷的。

The purpose of TLA+, then, is to programmatically explore these design issues. We want to give the tooling a system and a requirement and it can tell us whether or not we can break the requirement. If it can, then we know to change our design. If it can’t, we can be more confident that we’re correct. 这就是TLA+设计的初衷了：以编程的方式来探寻设计上的问题。我们给工具一个系统和一个需求，这个工具能告诉我们当前的设计是不是会破坏这个需求。如果需求被设计破坏了，那就需要更改设计了。如果需求没有被破坏，我们就可以充分相信自己的设计是正确的。

Structure - 结构

So there’s three parts to the conceptual framework of TLA+. 因此，TLA+的概念框架分为三个部分。

First, we need to describe the system and what it can do. This is called the specification, or spec. Our design might look like this: 第一个称为规约（specification），我们借此描述系统，以及系统能做什么。规约大约会设计为：

  • We have a set of accounts. Each account has a number, representing the balance. 定义一个账户的集合。每个账户都携带一个数字，代表账户余额。

  • Any account can attempt to transfer any amount of money to any other account. 任意账户可以对其他账户进行任意额度的转账。

  • A transfer first checks if there are sufficient funds. If there are, the amount is subtracted from the first account and added to the second. 对于每次转账，首先判断发起人的账户余额是否充足。如果充足，就把转账金额从发起方账户额度中扣掉，添加给接收方。

  • Transfers are nonatomic. Multiple transfers can happen concurrently. 转账不是原子性的，多笔转账可以同时进行。

The specification has a set of “behaviors”, or possible distinct executions. For the spec to be correct, every behavior must satisfy all of our system requirements, or properties. “No account can overdraft” is an example property, and is violated if there’s a behavior of the spec has a state where an account has a negative balance. It doesn’t matter if all of the other possible behaviors don’t have overdrafts. We’re looking for rare design error, so just one violation is enough. 规约包含一个“行为”的集合，或者可以称之为所有可能的不同执行方式。为了保证规约是正确的，每个行为都必须满足所有的系统需求，或者可以称之为系统属性。比如，“账户不能透支”就是一种系统属性，当规约中的某一个行为会导致某个账户的余额为负数的状态出现的时候，就意味着这个属性被违反了。如果所有的行为都不会导致账户透支，就没什么问题。我们使用TLA+要找的是设计错误，证明属性被违反一次就足够了。

“No account can overdraft” is an invariant property, which is one that must be true of every single state of every single behavior. There are other, more advanced properties, like liveness and action properties, which we’ll cover in time. “账户不能透支”是一个不变量属性，也就是说，每个行为导致系统状态发生变化后，这个属性都应该为true。除此之外，还有一些高阶的属性，比如活跃属性和行为属性，后边会陆续讲到。

Once we’ve written a spec and properties, we feed them into a “model checker”. The model checker takes the spec, generates every possible behavior, and sees if they all satisfy all of our properties. If one doesn’t, it will return an “error trace” showing how to reproduce the violation. There are a couple different model checkers for TLA+, but the most popular one is TLC, which is bundled with the toolbox. Unless I say otherwise, when I talk about model checkers I’m referring to TLC. 当我们完成规约和属性后，就把它们交给“模型检查器”。模型检查器基于规约，生成每一个可能的行为，然后看这些行为是否都满足属性。如果有一个不满足，就会返回一个“错误追踪”，展示如何复现这个违反过程。TLA+中有很多不同的模型检查器，不过最受欢迎的当属TLC，这是TLA+工具箱中内置的模型检查器。除非特别说明，之后的模型检查器都是指TLC。

Now we can’t check every possible behavior. In fact there’s an infinite number of them, since we can also add more accounts and transfers to the system. So we instead check all the behaviors under certain constraints, such as “all behaviors for three accounts, of up to 10 dollars in each account, and two transfers, of up to 10 dollars in each transfer.” We call this set of runtime parameters, along with all the other model checker configuration we do, the model. 我们无法检查每一个可能的行为。事实上，可能的行为有无数种，比如我们可以为上面的系统多添加几个账户和转账操作。因此，取而代之的是，我们要给检查明确一个特定的限制，比如“三个余额不大于10美元的账户，和没比转账不超过10美元的转账的所有行为”。我们把这一些运行时的参数，称之为模型。

This means that a passing model doesn’t guarantee the spec is correct. Maybe there’s an error that only appears with larger parameters. But empirically, in specification we’ve found that most errors appear with very small scopes: if a system works with 3 workers, it’ll probably also work with 25 workers. 这就意味着传入的模型并不能保证规约就是正确的。也许参数更多的时候，才会发生错误。不过根据经验，大部分的错误都会在小范围的参数内能够发现：如果一个系统在3个人的情况下能正常工作，那么25个人依然有可能是正常工作的。

Specifications - 规约

So what does this all look like in practice? Let’s present a spec for wire transfers, first with hardcoded parameters and then with model-parameterizable ones. 事件中，规约是什么样子的？我们来看一个电子转账的例子。首先对参数进行硬编码，然后再把参数模型化。

Over the rest of the book I’ll be covering how all of this works syntactically. For now I just want to call attention to various parts that TLA+ does different from code: 整个教程会覆盖上述的代码是如何工作的。不过现在只谈一下上述TLA+代码中的变量部分。

  • Definitions use ==. Sorry I don’t make the rules 使用== 定义变量。别喷我，反正规则不是我定的。

  • People and Money are sets, collections of unique and unordered values. While programming languages mostly use arrays and key-value maps (Sequences and Structures respectively), sets are a lot more foundational in specification. People 和Money 是集合，即一组不重复的、无序的值。编程语言大多数使用数组和字典（TLA+中分别为序列和结构体），规约中更常用的数据结构是集合。

  • [People -> Money] is also a set (in this case, a function set). It represents all possible assignments of people to money amounts: alice has 5 dollars and bob 1, alice 10 dollars and bob 6, etc. [People -> Money] 也是一个集合（函数集合）。这个语句表示所有用户和余额的可能的赋值：Aliace账户有5美元 & Bob账户有1美元，Alice账户有10美元 & Bob账户有6美元，等等。

  • The variable acct isn’t a fixed value, it is one of 100 different values, one for each element of [People -> Money]. When we model check this, TLC will explore every possible behavior starting from every one of these 100 possible initial values. 变量acct 不是固定值，而是100种可能性中的1个，每一个都是集合[People -> Money]里的一个元素。当我们针对它进行模型检查的时候，TLC会始于这100种初始状态，进而遍历每种初始状态的每一个可能的行为。

  • NoOverdrafts is a quantifier. It’s true if every account is >= 0 and false otherwise. In python, this might be equivalent to all([acct[p] >= 0 for p in People]). Quantifiers are an extremely powerful feature of TLA+, making it easy to write very complex properties. NoOverdrafts 是一个量词。当账户余额大于等于0时，返回true，否则返回false。如果用Python，这个语句相当于：all([acct[p] >= 0 for p in People])。量词是TLA+中一个很强大的feature，能够简化非常复杂的属性的实现。

  • We have more than one wire process running simultaneously. With NumTransfers == 2, there are two processes in the spec. But we can choose to have ten, a hundred, or a thousand processes if we really wanted, with only our patience and our RAM as limiting factors. 有多个wire 进程同时在运行。通过定义NumTransfers == 2，规约中描述了两个进程。不过只要我们有耐心，RAM的空间也足够大，可以改为10个、100个、1000个进程，

  • Each step of the algorithm belongs to a separate label. The labels determine what happens atomically and what can be interrupted by another process. That way we can represent race conditions. 算法的每一步都包含在一个标签中。通过标签，我们可以定义哪些操作是原子性的，哪些操作可以被其他进程打断。如此一来，我们的描述就引入了竞争条件。

Models - 模型

Once we have our design, we can model check it against some requirements. We can make a model and say that NoOverdrafts is an invariant. Then running the model will check every possible way the system can evolve. If any of those ways leads to a state where NoOverdrafts is false, then the model checker will raise an error. 当我们完成设计后，可以通过模型检查来看它是否满足一些需求。可以定义一个模型，说明NoOverdrafts是一个不变量。然后通过执行模型，检查系统的每一个可能的演进方向。如果有任何一个方向会导致NoOverdrafts的结果为false，模型检查器就会抛出一个错误。

If you want to run this yourself, see Setup. 如果你想自己执行一遍，可以看一下环境配置。

We checked it with two transfers. But what if we wanted to check it with four transfers? TLA+ makes it very easy to change our designs. We can parameterize any value, and then have different models check with different values. 上面的代码中，我们使用两笔转账来检查。不过如果我们想使用四笔转账来检查，使用TLA+也可以方便地进行修改。我们可以把任意值参数化，然后对不同的值使用不同的模型检查。

Now I can make separate models, with the same invariant, but different numbers of simultaneous transfers. So I can see that it works correctly with one transfer but not two. 这样一来，我就可以区分模型了，使用不同的同时进行的转账的数量，检查同一个不变量。执行完就会发现，1笔转账的时候，不变量能够通过，2笔转账同时进行的话，就不行了。

Discussion - 讨论

There’s a few concepts I haven’t introduced here: temporal properties, fairness, stutter-invariance, etc. All of these will be covered later. Hopefully, though, this is enough to give you a sense of what, if you decide to learn TLA+, you’ll actually be able to do with it. If you’re interested in continuing, check out the Core and Setup. 还有一些概念这里没有介绍：时序属性，公平性，stutter不变性等等。以上都会在教程的剩余部分讲到。不过，如果你已经决定了要学习TLA+，希望本章已经足以让你感受到什么是TLA+，并且知道它能够做什么。如果对接下来的章节依然有兴趣，就继续看核心和环境配置。

Previous最新更新Next术语表

Last updated