[herd] Fix non explicit atomic pairs

[maranget]

Compute rmw on non-explicit memory accesses from iico_data

[HadrienRenaud]

Why do we need _test here?

[maranget]

I used the test argument to display some graphs. We can remove it now.

[relokin]

Thanks for this Luc, I will try to have a look at the code as soon as possible.

I have a high level question. We discussed this with Hadrien as well, why can't we get this information from the instruction semantics? I understand why we can't do that for exclusives, but for atomic instructions (for example, CAS, SWP) and for atomic hardware updates, we know that the Memory Read Effect and the Memory Write Effect need to be paired together from the instruction semantics. Rather than searching through the list of Effect to find pairs of Effects that satisfy certain conditions, wouldn't it be preferable to retain that information from the instruction semantics?

[maranget]

I have a high level question. We discussed this with Hadrien as well, why can't we get this information from the instruction semantics? I understand why we can't do that for exclusives, but for atomic instructions (for example, CAS, SWP) and for atomic hardware updates, we know that the Memory Read Effect and the Memory Write Effect need to be paired together from the instruction semantics. Rather than searching through the list of Effect to find pairs of Effects that satisfy certain conditions, wouldn't it be preferable to retain that information from the instruction semantics?

I guess the process has been as follows: we first have implemented exclusives first (for Power) and then generalised without thinking of a different solution. The case of AArch64+ASL is also to be considered.

[HadrienRenaud]

The case of AArch64+ASL is also to be considered.

I think the case of AArch64+ASL is easy enough: we could run this algorithm, or implement it in asl.cat (a bit like Nikos' try). So I don't think AArch64+ASL would be the biggest problem here.

[relokin]

The case of AArch64+ASL is also to be considered.

I think the case of AArch64+ASL is easy enough: we could run this algorithm, or implement it in asl.cat (a bit like Nikos' try). So I don't think AArch64+ASL would be the biggest problem here.

I agree and longer term ASL will provide the means to identify pairs of Memory Read and Memory Write Effects that are intended to be atomic.

@maranget for Power and other architecture, is exclusives the only concern or is there support for atomics as well. Otherwise, it might be simple to do this hybrid approach, for atomic instructions and hardware updates we use the instruction semantics and for exclusives we use a version of this code.

[maranget]

I think the case of AArch64+ASL is easy enough: we could run this algorithm, or implement it in asl.cat (a bit like Nikos' try). So I don't think AArch64+ASL would be the biggest problem here.

Nice, we can implement rmw as amo|lssx in Cat. Notice that other architectures provide amo's or lxsx. In fact, all architectures provides at least one of them. As a consequence:

1. We need a general set of atomics. As far as I know the name of the set may differ from architecture. we also need to generalise the exclusives annotation (EXCL in your code).
2. stdlib.hva may be a beter place for your definitions.

[maranget]

Additonally, I am a bit concerned by the added complexity of an hybrid approach. Don't you think that an "all cat" or an "all mem.ml" approach would be more easy to maintain?

[maranget]

And to answer one of your questions : ARM -> exclusives, LISA -> amo, BPF -> amo, C -> amo, Java -> amo, MIPS -> exclusives, PPC -> exclusives, RISCV -> exclusives,amo, X86_64 -> amo, X86 -> amo.

[relokin]

I think the case of AArch64+ASL is easy enough: we could run this algorithm, or implement it in asl.cat (a bit like Nikos' try). So I don't think AArch64+ASL would be the biggest problem here.

Nice, we can implement rmw as amo|lssx in Cat. Notice that other architectures provide amo's or lxsx. In fact, all architectures provides at least one of them. As a consequence:

amo relies on the same code as rmw doesn't it?

herdtools7/herd/machModelChecker.ml

Line 440 in 161ed8e

"amo",

and lxsx is derived in stdlib.cat as let lxsx = rmw \ amo. I am not understand the suggestion.

1. We need a general set of atomics. As far as I know the name of the set may differ from architecture. we also need to generalise the exclusives annotation (EXCL in your code).
2. stdlib.hva may be a beter place for your definitions.

agreed.

[maranget]

I meant that amo an lxsx can be computed directly from the event sets EXCL and X as you do here. That is:

let lxsx = [Exp & R & EXCL]; po & same-loc \ (po; [Exp & M & EXCL]; po); [Exp & W & EXCL]
let amo = [Exp & R & X]; same-instance & same-loc; [Exp & W & X]
   | [Imp & TTD & R]; iico_data & same-loc; [Imp & TTD & W]
let rmw = amo | lxsx

To that aim we have to define EXCL and X for all architectures.

[HadrienRenaud]

I meant that amo an lxsx can be computed directly from the event sets EXCL and X as you do here. That is:

let lxsx = [Exp & R & EXCL]; po & same-loc \ (po; [Exp & M & EXCL]; po); [Exp & W & EXCL]
let amo = [Exp & R & X]; same-instance & same-loc; [Exp & W & X]
   | [Imp & TTD & R]; iico_data & same-loc; [Imp & TTD & W]
let rmw = amo | lxsx

To that aim we have to define EXCL and X for all architectures.

This is one possibility. At least this is how we could do it for AArch64+ASL.

Another possibility (which might be what Nikos was talking about) would be to have the instruction semantics define amo and EXCL: because amo is always in a single instruction, the instruction semantics seem a good place to do this, and have all the information necessary. EXCL could be simply defined by a new filter function in actions.ml called is_exclusive (note that is_atomic might not be precise enough here).

[maranget]

In any case we need support for the EXCL set or/and is_exclusive. As you noticed is_atomic is not precise enough. Consider the following test:

AArch64 LXSX06
{
 0:X0=x;
 1:X0=x;
}
 P0              |  P1         ;
 LDXR W1,[X0]    | MOV W1,#3   ;
 MOV W5,#2       | STR W1,[X0] ;
 STADD W5,[X0]   |             ;
 MOV W3,#1       |             ;
 STXR W4,W3,[X0] |             ;
exists 0:X1=0 /\ [x]=1

At the moment. herd7 allows the test because it consider that STADD and STXR behave the same.

[HadrienRenaud]

In any we need support for EXCL.

Should we still go ahead with this PR or do you think this is blocking?

[maranget]

Superseded by PR #1889?

[maranget]

Superseded by PR #1889.