.

KBackery.tla

@@ -2,12 +2,79 @@
 
 CONSTANT N  \* number of processes
 
+\* How the algorithm is designed:
+
+\* 1. start from algorithm directly created from words:
+\*
+\*      process(i \in 1..N)
+\*      variable j \in Nat
+\*      {
+\*          while (TRUE)  {
+\*      \*  > get a ticket
+\*              ticket[i]  := 1 + max(ticket[j]  \A j \in 1..N)
+\*
+\*      \*  > wait till when got ticket is < all other tickets
+\*              for  j \in 1..N  {
+\*          Lwait_jbehind:
+\*                  while (~(ticket[j]=0 \/ ticket[i] < ticket[j]))
+\*                      goto Lwait_jbehind;
+\*              }
+\*
+\*      \*  > service
+\*          cs: skip
+\*
+\*      \*  > end - recycle the ticket
+\*              ticket[i] := 0
+\*          }
+\*      }
+
+\* 2. Notice that there might be deadlock if proc[i] and proc[k] race on
+\* entry/entry: in that case ticket[i] might be = ticket[k] and both processes will
+\* deadlock looping on Lwait_jbehind.
+\*
+\*       P1              P2
+\*      t1=0            t2=0
+\*      t1=1            t2=1
+\*      while(t1>=t2)   while(t2>=t1)
+\*
+\* FIX: `ticket[i] < ticket[j]`   =>  `(ticket[i],i) < (ticket[j],j)`
+
+\* 3. Check wait[i]/entry[k] for race.
+\* If entry[i]/entry[k] raced and entry[k] lasts longer and overlaps with
+\* wait[i], it is possible for both proc[i] and proc[k] to enter cs at the same time:
+\*
+\*       P1              P2
+\*      t1=0            t2=0
+\*      # entry         # entry
+\*      <read t2        <read t1
+\*      >read t2(0)     >read t1(0)
+\*                      t2=1
+\*
+\*                      # wait
+\*                      read t1(0)
+\*      t1=1
+\*      # wait          <CS
+\*      read t2(1)      ...
+\*   Y: (t1,1)<(t2,2)   ...
+\*       |              ...
+\*       v              ...
+\*      <CS             ...         <-- ~ME(cs)
+\*
+\*
+\* FIX: Introduce inentry[i] and before Lwait_jbehind wait for proc[j] to first
+\* complete its entry phase if it was in there.
+
+
+\* 4. Check wait[i]/wait[j] for race.
+\* No variables are assigned in wait => there cannot be any race here.
+
+
 
 (*******
 --algorithm KBackery
 variables
 \*  > *[i] is located on memory unit of proc[i]
-    ticket  = [i \in 1..N |-> 0]      \* ticket=0 means "inactive"  XXX or `^\infty^' ?
+    ticket  = [i \in 1..N |-> 0]      \* ticket=0 means "inactive"
     inentry = [i \in 1..N |-> FALSE]  \* T while in entry. To avoid ~ME(cs) on wait/entry race
 
 process(i \in 1..N)