Data Race Handling

[coolmax3002]

When examining the lock implementations in the benchmarks directory, I noticed that threads often interact with non-atomic integers. In multi-threaded programs, using non-atomic variables can lead to data races. Given that Dat3M tests the validity of executions under different memory models and architectures, how does Dat3M handle data races?

cc: @camillegandotra, @reeselevine, @tyler-utah

[hernanponcedeleon]

Hi @coolmax3002

The benchmarks in the folder consist of two parts: (1) the implementation of the algorithm API, and (2) a client using the API.

Part (1) is implemented in the *.h files and it mostly uses atomic accesses (there are a few exceptions, like non atomically writing the fields of some node and make the node visible to other threads via an atomic operation, normally a CAS).

Part (2) is implemented in the *.c files and, as you said, will use non atomic variables, like the ones inside the lock critical section.

There are 3 properties you can check with dat3m: safety (i.e. assertions), liveness, and things that can be specified in the cat file (data races fit here, see e.g. here). By default dat3m only checks for assertions. You can enable all 3 properties by using --property=program_spec,cat_spec,liveness (or a subset of them).

Data races only make sense at the programming language level, that is why hardware memory models do not have a definition of data races in their cat file. If you want to check for data races, you should use either rc11, vmm or linux-kernel cat files. In principle c11.cat could also have a definition of races, but since the model has many known issues, we never used it that much. If you really need to use this one, let me know and I'll try to add the race definition there.

[ThomasHaas]

Data races only make sense at the programming language level, that is why hardware memory models do not have a definition of data races in their cat file. If you want to check for data races, you should use either rc11, vmm or linux-kernel cat files. In principle c11.cat could also have a definition of races, but since the model has many known issues, we never used it that much. If you really need to use this one, let me know and I'll try to add the race definition there.

We could also extend IMM with the race definition from RC11. I think IMM is the most canonical model when checking C-code and so it would make sense if that one also covered data races.

[hernanponcedeleon]

We could also extend IMM with the race definition from RC11. I think IMM is the most canonical model when checking C-code and so it would make sense if that one also covered data races.

I disagree here. IMM is supposed to be a wrapper for hardware models, and as such, the notion of data races does not make sense for this model. I think this is exactly why genmc (the other tool that uses IMM) does not check for races in IMM.

[ThomasHaas]

Ok, philosophically I buy this argument, but I'm wondering what would go wrong in practice if you added races to IMM.
I mean, IMM and RC11 would (likely) report the same races on the same C-code (cause they have the exact same definition of hb), yet if IMM does it, it's not valid because "it is a hardware model"? If that is the only argument, then I call bullshit :P.
I think there must be a deeper reason of why IMM has no race definition.

From a practicioners point of view, what models would you use to make sure your code is correct? You cannot use lkmm, because your code is no linux code. You cannot use rc11, because compilers don't preserve rc11 correctness and you cannot use imm because it lacks races. Depending on your intended compilation targets, you cannot use vmm either.
The full c11 model is also questionable.
It seems to me that your best bet is to use imm for safety/liveness and then separately use rc11 for data races.
A case in point for why having a combined "imm + races" model would be useful (even if theoretically/philosophically improper).

[hernanponcedeleon]

It seems to me that your best bet is to use imm for safety/liveness and then separately use rc11 for data races.

This is what the VSync project has been doing for quite some time due to lack of a better alternative. However, now that dartagnan is integrated into the vsyncer tool and we can properly use the vmm model (which does not have the limitations of rc11 and it has a definition of data races), we are slowly moving to use this model.

As you mentioned, this has the drawback that vmm is missing some compilation targets (e.g., power; @db7 @JonasOberhauser please correct me if I am wrong here). From a practitioner point of view, I would claim this currently the best option, but I am obviously biased here.

[reeselevine]

Ah ok, and it's because Dartagnan operates directly on the source files that it doesn't have to worry about UB caused by data races in the C code when running against the language models? And for the hardware models it assumes the C code is being run "as is" on the hardware?

It does seem a little strange to be checking for safety and liveness against a program that may be undefined completely according to the model, but using RC11 for data races and a hardware model for the other properties does seem like the most sound option. That's also why we were thinking of writing some versions of the benchmarks that use only atomics in the critical sections, so we can still check assertions in the language models without having to worry about data races.

[hernanponcedeleon]

Ah ok, and it's because Dartagnan operates directly on the source files that it doesn't have to worry about UB caused by data races in the C code when running against the language models? And for the hardware models it assumes the C code is being run "as is" on the hardware?

This is only partially true. Dartagnan operates at the LLVM-IR level so if the original C program has data races (or any other UB) the IR dartagnan gets might already be semantically different than the C code. We do use some compiler optimisations (those set in the OPTFLAGS env variable). Here we try to balance between making the life of dartagnan easier and avoiding unsound transformations, but at the end of the day we don't have 100% guarantees. When I get results that do not make sense to me, I simply set OPTFLAGS="" and if I get different verification results, then 99% chances there is UB.

It does seem a little strange to be checking for safety and liveness against a program that may be undefined completely according to the model, but using RC11 for data races and a hardware model for the other properties does seem like the most sound option.

In principle you are right that if the program has UB, we cannot make any claim about the other properties.

That's also why we were thinking of writing some versions of the benchmarks that use only atomics in the critical sections, so we can still check assertions in the language models without having to worry about data races.

If I understood @camillegandotra correctly, you are also exploring relaxed versions of the locks which do not guarantee mutual exclusion (and can thus be racy). If this is the case, then yes, probably you want to use atomics in the critical section to avoid UB.

[ThomasHaas]

We compile the C-code to LLVM and apply minor optimizations but none of which rely on data-race freedom.
In particular, no optimization eliminates data races. That is why the lock benchmarks of the form:

lock();
x = 5;
assert (x == 5);
unlock();

do not get trivialized to assert(true) even if the lock was broken (i.e., using relaxed atomics). Another way to avoid such optimizations is to mark the non-atomic variables volatile. Either way, the compiler will not hide the race and thus Dartagnan can find it.
That being said, if we check for safety/liveness in a racy program, we also do so under the assumption that the compiler is "nice" and keeps the program as is. So it could be the case that we judge a racy program safe but if you would compile it with optimizations the resulting program becomes unsafe.
For example, Dartagnan would say the following racy program is safe

T1:
x = 0xFF00;
T2
x = 0x00FF;
T3:
assert x != 0xFFFF

however, the compiler could theoretically split the 2-byte read into two 1-byte reads that each observe a different store and thus possibly see a combination of both writes.

[db7]

If I understood @camillegandotra correctly, you are also exploring relaxed versions of the locks which do not guarantee mutual exclusion (and can thus be racy). If this is the case, then yes, probably you want to use atomics in the critical section to avoid UB.

IIRC, the definition of sta races in VMM should take that into account up to some point, for example, racy accesses protected with seqlock are not data races.

[JonasOberhauser]

I mean, IMM and RC11 would (likely) report the same races on the same C-code (cause they have the exact same definition of hb)

Some RC11 graphs would never occur on IMM and vice versa, which would already be enough to get different data races.

The real IMM does not have a notion of non-atomic and therefore can't define races, and if you do add non-atomics, you have to think about what that means for ar.

In GenMC, non-atomics have historically been "broken" w.r.t. ar, for example a fence wouldn't order them at all.

Let's say you add them to ar though, then the hb definition of data race is also bogus for IMM, since the ar would prevent certain races (in the sense of preventing one of the two orders, i.e., there's no graph in which the events happen in another order) but you'd still be flagged for a data race.

And if you do add ar to the data race definition somehow, then you're likely to be unsound at the language level because of the compiler optimizations that IMM disallows.

Either way the results are unlikely to be perfect, even in practice.

[JonasOberhauser]

In particular, no optimization eliminates data races.

How sure are you about that? Do you have a full model of what the optimizations that you have enabled can do?

[JonasOberhauser]

If I understood @camillegandotra correctly, you are also exploring relaxed versions of the locks which do not guarantee mutual exclusion (and can thus be racy). If this is the case, then yes, probably you want to use atomics in the critical section to avoid UB.

IIRC, the definition of sta races in VMM should take that into account up to some point, for example, racy accesses protected with seqlock are not data races.

Yes, in VMM having well-formed races on non-atomics is completely fine.

[ThomasHaas]

In particular, no optimization eliminates data races.

How sure are you about that? Do you have a full model of what the optimizations that you have enabled can do?

Ok, fair enough. We currently run a CSE pass (*) that can eliminate "redundant" loads and actually will in the lock examples unless the plain accesses are volatile. All the other passes are related to simplifying control-flow structure and should neither eliminate memory operations(**) nor move them around (if the LLVM documentation is to be trusted).

(*) Technically we run nothing automatically. The passes are specified in an environment variable and we "just recommend" to enable CSE. @hernanponcedeleon have you tested how verification times are affected when disabling CSE?

(**) Well, we run mem2reg which obviously eliminates a lot of memory accesses but those cannot race obviously. Now, it may introduce dependencies due to essentially changing rfi to data, but RC11 doesn't care about dependencies anyways and LKMM/VMM are careful to include rfi in their dependency definitions.

[hernanponcedeleon]

(*) Technically we run nothing automatically. The passes are specified in an environment variable and we "just recommend" to enable CSE. @hernanponcedeleon have you tested how verification times are affected when disabling CSE?

I never did a fine-grained analysis of how each of the passes we recommend affect performance. However, based on some testing I did last week, it is not even clear if running these optimizations is helpful compared with simply annotating statics loops to be fully unrolled.

[hernanponcedeleon]

@coolmax3002 @reeselevine are there any open questions about this or can I close?

[hernanponcedeleon]

@coolmax3002 confirmed by email this could be closed.