/*
  Filename : driver.cvl
  Author   : XXX and YYY
  Created  : 2024-12-13
  Modified : 2025-01-16

  Driver contains main function to be linked with a concurrent data
  structure implementation, oracle, and schedule.  It executes the
  schedule on the concurrent implementation and then checks there is a
  matching sequential execution using the oracle.  Matching means (1)
  the sequential execution is a linearization of the concurrent
  schedule, and (2) if checking linearizabilty, a match also requires
  the linearizabilty criterion: if e1 and e2 are calls in the
  concurrent execution and e1 ends (returns) before e2 begins
  (invokes), then e1 must occur before e2 in the sequential execution.

  By default, this driver will require linearizability for a
  concurrent execution to match a sequential one.  To drop this
  requirement, verify using -DNLINEAR.

  some Lab
  some division
  some institution
 */
#pragma CIVL ACSL
#include "collection.h"
#include "oracle.h"
#include "perm.h"
#include "schedule.h"
#include "tid.h"
#include "types.h"
#include <stdbool.h>
#include <stdlib.h>

/* Creates the schedule to be used by this driver.  May be
 * deterministic or nondeterministic. */
schedule_t make_schedule();

// Global Vars...
schedule_t schedule; // the schedule
int nthread; // number of threads
#ifndef NLINEAR
static int time = 0;
static bool status = 0; // 0=last event was a start. 1=last event was a stop
#endif

/*@ depends_on \nothing; */
static $atomic_f int get_nsteps(int tid) {
  return schedule.nsteps[tid];
}

/*@ depends_on \nothing; */
static $atomic_f step_t get_step(int tid, int s) {
  return schedule.steps[tid][s];
}

// Sets result and stop time.
// Exit earlier linearizable => exit later linearizable
/*@ depends_on \nothing; */
static $atomic_f void set_result(int tid, int s, int result) {
#ifndef NLINEAR
  if (status == 0) status = 1;
  schedule.steps[tid][s].stop_time = time;
#endif
  schedule.steps[tid][s].result = result;
}

#ifndef NLINEAR
/*@ depends_on \access(&time); */
static $atomic_f void set_start_time(int tid, int s) {
  if (status == 1) {
    status = 0;
    time++;
  }
  schedule.steps[tid][s].start_time = time;
}
#endif

static void printMatchFail(void * collection, int stuckID) {
  $print("[FAIL]\t No matching sequentialized execution");
  if (stuckID >= 0)
    $print(" ending with thread ", stuckID, " blocked");
  $print(" found!\n");
  $print("Collection final state... ");
  collection_print(collection);
  $print("\n");
}

static void printOpInfo(int tid, int op, int val, int score, int result) {
  $print("  Thread ", tid, ": ");
  $print((op==ADD?"ADD":(op==REMOVE?"REMOVE":"CONTAINS")));
  if (val >= 0) {
    $print("(", val);
    if (score >= 0) $print(",", score, ")");
    else $print(")");
  }
  $print(" -> ");
  if (result != UNDEF) $print(result); else $print("STUCK");
  $print("\n");
}

static void printEquivSeqInfo(int nstep, int * perms, void * oracle,
                              int stuckID) {
  int nthread = schedule.nthread;
  int step_counters[nthread];
  for (int tid = 0; tid < nthread; tid++)
    step_counters[tid] = 0;
  $print("[PASS]\t Linearized execution:\n");
  for (int step_id = 0; step_id < nstep; step_id++) {
    int tid = perms[step_id];
    int step_local = step_counters[tid];
    step_t step = schedule.steps[tid][step_local];
    printOpInfo(tid, step.op, step.args[0], step.args[1], step.result);
    step_counters[tid]++;
  }
  if (stuckID >= 0) {
    int step_local = step_counters[stuckID];
    step_t step = schedule.steps[stuckID][step_local];
    printOpInfo(stuckID, step.op, step.args[0], step.args[1], step.result);
  }
  $print("Oracle final state....... ");
  oracle_print(oracle);
  $print("\n\n");
}

/* Determines whether the sequentialization of the schedule specified
   by perm matches the results of the concurrent execution.  The
   results of the concurrent execution are recorded in the schedule
   (before this function is called).  This function works for both
   normal executions (in which every thread completes all of its steps
   and terminates normally) and stuck executions, which end in
   deadlock.
  
   nstep: the total number of steps in the execution.  This is at most
   schedule.nstep.  Note: nstep does not include preAdds.
  
   perm: array of length nstep. perm[i] is the ID of the thread that
   executes step i in the linear sequence of steps.  Hence perm,
   together with global variable schedule, specifies a single
   sequentialization of the concurrent execution.
  
   oracle: the simple trusted sequential implementation of the data
   structure.  The sequentialized execution will be executed on this
   oracle.  Note that oracle may be nonempty when this function is
   called due to preAdds.
  
   stuckID: for a normal execution, this is -1.  For a stuck
   execution, this is the ID of the thread that got stuck in its last
   step: it called, but never returned from, a method.  This last
   incomplete step is the step just after the nstep steps of the
   schedule have been executed.  For a sequential execution to match,
   thread stuckID must have this next step disabled in the oracle.
 */
static bool permseq(int nstep, int * perm, void * oracle, int stuckID) {
  bool stuck = stuckID >= 0;
  if (oracle_trapped(oracle, stuck))
    return false; // might already been trapped due to pre-adds
  int nthread = schedule.nthread, step_counters[nthread];
  for (int tid = 0; tid < nthread; tid++)
    step_counters[tid] = 0;
  for (int step_seq = 0; step_seq < nstep; step_seq++) {
    int tid = perm[step_seq], step_id = step_counters[tid];
    step_t step = schedule.steps[tid][step_id];
    $assert(step.result != UNDEF);
    int op = step.op, a0 = step.args[0], a1 = step.args[1], result;
    if (op == ADD)
      result = (int)oracle_add(oracle, a0, a1);
    else if (op == REMOVE)
      // for a priority queue, you want to specify the value to
      // remove, which is not the argument a0, but the result.
      result = oracle_remove(oracle, a0, step.result);
    else if (op == CONTAINS)
      result = (int)oracle_contains(oracle, a0);
    else
      $assert(false);
    step_counters[tid]++;
    if (result != step.result || oracle_trapped(oracle, stuck))
      return false;
  }
  if (stuck) {
    // the next call from thread stuckID should make the oracle stuck.
    // the result can be ignored.
    int step_id = step_counters[stuckID];
    step_t step = schedule.steps[stuckID][step_id];
    $assert(step.result == UNDEF);
    int op = step.op, a0 = step.args[0], a1 = step.args[1];
    if (op == ADD)
      oracle_add(oracle, a0, a1);
    else if (op == REMOVE)
      oracle_remove(oracle, a0, -1); // don't specify expected value
    else if (op == CONTAINS)
      oracle_contains(oracle, a0);
    else $assert(false);
  }
  return oracle_accepting(oracle, stuck);
}

/* The code executed by one thread in the concurrent execution.  tid
   is the thread's ID number; c is a pointer to the concurrent data
   structure upon which it will act.  The thread will execute the
   sequence of steps specified in the schedule for the given ID. */
static void thread(int tid, void * c) {
  tid_register(tid);
  int num_steps_local = get_nsteps(tid);
  for (int s = 0; s < num_steps_local; s++) {
    step_t step = get_step(tid, s);
    int op = step.op, a0 = step.args[0], a1 = step.args[1];
#ifndef NLINEAR
    set_start_time(tid, s);
#endif
    if (op == ADD)
      step.result = (int)collection_add(c, a0, a1);
    else if (op == REMOVE)
      step.result = collection_remove(c, a0);
    else if (op == CONTAINS)
      step.result = (int)collection_contains(c, a0);
    else
      $assert(false);
    // if the operation above did not get stuck, then
    // collection_stuck() cannot return true, no matter what other
    // threads do now, because this thread hasn't terminated.  if the
    // operation above did get stuck then collection_stuck() must
    // return true, no matter what other threads do, because once
    // stuck becomes true it must remain true.
    if (collection_stuck()) {
      $print("Deadlock: thread ", tid, " exiting at step ", s, "\n");
      break;
    }
    set_result(tid, s, step.result);
  }
  if (!collection_stuck()) collection_terminate(tid);
  tid_unregister();
}

static bool match(void * collection, int nstep, int num_perms,
                   int ** perms, int stuckID) {
  void * oracle = NULL;
  int perm_id = 0;
  $print("numPerms=", num_perms, "\n");
  for (; perm_id < num_perms; perm_id++) {
    // check if this perm has been filtered out as non-linearizable
    // note: if nstep=1, the linearizability condition holds vacuously
    if (nstep > 1 && perms[perm_id][0] < 0) continue;
    oracle = oracle_create();
    for (int i=0; i<schedule.npreAdd; i++)
      oracle_add(oracle, schedule.preAdds[i].args[0],
                 schedule.preAdds[i].args[1]);
    if (permseq(nstep, perms[perm_id], oracle, stuckID))
      break; // match found
    oracle_destroy(oracle);
    oracle = NULL;
  }
  if (oracle) { // match found
    printEquivSeqInfo(nstep, perms[perm_id], oracle, stuckID);
    oracle_destroy(oracle);
    return $true;
  } else { // no match found
    printMatchFail(collection, stuckID);
    schedule_print(schedule);
    perm_print_all(num_perms, nstep, perms);
    $print("\n");
    return $false;
  }
}

static int ** compute_perms(int * counts) {
#ifdef NLINEAR
  return perm_compute(nthread, counts);
#else
  return perm_compute_linear(schedule, counts);
#endif
}

static void find_match_normal(void * collection) {
  int * counts = schedule.nsteps, nstep = schedule.nstep;
  int num_perms = perm_calc_num(nthread, counts);
  int ** perms = compute_perms(counts);
  $assert(match(collection, nstep, num_perms, perms, -1));
  for (int i = 0; i < num_perms; i++) free(perms[i]);
  free(perms);
}

static void find_match_stuck(void * collection) {
  int counts[nthread]; // number of completed steps in each thread
  int nstep = 0; // total number of completed steps (sum of counts[])
  for (int i=0; i<nthread; i++) {
    int j = 0, stop = schedule.nsteps[i];
    for (; j<stop && schedule.steps[i][j].result != UNDEF; j++) ;
    counts[i] = j;
    nstep += j;
  }
  int num_perms = perm_calc_num(nthread, counts);
  int ** perms = compute_perms(counts);
  for (int tid=0; tid<nthread; tid++) {
    if (counts[tid] != schedule.nsteps[tid]) // tid got stuck
      $assert(match(collection, nstep, num_perms, perms, tid));
  }
  for (int i = 0; i < num_perms; i++) free(perms[i]);
  free(perms);
}

//@ depends_on(\nothing);
$atomic_f static void startup(void * collection, int nthread) {
  tid_init(nthread);
  collection_initialize_context();
  collection_initialize(collection);
}

//@ depends_on(\nothing);
$atomic_f static void shutdown(void * collection) {
  collection_finalize(collection);
  collection_finalize_context();
  tid_finalize();
}

int main() {
  void * collection = collection_create();
  schedule = make_schedule();
  schedule_print(schedule);
  nthread = schedule.nthread;

  // Perform pre-adds:
  if (schedule.npreAdd > 0) {
    startup(collection, 1);
    tid_register(0);
    for (int i=0; i<schedule.npreAdd; i++) {
      collection_add(collection, schedule.preAdds[i].args[0],
                     schedule.preAdds[i].args[1]);
      $assert(!collection_stuck(), "Collection got stuck during pre-adds!\n");
    }
    collection_terminate(0);
    tid_unregister();
    shutdown(collection);
  }

  // run concurrent schedule with nthread threads:
  $print("Collection initial state. ");
  collection_print(collection);
  $print("\n");
  startup(collection, nthread);
  $parfor (int tid : 0 .. nthread-1) {
    thread(tid, collection);
  }
  bool deadlock = collection_stuck();
  shutdown(collection);
  schedule_print(schedule);
  $print("Collection final state... ");
  collection_print(collection);
  $print("\n");
  if (deadlock)
    find_match_stuck(collection);
  else 
    find_match_normal(collection);
  collection_destroy(collection);
  schedule_destroy(schedule);
}