Model-Checking Safety Properties

This has been a long journey. We learned scanning, then parsing, then how to interpret basic constant expressions. Statements were added next, then we mastered the difficult art of parsing conjunction & disjunction lists. Finally, we learned how to apply operators and move between states. Everything is in place; it is time to write a TLA⁺ model-checker.

We will write a checker for TLA⁺ safety properties. Formally, safety properties are properties that can be disproven by a counterexample state trace of finite length. This is a bit abstract; in concrete terms, safety properties are expressions that evaluate to either true or false in different system states. Ideally, a safety property is true in every system state! Safety properties are often informally described as "nothing bad happens" properties, also called invariants. For example, when developing a multi-core CPU memory caching system, a good safety property would be that no two CPU caches ever disagree about the value stored at a given memory address. However, our systems often surprise us and find their ways to corners of the state space where a safety property does not hold. When that happens, the best way to debug the problem is to see a path from some initial state to the state violating the invariant. This path is what is meant by a state trace counterexample of finite length. It isn't enough to just produce a state violating the invariant; we must also show how the system got there! That is the task of this chapter.

Inquisitive readers might wonder what sort of properties require counterexamples of infinite length. Those are what we call liveness properties, or "something good eventually happens" properties. A counterexample to something good eventually happening is a state trace ending in an infinite loop, showing it is possible for the system to run forever without ever satisfying the liveness property. Liveness properties (and how to check them) are a fascinating topic, but beyond the scope of this chapter.

Our overall approach to checking safety properties has the following structure:

1. Parse a TLA⁺ specification, identifying the Init, Next, and Inv definitions.
2. Find the spec's initial state(s) satisfying Init.
3. Repeatedly use Next to find all states in the system following from the initial state(s).
4. Check to ensure the Inv invariant holds in every discovered state.
5. If a state violates Inv, construct a state trace leading from some initial state to the violating state.

For this purpose, create a new file ModelChecker.java and pre-emptively import all the datastructures we'll need. Also define a constructor accepting an Interpreter instance and a list of parsed Stmt objects comprising the TLA⁺ spec:

package tla;
 
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Deque;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
 
class ModelChecker {
 
  private final Interpreter interpreter;
 
  ModelChecker(Interpreter interpreter, List<Stmt> spec) {
    this.interpreter = interpreter;
  }
}

The real TLA⁺ tools allow users to identify the init, next and invariant predicates in a model configuration file. We skip all that and simply require our specs to have operator definitions named Init, Next, and Inv. Iterate through all the spec statements to find them:

  private final Interpreter interpreter;
  private Stmt.OpDef init = null;
  private Stmt.OpDef next = null;
  private Stmt.OpDef invariantDef = null;
 
  ModelChecker(Interpreter interpreter, List<Stmt> spec) {
    this.interpreter = interpreter;
    for (Stmt unit : spec) {
      if (unit instanceof Stmt.OpDef) {
        Stmt.OpDef op = (Stmt.OpDef)unit;
        switch (op.name.lexeme) {
          case "Init"   : this.init = op;
          case "Next"   : this.next = op;
          case "Inv"    : this.invariantDef = op;
        }
      }
    }

We should be nice to the user and alert them if their spec is missing one of these definitions or the definition is not of the proper form. Add a validate() helper to the ModelChecker class:

  private static void validate(Stmt.OpDef op, String name) {
    if (op == null) {
      throw new IllegalArgumentException(
          "Spec requires '" + name + "' operator.");
    }
 
    if (!op.params.isEmpty()) {
      throw new IllegalArgumentException(
          "Spec '" + name + "' operator cannot take parameters.");
    }
  }

Then add calls to validate() at the bottom of our ModelChecker constructor:

    validate(this.init, "Init");
    validate(this.next, "Next");
    validate(this.invariantDef, "Inv");
  }

Step one complete!

Now we kick off the main event. Define a new checkSafety() method in the ModelChecker class:

  List<Map<String, Object>> checkSafety() {
 
    return null;
  }

This method indicates success (the invariant held in every state) by returning null. If the invariant does not hold in every state, the method returns a state trace leading to the failing state.