/* Filename : LockFreeQueue.cvl
   Authors  : YYY and XXX
   Created  : 2021-01-19
   Modified : 2025-01-17

   CIVL model of LockFreeQueue from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 10.5 "A lock-free unbounded queue", and companion code
   ch10/Queue/src/queue/LockFreeQueue.java.
  
   This is an unbounded queue implementation using lazy
   synchronization and no locks.  Where they differ, we follow the
   code from the book text, not the companion code.  This means no use
   of multiCompareAndSet.
  
   The original Java code relies on the garbage collector to reclaim
   memory.  By default, CIVL-C, like C, requires manual memory
   management.  Protocols for manually managing memory for this data
   structure are complicated and are described in Section 10.6 of the
   text.  We do not implement those here. Hence this CIVL model does
   leak memory.  Run CIVL in garbage collection model
   (-checkMemoryLeak=false) to ignore this issue.
  
   some Lab
   some division
   some institution
 */
#include "AtomicReference.cvh"
#include "Queue.h"
#include "tid.h"
#include "types.h"
#include <limits.h>
#include <stdbool.h>
#include <stdlib.h>

// Nodes...

typedef struct Node {
  T value;
  AtomicReference next;
} * Node;

static Node node_create(T value) {
  Node this = malloc(sizeof(struct Node));
  this->value = value;
  this->next = AtomicReference_create(NULL);
  return this;
}

// not in original code...
static void node_destroy(Node this) {
  AtomicReference_destroy(this->next);
  free(this);
}

// Queue...

struct Queue {
  AtomicReference head;
  AtomicReference tail;
};


Queue Queue_create() {
  Queue this = malloc(sizeof(struct Queue));
  Node node = node_create(-1); // new Node(null)
  this->head = AtomicReference_create(node);
  this->tail = AtomicReference_create(node);
  return this;
}

// not in original code...
void Queue_destroy(Queue queue) {
  // if node is not null, its next is not null
  Node curr = AtomicReference_get(queue->head);
  Node prev = NULL;
  while (curr != NULL) {
    prev = curr;
    curr = AtomicReference_get(curr->next);
    node_destroy(prev);
  }
  AtomicReference_destroy(queue->head);
  AtomicReference_destroy(queue->tail);
  free(queue);
}

void Queue_initialize_context(void) {}

void Queue_finalize_context(void) {}

void Queue_initialize(Queue queue) {}

void Queue_finalize(Queue queue) {}

void Queue_terminate(int tid) {}

bool Queue_stuck(void) {
  return false;
}

void Queue_enq(Queue this, T value) {
  Node node = node_create(value);
  while (true) {
    Node last = AtomicReference_get(this->tail);
    Node next = AtomicReference_get(last->next);
    // look at book Fig. 10.11, not companion code...
    if (last == AtomicReference_get(this->tail)) {
      if (next == NULL) {
        if (AtomicReference_compareAndSet(last->next, next, node)) {
          AtomicReference_compareAndSet(this->tail, last, node);
          return;
        }
      } else {
        AtomicReference_compareAndSet(this->tail, last, next);
      }
    }
  }
}

T Queue_deq(Queue this) {
  while (true) {
    Node first = AtomicReference_get(this->head);
    Node last = AtomicReference_get(this->tail);
    Node next = AtomicReference_get(first->next);
    if (first == AtomicReference_get(this->head)) {
      if (first == last) {
        if (next == NULL) {
          return -1; // throw new EmptyException
        }
        AtomicReference_compareAndSet(this->tail, last, next);
      } else {
        T value = next->value;
        if (AtomicReference_compareAndSet(this->head, first, next)) {
          return value;
        }
      }
    }
  }
}

void Queue_print(Queue queue) {
  Node curr = AtomicReference_get(queue->head);
  curr = AtomicReference_get(curr->next);
  $print("{ ");
  while (curr) {
    $print(curr->value, " ");
    curr = AtomicReference_get(curr->next);
  }
  $print("}\n");
  return;
}

#ifdef _LOCK_FREE_QUEUE_MAIN
int main() {
  Queue q = Queue_create();
  int n=3;
  tid_init(n);
  Queue_initialize_context();
  Queue_initialize(q);
  $parfor (int i: 0..2) {
    tid_register(i);
    Queue_enq(q, i);
    int x = Queue_deq(q);
    $assert(x >= 0);
    $assert(x < 3);
    Queue_terminate(i);
    tid_unregister();
  }
  Queue_finalize(q);
  Queue_finalize_context();
  tid_finalize();
  Queue_destroy(q);  
}
#endif