/* Filename : StripedHashSet.cvl
   Authors  : YYY and XXX
   Created  : 2017-11-30
   Modified : 2025-01-17

   CIVL model of StripedHashSet class from "The Art of Multiprocessor
   Programming" 2nd ed, by Herlihy, Luchangco, Shavit, and Spear,
   Sec. 13.2.2 "A striped hash set", and companion code
   ch13/src/hash/StripedHashSet.java.
  
   This is a concurrent closed-address hashset using lock striping.
  
   some Lab
   some division
   some institution
 */
#pragma CIVL ACSL
#include "ArrayList.h"
#include "Lock.h"
#include "Set.h"
#include "hash.cvh"
#include "tid.h"
#include "types.h"
#include <stdbool.h>
#include <stdlib.h>
#include <string.h>

#define INITIAL_CAPACITY 1

// Types...

struct Set {
  ArrayList* table;
  int size;
  int table_length;
  int locks_length;
  Lock* locks;
};

// Functions...

Set Set_create() {
  Set s = malloc(sizeof(struct Set));
  s->table_length = INITIAL_CAPACITY;
  s->size = 0;
  s->locks_length = s->table_length;
  s->table = malloc(s->table_length * sizeof(ArrayList));
  for (int i = 0; i < s->table_length; i++) {
    s->table[i] = ArrayList_create();
  }
  s->locks = malloc(s->locks_length * sizeof(Lock));
  for (int k = 0; k < s->locks_length; k++) {
    s->locks[k] = Lock_create();
  }
  return s;
}

void Set_destroy(Set s) {
  for (int l = 0; l < s->table_length; l++) {
    ArrayList_destroy(s->table[l]);
  }
  for (int l = 0; l < s->locks_length; l++) {
    Lock_destroy(s->locks[l]);
  }
  free(s->table);
  free(s->locks);
  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;
}

static void resize(Set s);

static void initializeFrom(Set s, ArrayList* oldTable, int oldCapacity);

static void acquire(Set s, T x);

static void release(Set s, T x);

static bool policy(Set s);

bool Set_contains(Set s, T x) {
  acquire(s, x);
  // try
  int myBucket = hash_code_bound(x, s->table_length);
  bool result = ArrayList_contains(s->table[myBucket], x);
  release(s, x); // finally
  return result;
}

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

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

// called if policy is true or a bucket is overfull
static void resize(Set s) {
  for (int i = 0; i < s->locks_length; i++)
    Lock_acquire(s->locks[i]);
  // try
  if (!policy(s)) {
    goto FINALLY; // someone beat us to it
    /* for (int i = 0; i < s->locks_length; i++) */
    /*   Lock_release(s->locks[i]); */
    /* return; // someone beat us to it */
  }
  int oldCapacity = s->table_length;
  int newCapacity = 2 * oldCapacity;
  ArrayList* oldTable = s->table;
  s->table = malloc(newCapacity * sizeof(ArrayList));
  s->table_length = newCapacity;
  for (int i = 0; i < newCapacity; i++)
    s->table[i] = ArrayList_create();
  initializeFrom(s, oldTable, oldCapacity);
  for (int i = 0; i < oldCapacity; i++)
    ArrayList_destroy(oldTable[i]);
  free(oldTable);
 FINALLY:
  for (int i = 0; i < s->locks_length; i++)
    Lock_release(s->locks[i]);
}

static void initializeFrom(Set s, ArrayList* oldTable, int oldCapacity) {
  for (int i = 0; i < oldCapacity; i++) {
    for (int j = 0; j < ArrayList_size(oldTable[i]); j++) {
      T x = ArrayList_get(oldTable[i], j);
      int myBucket = hash_code_bound(x, s->table_length);
      ArrayList_add(s->table[myBucket], x);
    }
  }
}

static void acquire(Set s, T x) {
  int myBucket = hash_code_bound(x, s->locks_length);
  Lock_acquire(s->locks[myBucket]);
}

static void release(Set s, T x) {
  int myBucket = hash_code_bound(x, s->locks_length);
  Lock_release(s->locks[myBucket]);
}

// resize policy to check if load factor exceeds a set limit
static bool policy(Set s) {
  return s->size / s->table_length > 2;
}

void Set_print(Set s) {
  $print("{ ");
  for (int i = 0; i < s->table_length; i++) {
    ArrayList_print(s->table[i]);
    $print(" ");
  }
  $print("}");
}

#ifdef _STRIPED_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, 2*i);
    Set_add(set, 2*i+1);
    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, 2*i);
    Set_remove(set, 2*i+1);
    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 .. 2*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, 2*i);
    Set_add(set, 2*i+1);
    Set_remove(set, 2*i);
    Set_remove(set, 2*i+1);
    Set_terminate(i);
    tid_unregister();
  }
  $for (int i : 0 .. 2*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