Safe, regular or atomic registers

[fl]

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.

http://www.college-de-france.fr/site/rachid-guerraoui/course-2018-10-26-10h00.htm

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.

https://lamport.azurewebsites.net/pubs/interprocess.pdf

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

[Leslie Lamport]

My original definitions of safe, regular, and atomic (for a single
writer) were given in a formalism whose semantics is not the trace
semantics of TLA, a direct translation of those concepts into TLA+ is
not nice.  But it's not difficult.  Here's one way.  Just let the
writer have a variable that contains the current value of the
register, and let have each reader have a data structure including a
sequence of writer operations to which, when the reader is currently
writing, the writer appends something when it begins and finishes each
write operation.

I believe the following simpler TLA+ implementations can be
proven to be equivalent.  For an atomic register, just make the reads
and writes atomic.  For safe and regular, here are implementations of
a register r to which a single writer can write a value in a set T of
possible values and any number of readers can read the value.

Safe Register - Method 1
--------------------------
   Define notValue == CHOOSE t : t \notin T

   Write(v)  a: r := notValue ;
             b: r := v ;

   Read      c: with  (v \in IF r = notValue THEN T ELSE {r})
                      { result := v }

Safe Register -  Method 2
--------------------------
   Write(v) a: with (v \in T) {r := v}
               either goto a
                   or await r = v ;
   Read      result := r

Regular Register
----------------
   Write(v)   r := v ;

   Read      Seen := {}
          a: either { Seen := Seen \cup {r};
                      goto a }
                or  with (v \in Seen)
                      { return v }

Leslie

[fl]

[macros]

These are macros of the Pluscal language aren't they. (3.5 p. 28)

https://lamport.azurewebsites.net/tla/c-manual.pdf

In fact I meant a predicate expressed as a TLA+ operator (17.5.3 p. 329)

https://lamport.azurewebsites.net/tla/book-02-08-08.pdf

Forgive the inaccuracy of my vocabulary.

Anyway I'll try to implement what you have suggested.

-- 

FL

[fl]

I think a trace of a safe register could look like this (1 writer, 1 reader, non-overlapping processes).

We have 4 variables Writer Reader Register Result.

Writer and Reader can take the values: None Start End

Register can take the value: 0, 1, 2

And Result can take the value: 0, 1 , 2 , 3

== Initial state ==

Writer = None

Reader = None

Register = 0

Result =  3

== State 1 ==

Writer = Start

Reader = None

Register = 0

Result =  3

== State 2 ==

Writer = Start

Reader = None

Register = 2

Result =  3

== State 3 ==

Writer = End

Reader = None

Register = 2

Result =  3

== State 4 ==

Writer = End

Reader = Start

Register = 2

Result =  3

== State 5 ==

Writer = End

Reader = Start

Register = 2

Result =  2

== Final State ==

Writer = End

Reader = End

Register = 2

Result =  2

[fl]

And a trace of a safe register  (1 writer, 1 reader, overlapping processes) could look like this for instance.

We have 4 variables Writer Reader Register Result.


Writer and Reader can take the values: None Start End


Register can take the value: 0, 1, 2


And Result can take the value: 0, 1 , 2 , 3


== Initial state ==


Writer = None
Reader = None
Register = 0
Result = 3

== State 1 ==

Writer = Start
Reader = None
Register = 0
Result = 3


== State 2 ==


Writer = Start
Reader = None
Register = 2
Result = 3

== State 3 ==

Writer = Start

Reader = Start
Register = 2
Result = 3

== State 4 ==

Writer = Start

Reader = Start
Register = 2

Result = 0

== State 5 ==

Writer = Start

Reader = End
Register = 2

Result = 0

== Final State ==

Writer = End
Reader = End
Register = 2

Result = 0