/* Filename : FairRentrantLock.cvl
   Authors  : YYY, XXX
   Created  : 2023-04-07
   Modified : 2025-01-17

   Implementation of Lock.h that models Java's ReentrantLock with
   fairness.  A thread trying to obtain a lock will be placed in a
   FIFO queue so that if the lock is repeatedly released and
   re-obtained, the thread will eventually get it.

   some Lab
   some division
   some institution
 */
#pragma CIVL ACSL
#include "Lock.h"
#include <seq.cvh>
#include <stdbool.h>
#include <stdlib.h>

struct Lock {
  $proc owner;
  int count;
  $proc waitset[]; // empty sequence of procs
};

Lock Lock_create() {
  Lock result = malloc(sizeof(struct Lock));
  result->owner = $proc_null;
  result->count = 0;
  $seq_init(&result->waitset, 0, NULL);
  return result;
}

void Lock_destroy(Lock l) {
  free(l);
}

/*@ depends_on \access(l); */
static $atomic_f void Lock_acquire_aux_1(Lock l) {
  int n = $seq_length(&l->waitset);
  $proc self = $self;
  if (!$exists (int i: 0..(n - 1)) l->waitset[i] == $self) {
    $seq_append(&l->waitset, &self, 1);
  }
}

// depends on nothing because if you are first in line,
// and the lock is free, you will get the lock no matter
// what anyone else does...
/*@ depends_on \nothing; */
static $atomic_f void Lock_acquire_aux_2(Lock l) {
  $when(l->owner == $proc_null && l->waitset[0] == $self) {
    l->owner = $self;
    $assert(l->waitset[0] == $self);
    $seq_remove(&l->waitset, 0, NULL, 1);
  }
}

/*@ depends_on \nothing; */
static $atomic_f void lock_increment(Lock l) {
  l->count++;
}

/*@ depends_on \nothing; */
static $atomic_f bool am_owner(Lock l) {
  return $self == l->owner;
}

_Bool Lock_isHeldByCurrentThread(Lock l) {
  return am_owner(l);
}

void Lock_acquire(Lock l) {
  if (!am_owner(l)) {
    Lock_acquire_aux_1(l);
    Lock_acquire_aux_2(l);
  }
  lock_increment(l);
}

// necessary to fully enable at release only to detect fair cycles...
#if defined(FAIR) || defined(_LOCK_TEST)
/*@ depends_on \access(l); */
#else
/*@ depends_on \nothing; */
#endif
$atomic_f void Lock_release(Lock l) {
  $assert($self == l->owner);
  l->count--;
  if (l->count == 0) l->owner = $proc_null;
}

#ifdef _LOCK_TEST
_Bool Lock_isLocked(Lock l) {
  return l->owner != $proc_null;
}
#endif