Skip to content

Commit fc13b47

Browse files
paulhdkpaulmckrcu
authored andcommitted
tools/memory-model: Weaken ctrl dependency definition in explanation.txt
The current informal control dependency definition in explanation.txt is too broad and, as discussed, needs to be updated. Consider the following example: > if(READ_ONCE(x)) > return 42; > > WRITE_ONCE(y, 42); > > return 21; The read event determines whether the write event will be executed "at all" - as per the current definition - but the formal LKMM does not recognize this as a control dependency. Introduce a new definition which includes the requirement for the second memory access event to syntactically lie within the arm of a non-loop conditional. Link: https://lore.kernel.org/all/[email protected]/ Cc: Marco Elver <[email protected]> Cc: Charalampos Mainas <[email protected]> Cc: Pramod Bhatotia <[email protected]> Cc: Soham Chakraborty <[email protected]> Cc: Martin Fink <[email protected]> Co-developed-by: Alan Stern <[email protected]> Signed-off-by: Alan Stern <[email protected]> Signed-off-by: Paul Heidekrüger <[email protected]> Signed-off-by: Paul E. McKenney <[email protected]>
1 parent 9abf231 commit fc13b47

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

tools/memory-model/Documentation/explanation.txt

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -464,9 +464,10 @@ to address dependencies, since the address of a location accessed
464464
through a pointer will depend on the value read earlier from that
465465
pointer.
466466

467-
Finally, a read event and another memory access event are linked by a
468-
control dependency if the value obtained by the read affects whether
469-
the second event is executed at all. Simple example:
467+
Finally, a read event X and a write event Y are linked by a control
468+
dependency if Y syntactically lies within an arm of an if statement and
469+
X affects the evaluation of the if condition via a data or address
470+
dependency (or similarly for a switch statement). Simple example:
470471

471472
int x, y;
472473

0 commit comments

Comments
 (0)