/* 
   Filename : Condition_dl.cvl
   Authors  : XXX and YYY
   Created  : 2024-02-26
   Modified : 2025-01-17

   Model of Java Condition interface (condition variable) that also
   detects deadlock.  When a deadlock occurs due to all nonterminated
   threads being blocked in an await call, this implementation
   releases all threads and sets a deadlock flag.  The client can
   check the deadlock flag immediately after each call to await and
   take appropriate action if a deadlock occurs.  Appropriate action
   might mean releasing the lock(s) held and returning immediately.

   some Lab
   some division
   some institution
*/
#pragma CIVL ACSL
#include "Condition_dl.h"
#include "Lock.h"
#include "seq.cvh"
#include "tid.h"
#include <stdbool.h>
#include <stdlib.h>

/* A Condition object */
struct Condition {
  Lock lock;
  bool * inWaitingRoom;
  int nwait; // number of threads in the waiting room
};

// The condition context: applies to all Condition objects...

static int nthread = -1;
static Condition stuckConds[]; // length nthread
static _Bool terminated[]; // length nthread
static int nstuck = 0; // number of nonterminated stuck threads
static int num_nonterm = 0; // number of nonterminated threads
static _Bool deadlock = false;

/* Call this first to create a new Condition object, before the
   threads are created or even known, and before the context has been
   initialized. */
Condition Condition_create(Lock lock) {
  $assert(nthread == -1);
  Condition result = malloc(sizeof(struct Condition));
  result->lock = lock;
  result->inWaitingRoom = NULL;
  result->nwait = 0;
  return result;
}

/* Call this last, after all threads have terminated, the Condition
   was finalized, and the context was finalized. */
void Condition_destroy(Condition cond) {
  free(cond);
}

/* Call this after the Conditions have been created and
   tid_init(nthread) has been called.  The threads do not yet need to
   exist. */
void Condition_init_context() {
  $assert(nthread == -1);
  nthread = tid_nthread();
  $assert(nthread >= 1, "Must call tid_init(nthread) first.");
  Condition c = NULL;
  $seq_init(&stuckConds, nthread, &c);
  _Bool b = false;
  $seq_init(&terminated, nthread, &b);
  nstuck = 0;
  num_nonterm = nthread;
  deadlock = false;
}

void Condition_finalize_context() {
  $seq_init(&stuckConds, 0, NULL);
  $seq_init(&terminated, 0, NULL);
  nthread = -1;
  nstuck = 0;
  num_nonterm = 0;
  deadlock = false;
}

/* Called after Condition has been created and context has been
   initialized. */
void Condition_initialize(Condition cond) {
  $assert(nthread >= 1);
  cond->inWaitingRoom = malloc(nthread*sizeof(bool));
  for (int i=0; i<nthread; i++)
    cond->inWaitingRoom[i] = false;
  cond->nwait = 0;
}

void Condition_finalize(Condition cond) {
  free(cond->inWaitingRoom);
  cond->nwait = 0;
}

/* Removes all threads from waiting room for cond. */
static $atomic_f void releaseAllStuck(Condition cond) {
  for (int i=0; i<nthread; i++)
    cond->inWaitingRoom[i] = false;
  cond->nwait = 0;
}

/* Marks the given thread as no longer stuck in any waiting room. */
static void release(int tid) {
  $assert(stuckConds[tid] != NULL);
  stuckConds[tid] = NULL;
  nstuck--;
}

void Condition_terminate(int tid) {
  $assert(!terminated[tid]);
  terminated[tid] = $true;
  num_nonterm--;
  if (nstuck == num_nonterm && nstuck >= 1) { // deadlock!
    deadlock = $true;
    for (int i=0; i<nthread; i++) {
      if (!terminated[i])
        releaseAllStuck(stuckConds[i]);
    }
  }
}

bool Condition_isDeadlocked() {
  return deadlock;
}

static bool awaiting(Condition cond, int tid) {
  $assert(stuckConds[tid] == NULL);
  stuckConds[tid] = cond;
  nstuck++;
  if (nstuck == num_nonterm) { // deadlock!
    deadlock = true;
    for (int i=0; i<nthread; i++) {
      if (!terminated[i])
        releaseAllStuck(stuckConds[i]);
    }
    return true;
  }
  return false;  
}

/*@ depends_on \nothing; */
static $atomic_f void wait1(Condition cond, int tid) {
  $assert(Lock_isHeldByCurrentThread(cond->lock));
  cond->inWaitingRoom[tid] = true;
  if (awaiting(cond, tid)) {
    // deadlock occurred. everyone was released
    Lock_release(cond->lock);
    return;
  }
  Lock_release(cond->lock);
  cond->nwait++;
}

// Leave the waiting room once signaled
/*@ depends_on \nothing; */
static $atomic_f void wait2(Condition cond, int tid) {
  $when(!cond->inWaitingRoom[tid]);
}

void Condition_await(Condition cond) {
  int tid = tid_get();
  wait1(cond, tid);
  wait2(cond, tid);
  Lock_acquire(cond->lock);
}

/*@ depends_on \access(cond); */
$atomic_f void Condition_signal(Condition cond) {
  int tid = tid_get();
  $assert(Lock_isHeldByCurrentThread(cond->lock));
  if (cond->nwait == 0) return;
  int c = $choose_int(cond->nwait); // choose c in 0..nwait-1
  for (int i=0; i<nthread; i++) {
    if (cond->inWaitingRoom[i]) {
      if (c == 0) {
        cond->inWaitingRoom[i] = false;
        release(i);
        cond->nwait--;
        return;
      }
      c--;
    }
  }
}

/*@ depends_on \access(cond); */
$atomic_f void Condition_signalAll(Condition cond) {
  int tid = tid_get();
  $assert(Lock_isHeldByCurrentThread(cond->lock));
  for (int i=0; i<nthread; i++) {
    if (cond->inWaitingRoom[i]) {
      cond->inWaitingRoom[i] = false;
      release(i);
      cond->nwait--;
    }
  }
}