/* Filename : FineList.cvl
   Authors  : ZZZ, WWW, YYY, XXX
   Created  : 2018-05-01
   Modified : 2025-01-17

   CIVL model of class FineList, from "The Art of Multiprocessor
   Programming", 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 9.5 "Fine-Grained Synchronization" and companion code
   ch9/src/lists/FineList.java.
  
   This is a concurrent fine grained list using one lock per node.
  
   some Lab
   some division
   some institution
 */
#include "Lock.h"
#include "Set.h"
#include "hash.cvh"
#include "tid.h"
#include "types.h"
#include <limits.h>
#include <stdbool.h>
#include <stdlib.h>

// Nodes...

typedef struct Node {
  T item;
  int key;
  struct Node * next;
  Lock lock;
} * Node;

static Node node_create(T item) {
  Node this = malloc(sizeof(struct Node));
  this->item = item;
  this->key = hash_code(item);
  this->lock = Lock_create();
  this->next = NULL;
  return this;
}

static Node node_create_sentinel(int key) {
  Node this = malloc(sizeof(struct Node));
  this->key = key;
  this->item = -1; // null
  this->lock = Lock_create();
  this->next = NULL;
  return this;
}

static void node_destroy(Node node) {
  Lock_destroy(node->lock);
  free(node);
}

static void node_destroy_rec(Node node) {
  if (node == NULL) return;
  node_destroy_rec(node->next);
  node_destroy(node);
}

// Set...

struct Set {
  Node head;
};

Set Set_create() {
  Set this = malloc(sizeof(struct Set));
  this->head = node_create_sentinel(INT_MIN);
  this->head->next = node_create_sentinel(INT_MAX);
  return this;
}

void Set_destroy(Set list) {
  node_destroy_rec(list->head);
  free(list);
}

void Set_initialize_context(void) {}

void Set_finalize_context(void) {}

void Set_initialize(Set set) {}

void Set_finalize(Set set) {}

void Set_terminate(int tid) {}

bool Set_stuck(void) {
  return false;
}

bool Set_add(Set this, T item) {
  int key = hash_code(item);
  Lock_acquire(this->head->lock);
  Node pred = this->head;
  // try...
  Node curr = pred->next;
  Lock_acquire(curr->lock);
  // try...
  while (curr->key < key) {
    Lock_release(pred->lock);
    pred = curr;
    curr = curr->next;
    Lock_acquire(curr->lock);
  }
  if (curr->key == key) {
    Lock_release(curr->lock); // finally
    Lock_release(pred->lock); // finally
    return false;
  }
  Node node = node_create(item);
  node->next = curr;
  pred->next = node;
  Lock_release(curr->lock); // finally
  Lock_release(pred->lock); // finally
  return true;
}

bool Set_remove(Set this, T item) {
  int key = hash_code(item);
  Lock_acquire(this->head->lock);
  Node pred = this->head;
  // try...
  Node curr = pred->next;
  Lock_acquire(curr->lock);
  // try...
  while (curr->key < key) {
    Lock_release(pred->lock);
    pred = curr;
    curr = curr->next;
    Lock_acquire(curr->lock);
  }
  if (curr->key == key) {
    pred->next = curr->next;
    Lock_release(curr->lock); // finally
    Lock_release(pred->lock); // finally
    node_destroy(curr); // not in original, but seems to work fine
    return true;
  }
  Lock_release(curr->lock); // finally
  Lock_release(pred->lock); // finally
  return false;
}

// this method from companion code...
bool Set_contains(Set this, T item) {
  // companion code contains unused variable last
  Node pred = NULL, curr = NULL;
  int key = hash_code(item);
  Lock_acquire(this->head->lock);
  // try...
  pred = this->head;
  curr = pred->next;
  Lock_acquire(curr->lock);
  // try...
  while (curr->key < key) {
    Lock_release(pred->lock);
    pred = curr;
    curr = curr->next;
    Lock_acquire(curr->lock);
  }
  bool result = (curr->key == key);
  Lock_release(curr->lock); // finally
  Lock_release(pred->lock); // finally
  return result;
}

void Set_print(Set this) {
  Node curr = this->head->next;
  $print("{ ");
  while (curr->next != NULL) {
    $print(curr->item, " ");
    curr = curr->next;
  }
  $print("}");
}

#ifdef _FINE_LIST_MAIN

static void startup(Set s, int nproc) {
  tid_init(nproc);
  Set_initialize_context();
  Set_initialize(s);
}

static void shutdown(Set s) {
  Set_finalize(s);
  Set_finalize_context();
  tid_finalize();
}

void main() {
  Set list = Set_create();
  startup(list, 3);
  $parfor(int i : 0 .. 2) {
    tid_register(i);
    Set_add(list, i);
    Set_terminate(i);
    tid_unregister();
  }
  Set_print(list);
  $print("\n");
  $for(int j : 0 .. 2)
    $assert(Set_contains(list, j));
  shutdown(list);

  startup(list, 3);
  $parfor(int i : 0 .. 2) {
    tid_register(i);
    Set_remove(list, i);
    Set_terminate(i);
    tid_unregister();
  }
  shutdown(list);

  startup(list, 1);
  tid_register(0);
  $for(int j : 0 .. 2) {
    $assert(!Set_contains(list, j));
  }
  Set_terminate(0);
  tid_unregister();
  shutdown(list);
  
  Set_print(list);
  $print("\n");
  Set_destroy(list);
}
#endif