Skip to main content

Building a Counter Service

This tutorial builds a Flex protocol for a counter service step by step: first a basic service, then a version that avoids integer overflow, and finally one the model checker can prove is safe using a loop invariant. For the syntax of individual protocol statements, see the Flex Protocols reference; for the conceptual background on protocols, see What Are Flex Protocols?.

A Simple Counter Service​

A service generally refers to a software program that, for an indefinite amount of time, reacts to incoming messages by updating its internal state and/or responding with messages of its own.

Below, counterProtocol1 is a service that maintains a count state which is an integer. It can handle requests to increment the count, output the count, or quit running altogether.

struct Increment {}
struct GetValue {}
struct Quit {}

component CounterService;
component Client;

local protocol counterProtocol1 in CounterService {
  var count: int32 = 0;

  loop {
    listen
    | recv _: Increment from Client => set count = count + 1;
    | recv _: GetValue from Client => send count to Client;
    | recv _: Quit from Client => break;
    end
  }
}

Adding a Loop Invariant to the Counter Protocol​

The counterProtocol1 that we defined earlier has a potential problem: if the value ever reaches the maximum integer value, then one more Increment would cause an overflow and make to value negative! Instead of overflowing, we would like the count to remain at the maximum integer value. Let's fix that by modifying the set statement:

local protocol counterProtocol2 in CounterService {
  var count: int32 = 0;

  loop {
    listen
    | recv _: Increment from Client =>
        set count = if count == 2147483647 then count else count + 1;
    | recv _: GetValue from Client => send count to Client;
    | recv _: Quit from Client => break;
    end
  }
}

Now we can use the model checker to prove that counterProtocol2 will never output a negative value. To do this, let's model a client protocol that sends an unspecified number of Increment and GetValue messages before sending a final Quit message and terminating. We attach assuming value >= 0 to the recv statement to indicate that we always want the received value to be nonnegative. The model checker will attempt to prove that this assumption is never violated.

local protocol clientProtocol in Client {
  loop {
    branch
    | true =>
        send any Increment to CounterService;
    | true =>
        send any GetValue to CounterService;
        recv any value: int32 assuming value >= 0 from CounterService;
    | true =>
        send any Quit to CounterService;
        break;
    end
  }
}

We also need a system containing our two protocols to pass to the model checker:

system counterSystem2 { counterProtocol2; clientProtocol; }

Unfortunately, even though the count will never overflow, the model checker can't prove it quite yet. The reason lies in the way the model checker handles looping. Software involving loops is typically tricky for verification tools to handle because loops can iterate a very large number of times (or sometimes even infinitely many times).

To avoid simulating a potentially infinite number of loop iterations, the model checker attempts to construct an inductive proof of some predicate P that is satisfied by the model. For a given P and a loop block in the model, the inductive proof that the model checker tries to build looks like this:

  • Base Case: P is true after zero loop iterations.
  • Inductive Case: If P is true after n iterations, then P is true after n+1 iterations.
  • Conclusion: P is true after any number of iterations.

The predicate P is called the loop invariant and can be provided by the invariant clause in a loop expression. In our example, using count >= 0 works as our loop invariant. This is coincidentally similar to the assuming value >= 0 clause that we want to verify, however this will not always be the case.

local protocol counterProtocol3 in CounterService {
  var count: int32 = 0;

  loop invariant (count >= 0) {
    listen
    | recv _: Increment from Client =>
        set count = if count == 2147483647 then count else count + 1;
    | recv _: GetValue from Client => send count to Client;
    | recv _: Quit from Client => break;
    end
  }
}

system counterSystem3 { counterProtocol3; clientProtocol; }

Now the model checker is able to prove that counterSystem3 is safe.

Where to Go Next​