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

[Leonardo de Moura]

Hi,

sal-smc assumes the transition relation is total, that is, there are  
no deadlocks.
Your specification has a deadlock state.
You can find deadlocks using the tool sal-deadlock-checker.

% sal-deadlock-checker pnueli_mutex2 system
Total number of deadlock states: 1.0
Deadlock states:
State 1
--- System Variables (assignments) ---
y1 = true
y2 = true
pi1 = l3
pi2 = m3
-----------------------------

You can avoid deadlocks using the ELSE transition.

Cheers,
Leonardo


You can avoid the deadlock with a ELSE transition:


On Aug 1, 2006, at 1:30 PM, sjo wrote:

> 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/65debf63/attachment.html