Page 1 of 1

claim that relaxed consistency can sometimes be ignored

Posted: Mon Sep 03, 2018 7:39 am
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.