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