In the first lesson of his course on distributed computing, Dr. Guerraoui gives a definition of a safe, regular or atomic register
at 6:15.
This definition is given informally and as such is ambiguous. And above all it is given for boolean variables.
In his article on p.19, Dr. Lamport gives slightly different definitions and in particular for multivalued variables.
Could someone give formal definitions of these notions (with TLAPLUS macros) and/or/xor show the compatibility of Dr. Gerraoui's and Dr. Lamport's définitions.
I think one must use temporal logic concepts to do so and it is not especially simple at first sight.
--
FL