Skip to content

[gen] Add wildcard Amo.Safe. #1745

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ShaleXIONG wants to merge 2 commits into
base: master
Choose a base branch
from
+19 −8
Open

[gen] Add wildcard Amo.Safe. #1745

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
db067df
[gen] Add wildcard `Amo.Safe`.
Mar 2, 2026
2d437a5
[MERGE] Address comments
Mar 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions gen/AArch64Compile_gen.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2192,7 +2192,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
| Cas -> map_some emit_cas
| LdOp op -> map_some (emit_ldop op)
| StOp op -> emit_stop op
| AllAmo -> assert false
| AllAmo | SafeAmo -> assert false

(* Fences *)
let emit_cachesync s isb r =
Expand Down Expand Up @@ -2844,7 +2844,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
| Swp -> map_some_dp (emit_ldop_dep swp swp_mixed)
| Cas -> map_some_dp emit_cas_dep
| StOp op -> emit_stop_dep op
| AllAmo -> assert false
| AllAmo | SafeAmo -> assert false

let emit_fence_dp st p init n f (dp,csel) r1 n1 =
let vdep = node2vdep n1 in
Expand Down
16 changes: 10 additions & 6 deletions gen/common/AArch64Arch_gen.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -975,7 +975,7 @@ let expand_dp_dir (dir,_) = D.expand_dp_dir dir

(* Read-Modify-Write *)
module RMW = struct
type rmw = LrSc | LdOp of atomic_op | StOp of atomic_op | Swp | Cas | AllAmo
type rmw = LrSc | LdOp of atomic_op | StOp of atomic_op | Swp | Cas | AllAmo | SafeAmo

type nonrec atom = atom

Expand All @@ -988,10 +988,13 @@ let pp_rmw compat = function
| LdOp op -> sprintf "Amo.Ld%s" (pp_aop op)
| StOp op -> sprintf "Amo.St%s" (pp_aop op)
| AllAmo -> sprintf "Amo"
(* `Amo` that gives distinct values,
therefore safe to generate tests.*)
| SafeAmo -> sprintf "Amo.Safe"

let is_one_instruction = function
| LrSc -> false
| LdOp _ | StOp _ | Swp | Cas | AllAmo -> true
| LdOp _ | StOp _ | Swp | Cas | AllAmo | SafeAmo -> true

let fold_aop f r =
let r = f A_ADD r in
Expand All @@ -1006,7 +1009,7 @@ let fold_rmw wildcard f r =
let r = f Cas r in
let r = fold_aop (fun op r -> f (LdOp op) r) r in
let r = fold_aop (fun op r -> f (StOp op) r) r in
let r = if wildcard then f AllAmo r else r in
let r = if wildcard then f AllAmo r |> f SafeAmo else r in
r

let all_concrete_rmw =
Expand All @@ -1016,6 +1019,7 @@ let all_concrete_rmw =
let expand_rmw rmw = match rmw with
| LrSc | Swp | Cas | LdOp _ | StOp _ -> [rmw]
| AllAmo -> all_concrete_rmw
| SafeAmo -> [Swp; Cas; LdOp A_ADD; StOp A_ADD]

let fold_rmw_compat f r = f LrSc r

Expand All @@ -1041,15 +1045,15 @@ let same_mixed (a1:atom option) (a2:atom option) =
let applies_atom_rmw rmw ar aw = match rmw with
| LrSc ->
ok_rw ar aw && (do_cu || same_mixed ar aw)
| Swp|Cas|LdOp _| AllAmo ->
| Swp|Cas|LdOp _ | AllAmo | SafeAmo ->
ok_rw ar aw && same_mixed ar aw
| StOp _ ->
ok_w ar aw && same_mixed ar aw

let show_rmw_reg = function
| StOp _ -> false
| LdOp _|Cas|Swp|LrSc -> true
| AllAmo -> assert false
| AllAmo | SafeAmo -> assert false

let compute_rmw r ~old ~operand =
match r with
Expand All @@ -1069,7 +1073,7 @@ let compute_rmw r ~old ~operand =
| A_CLR -> old land (lnot operand)
end
| LrSc | Swp | Cas -> operand
| AllAmo -> assert false
| AllAmo | SafeAmo -> assert false

(* Rule out `rmw_list` that contains the same type of atomic operation for a location. *)
let is_valid_rmw rmw_list =
Expand Down
Loading