[gen] Add store-only variant

[ShaleXIONG]

This adds a StoreOnly generator variant for memtag variant and emits it to herd7 metadata as store-only. The parser accepts both StoreOnly and store-only, and validation requires it to be used together with memtag.

For multi-instruction RMWs, store-only carries the memtag fault check from the read event to the write event. In particular, on Aarch64 LxSx instruction's generated fault label moves from the load-exclusive instruction to the store-exclusive instruction, for example, diyone7 -arch AArch64 -variant memtag,store-only PodRW T Rfe LxSx PodWW Rfe

AArch64 LB+popt+rmw-po
Variant=memtag store-only
Generator=diyone7 (version 7.58+1)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Rf
Orig=PodRWPT RfeTP LxSx PodWW Rfe
"PodRWPT RfeTP LxSx PodWW Rfe"
{
 0:X0=x:green; 0:X2=y:red; 0:X3=y:green;
 1:X0=x:green; 1:X2=y:red;
}
 P0          | P1                   ;
 LDR W1,[X0] | MOV W4,#1            ;
 STG X2,[X3] | Loop00:              ;
             | LDXR W1,[X2]         ;
             | L00: STXR W5,W4,[X2] ; (* <--- the label `L00` moves from `LDXR` to here ` STXR` *)
             | CBNZ W5,Loop00       ;
             | MOV W6,#1            ;
             | STR W6,[X0]          ;

exists ([y]=1 /\ 0:X1=1 /\ 1:X1=0 /\ not (fault(P1:L00,y)))

This means:

• In cycle.ml, we changed fault-label assignment to be event-aware rather than passing only a direction. The new logic detects multi-instruction RMWs, such as LxSx, and under store-only suppresses the read-side fault label while preserving the pending fault-check state for the write event.
• In AArch64Compile_gen.ml, we replaced the old “label the first instruction” via add_label_to_first_instructions handling for exclusive RMW code with logic that recognises exclusive loads and stores separately via add_label_to_exclusive_load_and_store. For LxSx, it can now attach the read event’s label to LDXR/LDAXR, and the write event’s label to STXR/STLXR/STXP.

[relokin]

Can you please explain how you chose these cycles/three tests?

[ShaleXIONG]

Given your comment, I have update some comments in the tests and also I add one more section. Now we have 3 set of tests:

• store-only completely removes the label and associated fault check, because there is no more STR afterwards to the same location.
• The newly added section contains two tests that without store-only, there are labels for both STR and LDR respectively, while with store-only the label to LDR is removed.
• LxSx test, this is the most tricky case in technical sense, because it is a form of rmw however it compiles to two separate instructions, LDXR and STXR. In this case, the label is moved from LDXR without store-only to STXR with store-only.

[relokin]

I think you have to be more specific about suppressing the fault check for loads. Take this test for example:

$> diyone7 -metadata false -arch AArch64 -variant vmsa,memtag,store-only -oneloc  PteV0 TLBI-sync.ISHsWR ISB Fri
AArch64 CoWR0+tlbi-sync.ishsptev0p-[isb]-fripptev0
Variant=memtag store-only vmsa
{
 [x]=1;
 0:X0=PTE(x:red); 0:X1=(oa:PA(x), valid:0); 0:X2=x:red; 0:X4=x;
}
 P0              ;
 STR X1,[X0]     ;
 DSB ISH         ;
 LSR X5,X4,#12   ;
 TLBI VAAE1IS,X5 ;
 DSB ISH         ;
 ISB             ;
 LDR W3,[X2]     ;

exists (true)

The LDR in this test needs to be checked for faults.

As a side comment, in the initialization, we shouldnot refer to PTE(x:red) but to PTE(x).

[relokin]

BTW, I think it is problematic that by default diyone7 will give the same name to the test above and this test.

[ShaleXIONG]

I opened an issue #1898 for this. I will update it in a separate PR.

[ShaleXIONG]

I think you have to be more specific about suppressing the fault check for loads. Take this test for example:

$> diyone7 -metadata false -arch AArch64 -variant vmsa,memtag,store-only -oneloc  PteV0 TLBI-sync.ISHsWR ISB Fri
AArch64 CoWR0+tlbi-sync.ishsptev0p-[isb]-fripptev0
Variant=memtag store-only vmsa
{
 [x]=1;
 0:X0=PTE(x:red); 0:X1=(oa:PA(x), valid:0); 0:X2=x:red; 0:X4=x;
}
 P0              ;
 STR X1,[X0]     ;
 DSB ISH         ;
 LSR X5,X4,#12   ;
 TLBI VAAE1IS,X5 ;
 DSB ISH         ;
 ISB             ;
 LDR W3,[X2]     ;

exists (true)

The LDR in this test needs to be checked for faults.

As a side comment, in the initialization, we shouldnot refer to PTE(x:red) but to PTE(x).

I will strengthen the store-only to exclusive to memtag, and disallowed when other variants such as vmsa exists.

WIll patch the x:red in a separate commit here.

[Update] I have patched the Pte(x:red) problem in a separate commit dc12e09

[relokin]

Is there a reason why this check is not implemented inside add_tag?

[ShaleXIONG]

This existing function add_tag is frankly of bad name. It basically appends the tag value (second parameter) such as green and red, after the location (first parameter) such as x and y. We can move the check inside add_tag but we will need extra parameter to carry the atom value.

Let me move those check into add_tag in a separate commit and we can decide if we like this change.

[ShaleXIONG]

I update another wrapper function get_tagged_loc which includes the check on Pte. This function already take a node event e as the input so we get all the information we need. ref: 5692616

[relokin]

I am really struggling with the way fault_update is structured. Specifically, I don't understand why you do match () with.

But specifically the new code makes the whole logic even more complex. Can you please move this case below the | _ when kvm and merge it with | do_memtag.

I would also favour a complete rewrite of this along the lines of relokin@a107a85

[ShaleXIONG]

Let me rewrite this function here; I will put in a separate commit.

Here match ()-when is basically a if-else if chain.

[ShaleXIONG]

I just update in a new commit ref: 7c64a52. it is mostly what you proposed but the first match |_,_ when do_no_fault will short-circuit all the rest of update/check, rather than a if-else branch just decide the st value.