Skip to content

[AARCH-25890] Ordering semantics of the address translation of tag checked instructions - #1932

Open
relokin wants to merge 6 commits into
herd:masterfrom
relokin:vmsa+mte
Open

[AARCH-25890] Ordering semantics of the address translation of tag checked instructions#1932
relokin wants to merge 6 commits into
herd:masterfrom
relokin:vmsa+mte

Conversation

@relokin

@relokin relokin commented Jul 28, 2026

Copy link
Copy Markdown
Member

No description provided.

relokin added 2 commits July 27, 2026 21:17
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
@relokin relokin changed the title AARCH-25890 Ordering semantics of the address translation of tag checked instructions [AARCH-25890] Ordering semantics of the address translation of tag checked instructions Jul 28, 2026
relokin added 4 commits July 28, 2026 15:55
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

@TiberiuBucur TiberiuBucur left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few small non-blocking comments. Happy to approve once we fix the merge conflicts.

Comment thread herd/AArch64Sem.ml
Comment on lines +1488 to +1489
match is_mte_sync dir with
| true ->

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we maybe use an if statement instead of a match on booleans?

Comment thread herd/AArch64Sem.ml
fun ma ->
let set_tfsr = write_reg AArch64Base.tfsr V.one ii in
let ma = ma >>*== (fun a -> (set_tfsr >>| mfault) >>! a) in
let ma = ma >>**== (fun a -> (set_tfsr >>| mfault) >>! a) in

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we want the extra data dependencies from the register and tag memory read effects to the TFSR_ELx write effect and to the fault effect?

Comment thread herd/AArch64Sem.ml
Comment on lines +1579 to +1581
match is_mte_sync dir with
| true -> mtag
| false ->

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ditto.

Comment thread herd/AArch64Sem.ml
Comment on lines +1635 to +1637
match is_mte_sync dir with
| true -> ma
| false -> ma >>*== (fun a -> noact >>! a)

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ditto.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants