Symmetry in the Bakery Algorithm (NuSMV)

Description of the Case Study

Lamport’s Bakery algorithm is a mutual exclusion protocol for concurrent processes. The symmetry property states that no specific process is privileged in terms of a faster access to the critical section, which is a desirable property because it implies that concrete process ids are not relevant for faster accesses. Symmetry is a hyperproperty that can be expressed with different HyperLTL formulas

\[\begin{split}\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)\end{split}\]

\[\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 \\ &\quad \neg(select_{\pi_A} < 3) \lor \neg(select_{\pi_B} < 3) \big) \ \mathcal{R} \\ &\quad \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 \\ &\quad \neg(select_{\pi_A} < 3) \lor \neg(select_{\pi_B} < 3) \lor \\ &\quad \neg \mathsf{sym}(sym\_break_{\pi_A}, sym\_break_{\pi_B}) \big) \ \mathcal{R} \\ &\quad \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_{\text{sym}_1} =\ & \forall \pi_A . \exists \pi_B . \Box \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \land (pause_{\pi_A} = pause_{\pi_B}) \land \\ &\quad (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B})\end{split}\]

\[\begin{split}\begin{aligned} \varphi_{\text{sym}_2} =\ & \forall \pi_A . \exists \pi_B . \Box \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \land (pause_{\pi_A} = pause_{\pi_B}) \land \\ &\quad (select_{\pi_A} < 3) \land (select_{\pi_B} < 3) \land \\ &\quad (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \end{aligned}\end{split}\]

In these formulas, each process \(P_{n}\) has a program counter \(pc(P_{n})\); select indicates which process is selected to process next; \(\text{pause}\) if both processes are not selected; \(\text{sym_break}\) is which process is selected after a tie; and sym(\(\text{select}\pi_{A}\) , \(\text{select}\pi_{B}\) ) indicates if two traces exchange the process ids of which processes proceeds. The basic Bakery algorithm does not satisfy symmetry (i.e. \(\varphi_{sym_{1}}\)), because when two or more processes are trying to enter the critical section with the same ticket number, the process with the smaller process ID has priority and process ID is statically fixed attribute. HyperQB returns SAT using the \(\text{pessimistic}\) semantics, indicating that there exists a counterexample to symmetry in the form of a falsifying witness to \(\pi_{A}\) in formula \(\varphi_{sym_{1}}\). The tool returns an observable witness within finite bound using the the pessimistic semantics. Therefore, we conclude that all future observations violate the property

Benchmarks

Case #1.1Case #1.2Case #1.3Case #1.4

The Model(s)

Bakery 3 Processes

--BAKERY ALGORITHM
MODULE main
	VAR
		-- p1_status: 0..2; -- 0: non-critical, 1: waiting, 2: critical
		-- p2_status: 0..2; -- 0: non-critical, 1: waiting, 2: critical
		-- p3_status: 0..2; -- 0: non-critical, 1: waiting, 2: critical

		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

		-- TOKEN: 1..3;

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

		-- STARTED : boolean;
		-- p1_TOKEN : boolean;
		-- p2_TOKEN : boolean;
		-- p3_TOKEN : boolean;


	ASSIGN

		-- init(STARTED) := FALSE;
		-- next(STARTED) :=
		-- 	case
		-- 		((p1_line != 0) | (p2_line != 0) | (p3_line != 0)) : TRUE;
		-- 		TRUE : FALSE;
		-- 	esac;

		-- init(p1_TOKEN) := FALSE;
		-- next(p1_TOKEN) :=
		-- 	case
		-- 		STARTED & (p1_line = 2) & ((p1_ticket < p2_ticket) & (p1_ticket < p3_ticket)) : TRUE;
		-- 		TRUE : FALSE;
		-- 	esac;

		-- init(p2_TOKEN) := FALSE;
		-- next(p2_TOKEN) :=
		-- 	case
		-- 		STARTED & (p2_line = 2) & (((p2_ticket < p1_ticket) & (p2_ticket < p3_ticket)) | !p1_TOKEN) : TRUE;
		-- 		TRUE : FALSE;
		-- 	esac;

		-- init(p3_TOKEN) := FALSE;
		-- next(p3_TOKEN) :=
		-- 	case
		-- 		STARTED & (p3_line = 2) & (((p3_ticket < p1_ticket) & (p3_ticket < p2_ticket)) | ((!p1_TOKEN) & (!p2_TOKEN))) : TRUE;
		-- 		TRUE : FALSE;
		-- 	esac;

			-- case
			-- 	(TOKEN=1) : {2,3};
			-- 	(TOKEN=2) : {1,3};
			-- 	(TOKEN=3) : {1,2};
			-- esac;
		-- init(p1_status) := 0;
		-- init(p2_status) := 0;
		-- init(p3_status) := 0;

		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(p3_line) := 1;



		-- init(TOKEN) := 1;
		-- next(TOKEN) :=
		-- 	case
		-- 		-- (p1_ticket > p2)
		-- 		(p1_line=3) : {1}; -- p1 has priority
		-- 		(p2_line=3) : {2};
		-- 		(p3_line=3) : {3};
		-- 		TRUE: {1,2,3};
		-- 	esac;
		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;

		-- This assignment tells me which line I execute next
		next(p1_line) :=
			case
				-- (TOKEN!=1) : p1_line;
				(p1_line=0) : {0,1};  -- stay, or proceed
				-- (p1_line=2 & !(TOKEN=1)) : {2}; -- draw ticket
				(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)));



	-- DEFINE
	-- 	CRITICAL := (proc1.line=3);
	-- 	SYM_SELECTED :=

--
-- MODULE a_process(my_ticket, others_ticket, my_status, others_status, MAX_ticket, ProcID, TOKEN)
-- 	VAR
-- 		line: 1..5;
--
--

	-- ASSIGN
	-- 	init(line) := 1;
	-- 	-- This assignment tells me which line I execute next
	-- 	next(line) :=
	-- 		case
	-- 			(ProcID!=TOKEN) : line;
	-- 			(line=1) : {1,2};  -- stay, or proceed
	-- 			(line=2) : 3;
	-- 			(line=3) & (others_status=2 | (others_status=1 & ProcID=2))  : 3 ; -- if some smaller IDs are trying
	-- 																																				-- keep waiting
	-- 			(line=3) & !(others_status=2 | (others_status=1 & ProcID=2))  : 4 ; -- go to critical section
	-- 			(line=4) : {5}; -- stay in critical section, or leave
	-- 			(line=5) : 1; -- back to starting point
	-- 		esac;
	--
	-- 	next(my_status) :=
	-- 		case
	-- 			(line=1) : 0;
	-- 			(line=2) : 0;
	-- 			(line=3) : 1;
	-- 			(line=4) : 2;
	-- 			(line=5) : 0;
	-- 			TRUE : my_status;	-- default case
	-- 		esac;
	--
	-- 	next(MAX_ticket):=
	-- 	  case
	-- 			(MAX_ticket=3): 0; --reset
	-- 			(line=2): MAX_ticket+1;
	-- 			!(line=2): MAX_ticket;
	-- 		esac;
	--
	-- 	next(my_ticket):=
	-- 		case
	-- 			(MAX_ticket=3): 0; --reset
	-- 			(line=2): MAX_ticket+1;
	-- 			!(line=2): my_ticket;
	-- 		esac;
	--
	--
	-- 	next(others_ticket) := others_ticket;	-- don't change it.
	-- 	next(others_status) := others_status;	-- don't change it.
	--
	-- 	DEFINE
	-- 		-- CHOSED:= (TOKEN=ProcID);
	-- 		STAND_BY := line=1;
	-- 		DRAW_TICKET := line=2;
	-- 		ATTEMPT := line=3;
	-- 		CRITICAL_SECTION := line=4;
	-- 		FINISHED := line=5;


-- For TESTING only
-- LTLSPEC F(proc1.my_status=1)

Formula

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_TOKEN[A] = p3_TOKEN[B])
        &(p3_TOKEN[A] = p2_TOKEN[B])
        &(p2_line[A] = p3_line[B])
        &(p3_line[A] = p2_line[B])
    )
)