@@ -1987,28 +1987,36 @@ outcome undefined.
1987
1987
1988
1988
In technical terms, the compiler is allowed to assume that when the
1989
1989
program executes, there will not be any data races. A "data race"
1990
- occurs when two conflicting memory accesses execute concurrently;
1991
- two memory accesses "conflict" if:
1990
+ occurs when there are two memory accesses such that:
1992
1991
1993
- they access the same location,
1992
+ 1. they access the same location,
1994
1993
1995
- they occur on different CPUs (or in different threads on the
1996
- same CPU),
1994
+ 2. at least one of them is a store,
1997
1995
1998
- at least one of them is a plain access ,
1996
+ 3. at least one of them is plain,
1999
1997
2000
- and at least one of them is a store.
1998
+ 4. they occur on different CPUs (or in different threads on the
1999
+ same CPU), and
2001
2000
2002
- The LKMM tries to determine whether a program contains two conflicting
2003
- accesses which may execute concurrently; if it does then the LKMM says
2004
- there is a potential data race and makes no predictions about the
2005
- program's outcome.
2001
+ 5. they execute concurrently.
2006
2002
2007
- Determining whether two accesses conflict is easy; you can see that
2008
- all the concepts involved in the definition above are already part of
2009
- the memory model. The hard part is telling whether they may execute
2010
- concurrently. The LKMM takes a conservative attitude, assuming that
2011
- accesses may be concurrent unless it can prove they cannot.
2003
+ In the literature, two accesses are said to "conflict" if they satisfy
2004
+ 1 and 2 above. We'll go a little farther and say that two accesses
2005
+ are "race candidates" if they satisfy 1 - 4. Thus, whether or not two
2006
+ race candidates actually do race in a given execution depends on
2007
+ whether they are concurrent.
2008
+
2009
+ The LKMM tries to determine whether a program contains race candidates
2010
+ which may execute concurrently; if it does then the LKMM says there is
2011
+ a potential data race and makes no predictions about the program's
2012
+ outcome.
2013
+
2014
+ Determining whether two accesses are race candidates is easy; you can
2015
+ see that all the concepts involved in the definition above are already
2016
+ part of the memory model. The hard part is telling whether they may
2017
+ execute concurrently. The LKMM takes a conservative attitude,
2018
+ assuming that accesses may be concurrent unless it can prove they
2019
+ are not.
2012
2020
2013
2021
If two memory accesses aren't concurrent then one must execute before
2014
2022
the other. Therefore the LKMM decides two accesses aren't concurrent
@@ -2171,8 +2179,8 @@ again, now using plain accesses for buf:
2171
2179
}
2172
2180
2173
2181
This program does not contain a data race. Although the U and V
2174
- accesses conflict , the LKMM can prove they are not concurrent as
2175
- follows:
2182
+ accesses are race candidates , the LKMM can prove they are not
2183
+ concurrent as follows:
2176
2184
2177
2185
The smp_wmb() fence in P0 is both a compiler barrier and a
2178
2186
cumul-fence. It guarantees that no matter what hash of
@@ -2326,12 +2334,11 @@ could now perform the load of x before the load of ptr (there might be
2326
2334
a control dependency but no address dependency at the machine level).
2327
2335
2328
2336
Finally, it turns out there is a situation in which a plain write does
2329
- not need to be w-post-bounded: when it is separated from the
2330
- conflicting access by a fence. At first glance this may seem
2331
- impossible. After all, to be conflicting the second access has to be
2332
- on a different CPU from the first, and fences don't link events on
2333
- different CPUs. Well, normal fences don't -- but rcu-fence can!
2334
- Here's an example:
2337
+ not need to be w-post-bounded: when it is separated from the other
2338
+ race-candidate access by a fence. At first glance this may seem
2339
+ impossible. After all, to be race candidates the two accesses must
2340
+ be on different CPUs, and fences don't link events on different CPUs.
2341
+ Well, normal fences don't -- but rcu-fence can! Here's an example:
2335
2342
2336
2343
int x, y;
2337
2344
@@ -2367,7 +2374,7 @@ concurrent and there is no race, even though P1's plain store to y
2367
2374
isn't w-post-bounded by any marked accesses.
2368
2375
2369
2376
Putting all this material together yields the following picture. For
2370
- two conflicting stores W and W', where W ->co W', the LKMM says the
2377
+ race-candidate stores W and W', where W ->co W', the LKMM says the
2371
2378
stores don't race if W can be linked to W' by a
2372
2379
2373
2380
w-post-bounded ; vis ; w-pre-bounded
@@ -2380,8 +2387,8 @@ sequence, and if W' is plain then they also have to be linked by a
2380
2387
2381
2388
w-post-bounded ; vis ; r-pre-bounded
2382
2389
2383
- sequence. For a conflicting load R and store W, the LKMM says the two
2384
- accesses don't race if R can be linked to W by an
2390
+ sequence. For race-candidate load R and store W, the LKMM says the
2391
+ two accesses don't race if R can be linked to W by an
2385
2392
2386
2393
r-post-bounded ; xb* ; w-pre-bounded
2387
2394
@@ -2413,20 +2420,20 @@ is, the rules governing the memory subsystem's choice of a store to
2413
2420
satisfy a load request and its determination of where a store will
2414
2421
fall in the coherence order):
2415
2422
2416
- If R and W conflict and it is possible to link R to W by one
2417
- of the xb* sequences listed above, then W ->rfe R is not
2418
- allowed (i.e., a load cannot read from a store that it
2423
+ If R and W are race candidates and it is possible to link R to
2424
+ W by one of the xb* sequences listed above, then W ->rfe R is
2425
+ not allowed (i.e., a load cannot read from a store that it
2419
2426
executes before, even if one or both is plain).
2420
2427
2421
- If W and R conflict and it is possible to link W to R by one
2422
- of the vis sequences listed above, then R ->fre W is not
2423
- allowed (i.e., if a store is visible to a load then the load
2424
- must read from that store or one coherence-after it).
2428
+ If W and R are race candidates and it is possible to link W to
2429
+ R by one of the vis sequences listed above, then R ->fre W is
2430
+ not allowed (i.e., if a store is visible to a load then the
2431
+ load must read from that store or one coherence-after it).
2425
2432
2426
- If W and W' conflict and it is possible to link W to W' by one
2427
- of the vis sequences listed above, then W' ->co W is not
2428
- allowed (i.e., if one store is visible to a second then the
2429
- second must come after the first in the coherence order).
2433
+ If W and W' are race candidates and it is possible to link W
2434
+ to W' by one of the vis sequences listed above, then W' ->co W
2435
+ is not allowed (i.e., if one store is visible to a second then
2436
+ the second must come after the first in the coherence order).
2430
2437
2431
2438
This is the extent to which the LKMM deals with plain accesses.
2432
2439
Perhaps it could say more (for example, plain accesses might
0 commit comments