/* Filename : LockFreeList.cvl
   Authors  : YYY and XXX
   Created  : 2021-06-30
   Modified : 2025-01-17

   CIVL model of class LockFreeList from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 9.8, "Nonblocking synchronization", and companion code
   ch9/src/lists/LockFreeList.java.
  
   This is a concurrent list-based set using lock-free
   synchronization.  It leaks memory (the original code relies on the
   Java garbage collector), so should be verified in garbage
   collection mode (-checkMemoryLeak=false).
  
   some Lab
   some division
   some institution
 */
#include "AtomicMarkableReference.cvh"
#include "Set.h"
#include "hash.cvh"
#include "tid.h"
#include "types.h"
#include <limits.h>
#include <stdbool.h>
#include <stdlib.h>

// Types...

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

struct Set {
  Node head;
};

typedef struct Window {
  Node pred;
  Node curr;
} Window;

// Functions...

static Node node_create(T item) {
  Node result = malloc(sizeof(struct Node));
  result->key = hash_code(item);
  result->item = item;
  result->next = AtomicMarkableReference_create(NULL, false);
  return result;
}

static Node sentinel_node_create(int key) {
  Node result = malloc(sizeof(struct Node));
  result->key = key;
  result->item = -1; // null
  result->next = AtomicMarkableReference_create(NULL, false);
  return result;
}

static void node_destroy(Node node) {
  AtomicMarkableReference_destroy(node->next);
  free(node);
}

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

static Window make_window(Node p, Node c) {
  return (Window){p, c};
}

Set Set_create() {
  Set this = malloc(sizeof(struct Set));
  this->head = sentinel_node_create(INT_MIN);
  Node tail = sentinel_node_create(INT_MAX);
  while (!AtomicMarkableReference_compareAndSet
         (this->head->next, NULL, (void*) tail, false, false));
  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;
}

static Window find(Node head, int key) {
  Node pred = NULL, curr = NULL, succ = NULL;
  bool f = false;
  bool* marked = &f;
  bool snip;
 retry: while (true) {
    pred = head;
    curr = AtomicMarkableReference_getReference(pred->next);
    while (true) {
      succ = AtomicMarkableReference_get(curr->next, marked);
      while (*marked) {
        snip = AtomicMarkableReference_compareAndSet
          (pred->next, curr, succ, false, false);
        if (!snip) goto retry;
        // companion code: curr = pred->next->reference;
        curr = succ;
        succ = AtomicMarkableReference_get(curr->next, marked);
      }
      if (curr->key >= key)
        return make_window(pred, curr);
      pred = curr;
      curr = succ;
    }
  }
}

bool Set_add(Set this, T item) {
  int key = hash_code(item);
  bool splice;
  while (true) {
    Window window = find(this->head, key);
    Node pred = window.pred, curr = window.curr;
    if (curr->key == key) {
      return false;
    } else {
      Node node = node_create(item);
      free(node->next); // TODO: really?  node destroy?
      node->next = AtomicMarkableReference_create(curr, false);
      if (AtomicMarkableReference_compareAndSet
          (pred->next, curr, node, false, false)) {
        return true;
      }
    }
  }
}

bool Set_remove(Set this, T item) {
  int key = hash_code(item);
  bool snip;
  while (true) {
    Window window = find(this->head, key);
    Node pred = window.pred, curr = window.curr;
    if (curr->key != key) {
      return false;
    } else {
      Node succ = AtomicMarkableReference_getReference(curr->next);
#ifdef ORIGINAL // companion code, known bug
      snip = AtomicMarkableReference_attemptMark(curr->next, succ, true);
#else
      snip = AtomicMarkableReference_compareAndSet
        (curr->next, succ, succ, false, true);
#endif
      if (!snip)
        continue;
      AtomicMarkableReference_compareAndSet
        (pred->next, curr, succ, false, false);
      return true;
    }
  }
}

/* The companion code has this:
bool Set_contains(Set this, T item) {
  int key = hash_code(item);
  Window window = find(this->head, key);
  Node pred = window.pred;
  Node curr = window.curr;
  return (curr->key == key);
}
*/

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

void Set_print(Set list) {
  Node curr = AtomicMarkableReference_getReference(list->head->next);
  $print("{ ");
  while (true) {
    Node next = AtomicMarkableReference_getReference(curr->next);
    if (next == NULL) break;
    $print(curr->item, " ");
    curr = next;
  }
  $print("}");
}

#ifdef _LOCK_FREE_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