/* Filename : StripedCuckooHashSet.cvl
   Authors  : YYY and XXX
   Created  : 2018-04-26
   Modified : 2025-01-17

   CIVL model of StripedCuckooHashSet class from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 13.4.3 "Striped concurrent cuckoo hashing", and companion code
   ch13/src/hash/StripedCuckooHashSet.java.

   This is a concurrent cuckoo hashset using lock striping and
   phasing.  It has bugs, including a possible null pointer
   dereference and non-termination.

   some Lab
   some division
   some institution
 */
#include "ArrayList.h"
#include "Lock.h"
#include "Set.h"
#include "hash.cvh"
#include "tid.h"
#include "types.h"
#include <stdbool.h>
#include <stdlib.h>

#define LIMIT 8
#define PROBE_SIZE 2
#define THRESHOLD (PROBE_SIZE / 2)
#define INITIAL_CAPACITY 1
// need this because our interface doesn't have a constructor
// that takes an initial size

// Types...

struct Set {
  int capacity;
  Lock* lock[2];
  ArrayList* table[2];
};

// Functions...

Set Set_create() {
  // PhasedCuckooHashSet constructor
  Set result = malloc(sizeof(struct Set));
  result->capacity = INITIAL_CAPACITY;
  for (int i = 0; i < 2; i++) {
    result->table[i] = malloc(result->capacity*sizeof(ArrayList));
    for (int j = 0; j < result->capacity; j++) {
      result->table[i][j] = ArrayList_create();
    }
  }
  // StripedCuckooHashSet constructor
  for (int i = 0; i < 2; i++) {
    result->lock[i] = malloc(result->capacity*sizeof(Lock));
    for (int j = 0; j < result->capacity; j++) {
      result->lock[i][j] = Lock_create();
    }
  }
  return result;
}

void Set_destroy(Set s) {
  for (int i = 0; i < 2; i++) {
    for (int j = 0; j < s->capacity; j++) {
      ArrayList_destroy(s->table[i][j]);
    }
    for (int j = 0; j < INITIAL_CAPACITY; j++) {
      Lock_destroy(s->lock[i][j]);
    }
    free(s->table[i]);
    free(s->lock[i]);
  }
  free(s);
}

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

// hash0 provided by hash.cvh
static int hash0(Set s, T x) {
  return hash_code_dual(x, 0);
}

// hash1 provided by hash.cvh
static int hash1(Set s, T x) {
  return hash_code_dual(x, 1);
}

static void acquire(Set s, T x) {
  Lock lock0 = s->lock[0][hash0(s, x) % INITIAL_CAPACITY];
  Lock lock1 = s->lock[1][hash1(s, x) % INITIAL_CAPACITY];
  Lock_acquire(lock0);
  Lock_acquire(lock1);
}

static void release(Set s, T x) {
  Lock lock0 = s->lock[0][hash0(s, x) % INITIAL_CAPACITY];
  Lock lock1 = s->lock[1][hash1(s, x) % INITIAL_CAPACITY];
  Lock_release(lock0);
  Lock_release(lock1);
}

bool Set_contains(Set s, T x) {
  acquire(s, x);
  // try
  int h0 = hash0(s, x) % s->capacity;
  if (ArrayList_contains(s->table[0][h0], x)) {
    release(s, x); // finally
    return true;
  } else {
    int h1 = hash1(s, x) % s->capacity;
    if (ArrayList_contains(s->table[1][h1], x)) {
      release(s, x); // finally
      return true;
    }
  }
  release(s, x); // finally
  return false;
}

bool Set_remove(Set s, T x) {
  acquire(s, x);
  // try
  ArrayList set0 = s->table[0][hash0(s, x) % s->capacity];
  if (ArrayList_contains(set0, x)) {
    ArrayList_remove_item(set0, x);
    release(s, x); // finally
    return true;
  } else {
    ArrayList set1 = s->table[1][hash1(s, x) % s->capacity];
    if (ArrayList_contains(set1, x)) {
      ArrayList_remove_item(set1, x);
      release(s, x); // finally
      return true;
    }
  }
  release(s, x); // finally
  return false;
}

// Unsynchronized version of contains()
static bool present(Set s, T x) {
  int h0 = hash0(s, x) % s->capacity;
  if (ArrayList_contains(s->table[0][h0], x)) {
    return true;
  } else {
    int h1 = hash1(s, x) % s->capacity;
    if (ArrayList_contains(s->table[1][h1], x)) {
      return true;
    }
  }
  return false;
}

// Forward declaration needed for Set_add
static bool relocate(Set s, T i, int hi);

// Forward declaration needed for Set_add
static void resize(Set s);

bool Set_add(Set s, T x) {
  T y = -1; // null
  acquire(s, x);
  int h0 = hash0(s, x) % s->capacity;
  int h1 = hash1(s, x) % s->capacity;
  int i = -1, h = -1;
  bool mustResize = false;
  // try
  if (present(s, x)) {
    release(s, x); // finally
    return false;
  }
  ArrayList set0 = s->table[0][hash0(s, x) % s->capacity];
  ArrayList set1 = s->table[1][hash1(s, x) % s->capacity];
  if (ArrayList_size(set0) < THRESHOLD) {
    ArrayList_add(set0, x);
    release(s, x); // finally
    return true;
  } else if (ArrayList_size(set1) < THRESHOLD) {
    ArrayList_add(set1, x);
    release(s, x); // finally
    return true;
  } else if (ArrayList_size(set0) < PROBE_SIZE) {
    ArrayList_add(set0, x);
    i = 0; h = h0;
  } else if (ArrayList_size(set1) < PROBE_SIZE) {
    ArrayList_add(set1, x);
    i = 1; h = h1;
  } else {
    mustResize = true;
  }
  release(s, x); // finally
  if (mustResize) {
    resize(s);
    Set_add(s, x);
  } else if (!relocate(s, i, h)) {
    resize(s);
  }
  return true; // x must have been present
}

static void resize(Set s) {
  int oldCapacity = s->capacity;
  for (int i = 0; i < INITIAL_CAPACITY; i++) {
    Lock_acquire(s->lock[0][i]);
  }
  // try
  if (s->capacity != oldCapacity) { // someone else resized first
    for (int i = 0; i < INITIAL_CAPACITY; i++) { // finally
      Lock_release(s->lock[0][i]);
    }
    return;
  }

  ArrayList* oldTable[2] = {s->table[0], s->table[1]};

  s->capacity = 2 * s->capacity;
#ifdef DEBUG
  $print("Resizing.  New size = ", s->capacity, "\n");
#endif
  for (int i = 0; i < 2; i++) {
    s->table[i] = malloc(s->capacity*sizeof(ArrayList));
    for (int j = 0; j < s->capacity; j++) {
      s->table[i][j] = ArrayList_create();
    }
  }
  for (int i = 0; i < 2; i++) {
    for (int j = 0; j < oldCapacity; j++) {
      for (int k = 0; k < ArrayList_size(oldTable[i][j]); k++) {
        Set_add(s, ArrayList_get(oldTable[i][j], k));
      }
    }
  }

  // clean up oldTable
  for (int i = 0; i < 2; i++) {
    for (int j = 0; j < oldCapacity; j++) {
      ArrayList_destroy(oldTable[i][j]);
    }
    free(oldTable[i]);
  }
  // end clean up oldTable

  for (int i = 0; i < INITIAL_CAPACITY; i++) { // finally
    Lock_release(s->lock[0][i]);
  }
}

static bool relocate(Set s, int i, int hi) {
  int hj = 0;
  int j = 1 - i;
  for (int round = 0; round < LIMIT; round++) {
    ArrayList iSet = s->table[i][hi];
    T y = ArrayList_get(iSet, 0);
    switch (i) {
      case 0: hj = hash1(s, y) % s->capacity; break;
      case 1: hj = hash0(s, y) % s->capacity; break;
    }
    acquire(s, y);
    ArrayList jSet = s->table[j][hj];
    // try
    if (ArrayList_remove_item(iSet, y)) {
      if (ArrayList_size(jSet) < THRESHOLD) {
        ArrayList_add(jSet, y);
        release(s, y); // finally
        return true;
      } else if (ArrayList_size(jSet) < PROBE_SIZE) {
        ArrayList_add(jSet, y);
        i = 1 - i;
        hi = hj;
        j = 1 - j;
      } else {
        ArrayList_add(iSet, y);
        release(s, y); // finally
        return false;
      }
    } else if (ArrayList_size(iSet) >= THRESHOLD) {
      release(s, y); // finally
      continue;
    } else {
      release(s, y); // finally
      return true;
    }
    release(s, y); // finally
  }
  return false;
}

void Set_print(Set s) {
  $print("{ ");
  for (int i = 0; i < 2; i++) {
    for (int j = 0; j < s->capacity; j++) {
      int size = ArrayList_size(s->table[i][j]);
      for (int k = 0; k < size; k++) {
        $print(ArrayList_get(s->table[i][j], k), " ");
      }
    }
  }
  $print("}");
}

#ifdef _STRIPED_CUCKOO_HASH_SET_MAIN

int main() {
  Set s = Set_create();
  int nthread = 5;
  tid_init(nthread);
  Set_initialize_context();
  Set_initialize(s);
  $parfor (int i : 0 .. nthread-1) {
    tid_register(i);
    Set_add(s, i);
    Set_terminate(i);
    tid_unregister();
  }
  Set_finalize(s);
  Set_finalize_context();
  tid_finalize();

  $print("Set after adding 0..", nthread-1, ": ");
  Set_print(s);
  $print("\n");

  tid_init(1);
  Set_initialize_context();
  Set_initialize(s);
  tid_register(0);
  $for (int i : 0 .. nthread-1)
    $assert(Set_contains(s, i));
  Set_terminate(0);
  tid_unregister();
  Set_finalize(s);
  Set_finalize_context();
  tid_finalize();

  tid_init(nthread);
  Set_initialize_context();
  Set_initialize(s);
  $parfor (int i : 1 .. 2) {
    tid_register(i);
    Set_remove(s, i);
    Set_terminate(i);
    tid_unregister();
  }
  Set_finalize(s);
  Set_finalize_context();
  tid_finalize();

  $print("Set after removing 1..2: ");
  Set_print(s);
  $print("\n");

  $for (int i : 0 .. nthread-1) {
    if (i == 1 || i == 2)
      $assert(!Set_contains(s, i));
    else
      $assert(Set_contains(s, i));
  }

  tid_init(nthread);
  Set_initialize_context();
  Set_initialize(s);
  $parfor (int i : 0 .. nthread-1) {
    tid_register(i);
    if (i == 2)
      Set_add(s, i);
    else
      Set_remove(s, i);
    Set_terminate(i);
    tid_unregister();
  }
  Set_finalize(s);
  Set_finalize_context();
  tid_finalize();

  $print("Set after adding 2 and removing everything else: ");
  Set_print(s);
  $print("\n");

  $for (int i : 0 .. nthread-1) {
    if (i == 2)
      $assert(Set_contains(s, i));
    else
      $assert(!Set_contains(s, i));
  }

  Set_destroy(s);
}
#endif