Delivering identical messages VS writing identical tuples in an ETS table

Receive

1) P: ets:insert(table, {x, 1})
2) P: R ! ok
3) Q: R ! ok
4) R: receives ok (from P)
5) R: ets:lookup(table, x)

If 2) and 3) are not in a race, then we cannot discover that there is a way for 5) to read a value different from 1 (there are no other races in this program, cause 1) -> 2) -> 4) -> 5) is ordered by happens-before).

ETS insert

7) P: ets:insert(table, {x, 1})
8) P: ets:insert(table, {y, 1})
10) Q: ets:insert(table, {y, 1})
12) R: ets:lookup(table, y)
13) R: ets:lookup(table, x)

Here we can declare that 2) and 3) are not in a race, but we must encode that 3) happens-before 4) so that the necessary value for y is available when reversing the race 2) - 4).