在现实世界中使用TLA+了解Glibc错误

TLA+是一种正式的规范语言，您可以使用它来验证程序。它与其他正式验证系统的不同之处在于它非常实用。它不是写校样，而是使用简单的方法运行程序的所有可能执行。您可以编写断言，如果它们对于任何可能的执行都不是真的，它会告诉您通过程序的最短路径来破坏您的断言。

事实上，它非常实用，甚至允许您用类似于C语言的语言编写代码。

我最近听说了glibc条件变量实现中的一个bug，由于我以前使用过TLA+来验证我自己的互斥体和条件变量，所以我想我应该调查一下。您能用它在现实世界的复杂代码中找到这个bug吗？是的，你几乎不能，这并不容易，但它给了我希望，程序验证真的变得很好，已经能够处理又大又乱的代码：

首先，让我们来谈谈这个bug是什么。这里又是链接。问题是，有时pthreadcondignal()什么也不做。这是条件变量的pthread实现的一部分，条件变量用于线程之间的通信。如果线程A告诉线程B它需要开始处理某件事，那么您必须确保线程B没有处于休眠状态，因此您可以使用pthreadcondignal()来唤醒它。如果没有发生唤醒，很容易导致系统死锁。(例如，如果线程A稍后等待线程B，它将永远等待)。

这个是在哪里用的？到处都是。几乎所有的编程语言都为这个调用提供了包装器，或者在内部使用它来协调线程。这可能会在许多C和C++程序中导致错误(C++在标准库中有一个用于pthreadcond()的包装器)，以及至少.NET core、Python和Ocaml的运行时。(根据对该漏洞的评论)。

现在我不在glibc上工作，所以我只能感觉到，对于一个外部观察者来说，进展看起来很慢。这个漏洞是在4月份报告的(但你可以在那之前找到人们)，从那时起，除了几天前的一些新评论外，它几乎一直保持沉默。我甚至在邮件列表上找不到对话。我怀疑问题的一部分是代码非常棘手，错误真的很难理解。目前还不清楚修复会是什么样子。一个变通方法发布得相当快，但是它调用pthreadcondBroadcast()，这是一个繁重的操作，所以理想情况下我们希望避免这种情况。

使用TLA+调查错误的好处之一是，一旦您可以重现错误，就很容易尝试其他修复方法。问题中的bug非常罕见，而且需要数年时间才能被发现，那么您如何知道您的修复不会引入另一个需要数年才能发现的细微bug呢？使用TLA+，您可以检查代码中所有可能的代码路径，让您更加自信。

互斥锁是一个对象，它确保一次只有一个线程进入一段代码。如果两个线程试图进入，则第二个线程必须等到第一个线程离开。要做到这一点，最简单的方法是使用自旋锁：

这是如何工作的并不明显，但请尝试考虑当两个线程同时调用lock()时会发生什么：Exchange返回旧值，因此对于第一个线程，exchange将返回false，并且不会循环。对于第二个线程，交换将返回TRUE，并且它将循环，直到第一线程再次解锁自旋锁。这个自旋锁有很多问题，但它工作正常，足以看到TLA+的样子。让我们来实现它：

这一次很多，但不应该看起来太疯狂。首先，我们声明一个全局变量“已锁定”。然后我们编写过程lock()，它有一个局部变量“old_value”。函数体中的第一件事是标签“exchange：”。PlusCal(这种语言就是这么叫的)的规则是，两个标签之间的任何代码都是原子的。因此，“exchange：”和“check：”之间的两行总是一起执行。没有内置的交换操作，所以我实现了自己的操作，将旧状态存储在old_value中，然后将true赋给lock。在那之后，我检查该值是否已经被锁定，然后在必要时进行循环。是的，PlusCal有Gotos。它也有While循环，我们将在下面看到一个循环，但这里我选择介绍Gotos。

Unlock()过程甚至更简单。我在函数的开头需要一个标签，因为在这种语言中，每个函数都必须以标签开始。我只是将其命名为“RESET_STATE”，因为这似乎是一个合适的名称。

最后，我们添加了一个“公平进程”，它是一个独立的执行线程。“公平”一词是可选的。这意味着这个过程不会随机停止。您可能希望指定即使某些进程随机停止也是健壮的代码，但我在这里不是这样做的，所以我要使我的进程“公平”。“P\in proc”为进程提供了一个名称P，这实际上并不重要，它说该名称是从set proc中选择的，我们将在不同的位置将其定义为全局的。如果proc中有N件事，这意味着TLA+将检查N个进程的所有可能的交错。

这个过程的主体从一个标签开始，我刚才把它称为“循环”。标签在循环体之外，所以您可能认为我们只会访问它一次，但实际上规则说我们在每次循环迭代后都要返回到这个标签。(重新评估WHILE循环的条件)。

我在标签后面加了一个减号“-”，这意味着这一句话不受“公平”规则的约束。这意味着如果进程在该标签处永久停止，我声称我的代码应该仍然可以正常工作。

在循环体中，我们只调用lock()，然后调用unlock()，但是在这两者之间，我们有一个标签“cs”，后跟语句“Skip；”。跳过只是意味着我们不会为这个标签做任何事。之所以有它，是因为标签是流程可以临时暂停的地方。因此，这模拟了这样一个事实，即在实际代码中，这是您的临界区所在的位置，而该临界区可能需要一段时间。这个标签就是我们的进程必须“公平”的原因：如果我用2个进程运行这个进程，其中一个随机地决定在标签“cs”处永远停止，那么我们将永远陷入僵局。一个“公平”的进程可以在这里等待，只要它不会永远等待。

有了这些，我们就可以编写我们的第一个断言了。上面的代码是用“PlusCal”编写的，PlusCal是一种类似C的语言，可以翻译成TLA+。断言实际上必须用TLA+编写。TLA+看起来更像是数学化的，更像是乳胶般的y。(这是有道理的，因为TLA+是由创建LaTeX的Leslie Lamport编写的)下面是我们要测试的第一个断言：

TLA+中有一个热键可以将其转换为PDF，为我们提供了更好的格式：

这里有几点需要解释：pc[i]=“cs”是比较，而不是赋值。这意味着该过程当前在标签“cs”处。符号是“布尔AND”运算符，TLA+的语法是将其放在多行前面来计算所有行的合取。最后，前面的符号否定结果。

因此，总的来说，这意味着对于任何一对进程，它们不可能都在“cs”标签上。

我们要检查的第二件事是我们不会陷入僵局。我们用这个断言来做到这一点：

这句话中间的箭头很重要。这意味着，如果它左边的东西是真的，那么在未来的某个时候，右边的东西也会变成真的。在本例中，我们说如果某个进程试图获取锁，那么某个进程最终将进入临界区。请注意，我们并不是说它必须是相同的过程。有了这个自旋锁我们不能保证。我们只是说，最终会有人进入，我们不会永远陷入僵局或忙碌循环。

在TLA+中检查这些时间属性的能力是其最强大的功能之一。稍后我们还需要它来验证我们的条件变量。

所有这些就绪后，我们可以使用TLA+验证上面的陈述。用两个进程运行它(通过为proc分配一个具有两个值的集合)，TLA+会找到36种不同的状态。它们都满足了我们上面的两个断言。进程越多，发现的状态越多，但仍然没有问题。

自旋锁的问题是等待的线程不会进入休眠状态。为了支持这一点，glibc使用futex实现了它们的互斥体。Futex有两个操作：1.比较和等待。2.唤醒。如果线程在Futex上休眠，则第二个操作只是唤醒线程，第一个操作更有趣。“比较并等待”意味着它会将Futex的值与参数进行比较，并且只有在它们比较相等时才进入睡眠状态。使用示例更容易解释，所以下面是一个使用Futex实现的简单互斥锁：

我对这个互斥实现感到非常自豪。花了几个星期才把它弄得这么小。(少量的代码也让它变得非常快)。

您可能想知道原子无符号整数有什么特别之处。为什么我们可以叫Futex行动来处理它？最酷的是，它没有什么特别之处。你可以在任何东西上调用Futex操作。它只需是指向至少32位可读存储器的指针即可。现在，“比较并等待”的含义也变得更加清晰：内核将比较指针后面的内存与传入的变量(在我的例子中，这是常量“睡眠”，值为2)，如果内存比较相等，它会使线程进入休眠状态。内核将以指针地址为关键字将休眠线程存储在哈希表中。唤醒只是在相同的哈希表中查找，如果存在条目，它就唤醒该线程。

要使上面的互斥体正确，比较是至关重要的。例如，请参见以下行为序列：

读取这种情况的方法是线程A先锁定，然后线程B锁定，但在进入睡眠状态之前，线程A会再次解锁。在本例中，最后的Futex_Wait(2)将注意到2！=0，实际上不会使线程进入休眠状态。

尽管如此，仍然有很多可能的代码路径贯穿其中。特别是如果我们有三个或更多的线程。请考虑以下执行开始：

因此，有三个线程试图进入，我们在解锁时以state=1结束，这意味着线程A不会唤醒休眠线程B。这是一个bug吗？这实际上是可以的，因为线程C做的下一件事是设置state=2，所以它会记得在解锁后唤醒线程B。

但是很难考虑所有的情况，所以让我们在TLA+中实现这一点。首先，让我们实现Futex操作：

在这里，我选择实现不同于它们在内核中实现的Futex。主要是因为您不能在PlusCal中获取变量的地址。而且我们不需要全部的细节。我们只需要和真品一样的东西就行了。如果我们想检查内核Futex实现的正确性，这是不行的。但是因为我们想检查建立在Futex之上的东西的正确性，所以我们可以抽象出Futex的细节。

那么这到底是怎么运作的呢？在Futex_Wait()中，我利用了两个标签之间的所有指令都是原子的这一事实。因此，“CHECK_STATE”和“WAIT_FOR_WAKE”之间的工作立即发生。这意味着我可以进行比较，并将自己加入到睡眠者中。(这里的术语“self”指的是进程ID，而\Union是如何将您自己添加到集合中)之后，我们可以使用PlusCal关键字“await”休眠，直到我们再次被删除。这在内核中显然要复杂得多，因为C没有“等待”原语。(您将如何实现这样的关键字？使用条件变量。所以幸运的是，我们正在研究条件变量中的错误)。

FUTEX_WAKE_ALL()非常简单，因为该语言提供了神奇的“等待”关键字。我们所要做的就是清除这组卧铺，另一个过程会自动找出答案。这里我们可以看到TLA+是如何设计来验证这类代码的。它提供了魔术原语，这些原语对于抽象细节很有用。

FUTEX_WAKE_SINGLE()更复杂。首先，如果没有人睡觉，我们就提早出门。否则，我们使用“with”关键字从一组睡眠者中选择一个随机的睡眠者并将其删除。由于TLA+运行程序的所有可能执行，因此它实际上会将执行分支到此处，以使用所有可能的值继续执行。

这就是为什么我如此喜欢TLA+的原因。它是C++代码的直接一对一翻译。唯一的区别是，我们使用的是上一段中的“FUTEX_STATE”变量，而不是给它自己的全局变量。我也可以直接将其命名为“mutex_state”，但它必须是相同的变量，因为Futex就是这样工作的。我们可以用与上面相同的断言验证这是否正确，只是我使用的是不同的标签，所以我们可以在断言DeadlockFreedom中将“exchange”替换为“exchange_lock”。实际上，您可能希望使该检查稍微复杂一些，但是有关详细信息，我将向您推荐TLA+附带的“DijkstraMutex”示例。就我们这里的目的而言，使用现有的时态检查是可以的。如果您继续实际实现这段代码，我建议您插入一些有意的bug，看看TLA+是如何为您提供发现问题的最短执行路径的。(如果TLA+在对上述代码进行更改后没有发现错误，请确保您没有意外地将其转变为自旋锁，这仍然可以满足我们所有的断言)。

通过这个互斥实现，我们可以了解到的一件事是，TLA+中的状态数量是如何爆炸的。如果我验证2个进程的断言，TLA+会发现213个不同的状态，并立即结束运行。对于3个进程，TLA+查找7013个不同的状态，运行时间为3秒。让我们把它做成一张桌子：

在使用TLA+进行验证时，状态数量的激增是一个常见问题。“尝试所有可能的执行路径”的方法很快就会爆炸，我们必须调整我们的模型来处理这个问题。对于这个互斥锁，我们大部分时间可以用3个进程运行我们的模型检查器，然后一旦完成，我们可以移动多达4到5个进程进行双重检查。(我们还可以通过利用不同进程之间的对称性来大量减少状态数，但这将在稍后讨论)。

条件变量试图解决与Futex相同的问题：我想检查一些共享变量，如果它处于不正确的状态，我想一直睡到正确状态。但是条件变量更通用：Futex只能比较32位内存，而条件变量允许您等待任何条件。(在C++中，这表示允许传入lambda)。

条件变量的核心接口甚至比futex的更简单：它只有“等待”和“唤醒”操作。您已经看到，对于futex，“比较并等待”中的“比较”对于避免死锁非常重要，那么如何才能使事情变得更简单呢？通过要求条件变量必须始终与互斥锁一起使用，并且您必须遵循特定的调用顺序。服务员必须执行以下步骤：

只要您遵循这些顺序，“等待”和“唤醒”就是您需要的全部操作。

一件奇怪的事情是，服务员在调用pthreadcondwait()之后解锁互斥锁。难道不应该因为它在睡眠时抓住互斥体而陷入僵局吗？这种怪异的答案是pthreadcondwait()在休眠前在内部解锁互斥体，稍后在唤醒后重新锁定互斥体。

每个人在第一次使用条件变量时都会犯一个错误，那就是您遇到了一个步骤“更改条件”可能是原子的地方。假设它只是递增一个int。所以您会想“为什么这个整数增量受互斥锁保护？让我们改用原子int，去掉lock/unlock调用。“。这样做会导致僵局。这非常令人惊讶，但是锁定/解锁是为了获得与另一个线程的正确顺序，而不是为了保护“改变条件”。(但您也可以为此使用它)在这种情况下，您可以做的一件有趣的事情是使“更改条件”成为原子，然后在步骤1之前执行步骤2。这意味着它变成了“更改条件，lock()，unlock()，pthreadcond_ignal()”。很奇怪，空锁/解锁仍然是必要的，但是您可以通过考虑所有可能的代码路径来说服自己。另一方面，这些细节很难，所以在使用条件变量时最好只遵循正常结构。

这遵循C++命名约定，其中NOTIFY_ONE()==pthreadCOND_SIGNAL()和NOTIFY_ALL()==pthreadcond_Broadcast()。另一件需要注意的事情是，我们提供了两个Wait实现：其中一个只是一个方便的包装器，它允许您为“检查条件”步骤传入一个谓词，从而为您正确地执行循环。

它的语义非常简单，因为互斥体和Futex为我们做了大部分工作。我们唯一需要做的额外工作就是对Notify()函数中的状态变量进行一些更改，以确保并发服务员不会因为错过唤醒而睡着。我们改变什么并不重要，因为我们只需要确保它不会等同于“old_state”。加1似乎很好，因为这样做要走很长一段路，然后才会回绕。如果过快地展开，我们可能会遇到ABA问题，但是似乎不太可能在一个等待()调用的同时收到40亿个通知()调用。

因为我们现在有两个Futex，所以我必须更改Futex_Wait()和Futex_WAKE_Single()的接口。我们现在有了一份关于Futex的全球地图/字典。为此，我们有两个索引：mutex_index=0和cv_index=1。每一个索引后面都有另一个映射，其中包含我们以前拥有的“state”和“sleepers”变量。我不得不更改前面所有过程的实现，但它只是搜索/替换，所以我不显示它。Lock_mutex()和unlock()中“Futex_state”的用法被“futex[mutex_index].State”取代，其他地方也有类似的变化。

Cv_Wait()和cv_Signal()的实现再次是从C++非常机械化的翻译。然而，我们这里有一个问题。TLA+想要探索所有可能的状态，而使用我们的计数器，我们有无限多个状态，因为您总是可以将+1加到计数器上以获得新的状态。我们可以让计数器回绕，但是TLA+会立即发现错误，如果计数器回绕，我们将错过唤醒。(例如，如果我们将计数器换成16，TLA+将找到交错，其中cv_wait()被调用一次，而在它完成之前，cv_signal()被调用16次)，但是在实践中该错误永远不会发生。

这有点难以解决，但目前我们只能限制我们发出的信号数量。我们可以编写流程，只调用cv_ignal()三次，然后永远停止。如果有一个bug只有在我们调用cv_ignal()四次时才会发生，我们就不会发现该bug，但我们只能希望这种情况不会发生。(著名的最后一句话)说到流程，我们如何测试条件变量？旧的“lock-gt；cs->；unlock”测试已经不再有意义了。让我从代码开始：