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

   CIVL model of UnboundedQueue class from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 10.4 "An unbounded total queue", and companion code
   ch10/Queue/src/queue/UnboundedQueue.java.
  
   This is a simple unbounded queue implementation using two locks.
  
   some Lab
   some division
   some institution
 */
#include "Lock.h"
#include "Queue.h"
#include "tid.h"
#include "types.h"
#include <limits.h>
#include <stdbool.h>
#include <stdlib.h>

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

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

static void node_destroy(Node node) {
  free(node);
}

struct Queue {
  Lock enqLock;
  Lock deqLock;
  Node head;
  Node tail;
};

Queue Queue_create() {
  Queue this = malloc(sizeof(struct Queue));
  this->head = node_create(-1);
  this->tail = this->head;
  this->enqLock = Lock_create();
  this->deqLock = Lock_create();
  return this;
}

// not in original code...
void Queue_destroy(Queue queue) {
  Node curr = queue->head;
  while (curr) {
    Node temp = curr;
    curr = curr->next;
    node_destroy(temp);
  }
  Lock_destroy(queue->enqLock);
  Lock_destroy(queue->deqLock);
  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 x) {
  Node e = node_create(x);
  Lock_acquire(this->enqLock);
  // try...
  // $print("Thread ", tid_get(), " is enqueing ", x, "\n");
  this->tail->next = e;
  this->tail = e;
  // finally...
  Lock_release(this->enqLock);
}

T Queue_deq(Queue this) {
  T result;
  Lock_acquire(this->deqLock);
  // try...
  if (this->head->next == NULL) {
    Lock_release(this->deqLock);  // finally
    return -1; // throw new EmptyException()
  }
  result = this->head->next->value;
  Node old_head = this->head;
  this->head = old_head->next;
  node_destroy(old_head);
  Lock_release(this->deqLock); // finally
  return result;
}

// not in original code...
void Queue_print(Queue this) {
  Node curr = this->head->next;
  $print("{ ");
  while (curr) {
    $print(curr->value, " ");
    curr = curr->next;
  }
  $print("}");
}

#ifdef _UNBOUNDED_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);
    //$print("Thread ", i, " dequeued ", x, "\n");
    $assert(x >= 0);
    $assert(x < 3);
    Queue_terminate(i);
    tid_unregister();
  }
  Queue_finalize(q);
  Queue_finalize_context();
  tid_finalize();
  //$print("Done.\n");
  Queue_destroy(q);  
}
#endif