I'm trying to use TLA+ write spec to verify concurrency correctness of my production problem:
one producer produce msg to Q a,
if it found no more consumer was scheduled. it schedule one consumer by send a notifyMsg to nofityQ b,
multiple consumers poll the notifyQ and consume the Q a to consume the msg.
each consumer will consume batch of msgs, then sleep and retry to pull notifyQ b.
to promise only one consumer process the Q a at any time point. the producer and consumer must make sure exactly one NotifyMsg send to notifyQ b.
there are third type Thread, IdleHandler, check the Q a is empty more than some time, it try to release the Q for release memory hold by this Queue.
thesis three type of thread concurrently working:
1. one producer thread
2. many consumer thread
3. one idleHandler thread
the following spec will translated, but after translated, parse failed with error Msg:
***Parse Error***
Encountered "Beginning of definition" at line 229, column 38 in module TableQueueVerify
Residual stack trace follows:
ExtendableExpr starting at line 229, column 24.
_expression_ starting at line 229, column 24.
IF THEN ELSE starting at line 229, column 21.
_expression_ starting at line 229, column 21.
Junction Item starting at line 229, column 18.
-------------------------- MODULE TableQueueVerify --------------------------
EXTENDS Integers
CONSTANT DispatchCmd, TableCMD
(* --algorithm tableQueue
variables
dispatchQueue = <<>>;
tableCmdQueue = [emptyQueue |-> FALSE, q |-> <<>>];
dispatchState = [consume |-> 0, produce |-> 0];
consumeLock = 0;
tableQueueLock = 0;
needFireDispatchMap = [produce |-> FALSE];
procedure setNeedDispatch(irole)
begin
\* !bufferQueue.empty
SND_T_N_EMPTY:
if Len(tableCmdQueue.q) /= 0 then
\* bufferState & CONSUME == 0
SND_N_C:
if dispatchState.consume == 0 then
\* bufferState &= CONSUME
dispatchState.consume := 1;
\* need = true
needFireDispatchMap[irole] := TRUE;
end if;
end if;
end procedure;
procedure needFireDispatch(role)
variable locked = FALSE;
begin NEED_FIRE:
needFireDispatchMap[role] := FALSE;
\* bufferState & CONSUME == 0
NF_LOOP:
while dispatchState.consume == 0 do
\* !bufferQueue.isEmpty
NF_T_TQ_N_E:
if Len(tableCmdQueue) /= 0 then
\* !consumeLock.get()
NF_C_N_L:
if consumeLock == 0 then
\* CAS -> consumeLock
TRY_LOCK:
if consumeLock == 0 then
consumeLock := 1;
locked := TRUE;
end if;
\* CAS succeed!
LOCKED:
if locked then
call setNeedDispatch(role);
UNLOCK:
\* consumeLock.set(false)
consumeLock := 0;
\* break;
goto NF_RET;
end if;
end if;
else
goto NF_RET;
end if;
end while;
NF_RET:
skip;
end procedure;
procedure scheduleDispatch()
begin D:
dispatchQueue := Append(dispatchQueue, DispatchCmd);
end procedure;
process consumer \in 1..10
variables
tableQueueCmd;
begin CONSUME:
needFireDispatchMap[self] := FALSE;
C_LOOP:
while TRUE do
Acquire_C:
await dispatchQueue /= <<>>;
tableQueueCmd := Head(dispatchQueue);
dispatchQueue := Tail(dispatchQueue);
\* start to consume
skip;
\* test Dispatch cancelable
if Len(tableCmdQueue.q) == 0 then
dispatchState.consume := 0;
call needFireDispatch(self);
C_TEST_R:
if needFireDispatch[self] then
call scheduleDispatch();
end if;
else
call scheduleDispatch();
end if;
end while;
end process;
process producer = 100
begin Produce:
while TRUE do
\* acquire queue and set In-produce state
Acquire_P:
while TRUE do
if tableQueueLock == 0 then
tableQueueLock := 1;
dispatchState.produce := 1;
goto P_OK;
end if;
end while;
P_OK:
skip;
\* put cmd to CMD_QUEUE
tableCmdQueue.q := Append(tableCmdQueue.q, TableCMD);
\* test Queue size == 1
if Len(tableCmdQueue) == 1 then
\* tryFireDispatch
call needFireDispatch('produce');
P_TEST_R:
if needFireDispatch.produce == 1 then
call scheduleDispatch();
end if;
end if;
\* leave: unset In-produce state
LEAVE:
dispatchState.produce := 0;
end while;
end process;
process idleHandler = 200
variable iLocked = FALSE;
begin IDLE_HANDLE:
while TRUE do
\* fast check any condition volatile
\* bufferQeueu == empty
IDLE_TQ_EMPTY:
if tableCmdQueue.empty then
goto LOOP_END;
end if;
\* bufferState != 0
DQ_IN_CONSUME:
if dispatchState.consume /= 0 then
goto LOOP_END;
end if;
DQ_IN_PRODUCE:
if diispatchState.produce /= 0 then
goto LOOP_END;
end if;
\* bufferQeueue.empty
TQ_N_EMPTY:
if Len(tableCmdQueue.q) /= 0 then
goto LOOP_END;
end if;
\* bufferLock.get()
TQ_LOCKED:
if tableQueueLock /= 0 then
goto LOOP_END;
end if;
\* acquire CMD_QUEUE's lock
AcquireLock_IDLE:
if tableQueueLock == 0 then
tableQueueLock := 1;
iLocked := TRUE;
end if;
if iLocked then
\* test Not In-produce
if dispatchState.produce == 0 then
\* test Queue's empty
if Len(tableCmdQueue.q) == 0 then
\* swap Qeueue if test pass
tableCmdQueue.empty := TRUE ||
tableCmdQueue.q := <<>>;
end if;
end if;
\* leave: release CMD_QUEUE's lock
ReleaseLock_IDLE:
tableQueueLock := 0;
end if;
LOOP_END:
skip;
end while;
end process;
end algorithm; *)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES dispatchQueue, tableCmdQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, pc, stack, irole, role, locked,
tableQueueCmd, iLocked
vars == << dispatchQueue, tableCmdQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, pc, stack, irole, role,
locked, tableQueueCmd, iLocked >>
ProcSet == (1..10) \cup {100} \cup {200}
Init == (* Global variables *)
/\ dispatchQueue = <<>>
/\ tableCmdQueue = [emptyQueue |-> FALSE, q |-> <<>>]
/\ dispatchState = [consume |-> 0, produce |-> 0]
/\ consumeLock = 0
/\ tableQueueLock = 0
/\ needFireDispatchMap = [produce |-> FALSE]
(* Procedure setNeedDispatch *)
/\ irole = [ self \in ProcSet |-> defaultInitValue]
(* Procedure needFireDispatch *)
/\ role = [ self \in ProcSet |-> defaultInitValue]
/\ locked = [ self \in ProcSet |-> FALSE]
(* Process consumer *)
/\ tableQueueCmd = [self \in 1..10 |-> defaultInitValue]
(* Process idleHandler *)
/\ iLocked = FALSE
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self \in 1..10 -> "CONSUME"
[] self = 100 -> "Produce"
[] self = 200 -> "IDLE_HANDLE"]
SND_T_N_EMPTY(self) == /\ pc[self] = "SND_T_N_EMPTY"
/\ IF Len(tableCmdQueue.q) /= 0
THEN /\ pc' = [pc EXCEPT ![self] = "SND_N_C"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue,
dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap,
stack, irole, role, locked,
tableQueueCmd, iLocked >>
SND_N_C(self) == /\ pc[self] = "SND_N_C"
/\ IF dispatchState.consume == 0
THEN /\ dispatchState' = [dispatchState EXCEPT !.consume = 1]
/\ needFireDispatchMap' = [needFireDispatchMap EXCEPT ![irole[self]] = TRUE]
ELSE /\ TRUE
/\ UNCHANGED << dispatchState, needFireDispatchMap >>
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, consumeLock,
tableQueueLock, stack, irole, role, locked,
tableQueueCmd, iLocked >>
setNeedDispatch(self) == SND_T_N_EMPTY(self) \/ SND_N_C(self)
NEED_FIRE(self) == /\ pc[self] = "NEED_FIRE"
/\ needFireDispatchMap' = [needFireDispatchMap EXCEPT ![role[self]] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "NF_LOOP"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, stack, irole,
role, locked, tableQueueCmd, iLocked >>
NF_LOOP(self) == /\ pc[self] = "NF_LOOP"
/\ IF dispatchState.consume == 0
THEN /\ pc' = [pc EXCEPT ![self] = "NF_T_TQ_N_E"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_RET"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
NF_T_TQ_N_E(self) == /\ pc[self] = "NF_T_TQ_N_E"
/\ IF Len(tableCmdQueue) /= 0
THEN /\ pc' = [pc EXCEPT ![self] = "NF_C_N_L"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_RET"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue,
dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd,
iLocked >>
NF_C_N_L(self) == /\ pc[self] = "NF_C_N_L"
/\ IF consumeLock == 0
THEN /\ pc' = [pc EXCEPT ![self] = "TRY_LOCK"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_LOOP"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
TRY_LOCK(self) == /\ pc[self] = "TRY_LOCK"
/\ IF consumeLock == 0
THEN /\ consumeLock' = 1
/\ locked' = [locked EXCEPT ![self] = TRUE]
ELSE /\ TRUE
/\ UNCHANGED << consumeLock, locked >>
/\ pc' = [pc EXCEPT ![self] = "LOCKED"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
tableQueueLock, needFireDispatchMap, stack,
irole, role, tableQueueCmd, iLocked >>
LOCKED(self) == /\ pc[self] = "LOCKED"
/\ IF locked[self]
THEN /\ /\ irole' = [irole EXCEPT ![self] = role[self]]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "setNeedDispatch",
pc |-> "UNLOCK",
irole |-> irole[self] ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "SND_T_N_EMPTY"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_LOOP"]
/\ UNCHANGED << stack, irole >>
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, role, locked,
tableQueueCmd, iLocked >>
UNLOCK(self) == /\ pc[self] = "UNLOCK"
/\ consumeLock' = 0
/\ pc' = [pc EXCEPT ![self] = "NF_RET"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
tableQueueLock, needFireDispatchMap, stack,
irole, role, locked, tableQueueCmd, iLocked >>
NF_RET(self) == /\ pc[self] = "NF_RET"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
needFireDispatch(self) == NEED_FIRE(self) \/ NF_LOOP(self)
\/ NF_T_TQ_N_E(self) \/ NF_C_N_L(self)
\/ TRY_LOCK(self) \/ LOCKED(self)
\/ UNLOCK(self) \/ NF_RET(self)
D(self) == /\ pc[self] = "D"
/\ dispatchQueue' = Append(dispatchQueue, DispatchCmd)
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << tableCmdQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, stack, irole,
role, locked, tableQueueCmd, iLocked >>
scheduleDispatch(self) == D(self)
CONSUME(self) == /\ pc[self] = "CONSUME"
/\ needFireDispatchMap' = [needFireDispatchMap EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "C_LOOP"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, stack, irole,
role, locked, tableQueueCmd, iLocked >>
C_LOOP(self) == /\ pc[self] = "C_LOOP"
/\ pc' = [pc EXCEPT ![self] = "Acquire_C"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
Acquire_C(self) == /\ pc[self] = "Acquire_C"
/\ dispatchQueue /= <<>>
/\ tableQueueCmd' = [tableQueueCmd EXCEPT ![self] = Head(dispatchQueue)]
/\ dispatchQueue' = Tail(dispatchQueue)
/\ TRUE
/\ IF Len(tableCmdQueue.q) == 0
THEN /\ dispatchState' = [dispatchState EXCEPT !.consume = 0]
/\ /\ role' = [role EXCEPT ![self] = self]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "needFireDispatch",
pc |-> "C_TEST_R",
locked |-> locked[self],
role |-> role[self] ] >>
\o stack[self]]
/\ locked' = [locked EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "NEED_FIRE"]
ELSE /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "scheduleDispatch",
pc |-> "C_LOOP" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "D"]
/\ UNCHANGED << dispatchState, role, locked >>
/\ UNCHANGED << tableCmdQueue, consumeLock, tableQueueLock,
needFireDispatchMap, irole, iLocked >>
C_TEST_R(self) == /\ pc[self] = "C_TEST_R"
/\ IF needFireDispatch[self]
THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "scheduleDispatch",
pc |-> "C_LOOP" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "D"]
ELSE /\ pc' = [pc EXCEPT ![self] = "C_LOOP"]
/\ stack' = stack
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, irole, role, locked,
tableQueueCmd, iLocked >>
consumer(self) == CONSUME(self) \/ C_LOOP(self) \/ Acquire_C(self)
\/ C_TEST_R(self)
Produce == /\ pc[100] = "Produce"
/\ pc' = [pc EXCEPT ![100] = "Acquire_P"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd, iLocked >>
Acquire_P == /\ pc[100] = "Acquire_P"
/\ IF tableQueueLock == 0
THEN /\ tableQueueLock' = 1
/\ dispatchState' = [dispatchState EXCEPT !.produce = 1]
/\ pc' = [pc EXCEPT ![100] = "P_OK"]
ELSE /\ pc' = [pc EXCEPT ![100] = "Acquire_P"]
/\ UNCHANGED << dispatchState, tableQueueLock >>
/\ UNCHANGED << dispatchQueue, tableCmdQueue, consumeLock,
needFireDispatchMap, stack, irole, role, locked,
tableQueueCmd, iLocked >>
P_OK == /\ pc[100] = "P_OK"
/\ TRUE
/\ tableCmdQueue' = [tableCmdQueue EXCEPT !.q = Append(tableCmdQueue.q, TableCMD)]
/\ IF Len(tableCmdQueue') == 1
THEN /\ /\ role' = [role EXCEPT ![100] = 'produce']
/\ stack' = [stack EXCEPT ![100] = << [ procedure |-> "needFireDispatch",
pc |-> "P_TEST_R",
locked |-> locked[100],
role |-> role[100] ] >>
\o stack[100]]
/\ locked' = [locked EXCEPT ![100] = FALSE]
/\ pc' = [pc EXCEPT ![100] = "NEED_FIRE"]
ELSE /\ pc' = [pc EXCEPT ![100] = "LEAVE"]
/\ UNCHANGED << stack, role, locked >>
/\ UNCHANGED << dispatchQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, irole,
tableQueueCmd, iLocked >>
P_TEST_R == /\ pc[100] = "P_TEST_R"
/\ IF needFireDispatch.produce == 1
THEN /\ stack' = [stack EXCEPT ![100] = << [ procedure |-> "scheduleDispatch",
pc |-> "LEAVE" ] >>
\o stack[100]]
/\ pc' = [pc EXCEPT ![100] = "D"]
ELSE /\ pc' = [pc EXCEPT ![100] = "LEAVE"]
/\ stack' = stack
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
irole, role, locked, tableQueueCmd, iLocked >>
LEAVE == /\ pc[100] = "LEAVE"
/\ dispatchState' = [dispatchState EXCEPT !.produce = 0]
/\ pc' = [pc EXCEPT ![100] = "Produce"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, consumeLock,
tableQueueLock, needFireDispatchMap, stack, irole,
role, locked, tableQueueCmd, iLocked >>
producer == Produce \/ Acquire_P \/ P_OK \/ P_TEST_R \/ LEAVE
IDLE_HANDLE == /\ pc[200] = "IDLE_HANDLE"
/\ pc' = [pc EXCEPT ![200] = "IDLE_TQ_EMPTY"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role, locked,
tableQueueCmd, iLocked >>
IDLE_TQ_EMPTY == /\ pc[200] = "IDLE_TQ_EMPTY"
/\ IF tableCmdQueue.empty
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "DQ_IN_CONSUME"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
DQ_IN_CONSUME == /\ pc[200] = "DQ_IN_CONSUME"
/\ IF dispatchState.consume /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "DQ_IN_PRODUCE"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
DQ_IN_PRODUCE == /\ pc[200] = "DQ_IN_PRODUCE"
/\ IF diispatchState.produce /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "TQ_N_EMPTY"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
TQ_N_EMPTY == /\ pc[200] = "TQ_N_EMPTY"
/\ IF Len(tableCmdQueue.q) /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "TQ_LOCKED"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd,
iLocked >>
TQ_LOCKED == /\ pc[200] = "TQ_LOCKED"
/\ IF tableQueueLock /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "AcquireLock_IDLE"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd,
iLocked >>
AcquireLock_IDLE == /\ pc[200] = "AcquireLock_IDLE"
/\ IF tableQueueLock == 0
THEN /\ tableQueueLock' = 1
/\ iLocked' = TRUE
ELSE /\ TRUE
/\ UNCHANGED << tableQueueLock, iLocked >>
/\ IF iLocked'
THEN /\ IF dispatchState.produce == 0
THEN /\ IF Len(tableCmdQueue.q) == 0
THEN /\ tableCmdQueue' = [tableCmdQueue EXCEPT !.empty = TRUE,
!.q = <<>>]
ELSE /\ TRUE
/\ UNCHANGED tableCmdQueue
ELSE /\ TRUE
/\ UNCHANGED tableCmdQueue
/\ pc' = [pc EXCEPT ![200] = "ReleaseLock_IDLE"]
ELSE /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
/\ UNCHANGED tableCmdQueue
/\ UNCHANGED << dispatchQueue, dispatchState, consumeLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd >>
ReleaseLock_IDLE == /\ pc[200] = "ReleaseLock_IDLE"
/\ tableQueueLock' = 0
/\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue,
dispatchState, consumeLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
LOOP_END == /\ pc[200] = "LOOP_END"
/\ TRUE
/\ pc' = [pc EXCEPT ![200] = "IDLE_HANDLE"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd, iLocked >>
idleHandler == IDLE_HANDLE \/ IDLE_TQ_EMPTY \/ DQ_IN_CONSUME
\/ DQ_IN_PRODUCE \/ TQ_N_EMPTY \/ TQ_LOCKED
\/ AcquireLock_IDLE \/ ReleaseLock_IDLE \/ LOOP_END
Next == producer \/ idleHandler
\/ (\E self \in ProcSet: \/ setNeedDispatch(self)
\/ needFireDispatch(self)
\/ scheduleDispatch(self))
\/ (\E self \in 1..10: consumer(self))
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
=============================================================================
\* Modification History
\* Last modified Tue Nov 19 00:41:13 CST 2019 by lambdacat
\* Created Mon Nov 18 19:00:24 CST 2019 by lambdacat
-------------------------- MODULE TableQueueVerify --------------------------
EXTENDS Integers
CONSTANT DispatchCmd, TableCMD
(* --algorithm tableQueue
variables
dispatchQueue = <<>>;
tableCmdQueue = [emptyQueue |-> FALSE, q |-> <<>>];
dispatchState = [consume |-> 0, produce |-> 0];
consumeLock = 0;
tableQueueLock = 0;
needFireDispatchMap = [produce |-> FALSE];
procedure setNeedDispatch(irole)
begin
\* !bufferQueue.empty
SND_T_N_EMPTY:
if Len(tableCmdQueue.q) /= 0 then
\* bufferState & CONSUME == 0
SND_N_C:
if dispatchState.consume == 0 then
\* bufferState &= CONSUME
dispatchState.consume := 1;
\* need = true
needFireDispatchMap[irole] := TRUE;
end if;
end if;
end procedure;
procedure needFireDispatch(role)
variable locked = FALSE;
begin NEED_FIRE:
needFireDispatchMap[role] := FALSE;
\* bufferState & CONSUME == 0
NF_LOOP:
while dispatchState.consume == 0 do
\* !bufferQueue.isEmpty
NF_T_TQ_N_E:
if Len(tableCmdQueue) /= 0 then
\* !consumeLock.get()
NF_C_N_L:
if consumeLock == 0 then
\* CAS -> consumeLock
TRY_LOCK:
if consumeLock == 0 then
consumeLock := 1;
locked := TRUE;
end if;
\* CAS succeed!
LOCKED:
if locked then
call setNeedDispatch(role);
UNLOCK:
\* consumeLock.set(false)
consumeLock := 0;
\* break;
goto NF_RET;
end if;
end if;
else
goto NF_RET;
end if;
end while;
NF_RET:
skip;
end procedure;
procedure scheduleDispatch()
begin D:
dispatchQueue := Append(dispatchQueue, DispatchCmd);
end procedure;
process consumer \in 1..10
variables
tableQueueCmd;
begin CONSUME:
needFireDispatchMap[self] := FALSE;
C_LOOP:
while TRUE do
Acquire_C:
await dispatchQueue /= <<>>;
tableQueueCmd := Head(dispatchQueue);
dispatchQueue := Tail(dispatchQueue);
\* start to consume
skip;
\* test Dispatch cancelable
if Len(tableCmdQueue.q) == 0 then
dispatchState.consume := 0;
call needFireDispatch(self);
C_TEST_R:
if needFireDispatch[self] then
call scheduleDispatch();
end if;
else
call scheduleDispatch();
end if;
end while;
end process;
process producer = 100
begin Produce:
while TRUE do
\* acquire queue and set In-produce state
Acquire_P:
while TRUE do
if tableQueueLock == 0 then
tableQueueLock := 1;
dispatchState.produce := 1;
goto P_OK;
end if;
end while;
P_OK:
skip;
\* put cmd to CMD_QUEUE
tableCmdQueue.q := Append(tableCmdQueue.q, TableCMD);
\* test Queue size == 1
if Len(tableCmdQueue) == 1 then
\* tryFireDispatch
call needFireDispatch('produce');
P_TEST_R:
if needFireDispatch.produce == 1 then
call scheduleDispatch();
end if;
end if;
\* leave: unset In-produce state
LEAVE:
dispatchState.produce := 0;
end while;
end process;
process idleHandler = 200
variable iLocked = FALSE;
begin IDLE_HANDLE:
while TRUE do
\* fast check any condition volatile
\* bufferQeueu == empty
IDLE_TQ_EMPTY:
if tableCmdQueue.empty then
goto LOOP_END;
end if;
\* bufferState != 0
DQ_IN_CONSUME:
if dispatchState.consume /= 0 then
goto LOOP_END;
end if;
DQ_IN_PRODUCE:
if diispatchState.produce /= 0 then
goto LOOP_END;
end if;
\* bufferQeueue.empty
TQ_N_EMPTY:
if Len(tableCmdQueue.q) /= 0 then
goto LOOP_END;
end if;
\* bufferLock.get()
TQ_LOCKED:
if tableQueueLock /= 0 then
goto LOOP_END;
end if;
\* acquire CMD_QUEUE's lock
AcquireLock_IDLE:
if tableQueueLock == 0 then
tableQueueLock := 1;
iLocked := TRUE;
end if;
if iLocked then
\* test Not In-produce
if dispatchState.produce == 0 then
\* test Queue's empty
if Len(tableCmdQueue.q) == 0 then
\* swap Qeueue if test pass
tableCmdQueue.empty := TRUE ||
tableCmdQueue.q := <<>>;
end if;
end if;
\* leave: release CMD_QUEUE's lock
ReleaseLock_IDLE:
tableQueueLock := 0;
end if;
LOOP_END:
skip;
end while;
end process;
end algorithm; *)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES dispatchQueue, tableCmdQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, pc, stack, irole, role, locked,
tableQueueCmd, iLocked
vars == << dispatchQueue, tableCmdQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, pc, stack, irole, role,
locked, tableQueueCmd, iLocked >>
ProcSet == (1..10) \cup {100} \cup {200}
Init == (* Global variables *)
/\ dispatchQueue = <<>>
/\ tableCmdQueue = [emptyQueue |-> FALSE, q |-> <<>>]
/\ dispatchState = [consume |-> 0, produce |-> 0]
/\ consumeLock = 0
/\ tableQueueLock = 0
/\ needFireDispatchMap = [produce |-> FALSE]
(* Procedure setNeedDispatch *)
/\ irole = [ self \in ProcSet |-> defaultInitValue]
(* Procedure needFireDispatch *)
/\ role = [ self \in ProcSet |-> defaultInitValue]
/\ locked = [ self \in ProcSet |-> FALSE]
(* Process consumer *)
/\ tableQueueCmd = [self \in 1..10 |-> defaultInitValue]
(* Process idleHandler *)
/\ iLocked = FALSE
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self \in 1..10 -> "CONSUME"
[] self = 100 -> "Produce"
[] self = 200 -> "IDLE_HANDLE"]
SND_T_N_EMPTY(self) == /\ pc[self] = "SND_T_N_EMPTY"
/\ IF Len(tableCmdQueue.q) /= 0
THEN /\ pc' = [pc EXCEPT ![self] = "SND_N_C"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue,
dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap,
stack, irole, role, locked,
tableQueueCmd, iLocked >>
SND_N_C(self) == /\ pc[self] = "SND_N_C"
/\ IF dispatchState.consume == 0
THEN /\ dispatchState' = [dispatchState EXCEPT !.consume = 1]
/\ needFireDispatchMap' = [needFireDispatchMap EXCEPT ![irole[self]] = TRUE]
ELSE /\ TRUE
/\ UNCHANGED << dispatchState, needFireDispatchMap >>
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, consumeLock,
tableQueueLock, stack, irole, role, locked,
tableQueueCmd, iLocked >>
setNeedDispatch(self) == SND_T_N_EMPTY(self) \/ SND_N_C(self)
NEED_FIRE(self) == /\ pc[self] = "NEED_FIRE"
/\ needFireDispatchMap' = [needFireDispatchMap EXCEPT ![role[self]] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "NF_LOOP"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, stack, irole,
role, locked, tableQueueCmd, iLocked >>
NF_LOOP(self) == /\ pc[self] = "NF_LOOP"
/\ IF dispatchState.consume == 0
THEN /\ pc' = [pc EXCEPT ![self] = "NF_T_TQ_N_E"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_RET"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
NF_T_TQ_N_E(self) == /\ pc[self] = "NF_T_TQ_N_E"
/\ IF Len(tableCmdQueue) /= 0
THEN /\ pc' = [pc EXCEPT ![self] = "NF_C_N_L"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_RET"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue,
dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd,
iLocked >>
NF_C_N_L(self) == /\ pc[self] = "NF_C_N_L"
/\ IF consumeLock == 0
THEN /\ pc' = [pc EXCEPT ![self] = "TRY_LOCK"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_LOOP"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
TRY_LOCK(self) == /\ pc[self] = "TRY_LOCK"
/\ IF consumeLock == 0
THEN /\ consumeLock' = 1
/\ locked' = [locked EXCEPT ![self] = TRUE]
ELSE /\ TRUE
/\ UNCHANGED << consumeLock, locked >>
/\ pc' = [pc EXCEPT ![self] = "LOCKED"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
tableQueueLock, needFireDispatchMap, stack,
irole, role, tableQueueCmd, iLocked >>
LOCKED(self) == /\ pc[self] = "LOCKED"
/\ IF locked[self]
THEN /\ /\ irole' = [irole EXCEPT ![self] = role[self]]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "setNeedDispatch",
pc |-> "UNLOCK",
irole |-> irole[self] ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "SND_T_N_EMPTY"]
ELSE /\ pc' = [pc EXCEPT ![self] = "NF_LOOP"]
/\ UNCHANGED << stack, irole >>
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, role, locked,
tableQueueCmd, iLocked >>
UNLOCK(self) == /\ pc[self] = "UNLOCK"
/\ consumeLock' = 0
/\ pc' = [pc EXCEPT ![self] = "NF_RET"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
tableQueueLock, needFireDispatchMap, stack,
irole, role, locked, tableQueueCmd, iLocked >>
NF_RET(self) == /\ pc[self] = "NF_RET"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
needFireDispatch(self) == NEED_FIRE(self) \/ NF_LOOP(self)
\/ NF_T_TQ_N_E(self) \/ NF_C_N_L(self)
\/ TRY_LOCK(self) \/ LOCKED(self)
\/ UNLOCK(self) \/ NF_RET(self)
D(self) == /\ pc[self] = "D"
/\ dispatchQueue' = Append(dispatchQueue, DispatchCmd)
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << tableCmdQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, stack, irole,
role, locked, tableQueueCmd, iLocked >>
scheduleDispatch(self) == D(self)
CONSUME(self) == /\ pc[self] = "CONSUME"
/\ needFireDispatchMap' = [needFireDispatchMap EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "C_LOOP"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, stack, irole,
role, locked, tableQueueCmd, iLocked >>
C_LOOP(self) == /\ pc[self] = "C_LOOP"
/\ pc' = [pc EXCEPT ![self] = "Acquire_C"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
Acquire_C(self) == /\ pc[self] = "Acquire_C"
/\ dispatchQueue /= <<>>
/\ tableQueueCmd' = [tableQueueCmd EXCEPT ![self] = Head(dispatchQueue)]
/\ dispatchQueue' = Tail(dispatchQueue)
/\ TRUE
/\ IF Len(tableCmdQueue.q) == 0
THEN /\ dispatchState' = [dispatchState EXCEPT !.consume = 0]
/\ /\ role' = [role EXCEPT ![self] = self]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "needFireDispatch",
pc |-> "C_TEST_R",
locked |-> locked[self],
role |-> role[self] ] >>
\o stack[self]]
/\ locked' = [locked EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "NEED_FIRE"]
ELSE /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "scheduleDispatch",
pc |-> "C_LOOP" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "D"]
/\ UNCHANGED << dispatchState, role, locked >>
/\ UNCHANGED << tableCmdQueue, consumeLock, tableQueueLock,
needFireDispatchMap, irole, iLocked >>
C_TEST_R(self) == /\ pc[self] = "C_TEST_R"
/\ IF needFireDispatch[self]
THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "scheduleDispatch",
pc |-> "C_LOOP" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "D"]
ELSE /\ pc' = [pc EXCEPT ![self] = "C_LOOP"]
/\ stack' = stack
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, irole, role, locked,
tableQueueCmd, iLocked >>
consumer(self) == CONSUME(self) \/ C_LOOP(self) \/ Acquire_C(self)
\/ C_TEST_R(self)
Produce == /\ pc[100] = "Produce"
/\ pc' = [pc EXCEPT ![100] = "Acquire_P"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd, iLocked >>
Acquire_P == /\ pc[100] = "Acquire_P"
/\ IF tableQueueLock == 0
THEN /\ tableQueueLock' = 1
/\ dispatchState' = [dispatchState EXCEPT !.produce = 1]
/\ pc' = [pc EXCEPT ![100] = "P_OK"]
ELSE /\ pc' = [pc EXCEPT ![100] = "Acquire_P"]
/\ UNCHANGED << dispatchState, tableQueueLock >>
/\ UNCHANGED << dispatchQueue, tableCmdQueue, consumeLock,
needFireDispatchMap, stack, irole, role, locked,
tableQueueCmd, iLocked >>
P_OK == /\ pc[100] = "P_OK"
/\ TRUE
/\ tableCmdQueue' = [tableCmdQueue EXCEPT !.q = Append(tableCmdQueue.q, TableCMD)]
/\ IF Len(tableCmdQueue') == 1
THEN /\ /\ role' = [role EXCEPT ![100] = 'produce']
/\ stack' = [stack EXCEPT ![100] = << [ procedure |-> "needFireDispatch",
pc |-> "P_TEST_R",
locked |-> locked[100],
role |-> role[100] ] >>
\o stack[100]]
/\ locked' = [locked EXCEPT ![100] = FALSE]
/\ pc' = [pc EXCEPT ![100] = "NEED_FIRE"]
ELSE /\ pc' = [pc EXCEPT ![100] = "LEAVE"]
/\ UNCHANGED << stack, role, locked >>
/\ UNCHANGED << dispatchQueue, dispatchState, consumeLock,
tableQueueLock, needFireDispatchMap, irole,
tableQueueCmd, iLocked >>
P_TEST_R == /\ pc[100] = "P_TEST_R"
/\ IF needFireDispatch.produce == 1
THEN /\ stack' = [stack EXCEPT ![100] = << [ procedure |-> "scheduleDispatch",
pc |-> "LEAVE" ] >>
\o stack[100]]
/\ pc' = [pc EXCEPT ![100] = "D"]
ELSE /\ pc' = [pc EXCEPT ![100] = "LEAVE"]
/\ stack' = stack
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
irole, role, locked, tableQueueCmd, iLocked >>
LEAVE == /\ pc[100] = "LEAVE"
/\ dispatchState' = [dispatchState EXCEPT !.produce = 0]
/\ pc' = [pc EXCEPT ![100] = "Produce"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, consumeLock,
tableQueueLock, needFireDispatchMap, stack, irole,
role, locked, tableQueueCmd, iLocked >>
producer == Produce \/ Acquire_P \/ P_OK \/ P_TEST_R \/ LEAVE
IDLE_HANDLE == /\ pc[200] = "IDLE_HANDLE"
/\ pc' = [pc EXCEPT ![200] = "IDLE_TQ_EMPTY"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role, locked,
tableQueueCmd, iLocked >>
IDLE_TQ_EMPTY == /\ pc[200] = "IDLE_TQ_EMPTY"
/\ IF tableCmdQueue.empty
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "DQ_IN_CONSUME"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
DQ_IN_CONSUME == /\ pc[200] = "DQ_IN_CONSUME"
/\ IF dispatchState.consume /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "DQ_IN_PRODUCE"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
DQ_IN_PRODUCE == /\ pc[200] = "DQ_IN_PRODUCE"
/\ IF diispatchState.produce /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "TQ_N_EMPTY"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
TQ_N_EMPTY == /\ pc[200] = "TQ_N_EMPTY"
/\ IF Len(tableCmdQueue.q) /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "TQ_LOCKED"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd,
iLocked >>
TQ_LOCKED == /\ pc[200] = "TQ_LOCKED"
/\ IF tableQueueLock /= 0
THEN /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
ELSE /\ pc' = [pc EXCEPT ![200] = "AcquireLock_IDLE"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd,
iLocked >>
AcquireLock_IDLE == /\ pc[200] = "AcquireLock_IDLE"
/\ IF tableQueueLock == 0
THEN /\ tableQueueLock' = 1
/\ iLocked' = TRUE
ELSE /\ TRUE
/\ UNCHANGED << tableQueueLock, iLocked >>
/\ IF iLocked'
THEN /\ IF dispatchState.produce == 0
THEN /\ IF Len(tableCmdQueue.q) == 0
THEN /\ tableCmdQueue' = [tableCmdQueue EXCEPT !.empty = TRUE,
!.q = <<>>]
ELSE /\ TRUE
/\ UNCHANGED tableCmdQueue
ELSE /\ TRUE
/\ UNCHANGED tableCmdQueue
/\ pc' = [pc EXCEPT ![200] = "ReleaseLock_IDLE"]
ELSE /\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
/\ UNCHANGED tableCmdQueue
/\ UNCHANGED << dispatchQueue, dispatchState, consumeLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd >>
ReleaseLock_IDLE == /\ pc[200] = "ReleaseLock_IDLE"
/\ tableQueueLock' = 0
/\ pc' = [pc EXCEPT ![200] = "LOOP_END"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue,
dispatchState, consumeLock,
needFireDispatchMap, stack, irole, role,
locked, tableQueueCmd, iLocked >>
LOOP_END == /\ pc[200] = "LOOP_END"
/\ TRUE
/\ pc' = [pc EXCEPT ![200] = "IDLE_HANDLE"]
/\ UNCHANGED << dispatchQueue, tableCmdQueue, dispatchState,
consumeLock, tableQueueLock, needFireDispatchMap,
stack, irole, role, locked, tableQueueCmd, iLocked >>
idleHandler == IDLE_HANDLE \/ IDLE_TQ_EMPTY \/ DQ_IN_CONSUME
\/ DQ_IN_PRODUCE \/ TQ_N_EMPTY \/ TQ_LOCKED
\/ AcquireLock_IDLE \/ ReleaseLock_IDLE \/ LOOP_END
Next == producer \/ idleHandler
\/ (\E self \in ProcSet: \/ setNeedDispatch(self)
\/ needFireDispatch(self)
\/ scheduleDispatch(self))
\/ (\E self \in 1..10: consumer(self))
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
=============================================================================
\* Modification History
\* Last modified Tue Nov 19 00:41:13 CST 2019 by lambdacat
\* Created Mon Nov 18 19:00:24 CST 2019 by lambdacat