Linearizability¶
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)
--SNARK1
--(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
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..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;
-- FAIL: boolean;
-- ##############################################################################
ASSIGN
-- ##############################################################################
-- 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))))
--- if full
|((proc1.line=13) & RightHat=2)
|((proc2.line=13) & RightHat=2)
|((proc2.line=20) & RightHat=0 & RightHat=0)
| BOTH_MODIFYING;
-- ##############################################################################
--SNARK1
--(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
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;
-- ##############################################################################
ASSIGN
-- ##############################################################################
-- 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. 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;
-- FAIL: 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;
-- (line=5) : 0;
-- ((proc1.line=5 & proc1.local_popR_RH=RightHat & proc1.local_popR_LH=LeftHat) |
-- (proc2.line=5 & proc2.local_popR_RH=RightHat & proc2.local_popR_LH=LeftHat)) : 0; -- set to DUMMY
((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)) : proc1.local_popR_RHL; -- set to RH->L of proc1
-- 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
-- ((proc2.line=8)) : proc2.local_popR_RHL; -- set to RH->L of proc2
-- 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
((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
-- (line=14) : local_pushR_newnode; -- set to new node
((proc1.line=14) | (proc2.line=14)) : 3; -- set to newnode
-- ((proc1.line=14) | (proc2.line=14)) : proc1.local_pushR_newnode; -- set to newnode
-- (line=17) : local_pushR_newnode;
((proc1.line=17 & RightHat=proc1.local_pushR_RH) |
(proc2.line=17 & RightHat=proc2.local_pushR_RH)) : 3; -- set to new node
-- ((proc1.line=17) | (proc2.line=17)) : proc1.local_pushR_newnode;
TRUE: RightHat;
esac;
next(LeftHat) :=
case
BOTH_MODIFYING : LeftHat;
-- ((proc1.line=5) | (proc2.line=5)) : 0; -- set toDUMMY
--- SWAP if DCAS
-- ((proc1.line=5 & proc1.local_popR_RH=RightHat & proc1.local_popR_LH=LeftHat) |
-- (proc2.line=5 & proc2.local_popR_RH=RightHat & proc2.local_popR_LH=LeftHat)) : 0; -- set toDUMMY
((proc1.line=5 & !FAIL) | (proc2.line=5 & !FAIL)) : 0; -- set to DUMMY
-- SWAP if DCAS
((proc1.line=22 & RightHat=proc1.local_pushR_RH) | (proc2.line=22 & RightHat=proc2.local_pushR_RH)) : 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) ) : 2; -- set to LH->R 0
((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
-- ((proc1.line=14) | (proc2.line=14)) : proc1.local_pushR_newnode; --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) & (proc2.local_popR_RH=1)): 1;
((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)): 3; -- newnode
((proc1.line=25) & !FAIL & (proc1.local_popL_LH=1)): 1;
--- ?
((proc1.line=9) & (proc1.local_popR_RH=1)& (RightHat=1)): 0;
-- ((proc1.line=9) & (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;
-- ((proc2.line=9) & (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=26) & (LeftHat=2)): 0;
((proc2.line=8) & !FAIL & (proc2.local_popR_RH=2)) : 2;
-- ?
((proc2.line=26) & (proc2.local_popL_LH=2) & (LeftHat=2)): 0;
-- ((proc2.line=26) & (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=17) & (proc1.local_pushR_RH=1)): 2; -- if another pushRight
-- ???
((proc1.line=17) & (proc1.local_pushR_RH=2)): 3; -- newnode
((proc1.line=9) & (proc1.local_popR_RH=2) & (RightHat=2)): 0;
-- ((proc1.line=9) & (RightHat=2)): 0;
((proc1.line=25) & !FAIL & (proc1.local_popL_LH=2)): 2;
-- (proc2.line=11): 0;
((proc2.line=17) & (proc2.local_pushR_RH=2)): 3; -- newnode
-- ((proc1.line=17) & (proc1.local_pushR_RH=1)): 2; -- if another pushRight
-- ???
((proc2.line=9) & (proc1.local_popR_RH=2) & (RightHat=2)): 0;
-- ((proc2.line=9) & (RightHat=2)): 0;
((proc2.line=25) & !FAIL & (proc2.local_popL_LH=2)): 2;
TRUE: AllNodes[2][1];
esac;
-- L<-Z
next(AllNodes[3][0]) :=
case
((proc2.line=16) & proc2.local_pushR_RH=1): 1;
((proc2.line=16) & proc2.local_pushR_RH=2): 2;
-- ((proc1.line=16) & proc1.local_pushR_RH=3): 3;
TRUE: AllNodes[3][0];
esac;
next(AllNodes[3][1]) :=
case
(proc2.line=11): 0;
TRUE: AllNodes[3][1]; -- Z->Y
esac;
-- --- when DCAS fails, error
-- init(FAIL) := false;
-- next(FAIL) :=
-- case
-- ((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))))
-- 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))));
-- |((proc3.line=5) & ( !(RightHat=proc3.local_popR_RH)
-- | !(LeftHat=proc3.local_popR_LH)))
-- |((proc3.line=8) & ( !(RightHat=proc3.local_popR_RH)
-- | !(proc3.local_popR_RH=1 -> (AllNodes[1][0]=proc3.local_popR_RHL))
-- | !(proc3.local_popR_RH=2 -> (AllNodes[2][0]=proc3.local_popR_RHL))
-- | !(proc3.local_popR_RH=3 -> (AllNodes[3][0]=proc3.local_popR_RHL))))
-- |((proc3.line=22) & ( !(RightHat=proc3.local_popL_RH)
-- | !(LeftHat=proc3.local_popL_LH)))
-- |((proc3.line=25) & ( !(LeftHat=proc3.local_popL_LH)
-- | !(proc3.local_popL_LH=1 -> (AllNodes[1][1]=proc3.local_popL_LHR))
-- | !(proc3.local_popL_LH=2 -> (AllNodes[2][1]=proc3.local_popL_LHR))
-- | !(proc3.local_popL_LH=3 -> (AllNodes[3][1]=proc3.local_popL_LHR))));
-- --- if full
-- |((proc1.line=13) & RightHat=2)
-- |((proc2.line=13) & RightHat=2);
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);
-- popLeft_X := (proc1.L_popped_X | proc2.L_popped_X | proc3.L_popped_X);
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
-- STNAD BY
-- (line=0) : {10}; -- STAND BY: could go to line:1/ line:10/ line:19
-- temp schedue
(line=0 & ProcID=1) : {0,1};
-- (line=0 & ProcID=1 & RightHat=2) : {1};
-- (line=0 & ProcID=1 & !(RightHat=2)) : {1,19}; -- STAND BY: could go to line:1/ line:10/ line:19
(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) : {0,1};
(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=0 & ProcID=3) : {1};
-- popRIGHT() start
-- (line=1 & LeftHat=0 & RightHat=0 & ProcID=1) : {1,2};
-- (line=1 & LeftHat=1 & RightHat=1 & ProcID=1) : {1,2};
-- (line=1 & LeftHat=1 & RightHat=2 & ProcID=1) : {1,2};
(line=1) : {2};
-- (line=1 & ProcID=1) : {2}; -- popRight() starts, getRightHat as rh
-- (line=1 & ProcID=2) : {2};
-- (line=1 & ProcID=3) : {2};
-- (line=2) : {3}; -- getLeftHat as lh
(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=2 & LeftHat=2 & RightHat=2 & 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 & LeftHat=1 & RightHat=2 & ProcID=1) : {2,3};
-- (line=3 & (AllNodes[local_popR_RH][1] = local_popR_RH)) : {0}; -- if (rh is self-pointing) return assign popRight_FAIL
(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};
--- Check your TOKEN only if you are change global variables
-- (line=3 & !(AllNodes[local_popR_RH][1] = local_popR_RH)) : {4}; -- if !(rh is self-pointing), go to 4
-- (line=4 & (local_popR_RH = local_popR_LH)) : {5};
(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=5) : {6}; -- DCAS (RightHat, LeftHat, rh, lh, Dummy, Dummy)
(line=6) : {6,0}; -- assign pop_result as rh->V, END
-- (line=4 & !(local_popR_RH = local_popR_LH)) : {7}; -- 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=7) : {7,8}; --assign rhl as rh->L -- proc1 could stuck --could delay
-- (line=7 & !RightHat=0) : {8}; --assign rhl as rh->L
(line=8) : {9}; -- DCAS (RightHat, rh->L, rh, rhL, rhL, rh)
--
-- (line=8 & COLLISION) : {0};
-- (line=8 & !COLLISION) : {9};
(line=9) : {9,0}; -- assign popRight_result as rh->V, assign rh->R as DUMMY
-- pushRIGHT
(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=14) : {15}; -- DCAS (RightHat, LeftHat, rh, lh, nd, nd)
-- (line=15) : {19}; -- return pushRight_SUCCESS
(line=15) : {0}; -- return pushRight_SUCCESS
(line=13 & !(local_pushR_RH = local_pushR_RHR)) : {16}; -- if !(rh == rhR) assign nd->L as rh
(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=18) : {19}; -- return pushRight_SUCCESS
-- popLeft
(line=19) : {20}; --- popLeft() starts, assign lh as LeftHat, assign rh as RightHat
-- (line=20) : {0} ; --if (lh is self-pointing), return assign popLeft_FAIL
(line=20) : {21}; -- if(!lh is self-pointing)
(line=21 & (local_popL_LH =local_popL_RH)) : {21, 22}; -- if(lh == rh)
(line=22) : {23}; -- DCAS (LeftHat, RightHat, lh, rh, Dummy, Dummy)
(line=23) : {0}; -- assign popLeft_result as lh -> V, END
(line=21 & !(local_popL_LH =local_popL_RH)) : {24}; -- if!(lh == rh)
(line=24) : {24,25}; -- assign lhR as lh->R -- could delay
-- (line=24 & local_popL_LH=2) : {24,25}; -- proc2 could stuck
(line=25) : {26}; -- DCAS (LeftHat, lh->R, lh, lhR, lfR, lh)
-- (line=26) : {0}; -- assign popLeft_result as lh->V, assign lh_L as DDUMMY
(line=26 & L_popped_X) : {19};
-- (line=26 & L_popped_Y) : {1};
TRUE: line; -- default case
esac;
-- local_popR local variables
next(local_popR_RH) :=
case
(line=1) : RightHat;
-- (line=1 & RightHat=1) : 1;
-- (line=1 & RightHat=2) : 2;
TRUE : local_popR_RH; -- default case
esac;
next(local_popR_LH) :=
case
(line=2) : LeftHat;
-- (line=2 & LeftHat=1) : 1;
-- (line=2 & LeftHat=2) : 2;
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;
-- next(local_popR_return_empty) :=
-- case
-- (line=3 & (AllNodes[local_popR_RH][1] = local_popR_RH)) : TRUE;
-- TRUE : FALSE; -- 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;
-- next(local_pushR_newnode) := local_pushR_newnode;
-- 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);
-- temp_trigger := (line=24 & local_popL_LH=2 & ProcID=2); --temp to move proc3
-- 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. 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);
-- 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]) := 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);
-- popLeft_X := (proc1.L_popped_X | proc2.L_popped_X | proc3.L_popped_X);
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=1 & RightHat=2) : {1}; -- STAND BY: could go to line:1/ line:4/ line:7
-- (line=0 & ProcID=1 & !(RightHat=2)) : {1,7};
(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=2) : {2,3}; -- wait -- this is super slow
(line=3) : {0}; -- popRight() Return, End
(line=4) : {5}; -- pushRight() starts, changing nodes
(line=5) : {5,0}; -- wait
-- (line=6) : {0}; -- pushRight End
(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};
-- (line=8) : {8,0}; -- wait -- this is super slow
-- (line=9) : {0}; -- pushRight End
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
forall A. exists B.
~(G(~GlobalQueue-FAIL[A] /\ ~GlobalQueue-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]))
/\ (GlobalQueue-popRightFAIL[A] <-> GlobalQueue-popRightFAIL[B])
/\ (GlobalQueue-popLeft_X[A] <-> GlobalQueue-popLeft_X[B])
/\ (GlobalQueue-popLeft_Y[A] <-> GlobalQueue-popLeft_Y[B])
/\ (GlobalQueue-popRight_Y[A] <-> GlobalQueue-popLeft_Y[B])
/\ (GlobalQueue-popRight_Z[A] <-> GlobalQueue-popRight_Z[B])))