await-while cases

mcslock.c

#include <pthread.h>
#include <stddef.h>
#include <stdbool.h>
#include <assert.h>
#include <lkmm.h>
#include <genmc.h>

#if 1
	// genmc -mo -lkmm -check-liveness mcslock.c
	#define await_while while
#elif 1
	// genmc -mo -lkmm -check-liveness -disable-spin-assume mcslock.c
	#define await_while(cond)                                                  \
		for (__VERIFIER_loop_begin(); __VERIFIER_spin_start(), (cond); )
#else
	// genmc -mo -lkmm -check-liveness -disable-spin-assume mcslock.c
	#define await_while(cond) for (int __tmp = (__VERIFIER_loop_begin(), 0); \
		(__tmp = 0, __VERIFIER_spin_start(), (cond) ? 1 : (__VERIFIER_spin_end(1), 0)); \
			__VERIFIER_spin_end(__tmp))
#endif

#define NTHREADS  2

typedef struct node_s {
	struct node_s* next;
	int spin;
} node_t;

void acquire(node_t **m, node_t *me)
{
	node_t *tail;

	me->next = NULL;
	me->spin = 1;

	smp_mb();

	tail = xchg_acquire(m,  me);
	if (!tail) return;

	WRITE_ONCE(tail->next, me);

	await_while (READ_ONCE(me->spin));
	smp_mb();
}

void release(node_t **m, node_t *me)
{
	if (!READ_ONCE(me->next)) {
		if (cmpxchg_release(m, me, NULL) == me) {
			return;
		}
		await_while (!smp_load_acquire(&me->next));
	}

	smp_mb();
	WRITE_ONCE(READ_ONCE(me->next)->spin, 0);
}

node_t *lock;
node_t nodes[NTHREADS];

unsigned int x;

void* run(void *arg)
{
	uint32_t tid = (intptr_t) arg;

	acquire(&lock, &nodes[tid]);
	x++;
	release(&lock, &nodes[tid]);
	return NULL;
}

int main()
{
	pthread_t t[NTHREADS];

	for (intptr_t i = 0; i < NTHREADS; i++)
		pthread_create(&t[i], 0, run, (void*)i);
	for (intptr_t i = 0; i < NTHREADS; i++)
		pthread_join(t[i], NULL);

	assert(x == NTHREADS && "unexpected sum");

	return 0;
}