Re: sem_getvalue conformance considerations

[Alexander Monakov <amonakov@ispras.ru>]

Hi,

If there's interest, my basic model file for semaphores in Promela/Spin is
pasted below.  Perhaps if I started doing this earlier it would help to avoid
some mistakes.

// spin -a sem.pml && gcc -O2 -DSAFETY pan.c && ./a.out

typedef sem_t {
  int value, waiters;  // Behavior
  int val0, val1;      // Implementation
};

sem_t sem;

#define sem_invariants (                  \
  (sem.value >= 0 && sem.waiters >= 0) && \
  (sem.value == 0 || sem.waiters == 0) && \
  sem.val0 == sem.value - sem.waiters  && \
  sem.val1 >= 0)

bool done;

active proctype monitor()
{
  do
  :: d_step { !sem_invariants -> assert(0); }
  :: done -> break;
  od
}

inline sem_trywait(retval)
{
  // d_step sequences are not preemptible
  if 
  :: d_step { sem.val0 > 0 -> sem.val0--; sem.value--; retval = 0; }
  :: else   { retval = -1; }
  fi
}

inline sem_post()
{
  int v;
  d_step {
    v = sem.val0;
    sem.val0++;
    if
    :: v >= 0 -> sem.value++;
    :: v <  0 -> sem.waiters--;
    fi
  }
  if
  :: v < 0 -> sem.val1++;
  :: else
  fi
}

inline sem_wait(interruptible, retval)
{
  int v;
  d_step {
    retval = 0;
    v = sem.val0;
    sem.val0--;
    if
    :: v >  0 -> sem.value--;
    :: v <= 0 -> sem.waiters++;
    fi
  }
  if
  :: v <= 0  ->
    if // non-deterministic if interruptible && sem.val1 > 0
    :: d_step {sem.val1 > 0 -> sem.val1--;}
    :: interruptible -> 
      d_step {
	v = sem.val0;
	if
	:: v < 0 -> sem.val0++; sem.waiters--; retval = -1;
	:: else
	fi
      }
      if
      :: v >= 0 -> d_step {sem.val1 > 0; sem.val1--;}
      :: else
      fi
    fi
  :: else
  fi
}

int n_posts, n_waits, n_waitfails;

proctype waiter(bool interruptible)
{
  int retval;
  n_waits++;
  sem_wait(interruptible, retval);
  n_waitfails = n_waitfails - retval;
}

proctype poster()
{
  n_posts++;
  sem_post();
}

#define NPROCMAX 4

init
{
  int n_procs = NPROCMAX;
  do // start a non-deterministic amount of posters
  :: n_procs > 0 -> run poster(); n_procs--;
  :: 1 -> break;
  od;
  do // ditto for waiters
  :: n_procs > 0 -> run waiter(false); n_procs--;
  :: 1 -> break;
  od;
  do
  :: n_procs > 0 -> run waiter(true); n_procs--;
  :: 1 -> break;
  od;
  timeout; // wait until quiescent state
  assert(sem.val1 == 0 && sem.val0 == n_posts + n_waitfails - n_waits);
  n_procs = sem.waiters;
  do
  :: n_procs > 0 -> run poster(); n_procs--;
  :: else -> break;
  od;
  timeout; // wait; there should be no processes except "monitor"
  assert(sem.val1 == 0 && sem.val0 == n_posts + n_waitfails - n_waits);
  assert(sem.waiters == 0);
  done = true;
}