[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

pluscal, tla+ and tekker algorithm



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?