/*
* There is two functions that thread can use to kill a victim
** User KILL-statement lets call it kill()
** BF lock conflict resolution lets call it bf_kill()
* Both kill functions awake thread executing it lets call this awake()
* Any thread can execute either kill() or bf_kill() not both
* Only one thread at time can execute awake()
* thread starting to execute kill() or bf_kill() will execute it
  to completition
* there is no need to wait for turn as if there is two thread
selecting same victim thread either thread_1 kills it or
thread_2 kills it
* there may not be any wait for turn as problem modelled
is caused by wait for mutex (thd->LOCK_thd_data) leading to
mutex lock in different orders between kill() and bf_kill().
* aborter variable represents TURN where 0 == free
                                         1 == reserved
if
:: aborter == 0 -> aborter= 1; awake(); aborter=0;
:: aborter == 1 -> skip;
fi

*/
bit aborter; /* TURN should be std::atomic<bit> aborter*/

byte count; /* # procs in the critical section */
byte count2;
byte count3;
bit flag; /* lock_sys->mutex */
bit flag2; /* thd->LOCK_thd_data mutex */

inline awake()
{
  count++;
  /* kill */
  count--;
  aborter=0; /* reset */
}
  
proctype kill() {
  /*
        aborter.compare_exchange_strong(0, 1,
        std::memory_order_acquire,
        std::memory_order_releaxed) */
  if
  :: atomic{aborter == 0 -> aborter=1;}
    /* thd->LOCK_thd_data mutex */
    atomic {flag2!=1; flag2=1;}
    count3++;
    /* lock_sys->mutex */
    atomic { flag!=1; flag=1;}
    count2++;
    count2--;
    flag=0;
    awake();
    count3--;
    flag2=0;
  :: atomic {aborter == 1 -> skip;}
  fi
}

proctype bf_kill() {
  /* lock_sys->mutex */
  atomic {flag!=1; flag=1;}
  count2++;
  /* 
        aborter.compare_exchange_strong(0, 1,
        std::memory_order_acquire,
        std::memory_order_releaxed) */
  if
  :: atomic{aborter == 0 -> aborter=1;}
    /* thd->LOCK_thd_data mutex */
    atomic {flag2!=1; flag2=1;}
    count3++;
    awake();
    count3--;
    flag2=0;
  :: atomic {aborter == 1 -> skip;}
  fi
  count2--;
  flag=0;
}

proctype monitor() {
    atomic { assert(count!=2); assert(count2!=2); assert(count3!=2); }
}

init {
  atomic { run kill(); run bf_kill(); run monitor(); }
}