/* Filename : CoarseHashSet.cvl
   Authors  : YYY and XXX
   Created  : 2018-04-15
   Modified : 2025-01-17
   
   CIVL-C model of CoarseHashSet class from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 13.2.1.   

   Simple concurrent hash set using a lock to fully protect
   each method call.

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

#define INIT_CAP 1

// Types...

struct Set {
  int length; // length of array table
  ArrayList* table;
  int size;
  Lock lock;
};

// Private (static) functions ...

static void resize(Set set) {
  int oldCapacity = set->length;
  Lock_acquire(set->lock);
  // try
  if (oldCapacity != set->length) {
    Lock_release(set->lock); // finally
    return; // someone beat us to it
  }
  int newCapacity = 2 * oldCapacity;
  ArrayList* oldTable = set->table;
  set->table = (ArrayList*) malloc(newCapacity*sizeof(ArrayList));
  set->length = newCapacity;
  for (int i = 0; i < newCapacity; i++)
    set->table[i] = ArrayList_create();
  for (int i = 0; i < oldCapacity; i++) {
    int m = ArrayList_size(oldTable[i]);
    for (int j = 0; j < m; j++) {
      T x = ArrayList_get(oldTable[i], j);
      int myBucket = hash_code_bound(x, set->length);
      ArrayList_add(set->table[myBucket], x);
    }
    ArrayList_destroy(oldTable[i]);
  }
  Lock_release(set->lock); // finally
  free(oldTable);
}

static void acquire(Set set, T x) {
  Lock_acquire(set->lock);
}

static void release(Set set, T x) {
  Lock_release(set->lock);
}

static bool policy(Set set) {
  return set->size / set->length > 4;
}

Set Set_create() {
  Set set = malloc(sizeof(struct Set));
  set->length = INIT_CAP;
  set->size = 0;
  set->table = malloc(set->length*sizeof(ArrayList));
  for (int i = 0; i < set->length; i++) {
    set->table[i] = ArrayList_create();
  }
  set->lock = Lock_create();
  return set;
}

void Set_destroy(Set set) {
  for(int i = 0; i < set->length; i++){
    ArrayList_destroy(set->table[i]);
  }
  free(set->table);
  Lock_destroy(set->lock);
  free(set);
}

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_contains(Set set, T value) {
  acquire(set, value);
  // try
  int myBucket = hash_code_bound(value, set->length); // hashCode
  bool result = ArrayList_contains(set->table[myBucket], value);
  release(set, value); // finally
  return result;
}

bool Set_add(Set set, T value) {
  bool result = false;
  acquire(set, value);
  // try
  int myBucket = hash_code_bound(value, set->length);
  // difference between 2nd ed. book text and companion code;
  // we use the book's version
  if (!ArrayList_contains(set->table[myBucket], value)) {
    ArrayList_add(set->table[myBucket], value);
    result = true;
    set->size = result ? set->size + 1 : set->size;
  }
  release(set, value); // finally
  if (policy(set))
    resize(set);
  return result;
}

bool Set_remove(Set set, T value) {
  acquire(set, value);
  // try
  int myBucket = hash_code_bound(value, set->length);
  bool result = ArrayList_remove_item(set->table[myBucket], value);
  set->size = result ? set->size - 1 : set->size;
  release(set, value); // finally
  return result;
}

void Set_print(Set set) {
  int n = set->length;
  $print("{ ");
  for (int i = 0; i < n; i++) {
    ArrayList row = set->table[i];
    int m = ArrayList_size(row);
    for (int j = 0; j < m; j++)
      $print(ArrayList_get(row, j), " ");
  }
  $print("}");
}

#ifdef _COARSE_HASH_SET_MAIN

static void test1(Set set, int nthread) {
  tid_init(nthread);
  Set_initialize_context();
  Set_initialize(set);
  $parfor (int i : 0 .. nthread-1) {
    tid_register(i);
    Set_add(set, i);
    Set_terminate(i);
    tid_unregister();
  }
  $print("Set after adds: ");
  Set_print(set);
  $print("\n");
  $assert(!Set_stuck());
  Set_finalize(set);
  Set_finalize_context();
  tid_finalize();
  
  for (int i=0; i<nthread; i++)
    $print("hash(", i, ")=", hash_code(i), " ");
  $print("\n");
  $for (int i : 0 .. nthread-1)
    $assert(Set_contains(set, i));
  
  tid_init(nthread);
  Set_initialize_context();
  Set_initialize(set);
  $parfor (int i : 0 .. nthread-1) {
    tid_register(i);
    Set_remove(set, i);
    Set_terminate(i);
    tid_unregister();
  }
  $print("Set after removes: ");
  Set_print(set);
  $print("\n");
  $assert(!Set_stuck());
  Set_finalize(set);
  Set_finalize_context();
  tid_finalize();
  $for (int i : 0 .. nthread-1)
    $assert(!Set_contains(set, i));
}

static void test2(Set set, int nthread) {
  tid_init(nthread);
  Set_initialize_context();
  Set_initialize(set);
  $parfor (int i: 0 .. nthread-1) {
    tid_register(i);
    Set_add(set, i);
    Set_remove(set, i);
    Set_terminate(i);
    tid_unregister();
  }
  $for (int i : 0 .. nthread-1)
    $assert(!Set_contains(set, i));
  Set_finalize(set);
  Set_finalize_context();
  tid_finalize();
}

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