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.
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, and is therefore omitted here. A temporal property is valid in a U-specification K iff it holds for all runs of K. It is shown that the validity of an LTL property in a U-specification can be proved by UNITY logic. The way to do this is to ``implement'' the negation of the property, so that all runs that satisfy the property are removed. If the property is valid, all runs are removed, and this can proved by UNITY logic. The implementation of an LTL property goes as follows. Determine an LTL formula that can be interpreted as the property. Construct a Buechi automaton for the LTL formula. Finally attach this automaton to the program. A new construction of the Buechi automaton is proposed. 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