[herd] Implement Aarch64 instruction stz2g #763

maranget · 2024-01-23T13:47:45Z

Adding the instruction revealed some shortcomings of the current MTE implementation. In particular, it is no longer realistic to assume that a complete array will never span over more than one granule, as the STZ2G instruction sets two granules.

The implementation is correct only in mixed-size mode, it is then an error to execute STZG (resp. STZ2G) on a memory location whose size is strictly less than one (resp. two) granules.

For instance, with the current granule size of 16 bytes, herd will fail on the following test:

AAArch64 TooSmall
Variant=mixed,mte
{
int x=1;
0:X1=x:green;
0:X2=x:red;
}
  P0           ;
 STZG X2,[X1]  ;
forall x=0

We have:

% herd7 TooSmall.litmus
Warning: File "TooSmall.litmus": Unaligned or out-of-bound access: x, 16 bytes (User error)

To reach granule size one has to declare an array:

AArch64 LargeEnough
Variant=mixed,mte
{
int64_t x[3] = {1,2,3};
0:X1=x:green;
0:X2=x:red;
}
  P0           ;
 STZG X2,[X1]  ;
forall x={0,0,3}

Now, the test is accepted, yielding the final values of zero for x[0] and x[1].

For backward compatibility STZG still operates in non-mixed mode, with the expected result of zeroing non-array locations, which is correct assuming that:

the size of non-array locations is less than one granule, and
different locations occupy different granules.

Finally, herd will fail, flagging an error, on tests that both have some array location and some STZG instruction, regardless of whether STZG touches some array or not.

maranget · 2024-01-25T13:26:48Z

Hi @relokin, this PR much elaborates from your work on MTE (In particular PR #695). If you have some time...

relokin

This is very good thanks Luc! I've done a quick review added a couple of comments and I will try and test it tomorrow as well.

relokin · 2024-01-25T23:43:44Z

herd/tests/instructions/AArch64.MTE/L00.litmus

+ STZG  X2,[X1]   ;
+ MOV W0,#7       ;
+ STR W0,[X2]     ;
+ STR W0,[X1,#20] ; 


It's a little weird that we allow an unchecked STR to x when previously we had a checked STR x. It makes sense to allow unchecked locations and checked locations but mixed uses of the same location is not very realistic. But this might not be in the scope for this PR.

Looking at L02 did you mean this to be:

Suggested change

STR W0,[X1,#20] ;

STR W0,[X2,#20] ;

I do not understand your remark on "unchecked" STR. Which STR are checked or unchecked ?

As to STR W0,[X1,#20], this is what I intended. As I understand it, both STR succeeds the first one STR W0,[X2] stores into the granule whose color has changed to :red, while the second STR W0,[X1,#20] stores into the next granule, whose color has not changed and hence stayed :green. Assuming a granule size of 16 bytes.

Ah sorry, do we assume a default tag (color) for symbolic addresses as well? Meaning x is assumed to be x:green? I was under the impression we only had default values for tag locations (tag(x)).

MTE doesn’t require that all memory instructions perform a tag check. There are cases where the instruction doesn’t perform a tag check (for example stg doesn't check or a load y where y is mapped as Normal Memory and not TaggedNormal doesn’t check either). So I thought, so without checking the code, that if a symbolic address didn’t specify a colour it would signal to herd to slide the tag check.

As I understand, all locations have a tag and this tag is green by default. In other words, all locations have the TaggedNormal attribute. Do we understand each other?

OK, I think I understand now. In -variant mte:

If tag(x) is not explicitly initialised then, herd7 will initialise to `:green"

If a register is initialised with a symbolic location which doesn't specify a tag (for example 0:X0=x), herd7 will assume that a default tag :green for this symbolic address (i.e. 0:X0=x:green).

All locations are assumed to be mapped as TaggedNormal

and now I also understand why L03 is correctly specified.

herd/tests/instructions/AArch64.MTE/L03.litmus

relokin · 2024-01-25T23:50:06Z

herd/tests/instructions/AArch64.MTE/L05.litmus

@@ -0,0 +1,16 @@
+AArch64 L05


It would be really good if herd7 could ignore the size of STZG for L03 but throw an error for L05. But I am not sure this is possible. So I guess you're suggesting that STZG should require mixed mode don't you?

You mean throw an error when the target location of STZG is an array in non-mixed mode?

I think so yes. I think it would be useful to allow herd7 to work without enabling -variant mixed in cases like L03 after all, L03 is not incorrect (the user didn't check x[1] they're only checking x aka x[0]). But L05 is wrong so they can't trust the result and they should enable -variant mixed. What do you think? Is it possible?

Your solution implies looking at several places in the execution: (1) apply STZG to an array location and (2) reading some array cell different from the first.

I'd favor a solution that would look at the STZG write only. Then if we can check that STZG base address is an array address, we can:

Fail with a message that suggests using -variant mixed, or

Fill all the array cells with zero, (up to granule size ?)

Also, if the address is not known (ie not read from a register initial state) 1. applies systematically.

A more simple but less expressive solution would be to fail, still suggesting -variant mixed when we both have some array and STZG instruction in the same test.

A more simple but less expressive solution would be to fail, still suggesting -variant mixed when we both have some array and STZG instruction in the same test.

I think that's a very good middle ground. But in any case don't worry too much if it's too hard we can fix in a subsequent PR.

I have finally implemented this middle ground, as it is relatively straightforward.

herd/eventsMonad.ml

herd/machAction.ml

relokin

LGTM. Very nice change, looking forward to see it merged!

Adding this instruction revealed some shortcomings of the current MTE implementation. In particular it is no longer realistic to assume that a complete array will never span over more than one granule, as the STZ2G instruction sets two granules. The STZG instruction writes zero into one granule and updates its tag location, while the STG2Z instruction writes zero into two granules and updates two tag locations, some changes are required. To account for STZ2G write of two tag locations, we change the previous hypothesis that every location reside in one granule. 1. An array can now span over several granules 2. We accept size mismatches for the write of zero of STGZ. As a consequence, in non-mixed size (default) mode, STGZ will zero any non-array location, whatever its size., which is correct as long as the size of the location is less than one granule. For arrays, only the first item would be zero-ed. Thus, having both arrays and STGZ in the same test triggers a "user error" failure. However, the instruction operates as expected in mixed-size mode (`-variant mixed`). 3. Mixed-size mode is mandatory for executing STZ2G, and for executing tests with some array location and some STZG instruction. Notice: granule size is currently fixed at G=16 bytes. If necessary, command-line configuration can be implemented in the future. Notation: For a base address x, successive tag addresses are written tag(x), tag(x+G) , tag(x+2G), etc. Said otherwise, the tag address of (byte) location x+o is tag(x+(o*G)/G). Notice: In vmsa mode, since PR #695, tag addresses are based upon physical addresses and will appear as tag(PA(x)), tag(PA(x)+G),...

maranget · 2024-02-09T12:15:07Z

LGTM. Very nice change, looking forward to see it merged!

@relokin, merging on its way. Thanks for your review.

maranget force-pushed the aarch64-stz2g branch 7 times, most recently from 0fa1147 to 051c3f5 Compare January 25, 2024 13:24

maranget marked this pull request as ready for review January 25, 2024 13:25

maranget mentioned this pull request Jan 25, 2024

ROR shift type implementation #698

Open

relokin reviewed Jan 25, 2024

View reviewed changes

maranget force-pushed the aarch64-stz2g branch from 051c3f5 to 14d916f Compare January 26, 2024 18:18

relokin reviewed Jan 31, 2024

View reviewed changes

herd/machAction.ml Show resolved Hide resolved

relokin approved these changes Jan 31, 2024

View reviewed changes

[herd] Merge memtag and mte variants

162f3a4

maranget force-pushed the aarch64-stz2g branch from 14d916f to 07a0380 Compare February 9, 2024 09:18

maranget added 2 commits February 9, 2024 13:04

[herd] Add tests

993e8af

maranget force-pushed the aarch64-stz2g branch from 07a0380 to 993e8af Compare February 9, 2024 12:07

maranget merged commit b95a692 into master Feb 9, 2024

maranget deleted the aarch64-stz2g branch February 9, 2024 12:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[herd] Implement Aarch64 instruction stz2g #763

[herd] Implement Aarch64 instruction stz2g #763

maranget commented Jan 23, 2024 •

edited

Loading

maranget commented Jan 25, 2024

relokin left a comment

relokin Jan 25, 2024

relokin Jan 25, 2024

maranget Jan 26, 2024 •

edited

Loading

relokin Jan 26, 2024

maranget Jan 26, 2024

relokin Jan 28, 2024 •

edited

Loading

relokin Jan 25, 2024

maranget Jan 26, 2024

relokin Jan 29, 2024

maranget Jan 31, 2024 •

edited

Loading

relokin Jan 31, 2024

maranget Feb 9, 2024

relokin left a comment

maranget commented Feb 9, 2024

[herd] Implement Aarch64 instruction stz2g #763

[herd] Implement Aarch64 instruction stz2g #763

Conversation

maranget commented Jan 23, 2024 • edited Loading

maranget commented Jan 25, 2024

relokin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maranget Jan 26, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

relokin Jan 28, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maranget Jan 31, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

relokin left a comment

Choose a reason for hiding this comment

maranget commented Feb 9, 2024

maranget commented Jan 23, 2024 •

edited

Loading

maranget Jan 26, 2024 •

edited

Loading

relokin Jan 28, 2024 •

edited

Loading

maranget Jan 31, 2024 •

edited

Loading