Confusion about "CoRR" (Coherence for Read-Read pairs) in RVWMO.

[diantaowang]

The original text is as follows:

• Overlapping-Address Orderings:
  • b is a store, and a and b access overlapping memory addresses
  • a and b are loads, x is a byte read by both a and b, there is no store to x between a and b in program order, and a and b return values for x written by different memory operations
  • a is generated by an AMO or SC instruction, b is a load, and b returns a value written by a

I can't understand the rule-2 (the load-load situation).

• “...between a and b in program order...”. What the meaning of "program order"? Furthermore, does it refers to the program order on a single hart, or the program order on all harts? I think it refers to the program order on a single hart.
• In which case a back-to-back loads will return values for x written by different memory operations? Please give an example.

I guess that:

hart0	hart1
(a) li t0, 2	(c) li t0, 1
(b) sw t0,0(s0)	(d) sw t0,0(s0)
	(e) lw a0,0(s0)
	(f) lw a1,0(s0)

Global memory order (d)(f)(b)(e) is prohibited because (e) and (f) return values from the same address written by different memory operations.

Thanks!

[aswaterman]

"Program order" is the sequence of a single hart's dynamic instruction stream.

The example you gave is more complicated than is necessary to demonstrate the CoRR requirement. Consider this simpler one:

hart 0	hart 1
(a) li t0, 1	(c) lw a0,0(s0)
(b) sw t0,0(s0)	(d) lw a1,0(s0)

The three legal outcomes are a0=a1=0, a0=a1=1, and a0=0/a1=1. a0=1/a1=0 is not a legal outcome because (c) precedes (d) in the global memory order.

[diantaowang]

Thanks! I got it.