Black-White Bakery Algorithm Made RW-Safe

doi:10.3390/computers15030196

2026-04-03

Libero Nigro *

Franco Cicirelli

DOI：10.3390/computers15030196

原文链接

查看原文

摘要

En 中文

Lamport的面包店算法是解决N ≥ 2个并发/并行进程的互斥问题的著名、简单且优雅的解决方案。然而，该算法会生成无界的票数，即使只有2个进程参与仲裁。文献中提出了各种方案来限制票数。但无论如何，几乎所有这些方案在仅使用原子寄存器（AR）时都被证明是正确的。当与非原子寄存器（NAR）一起工作时，它们会变得不正确，这种情况可能出现在具有多端口内存和宽松内存总线控制的嵌入式硬件平台中，例如微控制器、基于FPGA的系统或专用网络设备。一种具有有界票数的解决方案是Taubenfeld的黑白面包店（BWB）算法。BWB依赖于票对，形式为，其中mycolor可以是黑色或白色，而number的范围在[0, N]内。BWB也被非正式推理证实，仅在使用AR时是正确的。本文的主要贡献是对BWB进行重新表述，该版本在Uppaal工具箱中被形式化建模并由时间自动机进行彻底验证。在重新表述中，票对被编码为单个整数，并根据BWB逻辑进行解码和处理。重新表述的BWB在AR下无论进程数量N如何都保持完全正确，并且对于N = 2个进程，它在NAR下也是正确的。作为进一步的原创贡献，本文证明，2进程的BWB版本可以嵌入到一个通用的、最先进的基于二叉锦标赛树（TT）的解决方案中，使其成为AR/NAR正确的，即对于任意数量的进程都是RW-safe的。然而，由于模型复杂性，BWB的TT版本（即基于原子和非原子寄存器的版本）的正确性主要通过Java中形式化模型被简化为演员后的随机模拟进行研究。

Keyword:

concurrent/parallel programming

mutual exclusion

Lamport’s Bakery algorithm

unbounded tickets

Black-White Bakery algorithm

bounded tickets

atomic registers

non-atomic registers

formal modelling

timed automata

model checking