[SAL] SAL question on an incorrect version of Peterson's mutual exclusion algorithm

[sjo]

*I am wondering why liveness1 succeeds (proved) in the program below. It
should fail as there is anyway a deadlock in the program.

Also note that if add

  liveness4: THEOREM system |- G((y1) => F(pi1 = l4));

correctly provides a counterexample.

Thanks ... SJO

======
pnueli_mutex2: CONTEXT =
BEGIN
  state1: TYPE = {l0,l1,l2,l3,l4,l5,l6};
  state2: TYPE = {m0,m1,m2,m3,m4,m5,m6};

  system: MODULE =
    BEGIN
      OUTPUT y1,y2 : BOOLEAN
      OUTPUT pi1 : state1
        OUTPUT pi2: state2
      INITIALIZATION pi1 = l0; pi2 = m0; y1=FALSE; y2=FALSE
      TRANSITION
        [
         tl0:
           pi1=l0 --> pi1' = l1
         []
            tm0:
           pi2=m0 --> pi2' = m1
         []
            tl1_noncritical:
              pi1=l1 --> pi1'=l2
            []
            tm1_noncritical:
                pi2=m1 --> pi2'=m2
            []
            tl2:
           pi1=l2 --> pi1' = l3; y1'=TRUE
            []
            tm2:
             pi2=m2 --> pi2' = m3; y2'=TRUE
         []
            tl3m_await:
           pi1=l3 AND (NOT y2)  --> pi1' = l4
         []
            tm3_await:
           pi2=m3 AND (NOT y1)  --> pi2' = m4
            []
            tl4_critical:
           pi1=l4  --> pi1' = l5
         []
            tm4_critical:
          pi2=m4  --> pi2' = m5
            []
            tl5:
           pi1=l5 --> pi1' = l0; y1'=FALSE
            []
            tm5:
           pi2=m5 --> pi2' = m0;  y2'=FALSE
        ]
    END;


  mutex1: THEOREM system |- G(NOT(pi1 = l4 AND pi2 = m4));
  mutex2: THEOREM system |- G(NOT(pi1 = l3 AND pi2 = m3));
  liveness1: THEOREM system |- G((pi1 = l3) => F(pi1 = l4));
  liveness2: THEOREM system |- G((pi2 = m3) => F(pi2 = m4));
  liveness3: THEOREM system |- G(F(pi1=l4));

END
==================

The following execution indicates where the deadlock occurs and why
liveness1 and liveness2 should fail.

===
y1 = false
y2 = false
pi1 = l0
pi2 = m0
------------------------
Transition Information:
(module instance at [Context: pnueli_mutex2, line(54), column(18)]
  (label tl0
    transition at [Context: pnueli_mutex2, line(15), column(11)]))
------------------------
Step 1:
--- System Variables (assignments) ---
y1 = false
y2 = false
pi1 = l1
pi2 = m0
------------------------
Transition Information:
(module instance at [Context: pnueli_mutex2, line(54), column(18)]
  (label tl1_noncritical
    transition at [Context: pnueli_mutex2, line(21), column(8)]))
------------------------
Step 2:
--- System Variables (assignments) ---
y1 = false
y2 = false
pi1 = l2
pi2 = m0
------------------------
Transition Information:
(module instance at [Context: pnueli_mutex2, line(54), column(18)]
  (label tm0
    transition at [Context: pnueli_mutex2, line(18), column(11)]))
------------------------
Step 3:
--- System Variables (assignments) ---
y1 = false
y2 = false
pi1 = l2
pi2 = m1
------------------------
Transition Information:
(module instance at [Context: pnueli_mutex2, line(54), column(18)]
  (label tm1_noncritical
    transition at [Context: pnueli_mutex2, line(24), column(8)]))
------------------------
Step 4:
--- System Variables (assignments) ---
y1 = false
y2 = false
pi1 = l2
pi2 = m2
------------------------
Transition Information:
(module instance at [Context: pnueli_mutex2, line(54), column(18)]
  (label tl2
    transition at [Context: pnueli_mutex2, line(27), column(11)]))
------------------------
Step 5:
--- System Variables (assignments) ---
y1 = true
y2 = false
pi1 = l3
pi2 = m2
------------------------
Transition Information:
(module instance at [Context: pnueli_mutex2, line(54), column(18)]
  (label tm2
    transition at [Context: pnueli_mutex2, line(30), column(7)]))
------------------------
Step 6:
--- System Variables (assignments) ---
y1 = true
y2 = true
pi1 = l3
pi2 = m3

*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal/attachments/20060801/2614b26d/attachment.html