An Introduction to the UV System

This document is intended to give you a very brief overview of the UV system and the concepts it is based on. You find information here on the following topics:

What is UNITY?

UNITY is a programming notation and simple temporal logic for designing and reasoning about concurrent and parallel programs. It was developed originally by K.M.Chandy and J.Misra here at UT and is described in their book Parallel Program Design: A Foundation, Addison-Wesley, 1988.

UNITY is given a state-based transition system semantics and derives much of its simplicity from abstracting away from the notion of control flow. A UNITY program is essentially a bag of multiple assignment statements, a program execution consists of repeatedly selecting statments from the bag and executing them atomically (subject to the fairness constraint, that no statement be ignored forever).

Properties of UNITY logic can be devided into safety and progress properties. A typical safety property is the invariant property stating that some predicate invariantly holds during any program execution. For instance the property

invariant x>0
states that variable x is always positive in any program execution. A typical progress property on the other hand is the leads-to property, which states that whenever some predicate holds during some state in a program execution, some (other) predicate inevitably holds at the same or a later state of that execution. For instance the property
x=0 leads-to x>0
states that whenever x is equal to 0 during any program execution, it is positive at some later point in the execution.

In spite of its simplicity UNITY logic is sufficiently expressive for many interesing specifications that arise when designing concurrent programs.

What is model checking?

Model checking is a verification technique first introduced by E.M.Clarke, E.A.Emerson and A.P.Sistla in their TOPLAS 1986 paper Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. In principle a model checking task consists of determining whether a given program satisfies a given property of some temporal logic.

There is by now a vast amount of literature available on model checking. Due to progress with symbolic representation of finite state systems and temporal logic formulae based on binary decision diagrams, model checking has become a powerful technique with applications in particular to circuit verification.

What can I do with the UV system?

The UV system implements model checking algorithms for finite state UNITY programs and propositional UNITY properties. It supports an interactive style of proving properties through a graphical user interface by allowing the user to supply certain design knowledge to the system thereby facilitating the verification of properties.

Taking advantage of the special form of UNITY temporal operators it provides a very efficient way of determining whether a given UNITY program satisfies a given formula of UNITY logic.

Programs and properties are passed as input to the system written in a ASCII based input language. Simple finite data types (boolean, finite range integer, enumeration) and all temporal operators of UNITY logic are supported.

Show me a small example...

The following UNITY program is a 2 process mutual exclusion algorithm taken from the paper A Family of 2-process Mutual Exclusion Algorithms by Jayadev Misra, Notes on UNITY 13/1990. We exhibit here the input to the UV system for proving this program correct: 
program Mutex
  declare
    type PC = (noncritical, requesting, trying, critical, exiting);
    var m, n: PC;   	    	// 'program counters' for processes
    var u, v, p: boolean;
    var hu, hv: boolean;	// auxiliary variables to model non-
				// deterministic behaviour of processes
				// with respect to their finishing their
				// critical section
  initially
    ~u;
    ~v;
    m = noncritical;
    n = noncritical;
  assign

    // first process (u)
    hu   := ~hu;
    u, m := true, requesting   if hu /\ m = noncritical;
    p, m := v, trying          if m = requesting;
    m    := critical           if ~p /\ m = trying;
    u, m := false, exiting     if m = critical;
    p, m := true, noncritical  if m = exiting;

    // second process (v)
    hv   := ~hv;
    v, n := true, requesting   if hv /\ n = noncritical;
    p, n := ~u, trying         if n = requesting;
    n    := critical           if p /\ n = trying;
    v, n := false, exiting     if n = critical;
    p, n := false, noncritical if n = exiting;

end;
Two interesting properties one would like to prove for this program are mutual exclusion and absence of starvation: 
invariant ~(m = critical /\ n = critical);	// mutual exclusion
m = requesting --> m = critical;		// absence of starvation
Both of these properties can be easily proved with the UV system either in a fully automated way (by computing the strongest invariant of the program), or by using additional invariants supplied by the user following her/his understanding of the program.

The UV system was actually used to discover some errors in the manual proofs of the above properties by showing that some of the auxiliary properties given in the original paper are not satisfied by the program.

Where do I go next?

A good starting point for learning more about the current revised form of UNITY is a manuscript by Jay Misra.

On the UV System home page you find documentation about the current revision of the system, or you can download a distribution archive and experiment with the system yourself.

This page was last updated on 23-December-1994
Markus Kaltenbach (markus@cs.utexas.edu)