Trylock, a case for temporal logic and eternity variables

An example is given of a software algorithm that implements its specification in linear time temporal logic (LTL), but not in branching time temporal logic (CTL). In LTL, a prophecy of future behaviour is needed to prove the simulation. Eternity variables are used for this purpose. The final phase of the proof is a refinement mapping in which two threads exchange roles. The example is a software implementation of trylock in a variation of the fast mutual exclusion algorithm of Lamport (1987). It has been used fruitfully for the construction of software algorithms for high performance mutual exclusion. (C) 2021 The Author(s). Published by Elsevier B.V.