Surfing Complexity Lorin Hochstein 关于软件、复杂系统和事故的思考。

使用 FizzBee 建模锁、租约和 Fencing Tokens

Lorin Hochstein formal methods 2025年3月3日 7分钟

FizzBee 是一种新的形式化规约语言，最初在去年五月发布。 FizzBee 的作者 Jayaprabhakar (JP) Kadarkarai 最近联系我，问我对它的看法，所以我决定尝试一下。

为了体验 FizzBee，我决定对一些解决互斥问题的算法进行建模，这个问题通常被称为锁。互斥算法是形式化建模的经典用例，这里有一些额外的背景动机：几年前，Martin Kleppmann (优秀书籍 Designing Data-Intensive Applications 的作者，通常被称为 DDIA) 和 Salvatore Sanfilippo (Redis 的创建者，更广为人知的网名是 antirez) 之间发生了一场在线争论。他们争论的是一种名为 Redlock 的算法的正确性，该算法声称可以实现容错分布式锁。以下是一些相关链接：

• Distributed Locks with Redis - Redlock 算法的描述
• How to do distributed locking - Kleppmann 对 Redlock 算法的评论
• Is Redlock safe? - antirez 对 Kleppmann 的反驳

作为 FizzBee 的练习，我想看看对 Kleppmann 在 Redlock 中发现的问题进行建模有多困难。

请记住，我只是一个语言新手，写一些非常简单的模型作为学习练习。

临界区

这是我的第一个 FizzBee 模型，它模拟了两个进程的执行，并带有一个不变式，该不变式声明最多只能有一个进程同时处于临界区。请注意，此模型实际上并未强制执行互斥，因此我只是想看看断言是否被违反。

# Invariant to check
always assertion MutualExclusion:
  return not any([p1.in_cs and p2.in_cs for p1 in processes
                     for p2 in processes
                     if p1 != p2])
NUM_PROCESSES = 2
role Process:
  action Init:
    self.in_cs = False
  action Next:
    # before critical section
    pass
    # critical section
    self.in_cs = True
    pass
    # after critical section
    self.in_cs = False
    pass
action Init:
  processes = []
  for i in range(NUM_PROCESSES):
    processes.append(Process())

“pass” 语句是空操作，我只是将它们用作“在临界区之前/期间/之后执行的代码”的占位符。

FizzBee 构建在 Starlark 上，Starlark 是 Python 的一个子集，这就是为什么该模型看起来如此 Pythonic。编写 FizzBee 模型感觉就像编写 PlusCal 模型，无需显式指定标签，并且语法也更加熟悉。

缺少标签既是福也是祸。在 PlusCal 中，控制状态是您可以在模型中显式引用的内容。当您想将临界区指定为不变量时，这非常有用。因为 FizzBee 没有标签，所以我必须创建一个名为“in_cs”的单独变量才能对进程何时处于其临界区进行建模。但总的来说，我发现 PlusCal 的标签语法很烦人，我很高兴 FizzBee 不需要它。

FizzBee 有一个 在线 playground：您可以复制上面的模型并将其直接粘贴到 playground 中，然后单击“Run”，它会告诉您不变量失败。

FAILED: Model checker failed. Invariant: MutualExclusion

“Error Formatted”视图显示了两个进程都落在了第 17 行，因此违反了互斥：

锁

接下来，我在 FizzBee 中对锁进行了建模。一般来说，我喜欢将锁建模为一个集合，获取锁意味着将进程的 ID 添加到集合中，因为如果需要，我可以看到：

• 谁持有锁（通过集合的元素）
• 如果两个进程以某种方式设法获取了同一个锁（集合中的多个元素）

这是我的 FizzBee 模型：

always assertion MutualExclusion:
  return not any([p1.in_cs and p2.in_cs for p1 in processes
                     for p2 in processes
                     if p1 != p2])
NUM_PROCESSES = 2
role Process:
  action Init:
    self.in_cs = False
  action Next:
    # before critical section
    pass
    # acquire lock
    atomic:
      require not lock
      lock.add(self.__id__)
    #
    # critical section
    #
    self.in_cs = True
    pass
    self.in_cs = False
    # release lock
    lock.clear()
    # after critical section
    pass
action Init:
  processes = []
  lock = set()
  in_cs = set()
  for i in range(NUM_PROCESSES):
    processes.append(Process())

默认情况下，FizzBee 中的每个语句都被视为原子的，您可以指定一个 atomic 块来自动处理多个语句。

如果您在 playground 中运行此程序，您会看到不变量成立，但存在不同的问题：死锁

DEADLOCK detected
FAILED: Model checker failed

FizzBee 的模型检查器默认执行两件事：

1. 检查死锁
2. 假设线程可以在任何任意语句之后崩溃

在“Error Formatted”视图中，您可以看到发生了什么。第一个进程获取了锁，然后崩溃了。这会导致死锁，因为锁永远不会被释放。

租约

如果我们想构建一个容错的锁解决方案，我们需要处理进程在拥有锁时发生故障的情况。Redlock 算法使用了租约的概念，即在一段时间后过期的锁。

为了对租约进行建模，我们现在需要对时间进行建模。为了简单起见，我的模型假设所有进程都可以访问全局时钟。

NUM_PROCESSES = 2
LEASE_LENGTH = 10

always assertion MutualExclusion:
  return not any([p1.in_cs and p2.in_cs for p1 in processes
                     for p2 in processes
                     if p1 != p2])
action AdvanceClock:
  clock += 1
role Process:
  action Init:
    self.in_cs = False
  action Next:
    atomic:
      require lock.owner == None or \
          clock >= lock.expiration_time
      lock = record(owner=self.__id__,
             expiration_time=clock+LEASE_LENGTH)
    # check that we still have the lock
    if lock.owner == self.__id__:
      # critical section
      self.in_cs = True
      pass
      self.in_cs = False
      # release the lock
      if lock.owner == self.__id__:
        lock.owner = None
action Init:
  processes = []
  # global clock
  clock = 0
  lock = record(owner=None, expiration_time=-1)
  for i in range(NUM_PROCESSES):
    processes.append(Process())

现在锁有一个到期日期，所以我们不再有死锁问题。但是不变量不再总是成立。

FizzBee 还有一个很棒的视图，称为“Explorer”，您可以在其中逐步查看状态变量如何随时间变化。这是一张屏幕截图，显示了问题：

问题在于一个进程可能认为它持有锁，但该锁实际上已经过期，这意味着另一个进程可以获取该锁，并且它们最终都可能进入临界区。

Fencing Tokens

Kleppmann 指出了 Redlock 的这个问题，即它很容易受到进程的执行可能暂停一段时间（例如，由于垃圾收集）的问题的影响。Kleppmann 提议使用 fencing tokens 来防止进程使用过期的锁访问共享资源。

以下是我如何对 fencing tokens 进行建模：

NUM_PROCESSES = 2
LEASE_LENGTH = 10
always assertion MutualExclusion:
  return not any([p1.in_cs and p2.in_cs for p1 in processes
                     for p2 in processes
                     if p1 != p2])
atomic action AdvanceClock:
  clock += 1
role Process:
  action Init:
    self.in_cs = False
  action Next:
    atomic:
      require lock.owner == None or \
          clock >= lock.expiration_time
      lock = record(owner=self.__id__,
             expiration_time=clock+LEASE_LENGTH)
      self.token = next_token
      next_token += 1
    # can only enter the critical section
    # if we have the highest token seen so far
    atomic:
      if self.token > last_token_seen:
        last_token_seen = self.token
        # critical section
        self.in_cs = True
        pass
    # after critical section
    self.in_cs = False
    # release the lock
    atomic:
      if lock.owner == self.__id__:
        lock.owner = None
action Init:
  processes = []
  # global clock
  clock = 0
  next_token = 1
  last_token_seen = 0
  lock = record(owner=None, expiration_time=-1)
  for i in range(NUM_PROCESSES):
    processes.append(Process())

但是，如果您通过模型检查器运行此程序，您会发现不变量也被违反了！

事实证明，fencing tokens 不能防止两个进程都认为自己持有锁的情况，并且较低的 token 在较高的 token 之前到达共享资源：

fencing tokens 无法确保互斥的场景

我联系了 Martin Kleppmann 询问此事，他同意 fencing tokens 无法防止这种情况。

印象

我发现 FizzBee 出乎意料地容易上手，尽管我只是在这里触及了表面。就我而言，拥有 PlusCal 的经验帮助很大，因为我已经知道如何以类似的风格编写规范。您可以像编写 TLA+ 风格的规范一样，将其写成一系列原子操作，而不是写成一个大的非原子操作，但对于我正在建模的这些特定问题，PlusCal 风格感觉更自然。

对于程序员来说，Pythonic 语法将比 PlusCal 和 TLA+ 更熟悉，这应该有助于采用。但在某些情况下，我发现自己错过了 TLA+ 和 Alloy 等语言支持的集合符号的简洁性。我最终利用了 Python 的列表推导式，它们具有集合构建器符号的感觉。

形式化规约的新手仍然需要学习如何以 TLA+ 风格的模型进行思考：虽然 FizzBee 看起来像 Python，但在概念上它就像 TLA+，是用于指定一组状态机行为的符号，这与 Python 程序非常不同。我不知道这对学习者来说会是什么样子。

我对 FizzBee 默认线程能够在任何任意点崩溃的行为有点困惑，但这是可配置的，我能够很好地利用它来显示上面锁模型中的死锁。

最后，虽然我多年前读过 Kleppmann 的文章，但我从未注意到 fencing tokens 的问题，直到我真正尝试显式地建模它。这很好地提醒了正式指定算法的价值。我自欺欺人地认为我理解了它，但我实际上并没有。直到我完成了建模练习，我才发现了它行为的一些我以前没有意识到的东西。