基于原子步同时访问swap与fetch-and-increment对象的三进程无等待共识算法实现问询

前置定义 #

• swap对象：支持原子交换共享寄存器与本地寄存器的值。
• fetch-and-increment（F&I）对象：支持原子将共享寄存器值加1并返回其先前值。
• 允许单个原子步同时访问swap与F&I对象，执行期间其他进程无法操作这两个对象。

共享组件初始化 #

• swap_reg（swap对象）：初始值为0
• fi_reg（F&I对象）：初始值为0
• first_prop（共享原子寄存器）：初始值为0，用于存储首个完成复合操作进程的提案
• prop_1/prop_2/prop_3（共享原子寄存器）：分别对应进程P1/P2/P3的提案存储，初始值为0

每个进程Pi的执行步骤 #

1. 写入提案：原子性地将自身的共识提案写入对应的prop_i。
2. 原子复合操作：执行一个不可分割的原子步骤，同时完成：
   • 调用fi_reg.fetch_and_increment()，将返回的票号存入本地变量my_ticket（三个进程将分别拿到0、1、2）。
   • 调用swap_reg.swap(prop_i)，将返回的旧值存入本地变量prev_val。
3. 确定共识值：
   • 若my_ticket == 0：
     • 共识值为自身提案prop_i。
     • 原子性地将prop_i写入first_prop，供后续进程读取。
   • 若my_ticket == 1：
     • prev_val即为首个进程的提案，将其作为共识值。
     • 可选：原子性地将prev_val写入first_prop，确保第三个进程无需额外交互。
   • 若my_ticket == 2：
     • 原子性读取first_prop的值，将其作为共识值。

正确性验证 #

• 无等待性：每个进程仅需执行固定次数的原子操作，无需等待其他进程，满足无等待要求。
• 一致性：
  • 票号my_ticket由F&I对象原子生成，确保三个进程拿到唯一的0、1、2。
  • 首个进程（ticket=0）的提案是共识基准，first_prop寄存器保证所有进程最终获取到同一值。
  • ticket=1的进程通过swap操作原子获取到首个进程的提案，不会被其他进程干扰。
• 有效性：共识值必然是某个进程的原始提案，符合共识算法的有效性约束。

内容的提问来源于stack exchange，提问作者Algo