Go backward to B.3 Program Go up to B Distributed Snapshots Go forward to B.5 Verification

B.4 State Program

For the purpose of verification, we assume that the initializations

message = null;
mode = RUNNING;

have taken place and rewrite the program as shown below to make the interactions with other nodes explicit by state changes:

state = LOOP;
while (state != EXIT)
{
  switch (state)
    {
    case LOOP:
      {
        if (mode == TERMINATED)
          state = EXIT;
        else if (number == 0 && mode == RUNNING && random(10) == 0)
          {
            snap();
            state = TRIGGER;
          }
        else
          state = SELECT;
      }
    case TRIGGER:
      {
        out().send(new SnapMessage());
        state = SELECT;
      }
    case SELECT:
      {
        index = in().select(random(5));
        if (index == -1 && deposit > 0)
          {
            int value = random(deposit);
            deposit -= value;
            message = new ValueMessage(value);
            index = random(out().getSize());       
            state = DEPOSIT;
          }
        else
          state = RECEIVE;
      }
    case DEPOSIT:
      {
        out(index).send(message);
        message = null;
        state = LOOP;
      }
    case RECEIVE:
      {
        message = in(index).receive();
        if (message instanceof ValueMessage)
          {
            ValueMessage valueMessage = (ValueMessage)message;
            int value = valueMessage.getValue();
            deposit += value;
            if (mode == SNAPPING && !snapped[index])
              snapValue += value;
            message = null;
            state = LOOP;
          }
        else if (message instanceof SnapMessage)
          {
            if (mode != SNAPPING)
              {
                snap();
                state = SNAP;
              }
            else
              state = SNAP2;
          }
        else if (message instanceof ResultMessage)
          {
            ResultMessage resultMessage = (ResultMessage)message;
            int sender = resultMessage.getSender();
            if (!done[sender])
              {
                collect(sender, resultMessage.getValue());
                state = RESULT;
              }
            else
              {
                message = null;
                state = LOOP;
              }
          }
      }
    case SNAP:
      {
        out().send(message);
        state = SNAP2;
      }
    case SNAP2:
      {
        if (!snapped[index])
          {
            snapped[index] = true;
            missingSnaps--;
            if (missingSnaps == 0)
              {
                mode = BROADCASTING;
                collect(number, snapValue);
                state = SNAP3;
              }
            else
              {
                message = null;
                state = LOOP;
              }
          }
        else
          {
            message = null;
            state = LOOP;
          }
      }
    case SNAP3:
      {
        out().send(new ResultMessage(number, snapValue));
        message = null;
        state = LOOP;
      }
    case RESULT:
      {
        out().send(message);
        message = null;
        state = LOOP;
      }
    }
}

Above program pretends that sending a message to a set of output channels is an atomic operation. This is in fact not true in DAJ; the sender node may be interrupted while only some part of the output channels has received the message. This property can be modeled correctly in above framework by an iteration of send operations of single channels. However, the proof described in the next section will not involve any property that may be invalidated by the fact that messages are not put simultaneously into all output channels (only snap and result messages are broadcast); thus we stick to the simplified model.