Symmetry: Bakery Algorithm (NuSMV)

Description of the Case Study

Lamport’s Bakery algorithm [Lam74] is a classic first-come-first-served mutual exclusion protocol in which each process draws a ticket and enters the critical section once it observes that it holds the smallest number. While safety and liveness are guaranteed, the algorithm breaks ties using the intrinsic process identifier, potentially privileging lower-numbered processes. We examine symmetry: if two executions differ only by swapping process identifiers, the resulting behaviour should remain indistinguishable. The case study models configurations with 3, 7, 9, and 11 processes. HyperQB explores the reachable state space under pessimistic semantics, so any bounded counterexample to symmetry generalises to an infinite execution that demonstrates asymmetric access to the critical section.

The NuSMV model(s)

--BAKERY ALGORITHM
MODULE main
	VAR
		p1_ticket: 0..3; -- the ticket number of p1
		p2_ticket: 0..3; -- the ticket number of p2
		p3_ticket: 0..3; -- the ticket number of p2

		MAX_ticket: 0..3; -- let's say max ticket number is 3

		p1_line: 0..4;
		p2_line: 0..4;
		p3_line: 0..4;

	ASSIGN
		init(p1_ticket) := 3; -- set to MAX
		init(p2_ticket) := 3; -- set to MAX
		init(p3_ticket) := 3; -- set to MAX



		init(p1_line) := 0;
		init(p2_line) := 0;
		init(p3_line) := 0;
		init(MAX_ticket):= 0;
		next(MAX_ticket):=
			case
				(MAX_ticket=3): 0; --reset
				((p1_line=1) | (p2_line=1) | (p3_line=1)): (MAX_ticket+1);
				TRUE: MAX_ticket;
			esac;

		
		next(p1_line) :=
			case
				(p1_line=0) : {0,1};  -- stay, or proceed
				(p1_line=1) : {2}; -- draw ticket
				((p1_line=2) & !p1_TOKEN) : {2}; -- check TOKEN
				((p1_line=2) & p1_TOKEN) : {3}; -- check TOKEN
				(p1_line=3) : {4}; -- stay in critical section, or leave
				(p1_line=4) : {0}; -- back to starting point
				TRUE: p1_line;
			esac;

		next(p1_ticket):=
			case
				(MAX_ticket=3): 0; --reset
				(p1_line=1): MAX_ticket+1;
				TRUE: p1_ticket;
			esac;


		next(p2_line) :=
			case
				(p2_line=0) : {0,1};  -- stay, or proceed
				(p2_line=1) : {2};
				((p2_line=2) & !p2_TOKEN): {2}; -- check TOKEN
				((p2_line=2) & p2_TOKEN): {3}; -- check TOKEN
				(p2_line=3) : {4}; -- stay in critical section, or leave
				(p2_line=4) : {0}; -- back to starting point
				TRUE: p2_line;
			esac;

		next(p2_ticket):=
			case
				(MAX_ticket=3): 0; --reset
				(p2_line=1): MAX_ticket+1;
				TRUE: p2_ticket;
			esac;


		next(p3_line) :=
			case
				(p3_line=0) : {0};  -- stay, or proceed
				(p3_line=1) : {2};
				((p3_line=2) & !p3_TOKEN) : 2 ; -- check TOKEN
				((p3_line=2) & p3_TOKEN) : 3 ; -- check TOKEN
				(p3_line=3) : {4}; -- stay in critical section, or leave
				(p3_line=4) : {0}; -- back to starting point
				TRUE: p3_line;
			esac;


		next(p3_ticket):=
			case
				(MAX_ticket=3): 0; --reset
				(p3_line=1): MAX_ticket+1;
				TRUE: p3_ticket;
			esac;


	DEFINE
		STARTED  := ( (p1_line!=0) | (p2_line!=0) | (p3_line!=0));

		p1_TOKEN := (STARTED) & (p1_line=2) & (p1_ticket <= p2_ticket) & (p1_ticket <= p3_ticket);

		p2_TOKEN := (STARTED) & (p2_line=2) & (((p2_ticket <= p1_ticket) & (p2_ticket <= p3_ticket)) | (!p1_TOKEN));

		p3_TOKEN := (STARTED) & (p3_line=2) & (((p3_ticket <= p1_ticket) & (p3_ticket <= p2_ticket)) | ((!p1_TOKEN) & (!p2_TOKEN)));

The HyperLTL formula(s)

Symmetry can be expressed by relating pairs of traces that exchange process identifiers yet follow the same scheduling choices. The formulas below progressively reinforce the equality constraints on ticket selection and tie-breaking. HyperQB reports SAT for the standard Bakery implementation, producing witnesses that show how lower-numbered processes retain priority even when tickets match.

\[\varphi_{S1} = \forall \pi_A . \forall \pi_B . \left( \neg \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \lor \neg(pause_{\pi_A} = pause_{\pi_B}) \right) \mathcal{R} \left( (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \right)\]
\[\begin{split}\varphi_{S2} = {} & \forall \pi_A . \forall \pi_B . \big( \neg \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \lor \neg(pause_{\pi_A} = pause_{\pi_B}) \lor \neg(select_{\pi_A} < 3) \lor \neg(select_{\pi_B} < 3) \big) \ \mathcal{R} \\ & \big( (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \big)\end{split}\]
\[\begin{split}\varphi_{S3} = {} & \forall \pi_A . \forall \pi_B . \big( \neg \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \lor \neg(pause_{\pi_A} = pause_{\pi_B}) \lor \neg(select_{\pi_A} < 3) \lor \neg(select_{\pi_B} < 3) \lor \neg \mathsf{sym}(sym\_break_{\pi_A}, sym\_break_{\pi_B}) \big) \ \mathcal{R} \\ & \big( (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \big)\end{split}\]
\[\varphi_{\text{sym}_1} = \forall \pi_A . \exists \pi_B . \Box \Big( \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \land (pause_{\pi_A} = pause_{\pi_B}) \land (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \Big)\]
\[\begin{split}\varphi_{\text{sym}_2} = {} & \forall \pi_A . \exists \pi_B . \Box \Big( \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \land (pause_{\pi_A} = pause_{\pi_B}) \land (select_{\pi_A} < 3) \land (select_{\pi_B} < 3) \\ & \qquad \land (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \Big)\end{split}\]

The predicate \(sym(x_{\pi_A}, x_{\pi_B})\) asserts that traces \(\pi_A\) and \(\pi_B\) coincide up to a swap of process identifiers; select and pause capture the scheduler state; and sym_break records which process wins the tie after equal tickets. The program counter \(pc(P_n)\) tracks the stage of process \(P_n\) in the Bakery protocol. Together these constraints detect any trace where identifier swapping changes the observed behaviour.

Forall A . Exists B .
G(
    (
        (p1_TOKEN[A] = p2_TOKEN[B])
        &(p2_TOKEN[A] = p1_TOKEN[B])
        &(p1_line[A] = p2_line[B])
        &(p2_line[A] = p1_line[B])
    )
    &
    (
        (p1_TOKEN[A] = p3_TOKEN[B])
        &(p3_TOKEN[A] = p1_TOKEN[B])
        &(p1_line[A] = p3_line[B])
        &(p3_line[A] = p1_line[B])
    )
    &
    (
        (p2_line[A] = p3_line[B])
        &(p3_line[A] = p2_line[B])
    )
)

References