Model checking a round-robin scheduling algorithm

In this section we present a specification of a round-robin scheduling algorithm, and the mutual exclusion and guaranteed reentrance properties are proven about it. Both the algorithm and the property guaranteing that all processes reenter their critical sections are parameterized by the number of processes. We use Maude's model checker to prove the mutual exclusion and guaranteed reentrance properties. As we said in Section 14.2, to use the MODEL-CHECKER module, or any other Core Maude module, we just need to make sure that it has been loaded; we suggest loading the model-checker.maude file before starting Full Maude.

We first give a specification of natural numbers modulo. Since we want to be able to have any number of processes, we define the NAT/ module parameterized by the functional theory NZNAT#, which requires a constant of sort Nat. Thus, having a view, say 5 from TRIV to NZNAT# mapping # to the natural number 5, the module expression NAT/{5} specifies the natural numbers modulo 5.

  (fth NZNAT# is
     protecting NAT .
     op # : -> NzNat .
   endfth)

 (fmod NAT/{N :: NZNAT#} is
    sort Nat/{N} .
    op `[_`] : Nat -> Nat/{N} [ctor] .
    op _+_ : Nat/{N} Nat/{N} -> Nat/{N} .
    op _*_ : Nat/{N} Nat/{N} -> Nat/{N} .
    vars N M : Nat .
    ceq [N] = [N rem #] if N >= # .
    eq [N] + [M] = [N + M] .
    eq [N] * [M] = [N * M] .
  endfm)

The round-robin scheduling algorithm is specified in the module RROBIN below. Processes are represented as objects of class Proc, which may be in wait or critical mode, meaning that a process may be either in its critical section or waiting to enter into it. The process getting the token, which is represented as the message go, can enter its critical section. Once a process gets out of its critical section it forwards the token to the next process. The init operator sets up the initial configuration for a given number of processes. Note that Nat/{N} is made a subsort of Oid, making in this way natural numbers modulo N valid object identifiers.

 (omod RROBIN{N :: NZNAT#} is
    protecting NAT/{N} .

    sort Mode .
    ops wait critical : -> Mode [ctor] .

    subsort Nat/{N} < Oid .

    class Proc | mode : Mode .
    msg go : Nat/{N} -> Msg .

    var N : Nat .

    rl [enter] :
      go([N])
      < [N] : Proc | mode : wait >
      => < [N] : Proc | mode : critical > .

    rl [exit] :
      < [N] : Proc | mode : critical >
      => < [N] : Proc | mode : wait >
         go([s(N)]) .

    op init : -> Configuration .
    op make-init : Nat/{N} -> Configuration .

    ceq init = go([0]) make-init([N]) if s(N) := # .
    ceq make-init([s(N)])
      = < [s(N)] : Proc | mode : wait > make-init([N])
      if N < # .
    eq make-init([0]) = < [0] : Proc | mode : wait > .
  endom)

For proving mutual exclusion and guaranteed reentrance, we declare the propositions inCrit and twoInCrit in the module CHECK-RROBIN below (see Chapter 10 for a discussion on the use of Maude's model checker). The property inCrit takes a Nat/{N} as argument, thus making this property parameterized by the number of processes, and is true when such a process is in its critical section. The property twoInCrit is true if any two processes are in their critical sections simultaneously. Mutual exclusion will be proved directly below, while for proving guaranteed reentrance we use the auxiliary formula guaranteedReentrance, which allows us to specify the property of all processes reentering their critical sections in exactly $2N$ steps, for $N$ the number of processes. For a formula F, nextIter F returns O...O F (where O denotes the modal next operator), which specifies that the property is true in the next iteration, that is, $2N$ steps later. Note that the expression 2 * # will become two times $N$ once the module is instantiated.

 (omod CHECK-RROBIN{N :: NZNAT#} is
    pr RROBIN{N} .
    inc MODEL-CHECKER .
    inc SATISFACTION .
    ex LTL-SIMPLIFIER .
    inc LTL .

    subsort Configuration < State .

    op inCrit : Nat/{N} -> Prop .
    op twoInCrit : -> Prop .

    var  N : Nat .
    vars X Y : Nat/{N} .
    var  C : Configuration .
    var  F : Formula .

    eq < X : Proc | mode : critical > C |= inCrit(X) = true .
    eq < Y : Proc | mode : critical > < Y : Proc | mode : critical > C
         |= twoInCrit = true .

    op guaranteedReentrance : -> Formula .
    op allProcessesReenter : Nat -> Formula .
    op nextIter_ : Formula -> Formula .
    op nextIterAux : Nat Formula -> Formula .

    eq guaranteedReentrance = allProcessesReenter(#) .

    eq allProcessesReenter(s N)
      = (inCrit([s N]) -> nextIter inCrit([s N])) /\
        allProcessesReenter(N) .
    eq allProcessesReenter(0) = inCrit([0]) -> nextIter inCrit([0]) .

    eq nextIter F = nextIterAux(2 * #, F) .

    eq nextIterAux(s N, F) = O nextIterAux(N, F) .
    eq nextIterAux(0, F) = F .
  endom)

Note that the LTL formula describing the guaranteedReentrance property is not a single LTL formula, but an infinite parametric family of formulas

$$\texttt{guaranteedReentrance} = \{ \texttt{allProcessesReenter(}n\texttt{)} \mid n \in \mathbb{N} \} .$$

The use of equations in the above CHECK-RROBIN parameterized module allows us to define this infinite family of formulas by means of a few recursive equations. When this module is instantiated for a concrete value of $n$, we then obtain the concrete LTL formula allProcessesReenter($n$) for that $n$.

We now prove mutual exclusion and guaranteed reentrance for the case of five processes using the model checker.

 (view 5 from NZNAT# to NAT is
    op # to term 5 .
  endv)

  Maude> (reduce in CHECK-RROBIN{5} :  
            modelCheck(init, [] ~ twoInCrit) .)
  result Bool :
    true

  Maude> (reduce in CHECK-RROBIN{5} : 
            modelCheck(init, [] guaranteedReentrance) .)
  result Bool :
    true

Of course the answer depends on the property checked and is not always true. The following example shows how the model checker gives a counterexample as result when trying to prove that, for a configuration of five processes, process [1] is in its critical section three steps after it was in it.

  Maude> (red in CHECK-RROBIN{5} :
            modelCheck(init, [] (inCrit([1]) -> O O O inCrit([1]))) .)
  result ModelCheckResult :
    counterexample(
      {go([0]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : critical > <[1]: Proc | mode : wait >
       <[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
       <[4]: Proc | mode : wait >, 'exit}
      {go([1]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : wait > <[1]: Proc | mode : critical >
       <[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
       <[4]: Proc | mode : wait >, 'exit}
      {go([2]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
       <[2]: Proc | mode : critical > <[3]: Proc | mode : wait >
       <[4]: Proc | mode : wait >, 'exit},
      {go([3]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
       <[2]: Proc | mode : wait > <[3]: Proc | mode : critical >
       <[4]: Proc | mode : wait >, 'exit}
      {go([4]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
       <[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
       <[4]: Proc | mode : critical >, 'exit}
      {go([0]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : critical > <[1]: Proc | mode : wait >
       <[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
       <[4]: Proc | mode : wait >, 'exit}
      {go([1]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : wait > <[1]: Proc | mode : critical >
       <[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
       <[4]: Proc | mode : wait >, 'exit}
      {go([2]) <[0]: Proc | mode : wait >
       <[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
       <[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, 'enter}
      {<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
       <[2]: Proc | mode : critical > <[3]: Proc | mode : wait >
       <[4]: Proc | mode : wait >, 'exit})