Re:Google Is Uncovering Hundreds of Race Conditions Within t...
by schoen on Thursday October 03, 2019 @02:42PM
(#21150497)
Thanks for the tremendous detail on this point.
Could you or someone else please give a minimal example of an undefined access in C, just so that I can be sure of whether we're talking about the same phenomena here?
Re:Google Is Uncovering Hundreds of Race Conditions Within t...
by jcranmer on Thursday October 03, 2019 @03:15PM
(#21150903)
A minimal program (using C11 threads):
#include <threads.h>
int x;
int do_thread(void *) {
for (int i = 0; i < 10000; i++)
x = i;
return 0;
}
int main() {
thrd_t t;
thrd_create(&t, do_thread, NULL);
do_thread(NULL);
thrd_join(&t, NULL);
return 0;
}
Data races are one of those cases where "anything may go" undefined behavior is actually quite necessary. Actual hardware memory models (particularly on "weak" architectures like ARM or PowerPC, or especially the infamously weak Alpha) result in cases where the order of memory traffic is not a consistent view between different threads. Formally specifying the hardware memory model is actually surprisingly difficult, made all the more difficult when you want to give a hardware-agnostic definition [1]. And should you want to introduce hardware transactional memory, break down in despair at the complexity [2].
The great breakthrough in memory models is the definition of the "data-race-free" model. This model says that, if memory accesses are properly protected with locks (i.e., there are no "data races" [3]), you cannot observe a violation of sequential consistency, which makes reasoning much easier. Java used this model for its corrected memory model in Java 5, and then C++11 adapted Java's memory model, and C11 took C++11's model verbatim. The upshot of this approach is that, if you make data races undefined behavior, you don't have to try to figure out how typical memory optimizations, both by the compiler and by the physical hardware, affect visible memory. Trying to work out the effects of these optimizations on the memory system is extraordinarily difficult, and the benefits of doing so are manifestly unclear, since most programmers will need to properly synchronize their code anyways.
[1] The C++ memory model attempts to do this with atomic memory references. The resulting specification (in C++11) is generally considered to be wrong, and the question of how to fix it is still up in the air as of right now.
[2] PLDI 2018 had the first formal semantics that combined transactional memory and weak memory semantics, and went on to prove that ARM's hardware lock elision was broken. This should be showing just how difficult this is to grasp even for theoreticians pushing the boundary, let alone a language trying to make it accessible to typical programmers.
[3] There are two definitions of "data race" going on here. Vernacular definitions usually define it as accesses not protected by synchronization, which permit "benign" data races for regular loads/stores. C/C++ tweaks the definition so as to use it to proscribe undefined behavior, so "benign" data race is oxymoronic in those languages. However, the use of memory_order_relaxed is intended to indicate a permitted data race in the first sense but not the second sense.