/* Filename : AtomicMarkableReference.cvl
   Authors  : YYY, XXX
   Created  : 2024-01-25
   Modified : 2025-01-17

   Implements AtomicMarkableReference.cvh, a model of the Java class
   AtomicMarkableReference.

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

struct AtomicMarkableReference {
  void* reference;
  bool mark;
};

AtomicMarkableReference AtomicMarkableReference_create(void* ref, bool m) {
  AtomicMarkableReference amr =
    malloc(sizeof(struct AtomicMarkableReference));
  amr->reference = ref;
  amr->mark = m;
  return amr;
}

void AtomicMarkableReference_destroy(AtomicMarkableReference ref) {
  free(ref);
}

/*@ depends_on \access(amr); */
$atomic_f bool
AtomicMarkableReference_compareAndSet(AtomicMarkableReference amr,
                    void* exp_ref, void* new_ref,
                    bool exp_mark, bool new_mark) {
  if (amr->reference == exp_ref && amr->mark == exp_mark) {
    amr->reference = new_ref;
    amr->mark = new_mark;
    return true;
  } else {
    return false;
  }
}

/*@ depends_on \access(amr); */
$atomic_f bool
AtomicMarkableReference_attemptMark(AtomicMarkableReference amr,
                 void* exp_ref, bool new_mark) {
  if (amr->reference == exp_ref) {
    amr->mark = new_mark;
    return true;
  } else {
    return false;
  }
}

/*@ depends_on \access(amr); */
$atomic_f void
AtomicMarkableReference_set(AtomicMarkableReference amr, void* r, bool m) {
  amr->reference = r;
  amr->mark = m;
}

/*@ depends_on \access(amr); */
$atomic_f void*
AtomicMarkableReference_get(AtomicMarkableReference amr, bool* mark_out) {
  *mark_out = amr->mark;
  return amr->reference;
}

void*
AtomicMarkableReference_getReference(AtomicMarkableReference amr) {
  return amr->reference;
}

bool
AtomicMarkableReference_isMarked(AtomicMarkableReference amr) {
  return amr->mark;
}