dekker.maude

--- Dekker's algorithm, borrowed from:
--- Clavel. M. et al, All about maude-a high-performance logical framework: how to specify, program and verify systems in rewriting logic, LNCS 4350, 2007

fmod MEMORY is 
    inc INT + QID . 
    sorts Memory Bool? Int? .
    subsorts Bool < Bool? . subsorts Int < Int? .
    op null : -> Int? [ctor] .
    op none : -> Memory [ctor] .
    op __ : Memory Memory -> Memory [ctor assoc comm id: none] .
    op `[_`,_`] : Qid Int? -> Memory [ctor] .
    op _in_ : Qid Memory -> Bool? .
    var Q : Qid . var M : Memory . var N? : Int? .
    eq null + N? = null .
    eq null * N? = null .
    eq Q in [Q,N?] M = true .
endfm

fmod EXPRESSION is 
    inc MEMORY .
    sort Expression .
    subsorts Qid Int? < Expression .
    op _+'_ : Expression Expression -> Expression [ctor] .
    op _-'_ : Expression Expression -> Expression [ctor] .
    op _*'_ : Expression Expression -> Expression [ctor] .
    op eval : Expression Memory -> Int? .
    var Q : Qid .
    var M : Memory .
    vars N N' : Int .
    var N? : Int? .
    vars E E' : Expression .
    eq eval(N?, M) = N? .
    eq eval(Q, [Q, N?] M) = N? .
    ceq eval(Q,M) = null if Q in M =/= true .
    eq eval(E +' E', M) = eval(E,M) + eval(E',M) .
    eq eval(E -' E', M) = eval(E,M) - eval(E',M) .
    eq eval(E *' E', M) = eval(E,M) * eval(E',M) .
endfm

fmod TESTS is 
    inc EXPRESSION .
    sort Test .
    op _=_ : Expression Expression -> Test [ctor] . 
    op _!=_ : Expression Expression -> Test [ctor] . 
    op _<'_ : Expression Expression -> Test [ctor] .
    op eval : Test Memory -> Bool .
    var Q : Qid .
    var M : Memory .
    vars N? N'? : Int? .
    vars E E' : Expression .
    eq eval(E = E', M) = eval(E, M) == eval (E', M) .
    eq eval(E != E', M) = eval(E, M) =/= eval (E', M) .
    eq eval(E <' E', M) = eval(E, M) < eval (E', M) .
endfm

fmod SEQUENTIAL is inc TESTS + EXPRESSION .
    sorts UserStatement LoopingUserStatement Program .
    subsort LoopingUserStatement < UserStatement < Program .
    op skip : -> Program .
    op _;_ : Program Program -> Program [prec 61 assoc id: skip] .
    op _:=_ : Qid Expression -> Program .  
    op if_then_fi : Test Program -> Program .
    op while_do_od : Test Program -> Program .
    op repeat_forever : Program -> Program .

    op choose_|_ : Program Program -> Program .	--- nondeterministic choice
    op request_ : Qid -> Program .	--- acquire lock
    op release_ : Qid -> Program .	--- release lock
endfm

mod PARALLEL is inc SEQUENTIAL + TESTS .
    sorts Pid Process Soup MachineState .
    subsort Process < Soup .
    subsort Int < Pid .
    op `[_`,_`] : Pid Program -> Process [ctor] .
    op empty : -> Soup [ctor] .
    op _|_ : Soup Soup -> Soup [ctor prec 61 assoc comm id: empty] .
    op `{_`,_`} : Soup Memory -> MachineState [ctor] .

    vars P P' R : Program .
    var S : Soup .
    var U : UserStatement .
    var L : LoopingUserStatement .
    vars I J : Pid .
    var M : Memory .
    var Q : Qid .
    vars N? X? : Int? .
    var T : Test .
    var E : Expression .

    --- the definition of execution semantics with localized fairness
    --- declarations using renamed fairness items.

    rl [user] : 
        {[I, U ; R] | S, M} 
      => 
        {[I, R] | S, M}	    [metadata "just[exec(I)]"] .

    rl [loop] : 
        {[I, L ; R] | S, M} 
      => 
        {[I, L ; R] | S, M} [metadata "just[exec(I)]"] .

    rl [asgn] : 
        {[I, (Q := E) ; R] | S, [Q, X?] M} 
      => 
        {[I, R] | S, [Q,eval(E,[Q, X?] M)] M} [metadata "just[exec(I)]"] .

   crl [asgn] : 
        {[I, (Q := E) ; R] | S, M} 
      => 
        {[I, R] | S, [Q,eval(E,M)] M} 
     if Q in M =/= true [metadata "just[exec(I)]"] .

    rl [cond] : 
        {[I, if T then P fi ; R] | S, M} 
      =>
        {[I, if eval(T, M) then P else skip fi ; R] | S, M} 
    [metadata "just[exec(I)]"] .

    rl [whil] : 
        {[I, while T do P od ; R] | S, M} 
      =>
        {[I, if eval(T,M) then (P ; while T do P od) else skip fi ; R] | S, M} 
     [metadata "just[exec(I)]"].

    rl [rept] : 
        {[I, repeat P forever ; R] | S, M} 
      =>
        {[I, P ; repeat P forever ; R] | S, M} [metadata "just[exec(I)]"] .
endm

--- Dekker's algorithm
mod DEKKER is inc PARALLEL .
    subsort Int < Pid .
    op crit : -> UserStatement .
    op rem : -> LoopingUserStatement .
    ops p1 p2 : -> Program .
    op initMem : -> Memory .
    op init : -> MachineState .

    eq p1 =
    repeat
        'c1 := 1 ;
        while 'c2 = 1 do
    if 'turn = 2 then
        'c1 := 0 ;
    while 'turn = 2 do skip od ;
        'c1 := 1
    fi
        od ;
        crit ;
        'turn := 2 ;
        'c1 := 0 ;
        rem
    forever .
    eq p2 =
    repeat
        'c2 := 1 ;
        while 'c1 = 1 do
    if 'turn = 1 then
        'c2 := 0 ;
    while 'turn = 1 do skip od ;
        'c2 := 1
    fi
        od ;
        crit ;
        'turn := 1 ;
        'c2 := 0 ;
        rem
    forever .

    --- initial memory and state
    eq initMem = ['c1, 0] ['c2, 0] ['turn, 1] .
    eq init = { [1, p1] | [2, p2], initMem } .
endm

--- Full Maude interface

load ltlr-interface

--- predicate descriptions
(mod DEKKER-CHECK is 
    protecting DEKKER .
    including LTLR-MODEL-CHECKER .

    var M : Memory .  vars R : Program .  var S : Soup .  vars I : Pid .

    subsort MachineState < State .

  *** process I is in critical section
    op in-crit : Pid -> Prop .
    eq {[I, crit ; R] | S, M} |= in-crit(I) = true . 
    eq {[I, R] | S, M} |= in-crit(I) = false [owise] . 

  *** process I is in rem section
    op in-rem : Pid -> Prop .
    eq {[I, rem ; R] | S, M} |= in-rem(I) = true . 
    eq {[I, R] | S, M} |= in-rem(I) = false [owise] . 
endm)

set verbose on .

*** the mutual exclusion property
*** true
(mc init |= [] ~ (in-crit(1) /\ in-crit(2)) .)

*** liveness property
*** false
(mc init |= ((~ <>[] in-rem(1)) -> []<> in-crit(1)) /\
            ((~ <>[] in-rem(2)) -> []<> in-crit(2)) .)

*** false
(mc init |= ((~ <>[] in-rem(1)) -> []<> in-crit(1)) /\
            ((~ <>[] in-rem(2)) -> []<> in-crit(2)) 
 under just(exec(1)) .)

*** true
*** NOTE: the rule attributes automatically declare the simplified 
*** renamed action pattern exec(I).
(mc init |= ((~ <>[] in-rem(1)) -> []<> in-crit(1)) /\
            ((~ <>[] in-rem(2)) -> []<> in-crit(2)) 
 under just(exec(1)) ; just(exec(2)) .)

*** true
(mc init |= ((~ <>[] in-rem(1)) -> []<> in-crit(1)) /\
            ((~ <>[] in-rem(2)) -> []<> in-crit(2)) 
 under just(exec(I:Pid)) .)

*** true
(pfmc init |= ((~ <>[] in-rem(1)) -> []<> in-crit(1)) /\
            ((~ <>[] in-rem(2)) -> []<> in-crit(2)) .)