## Complete assertional proof rules for progress under weak and strong fairness

The UNITY rules for leads-to, based on totality of the commands
and weak fairness, are generalized to 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 is in print. 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.

## A new complete extension of UNITY logic with strong fairness by simulation

While finalizing the paper mentioned above, I was inspired by the
reviews of that paper to go considerably further on this road.

UNITY logic serves to prove for a concurrent program progress
properties of the form ``P leads to Q''. This logic is sound and
complete with respect to the operational semantics. When a UNITY
program is extended with axioms that postulate progress properties,
the logic can use these axioms and remain sound. It is unknown
whether the logic remains complete. It is shown here that the logic
remains complete when the axioms added are *moderate*, where
moderacy of an axiom "F leads to G" means that "F unless G" holds.

It is further shown that specifications with leads-to axioms that
are not moderate, as well as specifications with strong fairness
requirements, can be simulated faithfully by specifications with
moderate leads-to axioms. A paper is in preparation. The results
have been verified with PVS, see the PVS
dumpfile. This dump file may be somewhat better accessible than
the one above. They are independent. 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: Mon Nov 26 15:51:49 CET 2012