keyboard_backspace back home

Modeling ZLog in Promela: Part 1

9 December 2017

Introduction blurb about this post.

Articles in this series:

This post is part of the following series:

ZLog

  • Links
  • Basic ZLog
  • Is it correct?

Modeling

  • Basic idea about modeling
  • Other approaches
  • We are using Spin in this article

A ZLog Spin Model

We start with a constrained and simplified model of the system. Over the course of several posts we will increase the detail of the model until it accurately reflects the real-world implementation. In this simple model there is a single sequencer service that communicates with multiple objects to initialize the in-memory counter value, and one client that appends one value to the log. The primary aspect of the model that makes it simple is that there are no failures and communication is reliable. We’ll discuss this shortly when we introduce the model in the more detail.

First some basic setup. We cap the number of log entries, and use a fixed number of objects in the model. There are two message types used, one for writing to an object, and one reply to indicate success. The p2o macro defines how entries are mapped onto objects using a basic round-robin addressing scheme.

#define MAX_ENTRIES 5
#define NUM_OBJECTS 2

mtype {
  ok,
  write
};

#define p2o(pos) (pos % NUM_OBJECTS)

Next we define three sets of channels. The maxpos_req channel is used by the sequencer to request the maximum position written to an object. This is used during sequencer initialization. The entry_req channel is used by clients to perform actions on log entries, such as reading or writing. The nextpos_req channels is used by clients to request the next log position from the sequencer service.

// channel for requesting maximum position from object
chan maxpos_req[NUM_OBJECTS] = [0] of { chan };

// channel for object entry operations (read, write, etc...)
chan entry_req[NUM_OBJECTS] = [0] of { mtype, chan, byte };

// channel for sequencer next position requests
chan nextpos_req = [0] of { chan };

Object

The object process models a durable object in ZLog that stores log entries. It handles a variety of requests such as reading and writing log entries, as well as finding the maximum log position that has been written. The entries array below contains log entries. The value zero is used to indicate that the log position has not been written, and positive values encode non-empty states (Spin will initialize the array to zeros).

proctype Object(byte id) {
  chan reply;

  // log entries managed by this object
  byte entries[MAX_ENTRIES];

  // handling maxpos requests
  byte i, max;
  bool bare;

  // handling write requests
  byte pos;

This is the core request handling loop. First is the handler for finding the maximum position that has been written. This handler scans the entries array looking for non-zero values. The d_step is a deterministic step which reduces the state space complexity by not interleaving execution with other parts of the model during execution. Notice that the reply is the 2-tuple (bare, max) where bare is true only when no log entries are found. The max position is only defined when bare is false.

end:
  do
  // handle maxpos request. if bare, max is undefined
  :: maxpos_req[id] ? reply ->
    d_step {
      bare = true
      for (i in entries) {
        if
        :: entries[i] > 0 ->
          bare = false
          if
          :: i > max -> max = i
          :: else -> skip
          fi
        :: else -> skip
        fi
      }
    }
    reply ! bare, max

Handling a write request is simple. If the position is non-empty an assertion is thrown, otherwise the entry is marked as non-empty. In a real-world implementation it is not an error if the entry has already been written; clients handle this through a retry mechanism. However, in the simplified model we are working with now we use this assertion as a state that we can drive the system to to test out model checking in Spin. In later iterations we will remove this assertion and implement retry logic in the client.

  // handle write request
  :: entry_req[id] ? write(reply, pos) ->
    if
    :: entries[pos] > 0 ->
      assert(false)
    :: else ->
      entries[pos] = 1
      reply ! ok
    fi
  od;
}

Sequencer

The sequencer contains a single handler that clients invoke through an RPC mechanism to retrieve the tail position of the log. Before responding to any client request, the stored tail position must be initialized. This is done through an initialization process that the sequencer carries out by contacting each object and computing a maximum over all responses.

First some basic setup

proctype Sequencer() {
  chan maxpos_reply = [NUM_OBJECTS] of { bool, int };
  chan nextpos_reply;

  // log tail position
  byte seq;

  // initialization
  byte i, max;
  bool bare;

Initialization consists of two phases. First, the sequencer sends a maximum position request to each object

  // initialization. phase 1: send maxpos requests
  for (i in maxpos_req) {
    maxpos_req[i] ! maxpos_reply
  }

In the second phase the sequencer waits on all responses and computes the initialization value.

  // initialization. phase 2: reduce replies
  seq = 0;
  for (i in maxpos_req) {
    maxpos_reply ? bare, max;
    if
    :: !bare && (max + 1) > seq
      -> seq = max + 1
    :: else -> skip
    fi;
  }

The request loop is simple enough. It responds with the current tail and increments the counter.

end:
  do
  // handle nextpos request
  :: nextpos_req ? nextpos_reply ->
    nextpos_reply ! seq
    seq++
  od;
}

Client

Our client is very simple. It requests a position from the sequencer and then sends a write request to the object that the position maps to. This is repeated once.

proctype Client() {
  byte pos
  byte oid
  chan reply = [0] of { byte }
  chan entry_reply = [0] of { mtype };
  mtype status;

  nextpos_req ! reply
  reply ? pos
  oid = p2o(pos)
  entry_req[oid] ! write(entry_reply, pos)
  entry_reply ? status;
  printf("write %d -> %e\n", pos, status)

  nextpos_req ! reply
  reply ? pos
  oid = p2o(pos)
  entry_req[oid] ! write(entry_reply, pos)
  entry_reply ? status;
  printf("write %d -> %e\n", pos, status)
}

In Spin the init process can be used to startup the processes in the model, like so:

init {
  byte i;
  atomic {
    for (i : 0 .. (NUM_OBJECTS-1)) {
      run Object(i)
    }
    run Sequencer();
    run Client();
  }
}

Running the model

Spin is complex and there are a lot of ways to interact with the models that are written in Promela. First we start with something simple. We’ll ask Spin to run our model and use a single random execution. The following shows the output in which the client receives a success message after writing to positions 0 and 1.

The output at the end lists the state of each process when execution ended.

Noahs-MacBook-Air:spin nwatkins$ spin zlog.pml
                      write 0 -> ok
                      write 1 -> ok
      timeout
#processes: 4
115:    proc  3 (Sequencer:1) zlog.pml:93 (state 29) <valid end state>
115:    proc  2 (Object:1) zlog.pml:34 (state 33) <valid end state>
115:    proc  1 (Object:1) zlog.pml:34 (state 33) <valid end state>
115:    proc  0 (:init::1) zlog.pml:132 (state 13) <valid end state>
5 processes created

Using Spin we can generate a verifier that will explore the entire state space (see the Spin documentation for more information on compiling the model). There is a lot of output here, but notably absent is any mention of an assertion violation. In fact in the next snippet, observe that the assert(false) statement in our model is unreachable.

Noahs-MacBook-Air:spin nwatkins$ ./pan

(Spin Version 6.4.5 -- 1 January 2016)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states    +

State-vector 147 byte, depth reached 61, errors: 0
       58 states, stored
        4 states, matched
       62 transitions (= stored+matched)
        9 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.010    equivalent memory usage for states (stored*(State-vector + overhead))
    0.285    actual memory usage for states
  128.000    memory used for hash table (-w24)
    0.534    memory used for DFS stack (-m10000)
  128.730    total actual memory usage

The assert(false) statement is never executed

unreached in proctype Object
    zlog.pml:57, state 27, "assert(0)"
    zlog.pml:63, state 36, "-end-"
    (2 of 36 states)
unreached in proctype Sequencer
    zlog.pml:99, state 32, "-end-"
    (1 of 32 states)
unreached in proctype Client
    (0 of 13 states)
unreached in init
    (0 of 13 states)

pan: elapsed time 0 seconds

Sequencer restart

In a real system processes fail and restart. The following diff shows how we change the model to allow the sequencer to restart. The basic idea is that the sequencer non-deterministically selects to either handle a client request or re-initialize its counter by contacting each object. Note that even this is naive. In practice a failed sequencer may not be able to recover, and an entirely new process must be elected and started.

The initok flag is used to force an initialization round at least once before any client request is handled.

diff --git a/qa/spin/zlog.pml b/qa/spin/zlog.pml
index a2ddbea..41248f2 100644
--- a/qa/spin/zlog.pml
+++ b/qa/spin/zlog.pml
@@ -72,27 +72,31 @@ proctype Sequencer() {
   // initialization
   byte i, max;
   bool bare;
+  bool initok = false

Next the initialization logic that we had shown above is shifted into an outer do-construct which provides the selection between handling a request and simulating the restart. Note that initok is set to true after initialization is complete.

-  // initialization. phase 1: send maxpos requests
-  for (i in maxpos_req) {
-    maxpos_req[i] ! maxpos_reply
-  }
+  do
+  :: true ->
+    // initialization. phase 1: send maxpos requests
+    for (i in maxpos_req) {
+      maxpos_req[i] ! maxpos_reply
+    }
 
-  // initialization. phase 2: reduce replies
-  seq = 0;
-  for (i in maxpos_req) {
-    maxpos_reply ? bare, max;
-    if
-    :: !bare && (max + 1) > seq
-      -> seq = max + 1
-    :: else -> skip
-    fi;
-  }
+    // initialization. phase 2: reduce replies
+    seq = 0;
+    for (i in maxpos_req) {
+      maxpos_reply ? bare, max;
+      if
+      :: !bare && (max + 1) > seq
+        -> seq = max + 1
+      :: else -> skip
+      fi;
+    }
+    initok = true

The reply logic is also shifted into the outer do-construct, and a guard is added that activates the branch only when initok is true.

-end:
-  do
   // handle nextpos request
-  :: nextpos_req ? nextpos_reply ->
+  :: initok ->
+end:
+    nextpos_req ? nextpos_reply
     nextpos_reply ! seq
     seq++
   od;

Finally we update the print statements in the client so we can see what is happening before sending the requests.

@@ -108,16 +112,16 @@ proctype Client() {
   nextpos_req ! reply
   reply ? pos
   oid = p2o(pos)
+  printf("writing at pos %d\n", pos)
   entry_req[oid] ! write(entry_reply, pos)
   entry_reply ? status;
-  printf("write %d -> %e\n", pos, status)
 
   nextpos_req ! reply
   reply ? pos
   oid = p2o(pos)
+  printf("writing at pos %d\n", pos)
   entry_req[oid] ! write(entry_reply, pos)
   entry_reply ? status;
-  printf("write %d -> %e\n", pos, status)
 }
 
 init {

This time when we re-run the verifier we encounter the assertion error. That is, the client attempted to write to a location that was non-empty.

Noahs-MacBook-Air:spin nwatkins$ ./pan
pan:1: assertion violated 0 (at depth 84)
pan: wrote zlog.pml.trail

When Spin encounters an error like this it generates a trail file that allows the failed execution to be examined. The first thing we notice is that in fact the client did attempt to write to the same position 0 twice. But what execution resulted in this scenario?

Noahs-MacBook-Air:spin nwatkins$ spin -t zlog.pml
                      writing at pos 0
                      writing at pos 0
spin: zlog.pml:57, Error: assertion violated
spin: text of failed assertion: assert(0)
spin: trail ends after 85 steps
#processes: 5
 85:    proc  4 (Client:1) zlog.pml:124 (state 12)
 85:    proc  3 (Sequencer:1) zlog.pml:81 (state 4)
 85:    proc  2 (Object:1) zlog.pml:34 (state 33) <valid end state>
 85:    proc  1 (Object:1) zlog.pml:34 (state 33) <valid end state>
 85:    proc  0 (:init::1) zlog.pml:136 (state 13) <valid end state>

We can have the verifier print a detailed listing of the steps that were taken to arrive at the failure. First initialization:

Noahs-MacBook-Air:spin nwatkins$ ./pan -C zlog.pml.trail
1: :init:(0):[i = 0]
2: :init:(0):[((i<=(2-1)))]
3: :init:(0):[(run Object(i))]
4: :init:(0):[i = (i+1)]
5: :init:(0):[((i<=(2-1)))]
6: :init:(0):[(run Object(i))]
7: :init:(0):[i = (i+1)]
8: :init:(0):[else]
9: :init:(0):[(run Sequencer())]
10: :init:(0):[(run Client())]

Next are the steps required to initialize the sequencer, followed by the client executing its first write at position 0.

11:                         Sequencer(3):[(1)]
12:                         Sequencer(3):[((i<=1))]
13:                         Sequencer(3):[maxpos_req[i]!maxpos_reply]
14:         Object(1):[maxpos_req[id]?reply]
15:                         Sequencer(3):[i = (i+1)]
16:                         Sequencer(3):[((i<=1))]
17:         Object(1):[D_STEP37]
18:                         Sequencer(3):[maxpos_req[i]!maxpos_reply]
19:                 Object(2):[maxpos_req[id]?reply]
20:                         Sequencer(3):[i = (i+1)]
21:                         Sequencer(3):[else]
22:                         Sequencer(3):[seq = 0]
23:                         Sequencer(3):[((i<=1))]
24:                 Object(2):[D_STEP37]
25:                 Object(2):[reply!bare,max]
26:                         Sequencer(3):[maxpos_reply?bare,max]
27:                         Sequencer(3):[else]
28:                         Sequencer(3):[(1)]
29:                         Sequencer(3):[((i<=1))]
30:         Object(1):[reply!bare,max]
31:                         Sequencer(3):[maxpos_reply?bare,max]
32:                         Sequencer(3):[else]
33:                         Sequencer(3):[(1)]
34:                         Sequencer(3):[else]
35:                         Sequencer(3):[initok = 1]
36:                         Sequencer(3):[(initok)]
37:                                 Client(4):[nextpos_req!reply]
38:                         Sequencer(3):[nextpos_req?nextpos_reply]
39:                         Sequencer(3):[nextpos_reply!seq]
40:                                 Client(4):[reply?pos]
writing at pos 0

It is important to note here that the client has not actually sent the write request to the object. That is, it has been assigned a position of 0, but the object has not yet received the request. That write is in-flight. Now look what happens: the sequencer decides it is a good time to restart:

41:                                 Client(4):[oid = (pos%2)]
42:                         Sequencer(3):[seq = (seq+1)]
43:                         Sequencer(3):[(1)]
44:                         Sequencer(3):[((i<=1))]
45:                         Sequencer(3):[maxpos_req[i]!maxpos_reply]
46:         Object(1):[maxpos_req[id]?reply]
47:                         Sequencer(3):[i = (i+1)]
48:                         Sequencer(3):[((i<=1))]
49:         Object(1):[D_STEP37]
50:                         Sequencer(3):[maxpos_req[i]!maxpos_reply]
51:                 Object(2):[maxpos_req[id]?reply]
52:                         Sequencer(3):[i = (i+1)]
53:                         Sequencer(3):[else]
54:                         Sequencer(3):[seq = 0]
55:                         Sequencer(3):[((i<=1))]
56:                 Object(2):[D_STEP37]
57:                 Object(2):[reply!bare,max]
58:                         Sequencer(3):[maxpos_reply?bare,max]
59:                         Sequencer(3):[else]
60:                         Sequencer(3):[(1)]
61:                         Sequencer(3):[((i<=1))]
62:         Object(1):[reply!bare,max]

All of the maximum positions requests have been handled by the objects. Since the first write never landed, the result should be the same as the first initialization: the log is empty. Next the object completes the first write, and the sequencer finishes phase 2 of initialization setting its counter state to a now invalid value.

63:                                 Client(4):[entry_req[oid]!write,entry_reply,pos]
64:         Object(1):[entry_req[id]?write,reply,pos]
65:         Object(1):[else]
66:         Object(1):[entries[pos] = 1]
67:                         Sequencer(3):[maxpos_reply?bare,max]
68:                         Sequencer(3):[else]
69:                         Sequencer(3):[(1)]
70:                         Sequencer(3):[else]
71:                         Sequencer(3):[initok = 1]
72:                         Sequencer(3):[(initok)]
73:         Object(1):[reply!ok]

The remaining parts of the trace are simple: the client receives a stale value for the log tail from the sequencer for the second write, which results in a duplicate write to position 0.

74:                                 Client(4):[entry_reply?status]
75:                                 Client(4):[nextpos_req!reply]
76:                         Sequencer(3):[nextpos_req?nextpos_reply]
77:                         Sequencer(3):[nextpos_reply!seq]
78:                                 Client(4):[reply?pos]
writing at pos 0
79:                                 Client(4):[oid = (pos%2)]
80:                         Sequencer(3):[seq = (seq+1)]
81:                         Sequencer(3):[(1)]
82:                         Sequencer(3):[((i<=1))]
83:                                 Client(4):[entry_req[oid]!write,entry_reply,pos]
84:         Object(1):[entry_req[id]?write,reply,pos]
pan:1: assertion violated 0 (at depth 85)
spin: trail ends after 85 steps
#processes 5:
 85:    proc 0 (:init:)  zlog.pml:136 (state 13)
        -end-
 85:    proc 1 (Object)  zlog.pml:56 (state 31) (invalid end state)
        ((entries[pos]>0))

In the next post we’ll resolve this issue by forcing clients to get a new sequence number when it is determined that the one they have may be stale.