Zenn
Open2

TLA+ で Dekker のアルゴリズムを検証する

tla
nojimanojima

Dekker's algorithm - Wikipedia

Dekker.tla
------------------------------- MODULE Dekker -------------------------------
EXTENDS Integers

VARIABLE turn
VARIABLE wantsToEnter
VARIABLE pc

Init ==
    /\ turn = 0
    /\ wantsToEnter = [ i \in {0, 1} |-> FALSE ]
    /\ pc = [ i \in {0, 1} |-> "wants_to_enter" ]

WantsToEnterStep(p) ==
    /\ pc[p] = "wants_to_enter"
    /\ wantsToEnter' = [ wantsToEnter EXCEPT ![p] = TRUE ]
    /\ pc' = [ pc EXCEPT ![p] = "coordinate" ]
    /\ UNCHANGED << turn >>

CoordinateStep(p) ==
    /\ pc[p] = "coordinate"
    /\ IF wantsToEnter[1-p] THEN
           IF turn = p THEN
               UNCHANGED << turn, pc, wantsToEnter >>
           ELSE
               /\ wantsToEnter' = [ wantsToEnter EXCEPT ![p] = FALSE ]
               /\ pc' = [ pc EXCEPT ![p] = "wait" ]
               /\ UNCHANGED << turn >>
       ELSE
          /\ pc' = [ pc EXCEPT ![p] = "in_critical_section" ]
          /\ UNCHANGED << turn, wantsToEnter >>

WaitStep(p) ==
    /\ pc[p] = "wait"
    /\ IF turn = p THEN
           /\ wantsToEnter' = [ wantsToEnter EXCEPT ![p] = TRUE ]
           /\ pc' = [ pc EXCEPT ![p] = "coordinate" ]
           /\ UNCHANGED << turn >>
       ELSE
           UNCHANGED << turn, pc, wantsToEnter >>

InCriticalSectionStep(p) ==
    /\ pc[p] = "in_critical_section"
    /\ turn' = 1-p
    /\ pc' = [ pc EXCEPT ![p] = "exit_critical_section" ]
    /\ UNCHANGED << wantsToEnter >>

ExitCriticalSectionStep(p) ==
    /\ pc[p] = "exit_critical_section"
    /\ wantsToEnter' = [ wantsToEnter EXCEPT ![p] = FALSE ]
    /\ pc' = [ pc EXCEPT ![p] = "wants_to_enter" ]
    /\ UNCHANGED << turn >>

Run(p) ==
    \/ WantsToEnterStep(p)
    \/ CoordinateStep(p)
    \/ WaitStep(p)
    \/ InCriticalSectionStep(p)
    \/ ExitCriticalSectionStep(p)

Next ==
    \E p \in {0, 1} : Run(p)

Spec ==
    /\ Init
    /\ [][Next]_<<turn, wantsToEnter, pc>>
    /\ WF_<< turn, wantsToEnter, pc >>(Run(0))
    /\ WF_<< turn, wantsToEnter, pc >>(Run(1))

-----------------------------------------------------------------------------

TypeOK ==
    /\ turn \in 0..1
    /\ wantsToEnter \in [ 0..1 -> BOOLEAN ]
    /\ pc \in [ 0..1 -> STRING ]

\* Safety: ふたつのプロセスが同時にクリティカルセクションに入ることはない
SafetyProperty ==
    ~(pc[0] = "in_critical_section" /\ pc[1] = "in_critical_section")

\* Liveness: 任意のbehaviorにおいて、クリティカルセクションに無限回入る
LivenessProperty ==
    [](<>(pc[0] = "in_critical_section") /\ <>(pc[1] = "in_critical_section"))

=============================================================================
Dekker.cfg
SPECIFICATION Spec

PROPERTY
    LivenessProperty

INVARIANT
    SafetyProperty
    TypeOK
nojimanojima
Spec ==
    /\ Init
    /\ [][Next]_<<turn, wantsToEnter, pc>>
    /\ WF_<< turn, wantsToEnter, pc >>(Run(0))
    /\ WF_<< turn, wantsToEnter, pc >>(Run(1))

の WF_... の部分によって各プロセスが進行することを保証している。これがないとプロセス0だけ動いてプロセス1が全く動かないようなスケジューリングや、そもそもどのプロセスも動かないスケジューリングなども許容されてしまい、LivenessProperty が満たされなくなる。

WF_<<...>>(Run(0)) /\ WF_<<...>>(Run(1)) の代わりに WF_<<...>>(Next) と書いてしまうと、片方のプロセスだけが動いてもう片方が全く動かないスケジューリングを許してしまい、LivenessProperty が満たされなくなる。