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.
We have provided a tar archive of our code with example files.
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
rltoolThe example system specifications can be found in directory
rltool/systemsand the proof scripts can be found in
rltool/tests/systemsTo run any of the examples, do:
/path/to/maude-binary /path/to/rltool/tests/systems/test-name
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:
ctor
(this operator a constructor)assoc
(this operator is binary associative)comm
(this operator is binary commutative)id: elem
(this operator is binary with identity element elem
)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.
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.
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
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.
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:
wake
rule)crit
rule),exit
rule).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.