GenMC issue with mcs_spinlock.h from Linux 5.14

mcs-check.c

/*******************************************************************************

Step 1 -- Download mcs_spinlock.h, version 5.14 (and do 2 small changes):

  curl -o mcs_spinlock.h https://raw.githubusercontent.com/torvalds/linux/v5.14/kernel/locking/mcs_spinlock.h
  sed -i 's/#include/\/\/#include/g' mcs_spinlock.h
  sed -i 's/\twhile/\tawait_while/g' mcs_spinlock.h

Step 2 -- Reproduce problem:

  genmc -check-liveness -mo -lkmm \
    -disable-race-detection \
    -disable-load-annotation \
    -disable-cast-elimination \
    -disable-spin-assume \
    -- -DSPIN_ANNOTATION -I/usr/share/genmc/include mcs-check.c

<output>
WARNING: LKMM support is still at an experimental stage!
WARNING: Atomic xchg support is experimental under dependency-tracking models!
Error detected: Safety violation!
Event (0, 12) in graph:
<-1, 0> main:
	(0, 0): B
	(0, 1): M
	(0, 2): TC [forks 1] L.114
	(0, 3): Wna (t[0], 1) L.114
	(0, 4): TC [forks 2] L.114
	(0, 5): Wna (t[1], 2) L.114
	(0, 6): Rna (t[0], 1) [(0, 3)] L.115
	(0, 7): TJ L.115
	(0, 8): Rna (t[1], 2) [(0, 5)] L.115
	(0, 9): TJ L.115
	(0, 10): Rna (x, 1) [(2, 25)] L.116
	(0, 11): Rna (y, 1) [(2, 27)] L.116
	(0, 12): Rna (x, 1) [(2, 25)] L.116
<0, 1> run:
	(1, 0): B
	(1, 1): M
	(1, 2): M
	(1, 3): M
	(1, 4): Wna (nodes[0].locked, 0) L.70: mcs_spinlock.h
	(1, 5): Wna (nodes[0].next, 0x0) L.71: mcs_spinlock.h
	(1, 6): FBUG: Failure at EventLabel.cpp:202/operator<<()!
</output>


Step 3 -- Replace xchg definition:

  genmc -check-liveness -mo -lkmm \
    -disable-race-detection \
    -disable-load-annotation \
    -disable-cast-elimination \
    -disable-spin-assume \
    -- -DSPIN_ANNOTATION -DREPLACE_XCHG -I/usr/share/genmc/include mcs-check.c

<output>
WARNING: LKMM support is still at an experimental stage!
WARNING: Atomic xchg support is experimental under dependency-tracking models!
Error detected: Safety violation!
Event (0, 12) in graph:
<-1, 0> main:
        (0, 0): B
        (0, 1): M
        (0, 2): TC [forks 1] L.155
        (0, 3): Wna (t[0], 1) L.155
        (0, 4): TC [forks 2] L.155
        (0, 5): Wna (t[1], 2) L.155
        (0, 6): Rna (t[0], 1) [(0, 3)] L.156
        (0, 7): TJ L.156
        (0, 8): Rna (t[1], 2) [(0, 5)] L.156
        (0, 9): TJ L.156
        (0, 10): Rna (x, 1) [(2, 25)] L.157
        (0, 11): Rna (y, 1) [(2, 27)] L.157
        (0, 12): Rna (x, 1) [(2, 25)] L.157
<0, 1> run:
        (1, 0): B
        (1, 1): M
        (1, 2): M
        (1, 3): M
        (1, 4): Wna (nodes[0].locked, 0) L.70: mcs_spinlock.h
        (1, 5): Wna (nodes[0].next, 0x0) L.71: mcs_spinlock.h
        (1, 6): Fmb L.79: mcs_spinlock.h
        (1, 7): Wna (, 0x1b76990) L.79: mcs_spinlock.h
        (1, 8): Rna (, 28797328) [(1, 7)] L.79: mcs_spinlock.h
        (1, 9): Urlx (lock, 0) [INIT] L.79: mcs_spinlock.h
        (1, 10): Urlx (lock, 28797328) L.79: mcs_spinlock.h
        (1, 11): Wna (, 0) L.79: mcs_spinlock.h
        (1, 12): Rna (, 0x0) [(1, 11)] L.79: mcs_spinlock.h
        (1, 13): Fmb L.79: mcs_spinlock.h
        (1, 14): D L.95: mcs_spinlock.h
        (1, 15): D L.95: mcs_spinlock.h
        (1, 16): D L.95: mcs_spinlock.h
        (1, 17): Rna (x, 0) [INIT] L.147
        (1, 18): Wna (x, 1) L.147
        (1, 19): Rna (y, 0) [INIT] L.147
        (1, 20): Wna (y, 1) L.147
        (1, 21): M
        (1, 22): M
        (1, 23): M
        (1, 24): M
        (1, 25): Rrlx (nodes[0].next, 0) [(1, 5)] L.104: mcs_spinlock.h
        (1, 26): Wna (, 0) L.104: mcs_spinlock.h
        (1, 27): Rna (, 0x0) [(1, 26)] L.104: mcs_spinlock.h
        (1, 28): Wna (_o_, 0x1b76990) L.110: mcs_spinlock.h
        (1, 29): Wna (, 0x0) L.110: mcs_spinlock.h
        (1, 30): Rna (_o_, 28797328) [(1, 28)] L.110: mcs_spinlock.h
        (1, 31): Rna (, 0) [(1, 29)] L.110: mcs_spinlock.h
        (1, 32): Crel (lock, 28797344) [(2, 10)] L.110: mcs_spinlock.h
        (1, 33): Wna (_o_, 28797344) L.110: mcs_spinlock.h
        (1, 34): Rna (_o_, 0x1b769a0) [(1, 33)] L.110: mcs_spinlock.h
        (1, 35): LOOP_BEGIN L.113: mcs_spinlock.h
        (1, 36): SPIN_START L.113: mcs_spinlock.h
        (1, 37): Rrlx (nodes[0].next, 28797344) [(2, 16)] L.113: mcs_spinlock.h
        (1, 38): Wna (, 28797344) L.113: mcs_spinlock.h
        (1, 39): Rna (, 0x1b769a0) [(1, 38)] L.113: mcs_spinlock.h
        (1, 40): Wrel (nodes[1].locked, 1) L.118: mcs_spinlock.h
        (1, 41): D L.119: mcs_spinlock.h
        (1, 42): D L.119: mcs_spinlock.h
        (1, 43): D L.119: mcs_spinlock.h
        (1, 44): D L.119: mcs_spinlock.h
        (1, 45): E
<0, 2> run:
        (2, 0): B
        (2, 1): M
        (2, 2): M
        (2, 3): M
        (2, 4): Wna (nodes[1].locked, 0) L.70: mcs_spinlock.h
        (2, 5): Wna (nodes[1].next, 0x0) L.71: mcs_spinlock.h
        (2, 6): Fmb L.79: mcs_spinlock.h
        (2, 7): Wna (, 0x1b769a0) L.79: mcs_spinlock.h
        (2, 8): Rna (, 28797344) [(2, 7)] L.79: mcs_spinlock.h
        (2, 9): Urlx (lock, 28797328) [(1, 10)] L.79: mcs_spinlock.h
        (2, 10): Urlx (lock, 28797344) L.79: mcs_spinlock.h
        (2, 11): Wna (, 28797328) L.79: mcs_spinlock.h
        (2, 12): Rna (, 0x1b76990) [(2, 11)] L.79: mcs_spinlock.h
        (2, 13): Fmb L.79: mcs_spinlock.h
        (2, 14): Wna (, 0x1b769a0) L.91: mcs_spinlock.h
        (2, 15): Rna (, 28797344) [(2, 14)] L.91: mcs_spinlock.h
        (2, 16): Wrlx (nodes[0].next, 28797344) L.91: mcs_spinlock.h
        (2, 17): LOOP_BEGIN L.94: mcs_spinlock.h
        (2, 18): SPIN_START L.94: mcs_spinlock.h
        (2, 19): Rrlx (nodes[1].locked, 1) [(1, 40)] L.94: mcs_spinlock.h
        (2, 20): Frmb L.94: mcs_spinlock.h
        (2, 21): D L.95: mcs_spinlock.h
        (2, 22): D L.95: mcs_spinlock.h
        (2, 23): D L.95: mcs_spinlock.h
        (2, 24): Rna (x, 0) [INIT] L.147
        (2, 25): Wna (x, 1) L.147
        (2, 26): Rna (y, 0) [INIT] L.147
        (2, 27): Wna (y, 1) L.147
        (2, 28): M
        (2, 29): M
        (2, 30): M
        (2, 31): M
        (2, 32): Rrlx (nodes[1].next, 0) [(2, 5)] L.104: mcs_spinlock.h
        (2, 33): Wna (, 0) L.104: mcs_spinlock.h
        (2, 34): Rna (, 0x0) [(2, 33)] L.104: mcs_spinlock.h
        (2, 35): Wna (_o_, 0x1b769a0) L.110: mcs_spinlock.h
        (2, 36): Wna (, 0x0) L.110: mcs_spinlock.h
        (2, 37): Rna (_o_, 28797344) [(2, 35)] L.110: mcs_spinlock.h
        (2, 38): Rna (, 0) [(2, 36)] L.110: mcs_spinlock.h
        (2, 39): Crel (lock, 28797344) [(2, 10)] L.110: mcs_spinlock.h
        (2, 40): Crel (lock, 0) L.110: mcs_spinlock.h
        (2, 41): Rna (_o_, 0x1b769a0) [(2, 35)] L.110: mcs_spinlock.h
        (2, 42): D L.119: mcs_spinlock.h
        (2, 43): D L.119: mcs_spinlock.h
        (2, 44): D L.119: mcs_spinlock.h
        (2, 45): D L.119: mcs_spinlock.h
        (2, 46): E

Assertion violation: x == y && x == N
Number of complete executions explored: 1
Number of blocked executions seen: 2
Total wall-clock time: 0.03s
</output>

 ******************************************************************************/
#include <assert.h>
#include <pthread.h>
#include <stddef.h>
#include <stdbool.h>

/*******************************************************************************
 * workaround for misdetection of await loops
 ******************************************************************************/
#if !defined(SPIN_ANNOTATION)
    #define await_while(cond) while (cond)
    #define await_do          do
    #define while_await(cond) while (cond)
#else
    /* should only be used with -disable-spin-assume option in GenMC */
    void __VERIFIER_loop_begin(void);
    void __VERIFIER_spin_start(void);
    void __VERIFIER_spin_end(bool);
    #define await_while(cond)                                                  \
	for (int tmp = (__VERIFIER_loop_begin(), 0); __VERIFIER_spin_start(),  \
		 tmp = cond, __VERIFIER_spin_end(!tmp), tmp;)

    #define await_do                                                           \
	do {                                                                   \
	    int __tmp;                                                         \
	    __VERIFIER_loop_begin();                                           \
	    do {                                                               \
		__VERIFIER_spin_start();

    #define while_await(cond)                                                  \
	    } while (__tmp = (cond), __VERIFIER_spin_end(!__tmp), __tmp);      \
	} while (0)
#endif

/*******************************************************************************
 * use and extend genmc/lkmm.h
 ******************************************************************************/
#include <genmc/lkmm.h>

#define __scalar_type_to_expr_cases(type)                               \
		unsigned type:  (unsigned type)0,                       \
		signed type:    (signed type)0
#define __unqual_scalar_typeof(x) typeof(                               \
		_Generic((x),                                           \
			 char:  (char)0,                                \
			 __scalar_type_to_expr_cases(char),             \
			 __scalar_type_to_expr_cases(short),            \
			 __scalar_type_to_expr_cases(int),              \
			 __scalar_type_to_expr_cases(long),             \
			 __scalar_type_to_expr_cases(long long),        \
			 default: (x)))
#define smp_acquire__after_ctrl_dep() smp_rmb()
#define smp_cond_load_acquire(ptr, cond_expr) ({                \
	__unqual_scalar_typeof(*ptr) _val;                      \
	_val = smp_cond_load_relaxed(ptr, cond_expr);           \
	smp_acquire__after_ctrl_dep();                          \
	(typeof(*ptr))_val;                                     \
})
#define smp_cond_load_relaxed(ptr, cond_expr) ({              \
      typeof(ptr) __PTR = (ptr);                              \
      __unqual_scalar_typeof(*ptr) VAL;                       \
      await_do {                                              \
	      VAL = READ_ONCE(*__PTR); 	                      \
	   } while_await (!cond_expr);                        \
      (typeof(*ptr))VAL;                                      \
})

#ifdef REPLACE_XCHG
#undef xchg
#define xchg(p, v) ({                                                   \
	__typeof__((v)) _v_ = (v);                                      \
	smp_mb(); 				                    	\
	_v_ = __xchg(p, v, memory_order_relaxed);                       \
	smp_mb();                            				\
	_v_;                                                            \
})
#endif

/*******************************************************************************
 * Include mcs_spinlock.h from version 5.14
 ******************************************************************************/
#define unlikely(X) (X)
#define likely(X) (X)
#define __init
#define __pure
#define cpu_relax() do {} while(0)
#include "mcs_spinlock.h"

/*******************************************************************************
 * client code
 ******************************************************************************/
#define N 2

struct mcs_spinlock *lock;
struct mcs_spinlock nodes[N];

static int x = 0, y = 0;
static void* run(void *arg)
{
	uint32_t tid = (intptr_t)arg;
	mcs_spin_lock(&lock, &nodes[tid]);
	x++; y++;
	mcs_spin_unlock(&lock, &nodes[tid]);
	return NULL;
}

int main()
{
	pthread_t t[N];
	for (intptr_t i = 0; i < N; i++)	pthread_create(t+i, 0, run, (void*)i);
	for (intptr_t i = 0; i < N; i++) pthread_join(t[i], NULL);
	assert (x == y && x == N);
	return 0;
}