/* Filename : tid.cvl
   Author   : XXX
   Created  : 2024-03-12
   Modified : 2025-01-17

   Implements tid.h, a simple module to provide permanent thread IDs
   to threads in a concurrent program.

   some Lab
   some division
   some institution
 */
#pragma CIVL ACSL
#include "seq.cvh"
#include "tid.h"

static $proc threads[];

//@ depends_on \nothing;
$atomic_f void tid_init(int nthread) {
  $proc v = $proc_null;
  $seq_init(&threads, nthread, &v);
}

//@ depends_on \nothing;
$atomic_f int tid_nthread() {
  return $seq_length(&threads);
}

//@ depends_on \nothing;
$atomic_f void tid_finalize() {
  $seq_init(&threads, 0, NULL);
}
    
//@ depends_on \nothing;
$atomic_f void tid_register(int tid) {
  int n = $seq_length(&threads);
  $assert(0<=tid && tid<n);
  $assert(threads[tid] == $proc_null);
  threads[tid] = $self;
}

//@ depends_on \nothing;
$atomic_f void tid_unregister() {
  int tid = tid_get();
  $assert(tid >= 0);
  threads[tid] = $proc_null;
}

//@ depends_on \nothing;
$atomic_f int tid_get() {
  int n = $seq_length(&threads);
  for (int i=0; i<n; i++)
    if (threads[i] == $self)
      return i;
  return -1;
}