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 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.
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.