C kfifo_put(in)+kfifo_get(out)+writer_first

(* P0: writer, P1: reader
  in:  __kfifo.in
  out: __kfifo.out
  d:   __kfifo.data[0]
  b:   reader buffer
 *)

{
	in = 0;
	out = 0;
	d = 0;
	b = -1;
}

P0(int *in, int *out, int *d)
{
	if (*in == *out) {
		*d = 1;
		smp_wmb();
		*in = *in + 1;
	}
}

P1(int *in, int *out, int *d, int *b)
{
	int r;

	if (*in != *out) {
//		smp_rmb();	// kfifo missed a read barrier between read index and data
		r = *d;
		*b = r;
		smp_wmb();
		*out = *out + 1;
	}
}

exists (b=0)