/* Filename : SynchronousQueue.cvl
   Authors  : YYY and XXX
   Created  : 2024-11-04
   Modified : 2025-01-17

   CIVL model of SynchronousQueue class from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 10.6.1 "A naive synchronous queue", and companion code
   ch10/Queue/src/queue/SynchronousQueue.java.
  
   This is a simple model of the SynchronousQueue class, which is a
   simple blocking synchronized queue with a single item field.
  
   some Lab
   some division
   some institution
 */
#include "Condition_dl.h"
#include "Lock.h"
#include "Queue.h"
#include "tid.h"
#include "types.h"
#include <stdbool.h>
#include <stdlib.h>

struct Queue {
  T item;
  bool enqueueing;
  Lock lock;
  Condition condition;
};

Queue Queue_create() {
  Queue q = (Queue)malloc(sizeof(struct Queue));
  q->item = -1;
  q->enqueueing = false;
  q->lock = Lock_create();
  q->condition = Condition_create(q->lock);
  return q;
}

// not in original code...
void Queue_destroy(Queue q) {
  Lock_destroy(q->lock);
  Condition_destroy(q->condition);
  free(q);
}

void Queue_initialize_context(void) {
  Condition_init_context();
}

void Queue_finalize_context(void) {
  Condition_finalize_context();
}

void Queue_initialize(Queue queue) {
  Condition_initialize(queue->condition);
}

void Queue_finalize(Queue queue) {
  Condition_finalize(queue->condition);
}

void Queue_terminate(int tid) {
  Condition_terminate(tid);
}

bool Queue_stuck() {
  return Condition_isDeadlocked();
}

T Queue_deq(Queue q) {
  Lock_acquire(q->lock);
  // try
  while (q->item == -1) {
    Condition_await(q->condition);
    if (Condition_isDeadlocked()) {
      Lock_release(q->lock);
      return -1;
    }
  }
  T t = q->item;
  q->item = -1;
  Condition_signalAll(q->condition);
  // finally
  Lock_release(q->lock);
  return t;
}

void Queue_enq(Queue q, T value) {
  Lock_acquire(q->lock);
  // try
  while (q->enqueueing) {
    Condition_await(q->condition);
    if (Condition_isDeadlocked()) {
      Lock_release(q->lock);
      return;
    }
  }
  q->enqueueing = true;
  q->item = value;
  Condition_signalAll(q->condition);
  while (q->item != -1) {
    Condition_await(q->condition);
    if (Condition_isDeadlocked()) {
      Lock_release(q->lock);
      return;
    }
  }
  q->enqueueing = false;
  Condition_signalAll(q->condition);
  // finally
  Lock_release(q->lock);
}

void Queue_print(Queue this) {
  $print("{ ");
  if (this->item >= 0)
    $print(this->item, " ");
  $print("}");
}

// Tests ...

#ifdef _SYNC_QUEUE_MAIN

static void startup(Queue q, int nproc) {
  tid_init(nproc);
  Queue_initialize_context();
  Queue_initialize(q);
}

static void shutdown(Queue q) {
  Queue_finalize(q);
  Queue_finalize_context();
  tid_finalize();
}

/* 2N threads: even ones enqueue, odd ones dequeue.  Should never get
   stuck and should always result in an empty queue.  */
void testBalanced(Queue q, int N) {
  $assert(N>=1);
  int nthread=2*N;
  startup(q, nthread);
  $parfor (int i: 0..nthread-1) {
    tid_register(i);
    if (i%2 == 0)
      Queue_enq(q, i);
    else {
      int result = Queue_deq(q);
      $assert(result >= 0);
      $assert(result <= nthread-2 && result%2 == 0);
    }
    Queue_terminate(i);
    tid_unregister();
  }
  $print("Done: ");
  Queue_print(q);
  $print("\n");
  $assert(!Queue_stuck());
  $assert(q->item == -1); // q is empty
  shutdown(q);
}

/* All threads enqueue.  This should always get stuck. */
void testEnqs(Queue q, int nthread) {
  $assert(nthread >= 1);
  startup(q, nthread);
  $parfor (int i: 0..nthread-1) {
    tid_register(i);
    Queue_enq(q, i);
    Queue_terminate(i);
    tid_unregister();
  }
  $assert(Queue_stuck());
  shutdown(q);
}

/* Three threads: one enqueues, the other two dequeue.  Should get
   stuck. */
void testEDD(Queue q) {
  int nthread=3;
  startup(q, nthread);
  int ndeqdone = 0;
  $parfor (int i: 0..nthread-1) {
    tid_register(i);
    if (i==0) {
      Queue_enq(q, i);
      $assert(!Queue_stuck());
      Queue_terminate(i);
    } else {
      int x = Queue_deq(q);
      if (!Queue_stuck()) {
        ndeqdone++;
        $assert(ndeqdone <= 1);
        $assert(x >= 0);
        Queue_terminate(i);
      }
    }
    tid_unregister();
  }
  $assert(Queue_stuck());
  shutdown(q);
}

void testEED(Queue q) {
  int nthread=3;
  startup(q, nthread);
  int nenqdone = 0;
  $parfor (int i: 0..nthread-1) {
    tid_register(i);
    if (i<=1) {
      Queue_enq(q, i);
      if (!Queue_stuck()) {
        nenqdone++;
        $assert(nenqdone <= 1);
        Queue_terminate(i);
      }
    } else {
      int x = Queue_deq(q);
      $assert(x >= 0);
      $assert(!Queue_stuck());
      Queue_terminate(i);
    }
    tid_unregister();
  }
  $assert(Queue_stuck());
  shutdown(q);
}

int main(void) {
  Queue q = Queue_create();
  int test = $choose_int(6);
  switch (test) {
  case 0:
    testBalanced(q, 1);
    break;
  case 1:
    testBalanced(q, 2);
    break;
  case 2:
    testEnqs(q, 1);
    break;
  case 3:
    testEnqs(q, 2);
    break;
  case 4:
    testEDD(q);
    break;
  case 5:
    testEED(q);
    break;
  default:
    $assert(false);
  }
  Queue_destroy(q);
}
#endif