[herd,asl] Fix ambiguous PC writes

[HadrienRenaud]

This PR cherry picks a commit from #1735 that introduces some checks on the coherence of writes, and fixes the problems highlighted from those checks.

PC handling in ASL+herd

The aarch64 handwritten semantics in herd handle the program counter differently from the ASL code: the ASL code has an explicit PC register, whereas the handwritten semantics rely on po and BCC branching events.

We had introduced in #711 an AArch64 PC register in ASL to support the ASL code that uses it.
This implementation wrote 2 times to the PC:

1. First at the beginning of the instruction to correctly initialize the PC value
2. Secondly when the branching is committed and we actually increments the PC

This poses a few problems, mainly because the current herd algorithm does not handle multiple writes at the same register in a single instruction.

We thus remove the translation of the PC accesses, replaced here by a BCC commit event in case of a write. This leaves implicit the PC reads.

Intra-Instruction Dependencies starting from a register write

The PC handling described above had a strange graph, where a iico_data was starting at a register write. This is because this register write was read-from in the same instruction.

(Precisely, the first write to PC was read from to query the current PC and then increment it, resulting in a graph like the one shown by Luc in a comment on #1704).

We simply add guards on the Intra-Instruction Data dependencies to force them to start at a register read or at a memory read.

[HadrienRenaud]

Note that make test-all pass after 28c0c54 (see the workflow run here).

[maranget]

Is this call to check_total realy useful? (Just wondering)

[maranget]

And is the test complete?

[HadrienRenaud]

So I think it is if we assume that is_before_strict is transitive, then it is good enough to say that it is total.

[HadrienRenaud]

Useful or not is difficult to answer: Set.Make doesn't provide any guarantee if the ordered type is not a total order, so we cannot guarantee to find non-comparable elements. Because we rely on the absence of non-comparable stores, I think we should check that assumption, and a linear fold through the set does not seem too high a price for this.

I can remove it if you think that it is not useful.

[maranget]

Building the set also checks comparisons, I conjecture that if the set is built by adding elements one by one (which is not the case at the moment ?) and that is_before_strict is a non-total partial order, then building the set fails.

[HadrienRenaud]

As far as I understand the code in the standard library, the set is built by sorting the list first, and then assuming the element sorted.
The question is now: does List.sort_uniq do enough comparisons for us to be confident that if the order is non-total, sorting the set fails?

[HadrienRenaud]

The answer, I believe, is no. See the following test:

exception NonComparableFound

(** [compare j1 j2] is a comparison function on integers where the order is almost total: just j1 and j2 are non-comparable. *)
let compare j1 j2 i1 i2 =
  if i1 = j1 && i2 = j2 then raise NonComparableFound
  else Int.compare i1 i2

let () =
  try 
   let _ = List.sort_uniq (compare 2 3) [0; 1; 3; 4; 2] in
   Printf.printf "List.sort_uniq has not identified non-comparable items\n"
  with NonComparableFound -> Printf.printf "Correctly identified non-comparable items\n"
(* Prints: List.sort_uniq has not identified non-comparable items *)

See also this playground.

[HadrienRenaud]

(it also doesn't work with Set.of_list nor with Set.add, see this playground)

[HadrienRenaud]

Note: last push writes this reasoning in a comment in mem.ml.

[maranget]

LGTM (still curious about check_total)

[HadrienRenaud]

Thank you @maranget for the review. I think my last comment largely addresses your concerns, so I'm going to merge after lunch, unless you tell me otherwise.