Complete assertional proof rules for progress under weak and strong fairness (2012)

The UNITY rules for leads-to, based on totality of the commands and weak fairness, are generalized to U-specifications with nontotal commands and impartiality. The rules and the corresponding predicate transformers are proved to be sound and complete by elementary means. These results are subsequently extended to specifications where the liveness property also contains a finite number of strong fairness assumptions. This is illustrated by means of a proof of starvation freedom for the standard implementation of mutual exclusion by plain semaphores, with strong fairness for the P operations.

A paper Complete assertional proof rules for progress under weak and strong fairness (2013) has been published. A PVS dumpfile is available. PVS users can unzip it and undump it, and inspect the specification and proof files. It is made primarily for author confidence, not for communication. It is therefore not very instructive.

The strength of UNITY (2020)

This generalization to U-specifications with nontotal commands makes two extensions possible, as follows.

One can extend UNITY logic in a sound way by allowing leads-to hypotheses. It is shown here, however, that in general the logic does not remain complete in this way. It is proved that completeness is retained if the leads-to hypotheses are what is called moderate. A hypothesis "P leads-to Q" is moderate iff "P unless Q" holds.

The second extension of the theory concerns linear-time temporal logic, LTL. In LTL, we have the usual operators for always, eventually, release, and until. The traditional next-operator, however, is sensitive to stuttering. As UNITY allows stuttering, the next-operator has been adapted. If P is a temporal property, next(P) means that P holds after the first change of some view of the state, assuming such a change exists. The view thus becomes a second parameter of the operator. On the other hand, a weak next-operator appears where the change need not exist.

An LTL formula is valid in a U-specification K iff the formula holds for all runs of K. It is shown that the validity of an LTL formula in a U-specification can be proved by UNITY logic. The way to do this is to ``implement'' the negation of the formula, so that all runs that satisfy the formula are removed. If the formula is valid, all runs are removed, and this can proved by UNITY logic. The implementation of an LTL formula goes by induction over its structure. One auxiliary variable is needed for each occurrence of a temporal operator. A paper is in preparation. The results have been verified with PVS, see the PVS dumpfile. This dump file is independent of the one mentioned above. The completeness proof in the one above is redone here.

Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink

Last modified: Wed May 6 17:27:18 CEST 2020