claim that relaxed consistency can sometimes be ignored

OpenMP 5.0 will be the next version of the OpenMP specification, which we expect will be officially released in 2018. This technical report is the latest draft of the 5.0 specs for public discussion.
Forum rules
The OpenMP Forums are now closed to new posts. Please visit Stack Overflow if you are in need of help:
Posts: 12
Joined: Mon Mar 24, 2014 4:47 pm

claim that relaxed consistency can sometimes be ignored

Post by sfsiegel »

Sec. 1.4.6, p28:

"OpenMP programs that:
• do not use non-sequentially consistent atomic directives,
• do not rely on the accuracy of a false result from omp_test_lock
and omp_test_nest_lock, and
• correctly avoid data races as required in Section 1.4.1 on page 22
behave as though operations on shared variables were simply
interleaved in an order consistent with the order in which they are
performed by each thread. The relaxed consistency model is invisible
for such programs, and any explicit flush operations in such programs
are redundant."

Is this supposed to be a theorem that follows from the other
constraints specified in this Specification, or is it a new
constraint? It would be helpful to clarify which is the case. Also, if
it is supposed to follow from other constraints, it would be helpful
to sketch a proof, or at least give some intuition on why it is true.