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

   CIVL model of class LazyList from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 9.7, "Lazy synchronization", and companion code
   ch9/src/lists/LazyList.java.

   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;
  bool marked;
  Lock lock;
} * Node;

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

static Node node_create_sentinel(T key) {
  Node this = malloc(sizeof(struct Node));
  this->item = -1; // null
  this->key = key;
  this->next = NULL;
  this->marked = false;
  this->lock = Lock_create();
  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);
}

// Sets...

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;
}

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

static bool validate(Set this, Node pred, Node curr) {
  return !pred->marked && !curr->marked && pred->next == curr;
}

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

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

bool Set_contains(Set this, T item) {
  int key = hash_code(item);
  Node curr = this->head;
  while (curr->key < key)
    curr = curr->next;
  return curr->key == key && !curr->marked;
}

#ifdef _LAZY_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();
}

static void test1(Set list, int N) {
  startup(list, N);
  $parfor(int i: 0 .. N-1) {
    tid_register(i);
    Set_add(list, i);
    Set_terminate(i);
    tid_unregister();
  }
  Set_print(list);
  $print("\n");
  shutdown(list);

  startup(list, N);
  $parfor(int i: 0 .. N-1) {
    tid_register(i);
    $assert(Set_contains(list, i));
    Set_terminate(i);
    tid_unregister();
  }
  shutdown(list);
}

static void test2(Set list, int N) {
  startup(list, N);
  $parfor (int i: 0 .. N-1) {
    tid_register(i);
    int result = Set_add(list, i);
    $assert(result);
    result = Set_contains(list, i);
    $assert(result);
    result = Set_remove(list, i);
    $assert(result);
    result = Set_contains(list, i);
    $assert(!result);
    tid_unregister();
  }
  shutdown(list);
}

void main() {
  Set list = Set_create();
  int test = 1+$choose_int(2);
  $print("\n*** Starting test ", test, " ***\n");
  if (test == 1)
    test1(list, 3);
  else
    test2(list, 2);
  Set_destroy(list);
  $print("Test ", test, " complete.\n");
}
#endif