(relaxed hardware memory models) has been established with SC for data race-free programs (SC-for-DRF) [@Hill:DRF:SC]. Informally, a program has a data race if two tasks access the same memory location, at least one of them is a write, and there are no intervening synchronization operations that would order the accesses. “SC-for-DRF” requires programmers to ensure that programs are free of data races under SC. In turn, the relaxed memory model of a SC-for-DRF CPU guarantees SC for all executions of such a program.

It has been acknowledged in the literature [@Boehm:mem:survey] that Ada 83 was perhaps the first widely-use high-level programming language to provide first-class support for shared-memory programming. The approach taken with Ada 83 and later language revisions was to require legal programs to be without synchronization errors, which is the approach taken with SC-for-DRF. In contrast, for the Java memory model it was perceived that even programs with synchronization errors shall have defined semantics for reasons of safety and security of Java’s sand-boxed execution environment. (We do not consider this approach in the remainder of this paper, because it does not align with Ada’s current approach to regard the semantics of programs with synchronization errors as undefined, i.e., 