So, I got the dekker algorithm, which guarantees MutualExclusion and tests for deadlocks or starvations.
Here is the code:
EXTENDS Integers, Sequences
(*
--algorithm criticalsection5dekker
{
\* Global variables
variables turn = 1; wantp = FALSE; wantq = FALSE;
\* The non-critical section.
\* For checking for freedom from starvation, it is important that
\* a process might stay in the non-critical section forever (however,
\* each process must leave the critical section).
\* This procedure covers both cases: finite and infinite execution
\* of the non-critical section.
procedure NCS()
variable isEndless;
{
\* Non-deterministically choose whether the procedure will
\* be endless or finite.
ncs0: with (x \in {0,1}) {
isEndless := x;
};
ncs1: if (isEndless = 1) {
ncs2: while (TRUE) {
ncs3: skip;
}
} else {
ncs4: return;
}
}
\* First process (name P, pid 1)
process(P = 1) {
p0: while (TRUE) {
p1: call NCS(); \* non-critical section
p2: wantp := TRUE;
p3: while (wantq = TRUE) {
p4: if (turn = 2) {
p5: wantp := FALSE;
p6: await turn = 1;
p7: wantp := TRUE;
};
};
p8: skip; \* critical section
p9: turn := 2;
p10: wantp := FALSE;
}
}
\* Second process (name Q, pid 2)
process(Q = 2) {
q0: while (TRUE) {
q1: call NCS(); \* non-critical section
q2: wantq := TRUE;
q3: while (wantp = TRUE) {
q4: if (turn = 1) {
q5: wantq := FALSE;
q6: await turn = 2;
q7: wantq := TRUE;
};
};
q8: skip; \* critical section
q9: turn := 1;
q10: wantq := FALSE;
}
}
}
*)
\*** Mutual exclusion
\* For mutual exclusion, process 1 and process 2 must never be in the
\* critical section at the same time.
MutualExclusion == [] ~ (pc[1] = "p8" /\ pc[2] = "q8")
\*** Deadlock free
\* If P and Q both want to enter the critical section, one of them will
\* eventually enter the critical section.
NoDeadlock == /\ pc[1] = "p2"
/\ pc[2] = "q2"
~>
\/ pc[1] = "p8"
\/ pc[2] = "q8"
\*** Starvation free
\* If P wants to enter the critical section, P will eventually enter
\* the critical section. The same must hold for Q.
NoStarvationP == (pc[1] = "p2") ~> (pc[1] = "p8")
NoStarvationQ == (pc[2] = "q2") ~> (pc[2] = "q8")
NoStarvation == /\ NoStarvationP
/\ NoStarvationQ
\* Assume weakly fair scheduling of all commands
(* PlusCal options (wf) *)
==============================
I need to implement another feature of the algorithm, so if turn = 1, there will always be turn = 2. Thats what I wrote (not sure if it makes sense).
\***turn change
TurnChange == pc[2] = "q4" ~> pc[1] = "p9"
Now I use the commands to translate the code in the console:
java pcal.trans criticalsection5dekker.tla
and to run it:
java tlc2.TLC criticalsection5dekker.tla -config criticalsection5dekker.cfg -workers 1 -modelcheck -deadlock
And now, I have no clue at all what the console tells me. If what I wrote is correct or if I did another mistake.
http://imgur.com/a/RHuH8
Can anybody help me?