Program Composition in UNITY: A Mechanized Theory

UNITY is a formalism for reasoning about shared variable concurrent programs. It has been mechanized in higher-order logic using the theorem prover Isabelle. Many of the standard examples have been done, for example, Andersen's Lift.

With program composition, we wish to reason about a program by referring to the properties of its components. Such reasoning is easy for safety properties, but not for progress (liveness) properties. A new type of guarantees assertion, proposed by Chandy and Sanders, may provide a general framework for compositional reasoning.

A critical problem is that the different components of a system will typically declare different variables, and therefore have different state spaces. It is difficult to transfer program properties from one state-space to another, especially progress properties. However, we expect to be able to specify a component without knowing what other components it might be composed with. A solution to this dilemma using polymorphism is outlined.

LS Home page or Talks in 1999/2000