------------------------ MODULE lock_free_stack_ABA ------------------------

\*******************************************************************
\* Copyright (c) 2017, Gene Cooperman.  May be freely distributed
\* and modified as long as this copyright notice remains.
\*
\* For ABA problem, see:  https://en.wikipedia.org/wiki/ABA_problem
\*
\* NOTE:  The label "pop2a" in popStack() below "causes" the bug to be
\*        exposed.  Try deleting it. This would have the effect
\*        of atomically executing:
\*          CAS( HEAD, local_myhead, address[local_myhead].next );
\*        because it hides the internal assembly code that first
\*        computes the register value, reg_next, and then executes CAS().
\*
\*        Note that the field "onStack" is present only for debugging,
\*        and for assertions.  Don't hesitate to add extra fields and
\*        variables to ease the job of model checking.
\*
\*        The bug is the ABA problem.  When illustrating this bug,
\*        the errors in the "Model Checking Results" tab will have
\*        too many frames to easily read.  You can then remove many
\*        of the unnecessary labels in other routines to easily see
\*        the cause of the bug:  the ABA problem.
\*******************************************************************

\* Always include these PlusCal modules for basic data types.
EXTENDS Naturals, Sequences, TLC, FiniteSets

\* These constants will have to be assigned a value within the generated module.
CONSTANTS MAX_ITER_THR_A, MAX_ITER_THR_B, MAX_STACK_SIZE

\* NUM_THREADS is a PRE-DEFINED constant.  It cannot be changed later.
NUM_THREADS == 2

\* null is a unique value (pre-defined constant)
NULL == CHOOSE n: n \notin 1..MAX_STACK_SIZE

(*
--algorithm LockFreeStack {
variables retVal = [thread \in 1..NUM_THREADS |-> NULL],
          address = [ addr \in 1..MAX_STACK_SIZE |->
                      [next |-> NULL, onStack |-> FALSE, data |-> 0] ],
          initialized = FALSE;
          HEAD ;

\* CAS:  compare-and-swap
\* CAS must be a macro.  This reflects that it is an assembly instruction
\*   that modifies its arguments. It must not use the call-by-value of a procedure.
\* CAS is atomic.  So, there are no intermediate labels.
macro CAS(x, y, z)
{
  if (x = y) {
    x := z; \* swap y for z as value of x
    retVal[self] := TRUE;
  } else {
    retVal[self] := FALSE;
  } ;
}

procedure pushStack(elt)
  variable local_myhead;
{
  push1: address[elt].next := HEAD;
    assert address[elt].onStack = FALSE;
  push2: address[elt].onStack := TRUE;
  tryAgainPush: local_myhead := HEAD;
        address[elt].next := local_myhead;
        push5b: CAS( HEAD, local_myhead, elt );
        push5c: if (~retVal[self]) {
        goto tryAgainPush;
                } ;
  endPush:  return;
}

procedure popStack()
  variable local_myhead, reg_next, elt;
{
  tryAgainPop:
     local_myhead := HEAD;
   if (local_myhead = 0) { \* // If I believe HEAD = 0, return now.
  pop1a:  retVal[self] := NULL;
    return;
        } ;

  pop2:  reg_next :=  address[local_myhead].next;
  pop2a: CAS( HEAD, local_myhead, reg_next );
  pop2b: if (~retVal[self]) {
  pop2c:   goto tryAgainPop;
         } ;
  pop3: elt := local_myhead;
   assert address[elt].onStack = TRUE;
   address[elt].onStack := FALSE;              
   retVal[self] := elt ;
  endPop: return;
}

process (thread \in 1..NUM_THREADS)
  variable my_set = {}, myelt,
           init_thread, iterations = 0 ;
{ init0: if (self = 1) {iterations := MAX_ITER_THR_A;}
         else {iterations := MAX_ITER_THR_B;} ;
  init1: init_thread := CHOOSE thr \in 1..NUM_THREADS : TRUE ;
  if (self = init_thread) { \* // This thread will initialize global data
     HEAD := 0;
  init5: while (HEAD < MAX_STACK_SIZE) {
      address[HEAD+1] := [ next |-> HEAD, onStack |-> TRUE, data |-> 1 ];
       HEAD := HEAD+1;
           } ;
     initialized := TRUE; \* // init_thread will set this global var
         } ;
  init9: await initialized; \* // all threads will wait for this

  th1: while (iterations > 0) {
  th2:   either {if (my_set /= {}) {
                 \* // Set myelt at random (non-deterministically)
  th2a:          with (tmp \in my_set) { myelt := tmp } ;
             my_set := my_set \ {myelt};
             call pushStack(myelt);
               } }
         or {
  th3a:      call popStack();
  th3b:      if (retVal[self] /= NULL) {
  th3c:        my_set := my_set \cup { retVal[self] } \* // Add the popped elt to my_set
             } };
  th4: iterations := iterations - 1 ;
  print iterations;
  } ; \* end while
} ; \* end process

} \* end algorithm

*)
\* BEGIN TRANSLATION
\* Procedure variable local_myhead of procedure pushStack at line 62 col 12 changed to local_myhead_
\* Procedure variable elt of procedure popStack at line 77 col 36 changed to elt_
CONSTANT defaultInitValue
VARIABLES retVal, address, initialized, HEAD, pc, stack, elt, local_myhead_, 
          local_myhead, reg_next, elt_, my_set, myelt, init_thread, 
          iterations

vars == << retVal, address, initialized, HEAD, pc, stack, elt, local_myhead_, 
           local_myhead, reg_next, elt_, my_set, myelt, init_thread, 
           iterations >>

ProcSet == (1..NUM_THREADS)

Init == (* Global variables *)
        /\ retVal = [thread \in 1..NUM_THREADS |-> NULL]
        /\ address = [ addr \in 1..MAX_STACK_SIZE |->
                       [next |-> NULL, onStack |-> FALSE, data |-> 0] ]
        /\ initialized = FALSE
        /\ HEAD = defaultInitValue
        (* Procedure pushStack *)
        /\ elt = [ self \in ProcSet |-> defaultInitValue]
        /\ local_myhead_ = [ self \in ProcSet |-> defaultInitValue]
        (* Procedure popStack *)
        /\ local_myhead = [ self \in ProcSet |-> defaultInitValue]
        /\ reg_next = [ self \in ProcSet |-> defaultInitValue]
        /\ elt_ = [ self \in ProcSet |-> defaultInitValue]
        (* Process thread *)
        /\ my_set = [self \in 1..NUM_THREADS |-> {}]
        /\ myelt = [self \in 1..NUM_THREADS |-> defaultInitValue]
        /\ init_thread = [self \in 1..NUM_THREADS |-> defaultInitValue]
        /\ iterations = [self \in 1..NUM_THREADS |-> 0]
        /\ stack = [self \in ProcSet |-> << >>]
        /\ pc = [self \in ProcSet |-> "init0"]

push1(self) == /\ pc[self] = "push1"
               /\ address' = [address EXCEPT ![elt[self]].next = HEAD]
               /\ Assert(address'[elt[self]].onStack = FALSE, 
                         "Failure of assertion at line 65, column 5.")
               /\ pc' = [pc EXCEPT ![self] = "push2"]
               /\ UNCHANGED << retVal, initialized, HEAD, stack, elt, 
                               local_myhead_, local_myhead, reg_next, elt_, 
                               my_set, myelt, init_thread, iterations >>

push2(self) == /\ pc[self] = "push2"
               /\ address' = [address EXCEPT ![elt[self]].onStack = TRUE]
               /\ pc' = [pc EXCEPT ![self] = "tryAgainPush"]
               /\ UNCHANGED << retVal, initialized, HEAD, stack, elt, 
                               local_myhead_, local_myhead, reg_next, elt_, 
                               my_set, myelt, init_thread, iterations >>

tryAgainPush(self) == /\ pc[self] = "tryAgainPush"
                      /\ local_myhead_' = [local_myhead_ EXCEPT ![self] = HEAD]
                      /\ address' = [address EXCEPT ![elt[self]].next = local_myhead_'[self]]
                      /\ pc' = [pc EXCEPT ![self] = "push5b"]
                      /\ UNCHANGED << retVal, initialized, HEAD, stack, elt, 
                                      local_myhead, reg_next, elt_, my_set, 
                                      myelt, init_thread, iterations >>

push5b(self) == /\ pc[self] = "push5b"
                /\ IF HEAD = local_myhead_[self]
                      THEN /\ HEAD' = elt[self]
                           /\ retVal' = [retVal EXCEPT ![self] = TRUE]
                      ELSE /\ retVal' = [retVal EXCEPT ![self] = FALSE]
                           /\ HEAD' = HEAD
                /\ pc' = [pc EXCEPT ![self] = "push5c"]
                /\ UNCHANGED << address, initialized, stack, elt, 
                                local_myhead_, local_myhead, reg_next, elt_, 
                                my_set, myelt, init_thread, iterations >>

push5c(self) == /\ pc[self] = "push5c"
                /\ IF ~retVal[self]
                      THEN /\ pc' = [pc EXCEPT ![self] = "tryAgainPush"]
                      ELSE /\ pc' = [pc EXCEPT ![self] = "endPush"]
                /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                                local_myhead_, local_myhead, reg_next, elt_, 
                                my_set, myelt, init_thread, iterations >>

endPush(self) == /\ pc[self] = "endPush"
                 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
                 /\ local_myhead_' = [local_myhead_ EXCEPT ![self] = Head(stack[self]).local_myhead_]
                 /\ elt' = [elt EXCEPT ![self] = Head(stack[self]).elt]
                 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
                 /\ UNCHANGED << retVal, address, initialized, HEAD, 
                                 local_myhead, reg_next, elt_, my_set, myelt, 
                                 init_thread, iterations >>

pushStack(self) == push1(self) \/ push2(self) \/ tryAgainPush(self)
                      \/ push5b(self) \/ push5c(self) \/ endPush(self)

tryAgainPop(self) == /\ pc[self] = "tryAgainPop"
                     /\ local_myhead' = [local_myhead EXCEPT ![self] = HEAD]
                     /\ IF local_myhead'[self] = 0
                           THEN /\ pc' = [pc EXCEPT ![self] = "pop1a"]
                           ELSE /\ pc' = [pc EXCEPT ![self] = "pop2"]
                     /\ UNCHANGED << retVal, address, initialized, HEAD, stack, 
                                     elt, local_myhead_, reg_next, elt_, 
                                     my_set, myelt, init_thread, iterations >>

pop1a(self) == /\ pc[self] = "pop1a"
               /\ retVal' = [retVal EXCEPT ![self] = NULL]
               /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
               /\ local_myhead' = [local_myhead EXCEPT ![self] = Head(stack[self]).local_myhead]
               /\ reg_next' = [reg_next EXCEPT ![self] = Head(stack[self]).reg_next]
               /\ elt_' = [elt_ EXCEPT ![self] = Head(stack[self]).elt_]
               /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
               /\ UNCHANGED << address, initialized, HEAD, elt, local_myhead_, 
                               my_set, myelt, init_thread, iterations >>

pop2(self) == /\ pc[self] = "pop2"
              /\ reg_next' = [reg_next EXCEPT ![self] = address[local_myhead[self]].next]
              /\ pc' = [pc EXCEPT ![self] = "pop2a"]
              /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                              local_myhead_, local_myhead, elt_, my_set, myelt, 
                              init_thread, iterations >>

pop2a(self) == /\ pc[self] = "pop2a"
               /\ IF HEAD = local_myhead[self]
                     THEN /\ HEAD' = reg_next[self]
                          /\ retVal' = [retVal EXCEPT ![self] = TRUE]
                     ELSE /\ retVal' = [retVal EXCEPT ![self] = FALSE]
                          /\ HEAD' = HEAD
               /\ pc' = [pc EXCEPT ![self] = "pop2b"]
               /\ UNCHANGED << address, initialized, stack, elt, local_myhead_, 
                               local_myhead, reg_next, elt_, my_set, myelt, 
                               init_thread, iterations >>

pop2b(self) == /\ pc[self] = "pop2b"
               /\ IF ~retVal[self]
                     THEN /\ pc' = [pc EXCEPT ![self] = "pop2c"]
                     ELSE /\ pc' = [pc EXCEPT ![self] = "pop3"]
               /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                               local_myhead_, local_myhead, reg_next, elt_, 
                               my_set, myelt, init_thread, iterations >>

pop2c(self) == /\ pc[self] = "pop2c"
               /\ pc' = [pc EXCEPT ![self] = "tryAgainPop"]
               /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                               local_myhead_, local_myhead, reg_next, elt_, 
                               my_set, myelt, init_thread, iterations >>

pop3(self) == /\ pc[self] = "pop3"
              /\ elt_' = [elt_ EXCEPT ![self] = local_myhead[self]]
              /\ Assert(address[elt_'[self]].onStack = TRUE, 
                        "Failure of assertion at line 92, column 4.")
              /\ address' = [address EXCEPT ![elt_'[self]].onStack = FALSE]
              /\ retVal' = [retVal EXCEPT ![self] = elt_'[self]]
              /\ pc' = [pc EXCEPT ![self] = "endPop"]
              /\ UNCHANGED << initialized, HEAD, stack, elt, local_myhead_, 
                              local_myhead, reg_next, my_set, myelt, 
                              init_thread, iterations >>

endPop(self) == /\ pc[self] = "endPop"
                /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
                /\ local_myhead' = [local_myhead EXCEPT ![self] = Head(stack[self]).local_myhead]
                /\ reg_next' = [reg_next EXCEPT ![self] = Head(stack[self]).reg_next]
                /\ elt_' = [elt_ EXCEPT ![self] = Head(stack[self]).elt_]
                /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
                /\ UNCHANGED << retVal, address, initialized, HEAD, elt, 
                                local_myhead_, my_set, myelt, init_thread, 
                                iterations >>

popStack(self) == tryAgainPop(self) \/ pop1a(self) \/ pop2(self)
                     \/ pop2a(self) \/ pop2b(self) \/ pop2c(self)
                     \/ pop3(self) \/ endPop(self)

init0(self) == /\ pc[self] = "init0"
               /\ IF self = 1
                     THEN /\ iterations' = [iterations EXCEPT ![self] = MAX_ITER_THR_A]
                     ELSE /\ iterations' = [iterations EXCEPT ![self] = MAX_ITER_THR_B]
               /\ pc' = [pc EXCEPT ![self] = "init1"]
               /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                               local_myhead_, local_myhead, reg_next, elt_, 
                               my_set, myelt, init_thread >>

init1(self) == /\ pc[self] = "init1"
               /\ init_thread' = [init_thread EXCEPT ![self] = CHOOSE thr \in 1..NUM_THREADS : TRUE]
               /\ IF self = init_thread'[self]
                     THEN /\ HEAD' = 0
                          /\ pc' = [pc EXCEPT ![self] = "init5"]
                     ELSE /\ pc' = [pc EXCEPT ![self] = "init9"]
                          /\ HEAD' = HEAD
               /\ UNCHANGED << retVal, address, initialized, stack, elt, 
                               local_myhead_, local_myhead, reg_next, elt_, 
                               my_set, myelt, iterations >>

init5(self) == /\ pc[self] = "init5"
               /\ IF HEAD < MAX_STACK_SIZE
                     THEN /\ address' = [address EXCEPT ![HEAD+1] = [ next |-> HEAD, onStack |-> TRUE, data |-> 1 ]]
                          /\ HEAD' = HEAD+1
                          /\ pc' = [pc EXCEPT ![self] = "init5"]
                          /\ UNCHANGED initialized
                     ELSE /\ initialized' = TRUE
                          /\ pc' = [pc EXCEPT ![self] = "init9"]
                          /\ UNCHANGED << address, HEAD >>
               /\ UNCHANGED << retVal, stack, elt, local_myhead_, local_myhead, 
                               reg_next, elt_, my_set, myelt, init_thread, 
                               iterations >>

init9(self) == /\ pc[self] = "init9"
               /\ initialized
               /\ pc' = [pc EXCEPT ![self] = "th1"]
               /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                               local_myhead_, local_myhead, reg_next, elt_, 
                               my_set, myelt, init_thread, iterations >>

th1(self) == /\ pc[self] = "th1"
             /\ IF iterations[self] > 0
                   THEN /\ pc' = [pc EXCEPT ![self] = "th2"]
                   ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
             /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                             local_myhead_, local_myhead, reg_next, elt_, 
                             my_set, myelt, init_thread, iterations >>

th2(self) == /\ pc[self] = "th2"
             /\ \/ /\ IF my_set[self] /= {}
                         THEN /\ pc' = [pc EXCEPT ![self] = "th2a"]
                         ELSE /\ pc' = [pc EXCEPT ![self] = "th4"]
                \/ /\ pc' = [pc EXCEPT ![self] = "th3a"]
             /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                             local_myhead_, local_myhead, reg_next, elt_, 
                             my_set, myelt, init_thread, iterations >>

th2a(self) == /\ pc[self] = "th2a"
              /\ \E tmp \in my_set[self]:
                   myelt' = [myelt EXCEPT ![self] = tmp]
              /\ my_set' = [my_set EXCEPT ![self] = my_set[self] \ {myelt'[self]}]
              /\ /\ elt' = [elt EXCEPT ![self] = myelt'[self]]
                 /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "pushStack",
                                                          pc        |->  "th4",
                                                          local_myhead_ |->  local_myhead_[self],
                                                          elt       |->  elt[self] ] >>
                                                      \o stack[self]]
              /\ local_myhead_' = [local_myhead_ EXCEPT ![self] = defaultInitValue]
              /\ pc' = [pc EXCEPT ![self] = "push1"]
              /\ UNCHANGED << retVal, address, initialized, HEAD, local_myhead, 
                              reg_next, elt_, init_thread, iterations >>

th3a(self) == /\ pc[self] = "th3a"
              /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "popStack",
                                                       pc        |->  "th3b",
                                                       local_myhead |->  local_myhead[self],
                                                       reg_next  |->  reg_next[self],
                                                       elt_      |->  elt_[self] ] >>
                                                   \o stack[self]]
              /\ local_myhead' = [local_myhead EXCEPT ![self] = defaultInitValue]
              /\ reg_next' = [reg_next EXCEPT ![self] = defaultInitValue]
              /\ elt_' = [elt_ EXCEPT ![self] = defaultInitValue]
              /\ pc' = [pc EXCEPT ![self] = "tryAgainPop"]
              /\ UNCHANGED << retVal, address, initialized, HEAD, elt, 
                              local_myhead_, my_set, myelt, init_thread, 
                              iterations >>

th3b(self) == /\ pc[self] = "th3b"
              /\ IF retVal[self] /= NULL
                    THEN /\ pc' = [pc EXCEPT ![self] = "th3c"]
                    ELSE /\ pc' = [pc EXCEPT ![self] = "th4"]
              /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                              local_myhead_, local_myhead, reg_next, elt_, 
                              my_set, myelt, init_thread, iterations >>

th3c(self) == /\ pc[self] = "th3c"
              /\ my_set' = [my_set EXCEPT ![self] = my_set[self] \cup { retVal[self] }]
              /\ pc' = [pc EXCEPT ![self] = "th4"]
              /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                              local_myhead_, local_myhead, reg_next, elt_, 
                              myelt, init_thread, iterations >>

th4(self) == /\ pc[self] = "th4"
             /\ iterations' = [iterations EXCEPT ![self] = iterations[self] - 1]
             /\ PrintT(iterations'[self])
             /\ pc' = [pc EXCEPT ![self] = "th1"]
             /\ UNCHANGED << retVal, address, initialized, HEAD, stack, elt, 
                             local_myhead_, local_myhead, reg_next, elt_, 
                             my_set, myelt, init_thread >>

thread(self) == init0(self) \/ init1(self) \/ init5(self) \/ init9(self)
                   \/ th1(self) \/ th2(self) \/ th2a(self) \/ th3a(self)
                   \/ th3b(self) \/ th3c(self) \/ th4(self)

Next == (\E self \in ProcSet: pushStack(self) \/ popStack(self))
           \/ (\E self \in 1..NUM_THREADS: thread(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION
=============================================================================
\* Modification History
\* Last modified Thu Apr 11 14:39:27 EDT 2019 by gene
\* Last modified Sun Oct 22 06:26:25 EDT 2017 by celestekostopulos-cooperman
\* Created Fri Oct 20 22:08:53 EDT 2017 by celestekostopulos-cooperman