/* Filename : ReentrantLock.cvl
   Authors  : YYY, XXX
   Created  : 2021-08-06
   Modified : 2025-01-17

   Implements Lock.h, modeling Java's ReentrantLock class.  A thread
   may repeatedly obtain a lock so that it owns the lock with a
   positive integer multiplicity.

   If this class is used when verifying under the weak fairness
   assumption (CIVL's -fair=true), use -DFAIR, else the partial
   order reduction may not be sound.

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

struct Lock {
  $proc owner;
  int count;
};

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

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

/*@ depends_on \access(l); */
static $atomic_f void Lock_acquire_aux(Lock l) {
  $when(l->owner == $proc_null) l->owner = $self;
}

/*@ 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(l);
  }
  lock_increment(l);
}

#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