Skip to content

fix(arm): Propagate load-exclusive post-view through STXR forwarding #175

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
febyeji wants to merge 1 commit into
base: main
Choose a base branch
from
Open

fix(arm): Propagate load-exclusive post-view through STXR forwarding #175

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
62 changes: 39 additions & 23 deletions ArchSemArm/UMPromising.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,16 +165,33 @@ Module FwdItem.
make {
time : nat;
view : view;
xcl : bool
xcl_view : option nat (** Implements the new [[R];rmw;rfi;[A|Q]] rule in [aob]. *)
}.

Definition init := make 0 0 false.
Definition init := make 0 0 None.

(** The view of a read from a forwarded write *)
(** The view of a read from a forwarded write. If a successful store-exclusive
is forwarded to an acquire read, include the post-view of its paired
load-exclusive. Plain reads should only inherit the write-data view. *)
Definition read_fwd_view (macc : mem_acc) (f : t) :=
if f.(xcl) && is_rel_acq macc then f.(time) else f.(view).
match f.(xcl_view) with
| Some xv => if is_rel_acq macc then f.(view) ⊔ xv else f.(view)
| None => f.(view)
end.
End FwdItem.

(** Data of a load-exclusive: [time] is its external read time and [view] is
its [vpost]. *)
Module XclItem.
Record t :=
make {
time : nat;

@tperami tperami Jul 22, 2026

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.

Need to say this is the data of the load exclusive (time is the external read time, and view is the vpost of the load exclusive

addr : address;
size : N;
view : view
}.
End XclItem.

(** The thread state *)
Module TState.
Record t :=
Expand All @@ -200,13 +217,12 @@ Module TState.

(* Forwarding database. The first view is the timestamp of the
write while the second view is the max view of the dependencies
of the write. The boolean marks if the store was an exclusive*)
of the write. The optional view records the paired load-exclusive
post-view for successful store-exclusive forwarding. *)
fwdb : gmap address FwdItem.t;

(* Exclusive database. If there was a recent load exclusive but the
corresponding store exclusive has not yet run, this will contain
the timestamp, address, and size of the load exclusive *)
xclb : option (nat * address * N);
(* The latest unmatched load-exclusive. *)
xclb : option XclItem.t;
}.

#[global] Instance eta : Settable _ :=
Expand Down Expand Up @@ -260,14 +276,14 @@ Module TState.

(** Sets the same [FwdItem] for every byte address in a write range. *)
Definition set_fwdbs (addrs : list address)
(time : nat) (vdata : view) (xcl : bool) (ts : t) : t :=
let fi := FwdItem.make time vdata xcl in
(time : nat) (vdata : view) (xcl_view : option view) (ts : t) : t :=
let fi := FwdItem.make time vdata xcl_view in
foldr (λ a, set_fwdb a fi) ts addrs.

(** Sets the exclusive database to the footprint of the latest load
exclusive. *)
Definition set_xclb (time : nat) (addr : address) (size : N) : t → t :=
setv xclb (Some (time, addr, size)).
Definition set_xclb (time : nat) (addr : address) (size : N) (vpost : view) : t → t :=
setv xclb (Some (XclItem.make time addr size vpost)).

(** Clears the exclusive database, to mark a store exclusive *)
Definition clear_xclb : t → t := setv xclb None.
Expand Down Expand Up @@ -349,8 +365,8 @@ Definition read_candidates (addr : address) (size : N) (vpre : view)
byte/view/timestamp with the ones of the forwarded write. The timestamp
returned (last value) is for coherence checking purposes). Returns [None] if
no forwarding occurs *)
Definition read_fwd (fwdb : gmap address FwdItem.t) (macc : mem_acc)
(mem : Memory.t) (tread : nat) (addr : address) :
Definition read_fwd (fwdb : gmap address FwdItem.t) (macc : mem_acc) (mem : Memory.t)
(tread : nat) (addr : address) :
Exec.res string (option (bv 8 * view * nat)) :=
match fwdb !! addr with
| Some fwd =>
Expand Down Expand Up @@ -410,7 +426,7 @@ Definition read_mem (addr : address) (size : N) (macc : mem_acc) (init : memoryM
mset PPState.state $ TState.update TState.vacq (view_if (is_rel_acq macc) vpost);;
mset PPState.state $ TState.update TState.vcap vaddr;;
( if is_exclusive macc
then mset PPState.state $ TState.set_xclb tread addr size
then mset PPState.state $ TState.set_xclb tread addr size vpost
else mret ());;
mset PPState.iis $ IIS.add vpost;;
mret res.
Expand Down Expand Up @@ -461,20 +477,20 @@ Definition write_mem (tid : nat) (addr : address) (size : N) (macc : mem_acc)
( if (is_atomic_rmw macc && is_rel_acq macc && read_acquire)
then mset PPState.state $ TState.update TState.vacq time
else mret ());;
xcl ← if is_exclusive macc then
fwd_xcl_view ← if is_exclusive macc then
match TState.xclb ts with
| None => mdiscard
| Some (tread, raddr, rsize) =>
| Some xcl =>
mset PPState.state $ TState.clear_xclb;;
if decide (addr = raddr ∧ size = rsize) then
guard_discard' (Memory.exclusive tid addr size tread time mem);;
mret true
if decide (addr = xcl.(XclItem.addr) ∧ size = xcl.(XclItem.size)) then
guard_discard' (Memory.exclusive tid addr size xcl.(XclItem.time) time mem);;
mret (Some xcl.(XclItem.view))
else
(* Address/size mismatch fails the exclusive-monitor check; STXR failure is no-write. *)
mdiscard
end
else mret false;
mset PPState.state $ TState.set_fwdbs addrs time vdata xcl;;
else mret None;
mset PPState.state $ TState.set_fwdbs addrs time vdata fwd_xcl_view;;
mret (if (new_promise : bool) then Some vpre else None).


Expand Down
36 changes: 20 additions & 16 deletions ArchSemArm/VMPromising.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,7 @@ End Memory.
Import (hints) Memory.

Module FwdItem := UMPromising.FwdItem.
Module XclItem := UMPromising.XclItem.

Definition EL := (fin 4).
#[export] Typeclasses Transparent EL.
Expand Down Expand Up @@ -457,8 +458,9 @@ Module TState.
(* Per-byte forwarding database *)
fwdb : gmap address FwdItem.t;

(* Exclusive database: (load-time, physical address, size) *)
xclb : option (nat * address * N);
(* The latest load-exclusive, if its matching store-exclusive has not
run yet. *)
xclb : option XclItem.t;
}.

#[global] Instance eta : Settable _ :=
Expand Down Expand Up @@ -604,14 +606,15 @@ Module TState.

(** Set forwarding entries for all bytes in a range *)
Definition set_fwdbs (addrs : list address)
(time : nat) (vdata : view) (xcl : bool) (ts : t) : t :=
let fi := FwdItem.make time vdata xcl in
(time : nat) (vdata : view) (xcl_view : option view) (ts : t) : t :=
let fi := FwdItem.make time vdata xcl_view in
foldr (λ a, set_fwdb a fi) ts addrs.

(** Set the exclusive database to the footprint of the latest load
exclusive. *)
Definition set_xclb (time : nat) (addr : address) (size : N) : t → t :=
setv xclb (Some (time, addr, size)).
Definition set_xclb (time : nat) (addr : address) (size : N)
(vpost : view) : t → t :=
setv xclb (Some (XclItem.make time addr size vpost)).

(** Clears the exclusive database, to mark a store exclusive *)
Definition clear_xclb : t → t := setv xclb None.
Expand Down Expand Up @@ -1911,8 +1914,8 @@ Definition read_candidates (addr : address) (size : N) (vpre : view)
byte/view/timestamp with the ones of the forwarded write. The timestamp
returned (last value) is for coherence checking purposes). Returns [None] if
no forwarding occurs *)
Definition read_fwd (fwdb : gmap address FwdItem.t) (macc : mem_acc)
(mem : Memory.t) (tread : nat) (addr : address) :
Definition read_fwd (fwdb : gmap address FwdItem.t) (macc : mem_acc) (mem : Memory.t)
(tread : nat) (addr : address) :
Exec.res string (option (bv 8 * view * nat)) :=
match fwdb !! addr with
| Some fwd =>
Expand Down Expand Up @@ -1974,7 +1977,7 @@ Definition read_mem_explicit (addr : address) (size : N) (macc : mem_acc)
mset PPState.state $ TState.update TState.vacq (view_if (is_rel_acq macc) vpost);;
mset PPState.state $ TState.update TState.vspec vaddr;;
( if is_exclusive macc
then mset PPState.state $ TState.set_xclb tread addr size
then mset PPState.state $ TState.set_xclb tread addr size vpost
else mret ());;
mset PPState.iis $ IIS.add vpost;;
mret res.
Expand Down Expand Up @@ -2034,21 +2037,22 @@ Definition write_mem (tid : nat) (addr : address) (size : N) (macc : mem_acc)
mset PPState.state $ TState.update TState.vwr time;;
mset PPState.state $ TState.update TState.vrel (view_if is_release time);;

xcl ← if is_exclusive macc then
fwd_xcl_view ← if is_exclusive macc then
match TState.xclb ts with
| None => mdiscard
| Some (tread, raddr, rsize) =>
| Some xcl =>
mset PPState.state $ TState.clear_xclb;;
if decide (addr = raddr ∧ size = rsize) then
guard_discard' (Memory.exclusive tid addr size tread time mem);;
mret true
if decide (addr = xcl.(XclItem.addr) ∧ size = xcl.(XclItem.size)) then
guard_discard'
(Memory.exclusive tid addr size xcl.(XclItem.time) time mem);;
mret (Some xcl.(XclItem.view))
else
(* PA/size mismatch fails the exclusive-monitor check; STXR failure is no-write. *)
mdiscard
end
else mret false;
else mret None;

mset PPState.state $ TState.set_fwdbs addrs time vdata xcl;;
mset PPState.state $ TState.set_fwdbs addrs time vdata fwd_xcl_view;;
mret (if (new_promise : bool) then Some vpre else None).


Expand Down
Loading