A Constructor-Based Reachability Logic for Rewrite Theories

Abstract

Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs. It has been proved successful in verifying a wide range of sophisticated programs in conventional languages. Here we study how reachability logic can be made not just language-generic, but rewrite-theory-generic to make it available not just for conventional program verification, but also to verify rewriting-logic-based programs and distributed system designs. A theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. The logic’s automation is increased by means of constructor-based semantic unification, matching, and satisfiability procedures. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new methods are presented.

Downloads

We have provided a tar archive of our code with example files.

Running Examples

To run any of the examples in our system, you will first need to download a Maude interpreter. They can be downloaded from the Maude website. Then untar the archive, which will create a folder

rltool
The example system specifications can be found in directory
rltool/systems
and the proof scripts can be found in
rltool/tests/systems
To run any of the examples, do:
/path/to/maude-binary /path/to/rltool/tests/systems/test-name

Example Overview

See a (partial) table of the example systems and properties the paper considers below, in order (roughly) from simpler to more complex. Note all of these examples are in the tar archive.

The presentation of the examples below is slightly modified from the original Maude code. Maude evaluates code contained in units called modules. A module is a collection of sort, operator, variable, and rewrite rule declarations. Modules can import other modules. A typical module looks like:

mod NAME is pr NAME1 ... NAMEj .
  sort    declarations ...
  subsort declarations ...
  op      declarations ...
  var     declarations ...
  rule    declarations ...
endm

where NAME is the name of the module and NAME1 to NAMEj are the names of the modules which the current module imports.

Type declarations (called sorts in Maude) are denoted by:

sort Name1 Name2 ... Namej .

while subsort declarations are denoted by:

subsort Name1 ... < ... Namej ... < ... < ... Namek .

Operator declarations use a mixfix-style syntax where underbars represent argument positions. The following operator declaration:

op _|_ : Type1 Type2 -> Type3 [attribute list] .

if given arguments a and b of types Type1 and Type2 respectively, will be written a | b. The attribute list can contain:

Variable declarations (variables are used in rule declarations) are denoted by:

var Name1 Name2 ... Namej : Type .

Rewrite rule declarations use the syntax:

rl [name] : lhs => rhs if cond

The name and conditional part at the end are optional.

A Few Examples in More Detail

We list a few examples in more detail so that reader can get a flavor for the kinds of properties we have verified with our example tool.
The rest of the examples are available in the tar archive retrievable at the link above.

Nondeterministic Choice

fmod CHOICE-DATA is
  sort Nat MSet State .
  subsort Nat < MSet .
  op zero : -> Nat [ctor] .
  op s    : Nat -> Nat [ctor] .
  op __   : MSet MSet -> MSet [ctor assoc comm] .
  op {_}  : MSet -> State [ctor] .
endfm

mod CHOICE is pr CHOICE-DATA .
  vars U V : MSet .
  rl [choice] : {U V} => {U} .
endm

Our nondeterministic choice example has three types: Nat, MSet, and State where Nat is a subtype of MSet. A State is just a curly-brace ({}) wrapped multi-set. Type MSet represents a non-empty multi-set (associative/commutative) operator (represented by juxtaposition) over natural numbers. It has a single rewrite rule, which grabs a non-empty sub-multiset and discards it, defined in the CHOICE module.

The invariant we wish to verify is that, eventually, after repeatedly discarding non-empty sub-multisets, the multi-set in our State will contain a single element which belonged to our original multiset. Since this system is terminating, we can directly verify reachability sequents over it.

The reachability logic sequent we have in mind is:

{ M } | true   →   { N } | true

where N is a natural number element of M

2-Token Ring Mutual Exclusion Protocol

mod 2TOKEN is
  sorts Name Proc Token MSet State .
  subsorts Proc Token < MSet .
  op {_}      : MSet      -> State [ctor] .
  op none     :           -> MSet  [ctor] .
  ops * $     :           -> Token [ctor] .
  ops a b     :           -> Name  [ctor] .
  op __       : MSet MSet -> MSet  [assoc comm id: none] .
  op [_,wait] : Name      -> Proc  [ctor] .
  op [_,crit] : Name      -> Proc  [ctor] .
  var PS : MSet .
  rl [a-enter] : { $ [a,wait] PS } => { [a,crit]   PS } .
  rl [b-enter] : { * [b,wait] PS } => { [b,crit]   PS } .
  rl [a-exit]  : {   [a,crit] PS } => { [a,wait] * PS } .
  rl [b-exit]  : {   [b,crit] PS } => { [b,wait] $ PS } .
endm

mod 2TOKEN-stop is protecting 2TOKEN .
  op [_] : MSet -> State .
  var PS : MSet .
  rl [done] : { PS } => [ PS ] .
endm

The 2-Token Ring mutual exclusion protocol passes a shared token between two processes to control who is allowed to enter the critical section and is defined in the module 2TOKEN. As with any mutual exclusion protocol, the main property we wish to verify is that only one process can enter the critical section at any given moment. As before, we have a sort State which is a wrapper ({}) over (possibly empty) multi-sets (MSet) of processes and tokens defined by sorts Proc and Token respectively. A process has two contructors [_,wait] or [_,crit] representing waiting processes and processes in the critical section. It's only argument is a Name (either a or b). There are also two kinds of tokens: (*) and ($). There are four rules: two rules where a waiting process consumes a token to enter the critical section and two rules where a critical process produces a token and returns to the waiting state. Since this is a never-terminating system, we must apply the transformation given in the paper. This trasformed module is defined in 2TOKEN-stop and defines a new State wrapper ([]) and a new rule which rewrites any curly brace bracketed state into a square brace bracketed state (thus any square-bracketed state will now be terminating).

Then the invariant is given by the reachability logic sequent:

{[a,crit] [b,wait]} | true {[a,wait] [b,crit]} | true {[a,wait] [b,wait] T } | true
[[a,crit] [b,wait]] | true [[a,wait] [b,crit]] | true [[a,wait] [b,wait] T'] | true

where variables T and T' are variables of sort Token and our initial state is:

{[a,crit] [b,wait]}.

To complete the proof, we show that invariant is closed under rewriting and that it is a superset of the initial state. Since this is a finite state system, of course, model-checking methods could be used to solve it. The interesting feature here is the use of the theory transformation to prove invariants in reachability logic.

Unbounded Lamport's Bakery Protocol

fmod BAKERY-STATE is pr NAT .
  sort Conf MSet Proc Mode .
  subsort Proc < MSet .

  op idle  :              -> Mode  [ctor] .
  op wait  : Nat          -> Mode  [ctor] .
  op crit  : Nat          -> Mode  [ctor] .
  op [_,_] : Nat Mode     -> Proc  [ctor] .
  op none  :              -> MSet  [ctor] .
  op __    : MSet MSet    -> MSet  [ctor assoc comm id: none] .

  op _;_;_ : Nat Nat MSet -> Conf  [ctor] .
endfm

mod REVERSE-BAKERY is pr BAKERY-STATE .
  sort State .
  op <_> : Conf -> State [ctor] .

  var N M I : Nat .
  var PS : MSet .

  rl [wake]: < N :+ 1 ; M      ; [I,wait(N)] PS > => < N ; M ; [I,idle   ] PS > .
  rl [crit]: < N      ; M      ; [I,crit(M)] PS > => < N ; M ; [I,wait(M)] PS > .
  rl [exit]: < N      ; M :+ 1 ; [I,idle   ] PS > => < N ; M ; [I,crit(M)] PS > .
endm

mod REVERSE-BAKERY-stop is pr REVERSE-BAKERY .
  op [_] : Conf -> State [ctor] .
  var C : Conf .
  rl [term]: < C > => [ C ] .
endm

Lamport's Bakery Protocol is a classic mutual exclusion protocl where each process is assigned a unique ticket that identifies when it can enter the critical section. The ticket counter maintains two indices: an index for the next fresh ticket number and a separate index describing which process will enter the critical section. As with any mutual exclusion protocol, the main property we wish to verify is that only one process can enter the critical section at any given moment. The system state is defined in module BAKERY-STATE. Here, each process (sort Proc) is represented as a pair [_,_] with a natural number process identifier (sort Nat) and a mode (sort Mode). A mode can be either: idle, wait(_), or crit(_) where waiting and critical modes are assigned a natural number identifier (their ticket number). Sort MSet defines (possibly empty) multi-sets of processes. Sort Conf describes a system configuration which contains the two ticket counters as well as a multi-set of processes. There are two important things to note:

This unboundedness complicates the analysis; concrete model checking methods cannot verify it, and the system is not well-suited for equational abstractions.

The system rules are defined in the module REVERSE-BAKERY. Essentially, the rules allow:

Note that, all of the rewrite rules in our module are actually reversed when compared to the standard Lamport's Bakery definition. However, since our tool only evaluates rewrite theories symbolically, it matters little in which direction rewrite rules are evaluated.

Finally, given that Lamport's Bakery is a never-terminating system, we must apply the transformation given in the paper and defined in module REVERSE-BAKERY-stop. Now, we can specify the invariant we want to prove. Note that, since our theory is operating in reverse, we instead specify the co-invariant (the logical negation of the invariant) and show that it is closed under rewriting and disjoint from the intial state to complete our proof.

A reasonable first attempt at a co-invariant might be:

{ A ; B ; [I,crit(N)] [J,crit(M)] PS } | true   →   { A' ; B' ; [I',crit(N')] [J',crit(M')] PS' } | true

Essentially, this co-invariant states that any system that has two processes in the critical section at the same time will always evolve to a state that also has two critical processes. However, this co-invariant is not strong enough.

The complete co-invariant we used is quite complex with 11 different constrained constructor patterns considered, since we have to cover a large number of possible failure modes.