# Trylock with applications in the Rectangle Algorithm and Random Selection

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.

## Mutual exclusion with random selection

In this mutual exclusion algorithm, the thread in the critical
section selects its successor, by a uniform random choice among the
waiting threads. The function trylock is used for the situation that
all threads are idle and a first competing thread appears. A paper
is in preparation.
A
PVS proof script is available.

Comments and questions are welcome.

Back to my home page.

Last modified: Sun Jul 5 11:06:34 CEST 2020