Linearizability (NuSMV)¶
Description of the Case Study¶
The second study consists on verifying linearizability of the SNARK concurrent datatype [DDG+04]. SNARK implements a concurrent double-ended queue using double-compare-and-swap (DCAS) and a doubly linked-list. Linearizability [HW90] is a hyperproperty that requires that any history of execution of a concurrent data structure—where history is sequence of invocations and responses by different threads—matches some sequential order of invocations and responses.
\[\varphi_{\text{lin}} = \forall \pi_A.\exists \pi_B.\ \Box\left( \mathit{history}_{\pi_A} \leftrightarrow \mathit{history}_{\pi_B} \right)\]
SNARK is known to have two linearizability bugs. With the use of pessimistic semantics, a witness of linearizability violation of length \(k\) is enough to infer that the given system does not satisfy the linearizability property. HyperQB returns SAT identifying both bugs and producing two counterexamples. The bugs returned are consistent with the ones reported in [DDG+04].
Benchmarks¶
The Model(s)
--
-- // SNARK structure (with some accelerations):
-- // 0 ------- STAND BY: could go to line:1/ line:10/ line:19
-- // popRight() starts:
-- // 1 - getRightHat as rh
-- // 2 - getLeftHat as lh
-- // 3 - if (rh is self-pointing) return assign popRight_fAIL
-- // 4 - else if (rh equals lh)
-- // 5 DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
-- // 6 assign pop_result as rh->V
-- // 7 - else assign rhl as rh->L
-- // 8 DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
-- // 9 assign popRight_result as rh->V, assign rh->R as DUMMY
-- // pushRight() starts:
-- // 10 - assing nd as Y --> if null, return pushRight_fAIL
-- // 11 - assign nd->R as Dummy,assign nd-> V as something (zero for now)
-- // 12 - assign rh as RightHat, assign rhR as rh->R
-- // 13 if (rh == rhR), assign nd -> L = Dummy, assign lh = LeftHat
-- // 14 DCAS (RightHat, LeftHat, rh, lh, nd, nd)
-- // 15 return pushRight_SUCCESS
-- // 16 else assign nd->L as rh
-- // 17 DCAS(RightHat, rh->R, rh, rhR, nd, nd)
-- // 18 return pushRight_SUCCESS
-- // popLeft() starts:
-- // 19 - assign lh as LeftHat, assign rh as RightHat
-- // 20 - if (lh is self-pointing), return assign popLeft_fAIL
-- // 21 - else if (lh == rh)
-- // 22 DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
-- // 23 assign popLeft_result as lh -> V
-- // 24 - else assign lhR as lh->R
-- // 25 DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
-- // 26 assign popLeft_result as lh->V, assign lh_L as DDUMMY
MODULE main
VAR
fAIL: boolean;
BOTH_MODIFYING : boolean;
proc1.modifying : boolean;
proc1.popRightSTART : boolean;
proc1.popRightEND : boolean;
proc1.pushRightSTART : boolean;
proc1.pushRightEND : boolean;
proc1.popLeftSTART : boolean;
proc1.popLeftEND : boolean;
proc2.modifying : boolean;
proc2.popRightSTART : boolean;
proc2.popRightEND : boolean;
proc2.pushRightSTART : boolean;
proc2.pushRightEND : boolean;
proc2.popLeftSTART : boolean;
proc2.popLeftEND : boolean;
RightHat: 0..2; -- could be DUNNY, x, y, or z
LeftHat: 0..2; -- could be DUMMY, x, y, or z
AllNodes[0][0]: 0..2;
AllNodes[0][1]: 0..2;
AllNodes[1][0]: 0..2;
AllNodes[1][1]: 0..2;
AllNodes[2][0]: 0..2;
AllNodes[2][1]: 0..2;
First_ProcID: 1..2;
Second_ProcID: 1..2;
-- ##############################################################################
-- Proc 1 VAR
proc1.line: 0..26;
-- popRight local variables
proc1.local_popR_RH: 0..2; -- could be DUMMY, x,or y
proc1.local_popR_LH: 0..2; -- could be DUMMY, x,or y
proc1.local_popR_RHL: 0..2; -- could be DUMMY, x,or y
-- popLeft local variables
proc1.local_popL_RH: 0..2; -- could be DUMMY, x,or y
proc1.local_popL_LH: 0..2; -- could be DUMMY, x,or y
proc1.local_popL_LHR: 0..2; -- could be DUMMY, x,or y
-- pushRight local variables
proc1.local_pushR_RH: 0..2; -- could be DUMMY, x,or y
proc1.local_pushR_RHR: 0..2; -- xcould be DUMMY, x,or y
proc1.local_pushR_LH: 0..2; -- could be DUMMY, x,or y
-- ##############################################################################
-- ##############################################################################
-- Proc 2 VAR
proc2.line: 0..26;
-- popRight local variables
proc2.local_popR_RH: 0..2; -- could be DUMMY, x,or y
proc2.local_popR_LH: 0..2; -- could be DUMMY, x,or y
proc2.local_popR_RHL: 0..2; -- could be DUMMY, x,or y
-- popLeft local variables
proc2.local_popL_RH: 0..2; -- could be DUMMY, x,or y
proc2.local_popL_LH: 0..2; -- could be DUMMY, x,or y
proc2.local_popL_LHR: 0..2; -- could be DUMMY, x,or y
-- pushRight local variables
proc2.local_pushR_RH: 0..2; -- could be DUMMY, x,or y
proc2.local_pushR_RHR: 0..2; -- xcould be DUMMY, x,or y
proc2.local_pushR_LH: 0..2; -- could be DUMMY, x,or y
-- ##############################################################################
-- ##############################################################################
-- Queue VAR
newnode : 0..2; -- for push right
popRightfAIL: boolean;
-- ##############################################################################
ASSIGN
init(fAIL) := FALSE;
next(fAIL) :=
case
BOTH_MODIFYING : TRUE;
TRUE: fAIL;
esac;
init(BOTH_MODIFYING) := FALSE;
next(BOTH_MODIFYING) :=
case
(proc1.modifying & proc2.modifying) : TRUE ;
TRUE: BOTH_MODIFYING;
esac;
init(proc1.modifying) := FALSE;
next(proc1.modifying) :=
case
(proc1.line=5 | proc1.line=8 | proc1.line=14 | proc1.line=17 | proc1.line=16 | proc1.line=11 | proc1.line=22 | proc1.line=25) : TRUE;
TRUE: proc1.modifying;
esac;
init(proc1.popRightSTART) := FALSE;
next(proc1.popRightSTART) :=
case
(proc1.line=1 | proc1.line=2 | proc1.line=3 | proc1.line=4 | proc1.line=5 | proc1.line=6 | proc1.line=7 | proc1.line=8 | proc1.line=9) : TRUE;
TRUE : proc1.popRightSTART;
esac;
init(proc1.popRightEND) := FALSE;
next(proc1.popRightEND) :=
case
(proc1.line=0) : TRUE;
TRUE : proc1.popRightEND;
esac;
init(proc1.pushRightSTART) := FALSE;
next(proc1.pushRightSTART) :=
case
(proc1.line=10 | proc1.line=11 | proc1.line=12 | proc1.line=13 | proc1.line=14 | proc1.line=15 | proc1.line=16 | proc1.line=17 | proc1.line=18) : TRUE;
TRUE : proc1.pushRightSTART;
esac;
init(proc1.pushRightEND) := FALSE;
next(proc1.pushRightEND) :=
case
(proc1.line=0) : TRUE;
TRUE : proc1.pushRightEND;
esac;
init(proc1.popLeftSTART) := FALSE;
next(proc1.popLeftSTART) :=
case
(proc1.line=19 | proc1.line=20 | proc1.line=21 | proc1.line=22 | proc1.line=23 | proc1.line=24 | proc1.line=25 | proc1.line=26) : TRUE;
TRUE : proc1.popLeftSTART;
esac;
init(proc1.popLeftEND) := FALSE;
next(proc1.popLeftEND) :=
case
(proc1.line=0) : TRUE;
TRUE : proc1.popLeftEND;
esac;
init(proc2.modifying) := FALSE;
next(proc2.modifying) :=
case
(proc2.line=5 | proc2.line=8 | proc2.line=14 | proc2.line=17 | proc2.line=16 | proc2.line=11 | proc2.line=22 | proc2.line=25) : TRUE;
TRUE : proc2.modifying;
esac;
init(proc2.popRightSTART) := FALSE;
next(proc2.popRightSTART) :=
case
(proc2.line=1 | proc2.line=2 | proc2.line=3 | proc2.line=4 | proc2.line=5 | proc2.line=6 | proc2.line=7 | proc2.line=8 | proc2.line=9) : TRUE;
TRUE : proc2.popRightSTART;
esac;
init(proc2.popRightEND) := FALSE;
next(proc2.popRightEND) :=
case
(proc2.line=0) : TRUE;
TRUE : proc2.popRightEND;
esac;
init(proc2.pushRightSTART) := FALSE;
next(proc2.pushRightSTART) :=
case
(proc2.line=10 | proc2.line=11 | proc2.line=12 | proc2.line=13 | proc2.line=14 | proc2.line=15 | proc2.line=16 | proc2.line=17 | proc2.line=18) : TRUE;
TRUE : proc2.pushRightSTART;
esac;
init(proc2.pushRightEND) := FALSE;
next(proc2.pushRightEND) :=
case
(proc2.line=0) : TRUE;
TRUE : proc2.pushRightEND;
esac;
init(proc2.popLeftSTART) := FALSE;
next(proc2.popLeftSTART) :=
case
(proc2.line=19 | proc2.line=20 | proc2.line=21 | proc2.line=22 | proc2.line=23 | proc2.line=24 | proc2.line=25 | proc2.line=26) : TRUE;
TRUE : proc2.popLeftSTART;
esac;
init(proc2.popLeftEND) := FALSE;
next(proc2.popLeftEND) :=
case
(proc2.line=0) : TRUE;
TRUE : proc2.popLeftEND;
esac;
-- ##############################################################################
-- Global ASSIGN block
init(First_ProcID) := 1;
init(Second_ProcID) := 2;
next(First_ProcID) := First_ProcID;
next(Second_ProcID) := Second_ProcID;
init(RightHat) := 1;
init(LeftHat) := 1;
init(AllNodes[0][0]) := 0;
init(AllNodes[0][1]) := 0; -- DUMMY
init(AllNodes[1][0]) := 0;
init(AllNodes[1][1]) := 0; -- X
init(AllNodes[2][0]) := 2;
init(AllNodes[2][1]) := 2; -- Y
-- ##############################################################################
-- ##############################################################################
-- Proc 1 ASSIGN
init(proc1.line) := 0;
-- popRight local, all default to DUMMY
init(proc1.local_popR_RH) := 0;
init(proc1.local_popR_LH) := 0;
init(proc1.local_popR_RHL) := 0;
-- init(local_popR_return_empty):= FALSE;
-- popLeft local, all default to DUMMY
init(proc1.local_popL_RH) := 0;
init(proc1.local_popL_LH) := 0;
init(proc1.local_popL_LHR) := 0;
--pushRight local, all default to DUMMY
init(proc1.local_pushR_LH):= 0;
init(proc1.local_pushR_RH) := 0;
init(proc1.local_pushR_RHR) := 0;
next(proc1.line) :=
case
((proc1.line=0) & (First_ProcID=1)) : {1}; -- STAND BY: could go to line:1/ line:10/ line:19
((proc1.line=0) & (First_ProcID=2)) : {10,19}; -- STAND BY: could go to line:1/ line:10/ line:19
((proc1.line=1) & (First_ProcID=2)) : {1};
((proc1.line=1) & (First_ProcID=1)) : {2}; -- popRight() starts, getRightHat as rh
((proc1.line=2) & (LeftHat=1) & (RightHat=1) & (First_ProcID=1)) : {2,3};
((proc1.line=2) & (LeftHat=1) & (RightHat=2) & (First_ProcID=1)) : {2,3};
((proc1.line=3) & (proc1.local_popR_RH=1) & (AllNodes[1][1]=1)) : {0};
((proc1.line=3) & (proc1.local_popR_RH=2) & (AllNodes[2][1]=2)) : {0};
((proc1.line=3) & ((!((proc1.local_popR_RH=1) & (AllNodes[1][1]=1))) | ((proc1.local_popR_RH=2) & AllNodes[1][1]=2))) : {4};
((proc1.line=4) & ( (proc1.local_popR_RH=1) &
(proc1.local_popR_LH=1))) : {5};
((proc1.line=4) & ((proc1.local_popR_RH=2) & (proc1.local_popR_LH=2))) : {5}; -- if (rh equals lh)
(proc1.line=5) : {6}; -- DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
(proc1.line=6) : {0}; -- assign pop_result as rh->V, END
(proc1.line=4 & !((proc1.local_popR_RH=1) & proc1.local_popR_LH=1)) : {7};
(proc1.line=4 & !((proc1.local_popR_RH=2) & proc1.local_popR_LH=2)) : {7};
(proc1.line=7) : {8}; --assign rhl as rh->L
(proc1.line=8) : {9}; -- DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
(proc1.line=9) : {0}; -- assign popRight_result as rh->V, assign rh->R as DUMMY
-- pushRIGHT
(proc1.line=10) : {11}; -- pushRight() starts assing nd as Y --> if null, return pushRight_fAIL
(proc1.line=11) : {12}; -- assign nd->R as Dummy,assign nd-> V as something (zero for now)
(proc1.line=12) : {13}; -- assign rh as RightHat, assign rhR as rh->R
(proc1.line=13 & (proc1.local_pushR_RH = proc1.local_pushR_RHR)) : {14}; -- if (rh == rhR), assign nd -> L = Dummy, assign lh = LeftHat
(proc1.line=14) : {15}; -- DCAS (RightHat, LeftHat, rh, lh, nd, nd)
(proc1.line=15) : {0}; -- return pushRight_SUCCESS
(proc1.line=13 & !(proc1.local_pushR_RH = proc1.local_pushR_RHR)) : {16}; -- if !(rh == rhR) assign nd->L as rh
(proc1.line=16) : {17}; -- assign nd->L as rh
(proc1.line=17) : {18}; -- DCAS(RightHat, rh->R, rh, rhR, nd, nd)
(proc1.line=18) : {0}; -- return pushRight_SUCCESS
-- popLeft
(proc1.line=19) : {20}; --- popLeft() starts, assign lh as LeftHat, assign rh as RightHat
(proc1.line=20) : {21}; -- if(!lh is self-pointing)
(proc1.line=21 & (proc1.local_popL_LH =proc1.local_popL_RH)) : {22}; -- if(lh == rh)
(proc1.line=22) : {23}; -- DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
(proc1.line=23) : {0}; -- assign popLeft_result as lh -> V, END
(proc1.line=21 & !(proc1.local_popL_LH =proc1.local_popL_RH)) : {24}; -- if!(lh == rh)
(proc1.line=24) : {25}; -- assign lhR as lh->R
(proc1.line=25) : {26}; -- DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
(proc1.line=26) : {0}; -- assign popLeft_result as lh->V, assign lh_L as DDUMMY
TRUE: proc1.line; -- default case
esac;
-- local_popR local variables
next(proc1.local_popR_RH) :=
case
(proc1.line=1) : RightHat;
TRUE : proc1.local_popR_RH; -- default case
esac;
next(proc1.local_popR_LH) :=
case
(proc1.line=2) : LeftHat;
TRUE : proc1.local_popR_LH; -- default case
esac;
next(proc1.local_popR_RHL) :=
case
!(proc1.line=7) : proc1.local_popR_RHL;
(proc1.line=7 & (proc1.local_popR_RH=0)) : AllNodes[0][0];
(proc1.line=7 & (proc1.local_popR_RH=1)) : AllNodes[1][0];
(proc1.line=7 & (proc1.local_popR_RH=2)) : AllNodes[2][0];
TRUE : proc1.local_popR_RHL; -- default case
esac;
-- local_pushR local variables
next(proc1.local_pushR_RH) :=
case
(proc1.line=12): RightHat;
TRUE: proc1.local_pushR_RH;
esac;
next(proc1.local_pushR_LH) :=
case
(proc1.line=13 & (proc1.local_pushR_RH = proc1.local_pushR_RHR)): LeftHat;
TRUE: proc1.local_pushR_LH;
esac;
next(proc1.local_pushR_RHR) :=
case
(proc1.line=12 & proc1.local_pushR_RH = 0): AllNodes[0][1];
(proc1.line=12 & proc1.local_pushR_RH = 1): AllNodes[1][1];
(proc1.line=12 & proc1.local_pushR_RH = 2): AllNodes[2][1];
TRUE: proc1.local_pushR_RHR;
esac;
next(proc1.local_popL_LH) :=
case
(proc1.line=19) : LeftHat;
TRUE : proc1.local_popL_LH; -- default case
esac;
next(proc1.local_popL_RH) :=
case
(proc1.line=19) : RightHat;
TRUE : proc1.local_popL_RH; -- default case
esac;
next(proc1.local_popL_LHR) :=
case
(proc1.line=24 & proc1.local_popL_LH=0) : AllNodes[0][1];
(proc1.line=24 & proc1.local_popL_LH=1) : AllNodes[1][1];
(proc1.line=24 & proc1.local_popL_LH=2) : AllNodes[2][1];
TRUE : proc1.local_popL_LHR; -- default case
esac;
-- ##############################################################################
-- ##############################################################################
-- Proc 2 ASSIGN
init(proc2.line) := 0;
-- popRight local, all default to DUMMY
init(proc2.local_popR_RH) := 0;
init(proc2.local_popR_LH) := 0;
init(proc2.local_popR_RHL) := 0;
-- init(local_popR_return_empty):= FALSE;
-- popLeft local, all default to DUMMY
init(proc2.local_popL_RH) := 0;
init(proc2.local_popL_LH) := 0;
init(proc2.local_popL_LHR) := 0;
--pushRight local, all default to DUMMY
init(proc2.local_pushR_LH):= 0;
init(proc2.local_pushR_RH) := 0;
init(proc2.local_pushR_RHR) := 0;
next(proc2.line) :=
case
-- STNAD BY
(proc2.line=0 & Second_ProcID=1) : {1}; -- STAND BY: could go to line:1/ line:10/ line:19
(proc2.line=0 & Second_ProcID=2) : {10,19}; -- STAND BY: could go to line:1/ line:10/ line:19
-- popRIGHT() start
(proc2.line=1 & Second_ProcID=2) : {1};
(proc2.line=1 & Second_ProcID=1) : {2}; -- popRight() starts, getRightHat as rh
(proc2.line=2 & LeftHat=1 & RightHat=1 & Second_ProcID=1) : {2,3};
(proc2.line=2 & LeftHat=1 & RightHat=2 & Second_ProcID=1) : {2,3};
(proc2.line=3 & (proc2.local_popR_RH=1) & (AllNodes[1][1]=1)) : {0};
(proc2.line=3 & (proc2.local_popR_RH=2) & (AllNodes[2][1]=2)) : {0};
(proc2.line=3 & !((proc2.local_popR_RH=1) & AllNodes[1][1]=1)| (proc2.local_popR_RH=2) & AllNodes[1][1]=2) : {4};
(proc2.line=4 & (proc2.local_popR_RH=1 &
proc2.local_popR_LH=1)) : {5};
(proc2.line=4 & (proc2.local_popR_RH=2 & proc2.local_popR_LH=2)) : {5}; -- if (rh equals lh)
(proc2.line=5) : {6}; -- DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
(proc2.line=6) : {0}; -- assign pop_result as rh->V, END
(proc2.line=4 & !(proc2.local_popR_RH=1 & proc2.local_popR_LH=1)) : {7};
(proc2.line=4 & !(proc2.local_popR_RH=2 & proc2.local_popR_LH=2)) : {7};
(proc2.line=7) : {8}; --assign rhl as rh->L
(proc2.line=8) : {9}; -- DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
(proc2.line=9) : {0}; -- assign popRight_result as rh->V, assign rh->R as DUMMY
-- pushRIGHT
(proc2.line=10) : {11}; -- pushRight() starts assing nd as Y --> if null, return pushRight_fAIL
(proc2.line=11) : {12}; -- assign nd->R as Dummy,assign nd-> V as something (zero for now)
(proc2.line=12) : {13}; -- assign rh as RightHat, assign rhR as rh->R
(proc2.line=13 & (proc2.local_pushR_RH = proc2.local_pushR_RHR)) : {14}; -- if (rh == rhR), assign nd -> L = Dummy, assign lh = LeftHat
(proc2.line=14) : {15}; -- DCAS (RightHat, LeftHat, rh, lh, nd, nd)
(proc2.line=15) : {0}; -- return pushRight_SUCCESS
(proc2.line=13 & !(proc2.local_pushR_RH = proc2.local_pushR_RHR)) : {16}; -- if !(rh == rhR) assign nd->L as rh
(proc2.line=16) : {17}; -- assign nd->L as rh
(proc2.line=17) : {18}; -- DCAS(RightHat, rh->R, rh, rhR, nd, nd)
(proc2.line=18) : {0}; -- return pushRight_SUCCESS
-- popLeft
(proc2.line=19) : {20}; --- popLeft() starts, assign lh as LeftHat, assign rh as RightHat
(proc2.line=20) : {21}; -- if(!lh is self-pointing)
(proc2.line=21 & (proc2.local_popL_LH =proc2.local_popL_RH)) : {22}; -- if(lh == rh)
(proc2.line=22) : {23}; -- DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
(proc2.line=23) : {0}; -- assign popLeft_result as lh -> V, END
(proc2.line=21 & !(proc2.local_popL_LH =proc2.local_popL_RH)) : {24}; -- if!(lh == rh)
(proc2.line=24) : {25}; -- assign lhR as lh->R
(proc2.line=25) : {26}; -- DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
(proc2.line=26) : {0}; -- assign popLeft_result as lh->V, assign lh_L as DDUMMY
TRUE: proc2.line; -- default case
esac;
-- local_popR local variables
next(proc2.local_popR_RH) :=
case
(proc2.line=1) : RightHat;
TRUE : proc2.local_popR_RH; -- default case
esac;
next(proc2.local_popR_LH) :=
case
(proc2.line=2) : LeftHat;
TRUE : proc2.local_popR_LH; -- default case
esac;
next(proc2.local_popR_RHL) :=
case
!(proc2.line=7) : proc2.local_popR_RHL;
(proc2.line=7 & proc2.local_popR_RH=0) : AllNodes[0][0];
(proc2.line=7 & proc2.local_popR_RH=1) : AllNodes[1][0];
(proc2.line=7 & proc2.local_popR_RH=2) : AllNodes[2][0];
TRUE : proc2.local_popR_RHL; -- default case
esac;
-- local_pushR local variables
next(proc2.local_pushR_RH) :=
case
(proc2.line=12): RightHat;
TRUE: proc2.local_pushR_RH;
esac;
next(proc2.local_pushR_LH) :=
case
(proc2.line=13 & (proc2.local_pushR_RH = proc2.local_pushR_RHR)): LeftHat;
TRUE: proc2.local_pushR_LH;
esac;
next(proc2.local_pushR_RHR) :=
case
(proc2.line=12 & proc2.local_pushR_RH = 0): AllNodes[0][1];
(proc2.line=12 & proc2.local_pushR_RH = 1): AllNodes[1][1];
(proc2.line=12 & proc2.local_pushR_RH = 2): AllNodes[2][1];
TRUE: proc2.local_pushR_RHR;
esac;
next(proc2.local_popL_LH) :=
case
(proc2.line=19) : LeftHat;
TRUE : proc2.local_popL_LH; -- default case
esac;
next(proc2.local_popL_RH) :=
case
(proc2.line=19) : RightHat;
TRUE : proc2.local_popL_RH; -- default case
esac;
next(proc2.local_popL_LHR) :=
case
(proc2.line=24 & proc2.local_popL_LH=0) : AllNodes[0][1];
(proc2.line=24 & proc2.local_popL_LH=1) : AllNodes[1][1];
(proc2.line=24 & proc2.local_popL_LH=2) : AllNodes[2][1];
TRUE : proc2.local_popL_LHR; -- default case
esac;
-- ##############################################################################
-- ##############################################################################
-- Queue ASSIGN
init(newnode) := 2;
next(newnode) := newnode;
-- to cehck, use GlobalQueue-popRightfAIL[tid]
init(popRightfAIL) := FALSE;
next(popRightfAIL) :=
case
((proc1.line=3) & ((proc1.local_popR_RH=1) & (AllNodes[1][1]=1))) : TRUE;
((proc1.line=3) & ((proc1.local_popR_RH=2) & (AllNodes[2][1]=2))) : TRUE;
((proc2.line=3) & (proc2.local_popR_RH=0)) : TRUE;
TRUE: popRightfAIL;
esac;
next(RightHat) :=
case
BOTH_MODIFYING : RightHat;
(((proc1.line=5) & !(fAIL)) | ((proc2.line=5) & !(fAIL))) : 0; -- set to DUMMY
(((proc1.line=22) & (RightHat=proc1.local_popL_RH)) | ( (proc2.line=22) & (RightHat=proc2.local_popL_RH))) : 0; -- set to DUMMY
-- DCAS
((proc1.line=8) & !(fAIL) & (proc1.local_popR_RHL=0)) : 0; -- set to RH->L 0
((proc1.line=8) & !(fAIL) & (proc1.local_popR_RHL=1)) : 1; -- set to RH->L 0
((proc1.line=8) & !(fAIL) & (proc1.local_popR_RHL=2)) : 2; -- set to RH->L 0
-- DCAS
((proc2.line=8) & !(fAIL) & (proc2.local_popR_RHL=0)) : 0; -- set to RH->L 0
((proc2.line=8) & !(fAIL) & (proc2.local_popR_RHL=1)) : 1; -- set to RH->L 0
((proc2.line=8) & !(fAIL) & (proc2.local_popR_RHL=2)) : 2; -- set to RH->L 0
((proc1.line=14) | (proc2.line=14)) : 2; -- set to newnode
(((proc1.line=16) & (RightHat=proc1.local_pushR_RH)) | ((proc2.line=16) & (RightHat=proc2.local_pushR_RH))) : 2;
TRUE: RightHat;
esac;
next(LeftHat) :=
case
BOTH_MODIFYING : LeftHat;
--- SWAP if DCAS
(((proc1.line=5) & !(fAIL)) | ((proc2.line=5) & !(fAIL))) : 0; -- set to DUMMY
-- SWAP if DCAS
(((proc1.line=22) & (RightHat=proc1.local_popL_RH)) | ((proc2.line=22) & (RightHat=proc2.local_popL_RH))) : 0; -- set to DUMMY
((proc1.line=25) & (proc1.local_popL_LHR=0)) : 0; -- set to LH->R 0
((proc1.line=25) & (proc1.local_popL_LHR=1)) : 1; -- set to LH->R 0
((proc1.line=25) & (proc1.local_popL_LHR=2)) : 2; -- set to LH->R 0
((proc2.line=25) & (proc2.local_popL_LHR=0)) : 0; -- set to LH->R 0
((proc2.line=25) & (proc2.local_popL_LHR=1)) : 1; -- set to LH->R 0
((proc2.line=25) & (proc2.local_popL_LHR=2)) : 2; -- set to LH->R 0
((proc1.line=14) | (proc2.line=14)) : 2; --set to newnode
TRUE: LeftHat;
esac;
--- GLOBAL variables for double-ended queue
next(AllNodes[0][0]) := AllNodes[0][0]; -- DUMMY
next(AllNodes[0][1]) := AllNodes[0][1]; -- DUMMY
-- X -> L
next(AllNodes[1][0]) :=
case
BOTH_MODIFYING: AllNodes[1][0]; --?
((proc1.line=8) & !(fAIL) & (proc1.local_popR_RH=1)): 1;
((proc1.line=26) & (proc1.local_popL_LH=1) & (LeftHat=1)): 0;
((proc2.line=8) & !(fAIL) & (proc2.local_popR_RH=1)): 1;
((proc2.line=26) & (proc2.local_popL_LH=1) & (LeftHat=1)): 0;
TRUE: AllNodes[1][0];
esac;
-- X -> R
next(AllNodes[1][1]) :=
case
BOTH_MODIFYING : AllNodes[1][1]; --?
((proc1.line=17) & (proc1.local_pushR_RH=1)): 2; -- newnode
((proc1.line=25) & !(fAIL) & (proc1.local_popL_LH=1)): 1;
((proc1.line=9) & (proc1.local_popR_RH=1)& (RightHat=1)): 0;
((proc2.line=17) & (proc2.local_pushR_RH=1)): 2; -- newnode
((proc2.line=25) & !(fAIL) & (proc2.local_popL_LH=1)): 1;
((proc2.line=9) & (proc2.local_popR_RH=1) & (RightHat=1)): 0;
TRUE: AllNodes[1][1];
esac;
-- Y -> L
next(AllNodes[2][0]) :=
case
BOTH_MODIFYING : AllNodes[2][0];
((proc1.line=8) & !(fAIL) & (proc1.local_popR_RH=2)) : 2;
-- ?
((proc1.line=26) & (proc1.local_popL_LH=2) & (LeftHat=2)): 0;
((proc1.line=16) & (proc1.local_pushR_RH=1)): 1;
((proc1.line=16) & (proc1.local_pushR_RH=2)): 2;
((proc2.line=8) & !(fAIL) & (proc2.local_popR_RH=2)) : 2;
-- ?
((proc2.line=26) & (proc2.local_popL_LH=2) & (LeftHat=2)): 0;
((proc2.line=16) & (proc2.local_pushR_RH=1)): 1;
((proc2.line=16) & (proc2.local_pushR_RH=2)): 2;
TRUE: AllNodes[2][0];
esac;
-- Y -> R
next(AllNodes[2][1]) :=
case
BOTH_MODIFYING : AllNodes[2][1];
(proc1.line=11): 0;
((proc1.line=9) & (proc1.local_popR_RH=2) & (RightHat=2)): 0;
((proc1.line=25) & !(fAIL) & (proc1.local_popL_LH=2)): 2;
(proc2.line=11): 0;
((proc1.line=9) & (proc1.local_popR_RH=2) & (RightHat=2)): 0;
((proc2.line=25) & !(fAIL) & (proc2.local_popL_LH=2)): 2;
TRUE: AllNodes[2][1];
esac;
-- ##############################################################################
DEFINE
-- ##############################################################################
-- Proc1 DEFINE
-- proc1.modifying := (proc1.line=5 | proc1.line=8 | proc1.line=14 | proc1.line=17 | proc1.line=16 | proc1.line=11 | proc1.line=22 | proc1.line=25);
-- proc1.popRightSTART := proc1.line=1 | proc1.line=2 | proc1.line=3 | proc1.line=4 | proc1.line=5 | proc1.line=6 | proc1.line=7 | proc1.line=8 | proc1.line=9;
-- proc1.popRightEND := proc1.line=0;
-- proc1.pushRightSTART := proc1.line=10 | proc1.line=11| proc1.line=12 | proc1.line=13 | proc1.line=14 | proc1.line=15 | proc1.line=16 | proc1.line=17 | proc1.line=18;
-- proc1.pushRightEND := proc1.line=0;
-- proc1.popLeftSTART := proc1.line=19 | proc1.line=20 | proc1.line=21 | proc1.line=22 | proc1.line=23 | proc1.line=24 | proc1.line=25 | proc1.line=26;
-- proc1.popLeftEND := proc1.line=0;
-- ##############################################################################
-- ##############################################################################
-- Proc2 DEFINE
-- proc2.modifying := (proc2.line=5 | proc2.line=8 | proc2.line=14 | proc2.line=17 | proc2.line=16 | proc2.line=11 | proc2.line=22 | proc2.line=25);
-- proc2.popRightSTART := proc2.line=1 | proc2.line=2 | proc2.line=3 | proc2.line=4 | proc2.line=5 | proc2.line=6 | proc2.line=7 | proc2.line=8 | proc2.line=9;
-- proc2.popRightEND := proc2.line=0;
-- proc2.pushRightSTART := proc2.line=10 | proc2.line=11| proc2.line=12 | proc2.line=13 | proc2.line=14 | proc2.line=15 | proc2.line=16 | proc2.line=17 | proc2.line=18;
-- proc2.pushRightEND := proc2.line=0;
-- proc2.popLeftSTART := proc2.line=19 | proc2.line=20 | proc2.line=21 | proc2.line=22 | proc2.line=23 | proc2.line=24 | proc2.line=25 | proc2.line=26;
-- proc2.popLeftEND := proc2.line=0;
-- ##############################################################################
-- ##############################################################################
-- Queue DEFINE
-- BOTH_MODIFYING := (proc1.modifying & proc2.modifying);
-- fAIL := ((proc1.line=5) & (!(RightHat=proc1.local_popR_RH)| !(LeftHat=proc1.local_popR_LH))) |((proc1.line=8) & ( !(RightHat=proc1.local_popR_RH)| !(proc1.local_popR_RH=1 -> (AllNodes[1][0]=proc1.local_popR_RHL)) | !(proc1.local_popR_RH=2 -> (AllNodes[2][0]=proc1.local_popR_RHL))))|((proc1.line=22) & ( !(RightHat=proc1.local_popL_RH) | !(LeftHat=proc1.local_popL_LH)))|((proc1.line=25) & ( !(LeftHat=proc1.local_popL_LH) | !(proc1.local_popL_LH=1 -> (AllNodes[1][1]=proc1.local_popL_LHR)) | !(proc1.local_popL_LH=2 -> (AllNodes[2][1]=proc1.local_popL_LHR)))) |((proc1.line=13) & RightHat=2) |((proc2.line=13) & RightHat=2) |((proc2.line=20) & RightHat=0 & RightHat=0) | BOTH_MODIFYING;
-- ##############################################################################
--
-- // SNARK structure (with some accelerations):
-- // 0 ------- STAND BY: could go to line:1/ line:10/ line:19
-- // popRight() starts:
-- // 1 - getRightHat as rh
-- // 2 - getLeftHat as lh
-- // 3 - if (rh is self-pointing) return assign popRight_fAIL
-- // 4 - else if (rh equals lh)
-- // 5 DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
-- // 6 assign pop_result as rh->V
-- // 7 - else assign rhl as rh->L
-- // 8 DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
-- // 9 assign popRight_result as rh->V, assign rh->R as DUMMY
-- // pushRight() starts:
-- // 10 - assing nd as Y --> if null, return pushRight_fAIL
-- // 11 - assign nd->R as Dummy,assign nd-> V as something (zero for now)
-- // 12 - assign rh as RightHat, assign rhR as rh->R
-- // 13 if (rh == rhR), assign nd -> L = Dummy, assign lh = LeftHat
-- // 14 DCAS (RightHat, LeftHat, rh, lh, nd, nd)
-- // 15 return pushRight_SUCCESS
-- // 16 else assign nd->L as rh
-- // 17 DCAS(RightHat, rh->R, rh, rhR, nd, nd)
-- // 18 return pushRight_SUCCESS
-- // popLeft() starts:
-- // 19 - assign lh as LeftHat, assign rh as RightHat
-- // 20 - if (lh is self-pointing), return assign popLeft_fAIL
-- // 21 - else if (lh == rh)
-- // 22 DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
-- // 23 assign popLeft_result as lh -> V
-- // 24 - else assign lhR as lh->R
-- // 25 DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
-- // 26 assign popLeft_result as lh->V, assign lh_L as DDUMMY
MODULE main
VAR
-- ##############################################################################
RightHat: 0..2;
-- could be DUNNY, x, y, or z
LeftHat: 0..2;
-- could be DUMMY, x, y, or z
AllNodes[0][0]: 0..2;
AllNodes[0][1]: 0..2;
AllNodes[1][0]: 0..2;
AllNodes[1][1]: 0..2;
AllNodes[2][0]: 0..2;
AllNodes[2][1]: 0..2;
First_ProcID: 1..2;
Second_ProcID: 1..2;
-- ##############################################################################
-- ##############################################################################
-- Proc 1 VAR
proc1.line: 0..9;
-- ##############################################################################
-- ##############################################################################
-- Proc 2 VAR
proc2.line: 0..9;
-- ##############################################################################
-- ##############################################################################
-- Queue Var
newnode : 0..2;
-- for push right
popRightfAIL: boolean;
temp_popRightfAIL: boolean;
BOTH_MODIFYING : boolean;
proc1.popRightSTART : boolean;
proc1.popRightEND : boolean;
proc1.pushRightSTART : boolean;
proc1.pushRightEND : boolean;
proc1.popLeftSTART : boolean;
proc1.popLeftEND : boolean;
proc1.modifying : boolean;
proc2.popRightSTART : boolean;
proc2.popRightEND : boolean;
proc2.pushRightSTART : boolean;
proc2.pushRightEND : boolean;
proc2.popLeftSTART : boolean;
proc2.popLeftEND : boolean;
proc2.modifying : boolean;
-- ##############################################################################
ASSIGN
init(proc2.popRightSTART) := FALSE;
next(proc2.popRightSTART) :=
case
(proc2.line=1 | proc2.line=2 | proc2.line=3) : TRUE;
TRUE : proc2.popRightSTART;
esac;
init(proc2.popRightEND) := FALSE;
next(proc2.popRightEND) :=
case
(proc2.line=0) : TRUE;
TRUE : proc2.popRightEND;
esac;
init(proc2.pushRightSTART) := FALSE;
next(proc2.pushRightSTART) :=
case
(proc2.line=4 | proc2.line=5) : TRUE;
TRUE : proc2.pushRightSTART;
esac;
init(proc2.pushRightEND) := FALSE;
next(proc2.pushRightEND) :=
case
(proc2.line=0) : TRUE;
TRUE : proc2.pushRightEND;
esac;
init(proc2.popLeftSTART) := FALSE;
next(proc2.popLeftSTART) :=
case
(proc2.line=7 | proc2.line=8) : TRUE;
TRUE : proc2.popLeftSTART;
esac;
init(proc2.popLeftEND) := FALSE;
next(proc2.popLeftEND) :=
case
(proc2.line=0) : TRUE;
TRUE : proc2.popLeftEND;
esac;
init(proc2.modifying) := FALSE;
next(proc2.modifying) :=
case
(proc2.line=1 | proc2.line=4 | proc2.line=7) : TRUE;
TRUE : proc2.modifying;
esac;
init(proc1.popRightSTART) := FALSE;
next(proc1.popRightSTART) :=
case
(proc1.line=1 | proc1.line=2 | proc1.line=3) : TRUE;
TRUE : proc1.popRightSTART;
esac;
init(proc1.popRightEND) := FALSE;
next(proc1.popRightEND) :=
case
(proc1.line=0) : TRUE;
TRUE : proc1.popRightEND;
esac;
init(proc1.pushRightSTART) := FALSE;
next(proc1.pushRightSTART) :=
case
(proc1.line=4 | proc1.line=5) : TRUE;
TRUE : proc1.pushRightSTART;
esac;
init(proc1.pushRightEND) := FALSE;
next(proc1.pushRightEND) :=
case
(proc1.line=0) : TRUE;
TRUE : proc1.pushRightEND;
esac;
init(proc1.popLeftSTART) := FALSE;
next(proc1.popLeftSTART) :=
case
(proc1.line=7 | proc1.line=8) : TRUE;
TRUE : proc1.popLeftSTART;
esac;
init(proc1.popLeftEND) := FALSE;
next(proc1.popLeftEND) :=
case
(proc1.line=0) : TRUE;
TRUE : proc1.popLeftEND;
esac;
init(proc1.modifying) := FALSE;
next(proc1.modifying) :=
case
(proc1.line=1 | proc1.line=4 | proc1.line=7) : TRUE;
TRUE : proc1.modifying;
esac;
init(BOTH_MODIFYING):= FALSE;
next(BOTH_MODIFYING):=
case
(proc1.modifying & proc2.modifying) : TRUE;
TRUE: BOTH_MODIFYING;
esac;
-- ##############################################################################
-- Global ASSIGN
init(First_ProcID) := 1;
init(Second_ProcID) := 2;
next(First_ProcID) := First_ProcID;
next(Second_ProcID) := Second_ProcID;
init(RightHat) := 1;
init(LeftHat) := 1;
init(AllNodes[0][0]) := 0;
init(AllNodes[0][1]) := 0; -- DUMMY
init(AllNodes[1][0]) := 0;
init(AllNodes[1][1]) := 0; -- X
init(AllNodes[2][0]) := 2;
init(AllNodes[2][1]) := 2; -- Y
-- ##############################################################################
-- ##############################################################################
-- Proc 1 ASSIGN
init(proc1.line) := 0;
next(proc1.line) :=
case
(proc1.line=0 & First_ProcID=1) : {1,4,7}; -- STAND BY: could go to line:1/ line:4/ line:7
(proc1.line=0 & First_ProcID=2) : {1,4,7}; -- STAND BY: could go to line:1/ line:4/ line:7
(proc1.line=1) : {2}; -- popRight() starts, changing nodes
(proc1.line=2 & LeftHat=1 & RightHat=1) : {2,3}; -- wait
(proc1.line=2 & LeftHat=1 & RightHat=2) : {2,3}; -- wait
(proc1.line=3) : {0}; -- popRight() Return, End
(proc1.line=4) : {5}; -- pushRight() starts, changing nodes
(proc1.line=5) : {5,0}; -- wait
(proc1.line=7) : {8}; -- popLeftt() starts, changing nodes
(proc1.line=8 & LeftHat=1 & RightHat=1) : {8,0};
(proc1.line=8 & LeftHat=2 & RightHat=2) : {8,0};
(proc1.line=8 & LeftHat=1 & RightHat=2) : {8,0};
TRUE: proc1.line; -- default case
esac;
-- ##############################################################################
-- ##############################################################################
-- Proc 2 ASSIGN
init(proc2.line) := 0;
next(proc2.line) :=
case
(proc2.line=0 & Second_ProcID=1) : {1,4,7}; -- STAND BY: could go to line:1/ line:4/ line:7
(proc2.line=0 & Second_ProcID=2) : {1,4,7}; -- STAND BY: could go to line:1/ line:4/ line:7
(proc2.line=1) : {2}; -- popRight() starts, changing nodes
(proc2.line=2 & LeftHat=1 & RightHat=1) : {2,3}; -- wait
(proc2.line=2 & LeftHat=1 & RightHat=2) : {2,3}; -- wait
(proc2.line=3) : {0}; -- popRight() Return, End
(proc2.line=4) : {5}; -- pushRight() starts, changing nodes
(proc2.line=5) : {5,0}; -- wait
(proc2.line=7) : {8}; -- popLeftt() starts, changing nodes
(proc2.line=8 & LeftHat=1 & RightHat=1) : {8,0};
(proc2.line=8 & LeftHat=2 & RightHat=2) : {8,0};
(proc2.line=8 & LeftHat=1 & RightHat=2) : {8,0};
TRUE: proc2.line; -- default case
esac;
-- ##############################################################################
-- ##############################################################################
-- Queue ASSIGN
init(newnode) := 2;
next(newnode) := newnode;
-- for delaying return
init(temp_popRightfAIL) := FALSE;
next(temp_popRightfAIL) :=
case
((proc1.line=1) & (RightHat = 0)) : TRUE;
((proc2.line=1) & (RightHat = 0)) : TRUE;
TRUE: temp_popRightfAIL;
esac;
-- to cehck, use GlobalQueue-popRightfAIL[tid]
init(popRightfAIL) := FALSE;
next(popRightfAIL) :=
case
((proc1.line=3) & (temp_popRightfAIL)) : TRUE;
((proc2.line=3) & (temp_popRightfAIL)) : TRUE;
TRUE: popRightfAIL;
esac;
next(RightHat) :=
case
BOTH_MODIFYING : RightHat;
-- popRight
((proc1.line=1) & (RightHat = 2)) : 1;
((proc1.line=1) & (RightHat = 1)) : 0;
-- pushRight
(proc1.line=4) : 2;
-- popLeft
((proc1.line=7) & (RightHat = 1)) : 0;
((proc1.line=7) & (RightHat = 2)) : 1;
-- popRight
((proc2.line=1) & (RightHat = 2)) : 1;
((proc2.line=1) & (RightHat = 1)) : 0;
-- pushRight
(proc2.line=4) : 2;
-- popLeft
((proc2.line=7) & (RightHat = 1)) : 0;
((proc2.line=7) & (RightHat = 2)) : 1;
TRUE: RightHat;
esac;
next(LeftHat) :=
case
BOTH_MODIFYING : LeftHat;
-- popRight
((proc1.line=1) & (LeftHat = 1)) : 0;
-- pushRight
-- popLeft
((proc1.line=7) & (RightHat = 1)) : 2;
-- popRight
((proc2.line=1) & (LeftHat = 1)) : 0;
-- pushRight
-- popLeft
((proc2.line=7) & (RightHat = 1)) : 2;
TRUE: LeftHat;
esac;
--- GLOBAL variables for double-ended queue
next(AllNodes[0][0]) := AllNodes[0][0]; -- DUMMY
next(AllNodes[0][1]) := AllNodes[0][1]; -- DUMMY
-- X -> L
next(AllNodes[1][0]) :=
case
TRUE: AllNodes[1][0];
esac;
-- X -> R
next(AllNodes[1][1]) :=
case
BOTH_MODIFYING : AllNodes[1][1];
((proc1.line=1) & (RightHat=1)): 1;
((proc1.line=4) & (RightHat=1)): 2; -- push y
((proc1.line=7) & (LeftHat=1)): 1;
((proc2.line=1) & (RightHat=1)): 1;
((proc2.line=4) & (RightHat=1)): 2; -- push y
((proc2.line=7) & (LeftHat=1)): 1;
TRUE: AllNodes[1][1];
esac;
-- Y -> L
next(AllNodes[2][0]) :=
case
BOTH_MODIFYING : AllNodes[2][0];
((proc1.line=1) & (RightHat=2)): 2;
((proc1.line=4) & (RightHat=1)): 1;
((proc1.line=7) & (LeftHat=1)) : 0;
((proc2.line=1) & (RightHat=2)): 2;
((proc2.line=4) & (RightHat=1)): 1;
((proc2.line=7) & (LeftHat=1)) : 0;
TRUE: AllNodes[2][0];
esac;
-- Y -> R
next(AllNodes[2][1]) :=
case
BOTH_MODIFYING : AllNodes[2][1];
((proc1.line=4) & (RightHat=1)): 0;
((proc2.line=4) & (RightHat=1)): 0;
TRUE: AllNodes[2][1];
esac;
-- ##############################################################################
DEFINE
-- ##############################################################################
-- Proc 1 DEFINE
-- proc1.popRightSTART := proc1.line=1 | proc1.line=2 | proc1.line=3;
-- proc1.popRightEND := proc1.line=0 ;
-- proc1.pushRightSTART := proc1.line=4 | proc1.line=5;
-- proc1.pushRightEND := proc1.line=0 ;
-- proc1.popLeftSTART := proc1.line=7 | proc1.line=8;
-- proc1.popLeftEND := proc1.line=0 ;
-- proc1.modifying := proc1.line=1 | proc1.line=4| proc1.line=7;
-- ##############################################################################
-- ##############################################################################
-- Proc 2 DEFINE
-- proc2.popRightSTART := proc2.line=1 | proc2.line=2 | proc2.line=3;
-- proc2.popRightEND := proc2.line=0 ;
-- proc2.pushRightSTART := proc2.line=4 | proc2.line=5;
-- proc2.pushRightEND := proc2.line=0 ;
-- proc2.popLeftSTART := proc2.line=7 | proc2.line=8;
-- proc2.popLeftEND := proc2.line=0 ;
-- proc2.modifying := proc2.line=1 | proc2.line=4| proc2.line=7;
-- ##############################################################################
-- ##############################################################################
-- Queue DEFINE
-- BOTH_MODIFYING := (proc1.modifying & proc2.modifying);
-- ##############################################################################
Formula
Forall A . Exists B . ~(G(~fAIL[A]) & F~(((proc1.popRightSTART[A] = proc1.popRightSTART[B]) & (proc1.popRightEND[A] = proc1.popRightEND[B]) & (proc1.pushRightSTART[A] = proc1.pushRightSTART[B]) & (proc1.pushRightEND[A] = proc1.pushRightEND[B]) & (proc1.popLeftSTART[A]= proc1.popLeftSTART[B]) & (proc1.popLeftEND[A] = proc1.popLeftEND[B]) & (proc2.popRightSTART[A] = proc2.popRightSTART[B]) & (proc2.popRightEND[A] = proc2.popRightEND[B]) & (proc2.pushRightSTART[A] = proc2.pushRightSTART[B]) & (proc2.pushRightEND[A] = proc2.pushRightEND[B]) & (proc2.popLeftSTART[A] = proc2.popLeftSTART[B]) & (proc2.popLeftEND[A] = proc2.popLeftEND[B])) & ((popRightfAIL[A] = popRightfAIL[B]))))
The Model(s)
--SNARK 2
--(adopted from: Simon Doherty, David Detlefs, Lindsay Groves, Christine H. Flood, Victor Luchangco, Paul Alan Martin, Mark Moir, Nir Shavit, and Guy L. Steele Jr. DCAS is not a silver bullet for nonblocking algorithm design. In Proc. of the 16th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA’04),pages 216–224. ACM, 2004.)
-- // SNARK structure (with some accelerations):
-- // 0 ------- STAND BY: could go to line:1/ line:10/ line:19
-- // popRight() starts:
-- // 1 - getRightHat as rh
-- // 2 - getLeftHat as lh
-- // 3 - if (rh is self-pointing) return assign popRight_FAIL
-- // 4 - else if (rh equals lh)
-- // 5 DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
-- // 6 assign pop_result as rh->V
-- // 7 - else assign rhl as rh->L
-- // 8 DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
-- // 9 assign popRight_result as rh->V, assign rh->R as DUMMY
-- // pushRight() starts:
-- // 10 - assing nd as Y --> if null, return pushRight_FAIL
-- // 11 - assign nd->R as Dummy,assign nd-> V as something (zero for now)
-- // 12 - assign rh as RightHat, assign rhR as rh->R
-- // 13 if (rh == rhR), assign nd -> L = Dummy, assign lh = LeftHat
-- // 14 DCAS (RightHat, LeftHat, rh, lh, nd, nd)
-- // 15 return pushRight_SUCCESS
-- // 16 else assign nd->L as rh
-- // 17 DCAS(RightHat, rh->R, rh, rhR, nd, nd)
-- // 18 return pushRight_SUCCESS
-- // popLeft() starts:
-- // 19 - assign lh as LeftHat, assign rh as RightHat
-- // 20 - if (lh is self-pointing), return assign popLeft_FAIL
-- // 21 - else if (lh == rh)
-- // 22 DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
-- // 23 assign popLeft_result as lh -> V
-- // 24 - else assign lhR as lh->R
-- // 25 DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
-- // 26 assign popLeft_result as lh->V, assign lh_L as DDUMMY
-- NODE ID: DUMMY=0 x=1, y=2, z=3
-- Each node has three data:[leftpointer, value, rightpointer]
MODULE main
VAR
-- RightHat: array 0..1 of 0..2;
-- LeftHat: array 0..1 of 0..2;
RightHat: 0..3; -- could be DUNNY, x, y, or z
LeftHat: 0..3; -- could be DUMMY, x, y, or z
AllNodes: array 0..3 of array 0..1 of 0..3; -- store X,Y,Z and their pointers, ignore DUMMY
First_ProcID: 1..3;
Second_ProcID: 1..3;
Third_ProcID: 1..3;
--- ('process' is problmatic)
-- proc1: process SNARK(RightHat, LeftHat, AllNodes);
-- proc2: process SNARK(RightHat, LeftHat, AllNodes);
-- TOKEN: 1..3;
--- next(TOKEN) := {1,2,3};
-- with
proc1: SNARK(LeftHat, RightHat, AllNodes, First_ProcID);
proc2: SNARK(LeftHat, RightHat, AllNodes, Second_ProcID);
proc3: SNARK(LeftHat, RightHat, AllNodes, Third_ProcID);
GlobalQueue: Queue(LeftHat, RightHat, AllNodes, proc1, proc2, proc3);
ASSIGN
init(First_ProcID) := 1;
init(Second_ProcID) := 2;
init(Third_ProcID) := 3;
next(First_ProcID) := First_ProcID;
next(Second_ProcID) := Second_ProcID;
next(Third_ProcID) := Third_ProcID;
-- NODE ID: DUMMY=0 x=1, y=2, z=3
-- EMPTY QUEUE --
-- init(RightHat) := 0;
-- init(LeftHat) := 0;
-- init(AllNodes[0][0]) := 0;
-- init(AllNodes[0][1]) := 0; -- X
-- init(AllNodes[1][0]) := 1;
-- init(AllNodes[1][1]) := 1; -- Y
-- init(AllNodes[2][0]) := 2;
-- init(AllNodes[2][1]) := 2; -- Z
-- -- if [DUMMY --- X --- DUMMY]
-- init(RightHat) := 1;
-- init(LeftHat) := 1;
-- init(AllNodes[0][0]) := 0;
-- init(AllNodes[0][1]) := 0; -- DUMMY
-- init(AllNodes[1][0]) := 0;
-- init(AllNodes[1][1]) := 0; -- X
-- init(AllNodes[2][0]) := 2;
-- init(AllNodes[2][1]) := 2; -- Y
-- -- if [DUMMY --- X -- Y --- DUMMY] (BUG2)
init(RightHat) := 2;
init(LeftHat) := 1;
init(AllNodes[0][0]) := 0;
init(AllNodes[0][1]) := 0; -- DUMMY
init(AllNodes[1][0]) := 0;
init(AllNodes[1][1]) := 2; -- X
init(AllNodes[2][0]) := 1;
init(AllNodes[2][1]) := 0; -- Y
init(AllNodes[3][0]) := 3;
init(AllNodes[3][1]) := 3; -- Z
MODULE Queue(LeftHat, RightHat, AllNodes, proc1, proc2, proc3)
-- CHANGING GLOBAL VARIABLEs
VAR
newnode : 0..3; -- for push right
popRightFAIL: boolean;
ASSIGN
init(newnode) := 3;
next(newnode) := newnode;
-- to cehck, use GlobalQueue-popRightFAIL[tid]
init(popRightFAIL) := FALSE;
next(popRightFAIL) :=
case
((proc1.line=3) & (proc1.local_popR_RH=1 & AllNodes[1][1]=1)) : TRUE;
((proc1.line=3) & (proc1.local_popR_RH=2 & AllNodes[2][1]=2)) : TRUE;
((proc2.line=3) & (proc2.local_popR_RH=0)) : TRUE;
TRUE: popRightFAIL;
esac;
next(RightHat) :=
case
BOTH_MODIFYING : RightHat;
((proc1.line=5 & !fAIL) | (proc2.line=5 & !fAIL)) : 0; -- set to DUMMY
((proc1.line=22) | (proc2.line=22)) : 0; -- set to DUMMY
((proc1.line=8) & !fAIL& (proc1.local_popR_RHL=0)) : 0; -- set to RH->L 0
((proc1.line=8) & !fAIL& (proc1.local_popR_RHL=1)) : 1; -- set to RH->L 0
((proc1.line=8) & !fAIL& (proc1.local_popR_RHL=2)) : 2; -- set to RH->L 0
((proc2.line=8) & !fAIL& (proc2.local_popR_RHL=0)) : 0; -- set to RH->L 0
((proc2.line=8) & !fAIL& (proc2.local_popR_RHL=1)) : 1; -- set to RH->L 0
((proc2.line=8) & !fAIL& (proc2.local_popR_RHL=2)) : 2; -- set to RH->L 0
((proc3.line=8) & !fAIL& (proc3.local_popR_RHL=0)) : 0; -- set to RH->L 0
((proc3.line=8) & !fAIL& (proc3.local_popR_RHL=1)) : 1; -- set to RH->L 0
((proc3.line=8) & !fAIL& (proc3.local_popR_RHL=2)) : 2; -- set to RH->L 0
((proc1.line=14) | (proc2.line=14)) : 3; -- set to newnode
((proc1.line=17 & RightHat=proc1.local_pushR_RH) | (proc2.line=17 & RightHat=proc2.local_pushR_RH)) : 3; -- set to new node
TRUE: RightHat;
esac;
next(LeftHat) :=
case
BOTH_MODIFYING : LeftHat;
((proc1.line=5 & !fAIL) | (proc2.line=5 & !fAIL)) : 0; -- set to DUMMY
((proc1.line=22 & RightHat=proc1.local_pushR_RH) | (proc2.line=22 & RightHat=proc2.local_pushR_RH)) : 0; -- set to DUMMY
((proc1.line=25) & (proc1.local_popL_LHR=0)) : 0; -- set to LH->R 0
((proc1.line=25) & (proc1.local_popL_LHR=1)) : 1; -- set to LH->R 0
((proc1.line=25) & (proc1.local_popL_LHR=2)) : 2; -- set to LH->R 0
((proc1.line=25) & (proc1.local_popL_LHR=3)) : 3; -- set to LH->R 0
((proc2.line=25) & (proc2.local_popL_LHR=0)) : 0; -- set to LH->R 0
((proc2.line=25) & (proc2.local_popL_LHR=1)) : 1; -- set to LH->R 0
((proc2.line=25) & (proc2.local_popL_LHR=2)) : 2; -- set to LH->R 0
((proc2.line=25) & (proc2.local_popL_LHR=3)) : 3; -- set to LH->R 0
((proc1.line=14) | (proc2.line=14)) : 3; --set to newnode
TRUE: LeftHat;
esac;
next(AllNodes[0][0]) := AllNodes[0][0]; -- DUMMY
next(AllNodes[0][1]) := AllNodes[0][1]; -- DUMMY
next(AllNodes[1][0]) :=
case
BOTH_MODIFYING: AllNodes[1][0]; --?
((proc1.line=8) & !fAIL& (proc1.local_popR_RH=1)): 1;
((proc1.line=26) & (proc1.local_popL_LH=1) & (LeftHat=1)): 0;
((proc2.line=8) & !fAIL& (proc2.local_popR_RH=1)): 1;
((proc2.line=26) & (proc2.local_popL_LH=1) & (LeftHat=1)): 0;
TRUE: AllNodes[1][0];
esac;
next(AllNodes[1][1]) :=
case
BOTH_MODIFYING : AllNodes[1][1]; --?
((proc1.line=17) & (proc1.local_pushR_RH=1)): 3; -- newnode
((proc1.line=25) & !fAIL& (proc1.local_popL_LH=1)): 1;
((proc1.line=9) & (proc1.local_popR_RH=1)& (RightHat=1)): 0;
((proc2.line=17) & (proc2.local_pushR_RH=1)): 3; -- newnode
((proc2.line=25) & !fAIL& (proc2.local_popL_LH=1)): 1;
((proc2.line=9) & (proc2.local_popR_RH=1) & (RightHat=1)): 0;
TRUE: AllNodes[1][1];
esac;
next(AllNodes[2][0]) :=
case
BOTH_MODIFYING : AllNodes[2][0];
((proc1.line=8) & !fAIL& (proc1.local_popR_RH=2)) : 2;
((proc1.line=26) & (proc1.local_popL_LH=2) & (LeftHat=2)): 0;
((proc2.line=8) & !fAIL& (proc2.local_popR_RH=2)) : 2;
((proc2.line=26) & (proc2.local_popL_LH=2) & (LeftHat=2)): 0;
TRUE: AllNodes[2][0];
esac;
next(AllNodes[2][1]) :=
case
BOTH_MODIFYING : AllNodes[2][1];
((proc1.line=17) & (proc1.local_pushR_RH=2)): 3; -- newnode
((proc1.line=9) & (proc1.local_popR_RH=2) & (RightHat=2)): 0;
((proc1.line=25) & !fAIL& (proc1.local_popL_LH=2)): 2;
((proc2.line=17) & (proc2.local_pushR_RH=2)): 3; -- newnode
((proc2.line=9) & (proc1.local_popR_RH=2) & (RightHat=2)): 0;
((proc2.line=25) & !fAIL& (proc2.local_popL_LH=2)): 2;
TRUE: AllNodes[2][1];
esac;
next(AllNodes[3][0]) :=
case
((proc2.line=16) & proc2.local_pushR_RH=1): 1;
((proc2.line=16) & proc2.local_pushR_RH=2): 2;
TRUE: AllNodes[3][0];
esac;
next(AllNodes[3][1]) :=
case
(proc2.line=11): 0;
TRUE: AllNodes[3][1]; -- Z->Y
esac;
DEFINE
BOTH_MODIFYING := (proc1.modifying & proc2.modifying) | (proc1.modifying & proc3.modifying) | (proc2.modifying & proc3.modifying);
COLLISION := (proc1.modifying & proc2.modifying) | (proc1.modifying & proc3.modifying) | (proc2.modifying & proc3.modifying);
fAIL:= ((proc1.line=5) & ( !(RightHat=proc1.local_popR_RH)
| !(LeftHat=proc1.local_popR_LH)))
|((proc1.line=8) & ( !(RightHat=proc1.local_popR_RH)
| !(proc1.local_popR_RH=1 -> (AllNodes[1][0]=proc1.local_popR_RHL))
| !(proc1.local_popR_RH=2 -> (AllNodes[2][0]=proc1.local_popR_RHL))
| !(proc1.local_popR_RH=3 -> (AllNodes[3][0]=proc1.local_popR_RHL))))
|((proc1.line=22) & ( !(RightHat=proc1.local_popL_RH)
| !(LeftHat=proc1.local_popL_LH)))
|((proc1.line=25) & ( !(LeftHat=proc1.local_popL_LH)
| !(proc1.local_popL_LH=1 -> (AllNodes[1][1]=proc1.local_popL_LHR))
| !(proc1.local_popL_LH=2 -> (AllNodes[2][1]=proc1.local_popL_LHR))
| !(proc1.local_popL_LH=3 -> (AllNodes[3][1]=proc1.local_popL_LHR))))
|((proc2.line=5) & ( !(RightHat=proc2.local_popR_RH)
| !(LeftHat=proc2.local_popR_LH)))
|((proc2.line=8) & ( !(RightHat=proc2.local_popR_RH)
| !(proc2.local_popR_RH=1 -> (AllNodes[1][0]=proc2.local_popR_RHL))
| !(proc2.local_popR_RH=2 -> (AllNodes[2][0]=proc2.local_popR_RHL))
| !(proc2.local_popR_RH=3 -> (AllNodes[3][0]=proc2.local_popR_RHL))))
|((proc2.line=22) & ( !(RightHat=proc2.local_popL_RH)
| !(LeftHat=proc2.local_popL_LH)))
|((proc2.line=25) & ( !(LeftHat=proc2.local_popL_LH)
| !(proc2.local_popL_LH=1 -> (AllNodes[1][1]=proc2.local_popL_LHR))
| !(proc2.local_popL_LH=2 -> (AllNodes[2][1]=proc2.local_popL_LHR))
| !(proc2.local_popL_LH=3 -> (AllNodes[3][1]=proc2.local_popL_LHR))));
popLeft_X := (proc1.L_popped_X | proc2.L_popped_X | proc3.L_popped_X);
popRight_Z := (proc1.R_popped_Z | proc2.R_popped_Z | proc3.R_popped_Z);
popLeft_Y := (proc1.L_popped_Y | proc2.L_popped_Y | proc3.L_popped_Y);
popRight_Y := (proc1.L_popped_Y | proc2.L_popped_Y | proc3.L_popped_Y);
popLeft_Z := (proc1.L_popped_Z | proc2.L_popped_Z | proc3.L_popped_Z);
popRight_X := (proc1.R_popped_Y | proc2.R_popped_Y | proc3.R_popped_Y);
MODULE SNARK(LeftHat, RightHat, AllNodes, ProcID)
VAR
line: 0..26;
-- popRight local variables
local_popR_RH: 0..3; -- could be DUMMY, x,or y
local_popR_LH: 0..3; -- could be DUMMY, x,or y
local_popR_RHL: 0..3; -- could be DUMMY, x,or y
-- local_popR_return_empty: boolean; -- move to global queue
-- popLeft local variables
local_popL_RH: 0..3; -- could be DUMMY, x,or y
local_popL_LH: 0..3; -- could be DUMMY, x,or y
local_popL_LHR: 0..3; -- could be DUMMY, x,or y
-- pushRight local variables
-- local_pushR_newnode: array 0..2 of 0..2;
-- local_pushR_newnode: 0..2;
local_pushR_RH: 0..3; -- could be DUMMY, x,or y
local_pushR_RHR: 0..3; -- xcould be DUMMY, x,or y
local_pushR_LH: 0..3; -- could be DUMMY, x,or y
ASSIGN
init(line) := 0;
-- popRight local, all default to DUMMY
init(local_popR_RH) := 0;
init(local_popR_LH) := 0;
init(local_popR_RHL) := 0;
-- init(local_popR_return_empty):= FALSE;
-- popLeft local, all default to DUMMY
init(local_popL_RH) := 0;
init(local_popL_LH) := 0;
init(local_popL_LHR) := 0;
--pushRight local, all default to DUMMY
init(local_pushR_LH):= 0;
init(local_pushR_RH) := 0;
init(local_pushR_RHR) := 0;
-- FUNTIONS
next(line) :=
case
(line=0 & ProcID=1) : {0,1};
(line=0 & ProcID=2 & RightHat=2):{10}; -- beginning
(line=0 & ProcID=2 & !(RightHat=2)):{0,10,19}; -- STAND BY: could go to line:1/ line:10/ line:19
(line=0 & ProcID=3 & !(LeftHat=2)): {0}; -- STAND BY: could go to line:1/ line:10/ line:19
(line=0 & ProcID=3 & (LeftHat=2)): {0,1}; -- STAND BY: could go to line:1/ line:10/ line:19
(line=1) : {2};
(line=2 & LeftHat=1 & RightHat=1 & ProcID=1) : {2,3};
(line=2 & LeftHat=1 & RightHat=2 & ProcID=1) : {2,3};
(line=2 & LeftHat=2 & RightHat=1 & ProcID=1) : {2,3};
(line=2 & ProcID=2) : {3};
(line=2 & ProcID=3) : {3};
(line=3 & (local_popR_RH=1) & AllNodes[1][1]=1) : {0};
(line=3 & (local_popR_RH=2) & AllNodes[2][1]=2) : {0};
(line=3 & !((local_popR_RH=1) & AllNodes[1][1]=1)| (local_popR_RH=2) & AllNodes[1][1]=2) : {4};
(line=4 & (local_popR_RH=1 & local_popR_LH=1)) : {4,5};
(line=4 & (local_popR_RH=2 & local_popR_LH=2)) : {4,5}; -- if (rh equals lh)
(line=4 & (local_popR_RH=3 & local_popR_LH=3)) : {4,5}; -- if (rh equals lh)
(line=4 & !(local_popR_RH=1 & local_popR_LH=1)) : {7};
(line=4 & !(local_popR_RH=2 & local_popR_LH=2)) : {7};
(line=4 & !(local_popR_RH=3 & local_popR_LH=3)) : {7};
(line=5) : {6}; -- DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
(line=6) : {6,0}; -- assign pop_result as rh->V, END
(line=7) : {7,8}; --assign rhl as rh->L -- proc1 could stuck --could delay
(line=8) : {9}; -- DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
(line=9) : {9,0}; -- assign popRight_result as rh->V, assign rh->R as DUMMY
(line=10) : {11}; -- pushRight() starts assing nd as Y --> if null, return pushRight_FAIL
(line=11) : {12}; -- assign nd->R as Dummy,assign nd-> V as something (zero for now)
(line=12) : {13}; -- assign rh as RightHat, assign rhR as rh->R
(line=13 & (local_pushR_RH = local_pushR_RHR)) : {13, 14}; -- if (rh == rhR), assign nd -> L = Dummy, assign lh = LeftHat
(line=13 & !(local_pushR_RH = local_pushR_RHR)) : {16}; -- if !(rh == rhR) assign nd->L as rh
(line=14) : {15}; -- DCAS (RightHat, LeftHat, rh, lh, nd, nd)
(line=15) : {0}; -- return pushRight_SUCCESS
(line=16) : {16, 17}; -- assign nd->L as rh
(line=17) : {18}; -- DCAS(RightHat, rh->R, rh, rhR, nd, nd)
(line=18) : {0}; -- return pushRight_SUCCESS
(line=19) : {20}; --- popLeft() starts, assign lh as LeftHat, assign rh as RightHat
(line=20) : {21}; -- if(!lh is self-pointing)
(line=21 & (local_popL_LH =local_popL_RH)) : {21, 22}; -- if(lh == rh)
(line=21 & !(local_popL_LH =local_popL_RH)) : {24}; -- if!(lh == rh)
(line=22) : {23}; -- DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
(line=23) : {0}; -- assign popLeft_result as lh -> V, END
(line=24) : {24,25}; -- assign lhR as lh->R -- could delay
(line=25) : {26}; -- DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
(line=26 & L_popped_X) : {19};
TRUE: line; -- default case
esac;
-- local_popR local variables
next(local_popR_RH) :=
case
(line=1) : RightHat;
TRUE : local_popR_RH; -- default case
esac;
next(local_popR_LH) :=
case
(line=2) : LeftHat;
TRUE : local_popR_LH; -- default case
esac;
next(local_popR_RHL) :=
case
!(line=7) : local_popR_RHL;
(line=7) : AllNodes[local_popR_RH][0];
TRUE : local_popR_RHL; -- default case
esac;
-- local_pushR local variables
next(local_pushR_RH) :=
case
(line=12): RightHat;
TRUE: local_pushR_RH;
esac;
next(local_pushR_LH) :=
case
(line=13 & (local_pushR_RH = local_pushR_RHR)): LeftHat;
TRUE: local_pushR_LH;
esac;
next(local_pushR_RHR) :=
case
(line=12): AllNodes[local_pushR_RH][1];
TRUE: local_pushR_RHR;
esac;
-- local_popL local variables
next(local_popL_LH) :=
case
(line=19) : LeftHat;
TRUE : local_popL_LH; -- default case
esac;
next(local_popL_RH) :=
case
(line=19) : RightHat;
TRUE : local_popL_RH; -- default case
esac;
next(local_popL_LHR) :=
case
(line=24) : AllNodes[local_popL_LH][1];
TRUE : local_popL_LHR; -- default case
esac;
DEFINE
modifying := (line=5 | line=8 | line=14 | line=17 | line=16 | line=11 | line=22 | line=25);
popRightSTART := line=1 | line=2 | line=3 | line=4 | line=5 | line=6 | line=7 | line=8 | line=9;
popRightEND := line=0;
pushRightSTART := line=10 | line=11| line=12 | line=13 | line=14 | line=15 | line=16 | line=17 | line=18;
pushRightEND := line=0;
popLeftSTART := line=19 | line=20 | line=21 | line=22 | line=23 | line=24 | line=25 | line=26;
popLeftEND := line=0;
L_popped_X := (line=26 & local_popL_LH=1);
L_popped_Y := (line=26 & local_popL_LH=2);
L_popped_Z := (line=26 & local_popL_LH=3);
R_popped_Z := (line=9 & local_popR_RH=3);
R_popped_Y := (line=9 & local_popR_RH=2 & ProcID=1);
R_popped_X := (line=9 & local_popR_RH=1);
-- SNARK 2
-- (adopted from: Simon Doherty, David Detlefs, Lindsay Groves, Christine H. Flood, Victor Luchangco, Paul Alan Martin, Mark Moir, Nir Shavit, and Guy L. Steele Jr. DCAS is not a silver bullet for nonblocking algorithm design. In Proc. of the 16th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA’04),pages 216–224. ACM, 2004.)
-- // SNARK structure (with some accelerations):
-- // 0 ------- STAND BY: could go to line:1/ line:10/ line:19
-- // popRight() starts:
-- // 1 - getRightHat as rh
-- // 2 - getLeftHat as lh
-- // 3 - if (rh is self-pointing) return assign popRight_FAIL
-- // 4 - else if (rh equals lh)
-- // 5 DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
-- // 6 assign pop_result as rh->V
-- // 7 - else assign rhl as rh->L
-- // 8 DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
-- // 9 assign popRight_result as rh->V, assign rh->R as DUMMY
-- // pushRight() starts:
-- // 10 - assing nd as Y --> if null, return pushRight_FAIL
-- // 11 - assign nd->R as Dummy,assign nd-> V as something (zero for now)
-- // 12 - assign rh as RightHat, assign rhR as rh->R
-- // 13 if (rh == rhR), assign nd -> L = Dummy, assign lh = LeftHat
-- // 14 DCAS (RightHat, LeftHat, rh, lh, nd, nd)
-- // 15 return pushRight_SUCCESS
-- // 16 else assign nd->L as rh
-- // 17 DCAS(RightHat, rh->R, rh, rhR, nd, nd)
-- // 18 return pushRight_SUCCESS
-- // popLeft() starts:
-- // 19 - assign lh as LeftHat, assign rh as RightHat
-- // 20 - if (lh is self-pointing), return assign popLeft_FAIL
-- // 21 - else if (lh == rh)
-- // 22 DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
-- // 23 assign popLeft_result as lh -> V
-- // 24 - else assign lhR as lh->R
-- // 25 DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
-- // 26 assign popLeft_result as lh->V, assign lh_L as DDUMMY
-- NODE ID: DUMMY=0 x=1, y=2, z=3
-- Each node has three data:[leftpointer, value, rightpointer]
MODULE main
VAR
RightHat: 0..3; -- could be DUNNY, x, y, or z
LeftHat: 0..3; -- could be DUMMY, x, y, or z
AllNodes: array 0..3 of array 0..1 of 0..3; -- store X,Y,Z and their pointers, ignore DUMMY
First_ProcID: 1..3;
Second_ProcID: 1..3;
Third_ProcID: 1..3;
proc1: SNARK(LeftHat, RightHat, AllNodes, First_ProcID);
proc2: SNARK(LeftHat, RightHat, AllNodes, Second_ProcID);
proc3: SNARK(LeftHat, RightHat, AllNodes, Third_ProcID);
GlobalQueue: Queue(LeftHat, RightHat, AllNodes, proc1, proc2, proc3);
ASSIGN
init(First_ProcID) := 1;
init(Second_ProcID) := 2;
init(Third_ProcID) := 3;
next(First_ProcID) := First_ProcID;
next(Second_ProcID) := Second_ProcID;
next(Third_ProcID) := Third_ProcID;
init(RightHat) := 2;
init(LeftHat) := 1;
init(AllNodes[0][0]) := 0;
init(AllNodes[0][1]) := 0; -- DUMMY
init(AllNodes[1][0]) := 0;
init(AllNodes[1][1]) := 2; -- X
init(AllNodes[2][0]) := 1;
init(AllNodes[2][1]) := 0; -- Y
init(AllNodes[3][0]) := 1;
init(AllNodes[3][1]) := 0; -- Y
MODULE Queue(LeftHat, RightHat, AllNodes, proc1, proc2, proc3)
-- CHANGING GLOBAL VARIABLEs
VAR
newnode : 0..3; -- for push right
popRightFAIL: boolean;
temp_popRightFAIL: boolean;
ASSIGN
init(newnode) := 3;
next(newnode) := newnode;
-- for delaying return
init(temp_popRightFAIL) := FALSE;
next(temp_popRightFAIL) :=
case
((proc1.line=1) & (RightHat = 0)) : TRUE;
((proc2.line=1) & (RightHat = 0)) : TRUE;
((proc3.line=1) & (RightHat = 0)) : TRUE;
TRUE: temp_popRightFAIL;
esac;
-- to cehck, use GlobalQueue-popRightFAIL[tid]
init(popRightFAIL) := FALSE;
next(popRightFAIL) :=
case
((proc1.line=3) & (temp_popRightFAIL)) : TRUE;
((proc2.line=3) & (temp_popRightFAIL)) : TRUE;
((proc3.line=3) & (temp_popRightFAIL)) : TRUE;
TRUE: popRightFAIL;
esac;
next(RightHat) :=
case
BOTH_MODIFYING : RightHat;
-- popRight
((proc1.line=1) & (RightHat = 2)) : 1;
((proc1.line=1) & (RightHat = 1)) : 0;
-- pushRight
(proc1.line=4) : 2;
-- popLeft
((proc1.line=7) & (RightHat = 1)) : 0;
((proc1.line=7) & (RightHat = 2)) : 1;
-- popRight
((proc2.line=1) & (RightHat = 2)) : 1;
((proc2.line=1) & (RightHat = 1)) : 0;
-- pushRight
(proc2.line=4) : 2;
-- popLeft
((proc2.line=7) & (RightHat = 1)) : 0;
((proc2.line=7) & (RightHat = 2)) : 1;
-- popRight
((proc3.line=1) & (RightHat = 2)) : 1;
((proc3.line=1) & (RightHat = 1)) : 0;
-- pushRight
(proc3.line=4) : 2;
-- popLeft
((proc3.line=7) & (RightHat = 1)) : 0;
((proc3.line=7) & (RightHat = 2)) : 1;
TRUE: RightHat;
esac;
next(LeftHat) :=
case
BOTH_MODIFYING : LeftHat;
-- popRight
((proc1.line=1) & (LeftHat = 1)) : 0;
-- pushRight
-- popLeft
((proc1.line=7) & (RightHat = 1)) : 2;
-- popRight
((proc2.line=1) & (LeftHat = 1)) : 0;
-- pushRight
-- popLeft
((proc2.line=7) & (RightHat = 1)) : 2;
-- popRight
((proc3.line=1) & (LeftHat = 1)) : 0;
-- pushRight
-- popLeft
((proc3.line=7) & (RightHat = 1)) : 2;
TRUE: LeftHat;
esac;
--- GLOBAL variables for double-ended queue
next(AllNodes[0][0]) := AllNodes[0][0]; -- DUMMY
next(AllNodes[0][1]) := AllNodes[0][1]; -- DUMMY
-- X -> L
next(AllNodes[1][0]) :=
case
TRUE: AllNodes[1][0];
esac;
-- X -> R
next(AllNodes[1][1]) :=
case
BOTH_MODIFYING : AllNodes[1][1];
((proc1.line=1) & (RightHat=1)): 1;
((proc1.line=4) & (RightHat=1)): 2; -- push y
((proc1.line=7) & (LeftHat=1)): 1;
((proc2.line=1) & (RightHat=1)): 1;
((proc2.line=4) & (RightHat=1)): 2; -- push y
((proc2.line=7) & (LeftHat=1)): 1;
((proc3.line=1) & (RightHat=1)): 1;
((proc3.line=4) & (RightHat=1)): 2; -- push y
((proc3.line=7) & (LeftHat=1)): 1;
TRUE: AllNodes[1][1];
esac;
-- Y -> L
next(AllNodes[2][0]) :=
case
BOTH_MODIFYING : AllNodes[2][0];
((proc1.line=1) & (RightHat=2)): 2;
((proc1.line=4) & (RightHat=1)): 1;
((proc1.line=7) & (LeftHat=1)) : 0;
((proc2.line=1) & (RightHat=2)): 2;
((proc2.line=4) & (RightHat=1)): 1;
((proc2.line=7) & (LeftHat=1)) : 0;
((proc3.line=1) & (RightHat=2)): 2;
((proc3.line=4) & (RightHat=1)): 1;
((proc3.line=7) & (LeftHat=1)) : 0;
TRUE: AllNodes[2][0];
esac;
-- Y -> R
next(AllNodes[2][1]) :=
case
BOTH_MODIFYING : AllNodes[2][1];
((proc1.line=4) & (RightHat=1)): 0;
((proc2.line=4) & (RightHat=1)): 0;
((proc3.line=4) & (RightHat=1)): 0;
TRUE: AllNodes[2][1];
esac;
next(AllNodes[3][0]) := AllNodes[3][0]; -- ZL
next(AllNodes[3][1]) := AllNodes[3][1]; -- ZR
DEFINE
BOTH_MODIFYING := (proc1.modifying & proc2.modifying) | (proc1.modifying & proc3.modifying) | (proc2.modifying & proc3.modifying);
popLeft_X := (proc1.L_popped_X | proc2.L_popped_X | proc3.L_popped_X);
popRight_Z := (proc1.R_popped_Z | proc2.R_popped_Z | proc3.R_popped_Z);
popLeft_Y := (proc1.L_popped_Y | proc2.L_popped_Y | proc3.L_popped_Y);
popRight_Y := (proc1.R_popped_Y | proc2.R_popped_Y | proc3.R_popped_Y);
popRight_X := (proc1.R_popped_Y | proc2.R_popped_Y | proc3.R_popped_Y);
popLeft_Z := (proc1.L_popped_Z | proc2.L_popped_Z | proc3.L_popped_Z);
MODULE SNARK(LeftHat, RightHat, AllNodes, ProcID)
VAR
line: 0..9;
ASSIGN
init(line) := 0;
-- FUNCTIONS
next(line) :=
case
(line=0 & ProcID=1) : {0,1,4};
(line=0 & ProcID=2 & RightHat=2) : {4};
(line=0 & ProcID=2 & !(RightHat=2)) : {4,7}; -- STAND BY: could go to line:1/ line:4/ line:7
(line=0 & ProcID=3) : {0,1};
(line=1) : {2}; -- popRight() starts, changing nodes
(line=2 & LeftHat=1 & RightHat=1) : {2,3}; -- wait
(line=2 & LeftHat=1 & RightHat=2) : {2,3}; -- wait
(line=2 & LeftHat=2 & RightHat=2) : {2,3}; -- wait
(line=3) : {0}; -- popRight() Return, End
(line=4) : {5}; -- pushRight() starts, changing nodes
(line=5) : {5,0}; -- wait
(line=7) : {8}; -- popLeftt() starts, changing nodes
(line=8 & LeftHat=1 & RightHat=1) : {8,0};
(line=8 & LeftHat=1 & RightHat=2) : {8,0};
(line=8 & LeftHat=2 & RightHat=2) : {8,0};
TRUE: line; -- default case
esac;
DEFINE
popRightSTART := line=1 | line=2 | line=3;
popRightEND := line=0 ;
pushRightSTART := line=4 | line=5;
pushRightEND := line=0 ;
popLeftSTART := line=7 | line=8;
popLeftEND := line=0 ;
modifying := line=1 | line=4| line=7;
L_popped_X := (line=8 & LeftHat=2);
L_popped_Y := (line=8 & LeftHat=3);
L_popped_Z := (line=8 & LeftHat=0);
R_popped_Z := (line=3 & RightHat=2);
R_popped_Y := (line=3 & RightHat=1);
R_popped_X := (line=3 & RightHat=0);
Formula
Exists A . Forall B .
G(~ fAIL[A] & ~ COLLISION[A]) &
F~(
(
(proc1.popRightSTART[A] = proc1.popRightSTART[B]) & (proc1.popRightEND[A] = proc1.popRightEND[B])
& (proc1.pushRightSTART[A] = proc1.pushRightSTART[B]) & (proc1.pushRightEND[A] = proc1.pushRightEND[B])
& (proc1.popLeftSTART[A] = proc1.popLeftSTART[B]) & (proc1.popLeftEND[A] = proc1.popLeftEND[B])
& (proc2.popRightSTART[A] = proc2.popRightSTART[B]) & (proc2.popRightEND[A] = proc2.popRightEND[B])
& (proc2.pushRightSTART[A] = proc2.pushRightSTART[B]) & (proc2.pushRightEND[A] = proc2.pushRightEND[B])
& (proc2.popLeftSTART[A] = proc2.popLeftSTART[B]) & (proc2.popLeftEND[A] = proc2.popLeftEND[B])
& (proc3.popRightSTART[A] = proc3.popRightSTART[B]) & (proc3.popRightEND[A] = proc3.popRightEND[B])
& (proc3.pushRightSTART[A] = proc3.pushRightSTART[B]) & (proc3.pushRightEND[A] = proc3.pushRightEND[B])
& (proc3.popLeftSTART[A] = proc3.popLeftSTART[B]) & (proc3.popLeftEND[A] = proc3.popLeftEND[B])
)
& (popRightFAIL[A] = popRightFAIL[B])
& (popLeft_X[A] = popLeft_X[B])
& (popLeft_Y[A] = popLeft_Y[B])
& (popRight_Y[A] = popLeft_Y[B])
& (popRight_Z[A] = popRight_Z[B])
)