False positive in LKMM race detection?

[db7]

GenMC 0.7 detects a race in the following code with LKMM. I am unsure whether that is a real race or something else:

#include <lkmm.h>
int spin, lock;

T0( ) {
	spin = 0;
	smp_wmb();
	WRITE_ONCE(lock, 1);
}

T1( ) {
	if (READ_ONCE(lock) != 0) {
		smp_mb();
		spin = 1;
	}
}

GenMC detects a race between both updates of spin (line number wont match, sorry):

$ genmc -lkmm test.c 
WARNING: LKMM support is still at an experimental stage!
Error detected: Non-Atomic race!
Event (1, 3) conflicts with event (0, 2) in graph:
<-1, 0> main:
        (0, 0): B
        (0, 1): TC [forks 1] L.39
        (0, 2): Wna (spin, 0) L.9
        (0, 3): Fwmb L.11
        (0, 4): Wrlx (lock, 1) L.12
        (0, 5): TJ L.41
<0, 1> run1:
        (1, 0): B
        (1, 1): Rrlx (lock, 1) [(0, 4)] L.25
        (1, 2): Fmb L.26
        (1, 3): Wna (spin, 1) L.27

Number of complete executions explored: 0
Number of blocked executions seen: 1
Total wall-clock time: 0.01s

The issue can be fixed if T0 writes to lock with smp_store_release or if we use smp_mb() instead of smp_wmb(), but I thought the smp_wmb() should guarantee the order of both writes.

Here is a gist with the complete code and a few other variants.

PS: The data race is also detected in GenMC 0.6.1.

[db7]

Here is another example based on this article in LWN.

// example based on https://lwn.net/Articles/846700/
#include <pthread.h>
#include <lkmm.h>
#include <stddef.h>
#include <assert.h>

struct stuff {
    int x;
};

struct stuff *message;
struct stuff a;

void* run0(void *arg)
{
    a.x = 1;
    smp_wmb();
    WRITE_ONCE(message, &a);
    return 0;
}

void *run1(void *arg)
{
    struct stuff *datum = READ_ONCE(message);
    smp_rmb();
    if (datum != NULL)
        assert(datum->x == 1);
    return 0;
}

int main()
{
    pthread_t t;
    pthread_create(&t, 0, run1, 0);
    run0(0);    
    pthread_join(t, 0);
    return 0;
}

This is the error I get:

$ genmc -lkmm -disable-race-detection test.c 
WARNING: LKMM support is still at an experimental stage!
Error detected: Safety violation!
Event (1, 6) in graph:
<-1, 0> main:
        (0, 0): B
        (0, 1): TC [forks 1] L.34
        (0, 2): M
        (0, 3): Wna (a.x, 1) L.16
        (0, 4): Fwmb L.17
        (0, 5): Wna (.atomictmp, 0x8000000000000000) L.18
        (0, 6): Rna (.atomictmp, -9223372036854775808) [(0, 5)] L.18
        (0, 7): Wrlx (message, -9223372036854775808) L.18
        (0, 8): D L.19
        (0, 9): TJ L.36
<0, 1> run1:
        (1, 0): B
        (1, 1): M
        (1, 2): Rrlx (message, -9223372036854775808) [(0, 7)] L.24
        (1, 3): Wna (atomic-temp, -9223372036854775808) L.24
        (1, 4): Rna (atomic-temp, 0x8000000000000000) [(1, 3)] L.24
        (1, 5): Frmb L.25
        (1, 6): Rna (a.x, 0) [INIT] L.27

Assertion violation: datum->x == 1
Number of complete executions explored: 1
Number of blocked executions seen: 1
Total wall-clock time: 0.14s

According to the article the assert shouldn't fail.

However, GenMC stops complaining if both fences are smp_mb() or if the accesses are atomic-relaxed like this:

void* run0(void *arg)
{
    WRITE_ONCE(a.x, 1);
...
void *run1(void *arg)
{
...
        assert(READ_ONCE(datum->x) == 1);

[michaliskok]

Thanks for the report.

The first example is an actual race. LKMM's race definition is complicated but, very roughly, in order for the two spin accesses not to be considered racy, the access performed by T0 needs to be "r-post-bounded", and smp_wmb() is not sufficient for that. Using an smp_mb() does make it "r-post-bounded", and thus the race no longer occurs.

For the second example, you are right that the assert should not fail. GenMC is missing some consistency checks for plain accesses. I'll see if I can do something about this in the next release.

Note that GenMC does not exactly follow the LKMM definition for data races due to some temporary accesses that clang generates. Since LKMM's definition utilizes dependencies in order to check whether two plain accesses are in a race or not (and temporaries affect the calculation of dependencies), the definition that GenMC follows is generally stronger than LKMM's (modulo the above bug and another one I believe I found).

Michalis

[db7]

The first example is an actual race. LKMM's race definition is complicated but, very roughly, in order for the two spin accesses not to be considered racy, the access performed by T0 needs to be "r-post-bounded", and smp_wmb() is not sufficient for that. Using an smp_mb() does make it "r-post-bounded", and thus the race no longer occurs.

I am a bit confused, sorry if I sound repetitive, but I would like to understand this a bit better.

If the spin accesses form a data race, then they cannot be ordered, right? In some executions T0 writes spin last, in others T1 writes spin last. I ran the (almost) same example in Herd7 with LKMM and these accesses have an order. Here is the example:

(* http://diy.inria.fr/www/# *)
C lkmm-race
{}

P0(int *x, int *y)
{
	*x = 1;
	smp_wmb();
	WRITE_ONCE(*y, 1);
}

P1(int *x, int *y)
{
	int r = 0;

	if (READ_ONCE(*y)) {
		smp_mb();
		*x = 2;
  		r = *x;
	}
}
exists (1:r1=0 \/ 1:r1=2)

The exists is always positive, ie, T1 never overwrites the T2's update to spin:

Test issue-35 Allowed
States 1
1:r1=0;
Ok
Witnesses
Positive: 2 Negative: 0
Flag data-race
Condition exists (1:r1=0 \/ 1:r1=2)
Observation issue-35 Always 2 0
Time issue-35 0.12
Hash=004242d45a51e1b5b8123c2c70c70202

The same thing in GenMC fails with non-atomic accesses:

#include <pthread.h>
#include <lkmm.h>
#include <assert.h>

int spin;
int lock;

void* run0(void *arg)
{
	spin = 1;
	//WRITE_ONCE(spin, 1);
	smp_wmb();
	WRITE_ONCE(lock, 1);
	return 0;
}

void *run1(void *arg)
{
	if (READ_ONCE(lock) != 0) {
		smp_mb();
		spin = 2;
		//WRITE_ONCE(spin, 2);
		assert (spin == 2);
		//assert (READ_ONCE(spin) == 2);
	}
	return 0;
}

int main()
{
	pthread_t t;
	pthread_create(&t, 0, run1, 0);
	run0(0);    
	pthread_join(t, 0);
	return 0;
}

$ genmc -mo -lkmm -disable-race-detection issue-35.c 
WARNING: LKMM support is still at an experimental stage!
Error detected: Safety violation!
Event (1, 4) in graph:
<-1, 0> main:
        (0, 0): B
        (0, 1): TC [forks 1] L.32
        (0, 2): Wna (spin, 1) L.10
        (0, 3): Fwmb L.12
        (0, 4): Wrlx (lock, 1) L.13
        (0, 5): TJ L.34
<0, 1> run1:
        (1, 0): B
        (1, 1): Rrlx (lock, 1) [(0, 4)] L.19
        (1, 2): Fmb L.20
        (1, 3): Wna (spin, 2) L.21
        (1, 4): Rna (spin, 1) [(0, 2)] L.23

Assertion violation: spin == 2
Number of complete executions explored: 1
Number of blocked executions seen: 1
Total wall-clock time: 0.01s

If we replace those accesses with READ_ONCE and WRITE_ONCE, GenMC does not report a race and the assert does not trigger. So I am confused why this is a genuine data race:

• Why can the barriers order the relaxed accesses but not the non-atomic ones? Is this due to the missing consistency checks?
• Assuming that this is due to the missing consistency checks, then the barriers should order the non-atomics (like in Herd7). But then why would the non-atomic accesses to spin be a race if they have an order?

[michaliskok]

There are two (orthogonal) issues: the data race detected by GenMC (which is an actual data race), and the missing consistency checks that lead to the safety violations.

I am a bit confused, sorry if I sound repetitive, but I would like to understand this a bit better.

If the spin accesses form a data race, then they cannot be ordered, right? In some executions T0 writes spin last, in others T1 writes spin last.

It is not merely about ordering, but also about being able to predict the outcome of a given piece of code in the presence of compiler optimizations.

When it comes to the plain store spin = 0 in your example, the compiler is theoretically allowed to transform it to if (spin != 0) spin = 0. So, even though the store spin = 0 is ordered wrt the write to y, the load that the compiler may introduce is not (an smp_wmb() is not enough). Is LKMM being too cautious? Probably. Still, according to the current definition, that is a race.

I ran the (almost) same example in Herd7 with LKMM and these accesses have an order. Here is the example:

[...]

The exists is always positive, ie, T1 never overwrites the T2's update to spin:

Test issue-35 Allowed
States 1
1:r1=0;
Ok
Witnesses
Positive: 2 Negative: 0
Flag data-race
Condition exists (1:r1=0 \/ 1:r1=2)
Observation issue-35 Always 2 0
Time issue-35 0.12
Hash=004242d45a51e1b5b8123c2c70c70202

herd reports a data race as well (see Flag data-race). (As a side note, the exists condition tests r1 which does not appear in the code.)

The same thing in GenMC fails with non-atomic accesses:

[...]

$ genmc -mo -lkmm -disable-race-detection issue-35.c 
WARNING: LKMM support is still at an experimental stage!
Error detected: Safety violation!
Event (1, 4) in graph:
<-1, 0> main:
        (0, 0): B
        (0, 1): TC [forks 1] L.32
        (0, 2): Wna (spin, 1) L.10
        (0, 3): Fwmb L.12
        (0, 4): Wrlx (lock, 1) L.13
        (0, 5): TJ L.34
<0, 1> run1:
        (1, 0): B
        (1, 1): Rrlx (lock, 1) [(0, 4)] L.19
        (1, 2): Fmb L.20
        (1, 3): Wna (spin, 2) L.21
        (1, 4): Rna (spin, 1) [(0, 2)] L.23

Assertion violation: spin == 2
Number of complete executions explored: 1
Number of blocked executions seen: 1
Total wall-clock time: 0.01s

The reported error is not a race though: it is a safety violation. And it is the same (buggy) report than GenMC produces in your previous LWN example. This is due to the missing consistency checks and I need to fix it (i.e., it shouldn't fire).

Michalis

[db7]

Thanks for the detailed answer. I was thinking that this safety violation would be a consequence of the data race. The example of the compiler transforming the store to something like if (spin != 0) spin = 0 was helpful.

It is weird that, on the one hand, LKMM has such careful data race definition, and, on the other, Linux qspinlock has exactly this (LKMM) data race. I wonder if Linux developers would consider that as a bug or simply ignore the data race.

[michaliskok]

Does it? I don't recall the details off the top of my head, but the code should use WRITE_ONCE/READ_ONCE when manipulating key fields of the lock (e.g., locked, pending, etc). If that's the case, then the code is non-racy, as the compiler is not allowed to optimize such accesses (and this is also why GenMC does not report a race when you use {WRITE,READ}_ONCE for spin with race detection enabled).

Just in case this is unclear, in LKMM you can have both plain and "marked" accesses to non-annotated variables like spin. The data-race definition applies for plain accesses only, i.e., it does not apply if accesses are marked with WRITE_ONCE/READ_ONCE.

[db7]

Does it? I don't recall the details off the top of my head, but the code should use WRITE_ONCE/READ_ONCE when manipulating key fields of the lock (e.g., locked, pending, etc).

MCS node initialization in the slowpath (see here)

node->locked = 0;
node->next = NULL;
pv_init_node(node);

After changing the tail, node is then written in tail->next with WRITE_ONCE here.
Between the the write to node->locked and the update of tail->next there is an smp_wmb.

The current lock owner updates node->locked with smp_store_release here.

GenMC detects a race there beyond other problems that seem to be related to the missing consistency checks.

[vafeiadis]

The first example is an actual race. LKMM's race definition is complicated but, very roughly, in order for the two spin accesses not to be considered racy, the access performed by T0 needs to be "r-post-bounded", and smp_wmb() is not sufficient for that.

Specifically, the following part of https://github.com/herd/herdtools7/blob/master/catalogue/linux/cats/linux-kernel.cat is responsible for the race.

let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; [Marked]
let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded)
let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis)
let ww-race = (pre-race & co) \ ww-nonrace
[...]
flag ~empty (ww-race | wr-race | rw-race) as data-race

To me, it seems to be a bug in the LKMM definition: ww-nonrace should simply have been defined to be ww-vis.

[michaliskok]

I also thought it’s a bug in the definition in the beginning, but the accompanying manual explicitly says that it needs to be r-post-bounded as well, giving a justification similar to the one I posted above. I’m ooo right now, but will post a link when I get back.

[michaliskok]

As promised: L2232 -- L2248

[db7]

This seems to be related to this issue, but with respect to smp_rmb():

#include <pthread.h>
#include <lkmm.h>
#include <assert.h>
#define NTHREADS  2

atomic_t ticket;
int grant;
unsigned int shared;

// https://elixir.bootlin.com/linux/latest/source/include/asm-generic/barrier.h#L191
#define smp_acquire__after_ctrl_dep()		smp_rmb()

void *run(void *arg) {
	/* LOCK ACQUIRE */ 
	int t = atomic_fetch_add_relaxed(1, &ticket);
	while (READ_ONCE(grant) != t) {}
	smp_acquire__after_ctrl_dep();
	/* According to barrier.h#L232, the control dependency + smp_rmb() are
	 * equivalent to an acquire barrier. However, genmc detects races in the
	 * critical section. */

	/* CRITICAL SECTION */
	shared++;

	/* LOCK RELEASE */
	smp_store_release(&grant, READ_ONCE(grant)+1);
	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(shared == NTHREADS);
	return 0;
}

And this (possibly) incorrect error message:

$ genmc -mo -lkmm test.c
WARNING: LKMM support is still at an experimental stage!
Error detected: Non-Atomic race!
Event (2, 6) conflicts with event (1, 5) in graph:
<-1, 0> main:
        (0, 0): B
        (0, 1): M
        (0, 2): TC [forks 1] L.32
        (0, 3): Wna (t[0], 1) L.32
        (0, 4): TC [forks 2] L.32
        (0, 5): Wna (t[1], 2) L.32
        (0, 6): Rna (t[0], 1) [(0, 3)] L.33
        (0, 7): TJ L.33
        (0, 8): Rna (t[1], 2) [(0, 5)] L.33
        (0, 9): TJ L.33
<0, 1> run:
        (1, 0): B
        (1, 1): Urlx (ticket.counter, 0) [INIT] L.15
        (1, 2): Urlx (ticket.counter, 1) L.15
        (1, 3): Rrlx (grant, 0) [INIT] L.16
        (1, 4): Frmb L.17
        (1, 5): Rna (shared, 0) [INIT] L.23
        (1, 6): Wna (shared, 1) L.23
        (1, 7): Rrlx (grant, 0) [INIT] L.26
        (1, 8): Wrel (grant, 1) L.26
        (1, 9): E
<0, 2> run:
        (2, 0): B
        (2, 1): Urlx (ticket.counter, 1) [(1, 2)] L.15
        (2, 2): Urlx (ticket.counter, 2) L.15
        (2, 3): Rrlx (grant, 1) [(1, 8)] L.16
        (2, 4): Frmb L.17
        (2, 5): Rna (shared, 1) [(1, 6)] L.23
        (2, 6): Wna (shared, 2) L.23

Number of complete executions explored: 0
Number of blocked executions seen: 1
Total wall-clock time: 0.02s

If this is not incorrect, and it is a genuine data race, then the LKMM definition of data race is really weird.

Also, if we disable race detection, the assert fails. That must be related to the missing checks you mentioned above.

[michaliskok]

If this is not incorrect, and it is a genuine data race, then the LKMM definition of data race is really weird.

Judging by a quick look, I believe this is the other bug I mentioned a few messages back:

[...] the definition that GenMC follows is generally stronger than LKMM's (modulo the above bug and another one I believe I found).

GenMC does not take the smp_rmb() into account when checking whether an event is r-{post,pre}-bounded, hence the race report.

Also, if we disable race detection, the assert fails. That must be related to the missing checks you mentioned above.

Indeed. Let me try to work out a fix for all the issues and then see if the next version behaves weirdly.

Michalis