This project is a theoretical offshoot of the collaboration with Peter Buhr and Dave Dice. It 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. The paper has been accepted by Science of Computer Programming. A PVS proof script of 28 Nov. 2021 is available.
The PVS proof script is not for human reading. One can "undump" it with the proof assistant PVS. This generates files with the extensions pvs and prf. The files with extension pvs contain theories that can be read by humans, and can be proved with PVS, using the prf files. The theory `specification' treats specifications, including invariants and UNITY. Different specifications are related by means of the theories simulation, restriction, and composition. Auxiliary theories are named sums, property, and ownpred. The various specifications TryL are treated in the files tryLamport[0123].pvs.
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.
This mutual exclusion algorithm allows selection of the next thread that gets exclusive access to CS, among the threads that have asked for it. One of the possibilities is 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.