[herd] Consequences of splitting exclusive effects from the X events set (PR #1889)

[maranget]

This PR groups three commits

1. Fixing the RISCV model (and the collect_atomics function from memUtils.ml)
2. Add some RISCV tests that check the problem fixed in 1.
3. Fix the computation of "atomic pairs" in OCaml, this computation was wrong before PR [herd] Split exclusive accesses from the X event set #1889: the cases of AMO's and exclusive accessed were not separated as they should be.

As to 3., notice that, since PR #1889, there is no need to compute atomic pairs in OCaml for AArch64 and possibly for all Cat model (perhaps at the price of a small optimisation of -optace iico). Implementation of limiting the usage of the OCaml code for atomic pairs not being that straightforward, we leave that to a further PR.

[HadrienRenaud]

Maybe good to add that this would not work for AArch64 because it only constructs pairs at the same location? And that it constructs pairs that have an interleaving read at a different location?

Suggested change

	* between the read and the write.
	* between the read and the write. Notice that the pairs generated here
	* have the same location. Notice that the pairs generated do not check
	* for the presence of an interleaving read at another location.

I do not know if the riscv semantics in herd prevent those cases from happening, or if those cases are not a problem for riscv, but I thought it would be important to flag this.
If this is a problem for riscv, it can be left as a subsequent PR, or an open issue, as this behaviour was present before this PR.

[maranget]

I do not understand "This would not work for AArch64 [...]".

As for the presence of an interleaving (exclusive) read at another location, we should at least add a test. At the moment, the current code pairs LDXR [x] abd STXR [x] in LDXR [x]; LDXR [y]; STXR [x] (The STXR [x] can succeed and generate a write effect in spite of the reservation being to y). This contradicts the Cat definition of lxsx:

let lxsx = [R&EX]; po \ (p; [M&EX]; po); [W&EX]

Namely, the Cat definition does not pair LDXR [x] and STXR [X], due to the interleaving exclusive read on y (po; [M&EX]; po above).

[maranget]

Here is the test:

AArch64 LXSX0C
{
0:X0=x;
0:X2=y;
0:X1=1;
1:X0=x;
1:X1=2;
}
  P0             | P1          ;
 LDXR W3,[X0]    | STR W1,[X0] ;
 LDXR W5,[X2]    |             ;
 STXR W7,W1,[X0] |             ;
exists 0:X3=0 /\ [x]=1

Diagram made with PR #1896.

[maranget]

This test is observed on a variety of machines with option -mode presi.

[HadrienRenaud]

This contradicts the Cat definition of lxsx

My comment was exactly this: we should document that what this ocaml code computes is not in sync with the cat definition of lxsx, and would roughly correspond to the following definition:

let lxsx' =
  let poloc = po & loc in
  [R&EX]; poloc \ (poloc; [M&EX]; poloc); [W&EX]

As far as I understand, this does not have any consequences for AArch64, because the results of this algorithm are overridden by the cat definition. However, maybe it has a consequence for riscv because the results of this algorithm are used to compute ppo?

---

This test is observed on a variety of machines with option -mode presi.

I'm not familiar with the -mode presi, could you explain what this means?

---

we should at least add a test

Agreed. Please do add it!

[maranget]

My idea would rather be to have OCaml and Cat to compute the same lxsx. Stay tuned.

I suspect that the test succeeds when x and y are in the same cache line or, less precisely, when their addresses are close. In mode -mode presi x and y are either in the same cache line or in successive cache lines. In standard mode, x and y are close with small size parameter (e.g. -s 4). This "x and y are close" assumption is compatible with experiments.

This test is for PR #1896, it would fail here.

[relokin]

My idea would rather be to have OCaml and Cat to compute the same lxsx. Stay tuned.

I haven't had a look at the code yet, but is this about lxsx only or about the whole of rmw?

What is the benefit in having this ability? The Ocaml code is relatively complex and evidently hard to get right.

Also is the idea that both calculations would be enabled at the same time?

[maranget]

Hi @relokin. You are right, this PR lacks motivation. At the moment the OCaml code for computing lxsx, amo and rmw as lxsx|amo is still useful

1. For the few, legacy, non-cat models
2. For optimisations (as far as I have checked, for -optace iico|true)
3. For computing dependencies in OCaml, which applies to all models except aarch64.cat

We have to keep the code for 1. alone, we can probably get rid of 2. and 3. is still unclear to me. I plan to look at this when I am back at the end of July. But before, I'd like to have the OCaml code to match the Cat definitions.

[HadrienRenaud]

Isn't this just EventRel.of_pred es es E.po_strict?

Suggested change

	let po =
	let rec do_rec k = function
	| [] -> E.EventRel.of_list k
	| e0::es ->
	let k =
	List.fold_left
	(fun k e ->
	if E.po_strict e0 e then (e0,e)::k
	else if E.po_strict e e0 then (e,e0)::k
	else k)
	k es in
	do_rec k es in
	do_rec [] evts in
	let po = E.EventRel.of_pred es es E.po_strict in

[maranget]

Because es is a list and not a set....

[maranget]

Admittedly, I could have written a function fold_pairs_once in misc.ml.

[maranget]

Thanks @HadrienRenaud and @relokin, merging.