# Trylock and the Rectangle Algorithm

The projects below are closely related. They are done with Peter A. Buhr
and David Dice.
## Trylock, a case for temporal logic and eternity variables

This project concerns a software implementation TryL of trylock
based on Lamport's Fast Algorithm for mutual exclusion. It implements
trylock in linear time temporal logic (LTL), but not in computation
tree temporal logic (CTL). The proof for the LTL case uses simulation
techniques. It needs a prophecy of the succeeding thread, which is
supplied by an eternity variable. The proof uses UNITY for two
progress properties. A paper is in preparation.
A
PVS proof script is available.

## The Rectangle Algorithm for mutual exclusion

The Rectangle Algorithm uses N-1 instances of TryL (trylock) to sort the
competing threads without waiting. The sorted threads compete in a
biased binary tournament for access to the critical section. A paper
is in preparation.
A
PVS proof script is available.

Comments and questions are welcome.

Back to my home page.

Last modified: 11 February 2020.