/*
* 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()

This is model of original code before MDEV-21910

*/
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--;
  flag=0;
  aborter=0; /* reset */
}
  
proctype kill() {
    /* thd->LOCK_thd_data mutex */
    atomic {flag2!=1; flag2=1;}
    count3++;
    /* lock_sys->mutex */
    atomic { flag!=1; flag=1;}
    count2++;
    count2--;
    awake();
    count3--;
    flag2=0;
}

proctype bf_kill() {
  /* lock_sys->mutex */
  atomic {flag!=1; flag=1;}
  count2++;
  /* thd->LOCK_thd_data mutex */
  atomic {flag2!=1; flag2=1}
  count3++;
  awake();
  count3--;
  count2--;
  flag=0;
  flag2=0;
}

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

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