pluscal, tla+ and tekker algorithm

[Kai Tsching]

This is my first time using pluscal and tla+. So honestly, I have no clue how this works and what to do.

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?

[Leslie Lamport]

You didn't say if the translation succeeded.  It probably did, since

you didn't indicate that it produced an error message.  You could find

out by looking at the tla file to make sure that it put the

translation there.

 

TLC's console output makes it pretty clear if there was an error.

Since you don't know if it it found an error, it probably didn't.  But

we'd have to see the console output to be sure.  But assuming the

translation succeeded and TLC found no error, this means that you have

correctly specified some protocol that has a finite number of

reachable states.  What else it means depends on what the

configuration file told it to check.  You also didn't say what was in

the configuration file.

 

But before you go any further, you should stop running TLC from a shell

and run it from the Toolbox.  See the TLA+ web page to find out how to

download and install the Toolbox.

 

Leslie