The behaviors of a correct program are a subset of those that are allowed byits specification. A program is said to be maximal if in addition to
being correct, it is capable of exhibiting all of the behaviors
permitted by its specification.
Requiring maximality is important for many applications. However, the existing
body of work on maximal software focuses on answering only one question: how
can one, given a specification and a program implementing it, prove the program
is maximal?
This thesis answers other questions about the
nature of maximality: Does the verification technique for maximality
extend to component-based systems? Do all specifications
have maximal implementations?
The first question we answer in the affirmative by extending the existing
verification technique to apply to such systems. The second question we answer
in the negative by showing that there are important and practically useful
specifications with no maximal implementation.
Specifically, the contributions of this thesis begin with the observation that
maximality is non-compositional. That is, given a system built from a set of
components, the maximality of components to their individual specifications is
not a sufficient condition for the maximality of the composed
system. We present a technique that allows for modular reasoning about
maximality properties by augmenting component specifications with
additional requirements that allow one to conclude that the composed system is
maximal if all components satisfy their augmented specifications.
We demonstrate the effectiveness of this technique by proving the maximality of
two algorithms solving a classic resource allocation problem in distributed
systems; later, we show the correspondence of this problem to the weakly-fair
scheduling problem. We address the problem of strongly-fair scheduling by
presenting the first distributed and maximal strongly-fair scheduler for atomic
actions. We then demonstrate that in general, where action execution
may be interleaved, no maximal scheduler exists. This is the first
problem to be shown to have no maximal solution.
The impossibility of maximal distributed strongly-fair scheduling motivates an
exploration of specifications for which no maximal solutions exist. We present
other specifications without maximal solutions and show that maximal
implementability is non-monotonic in the refinement hierarchy.