From 77bc0715373e58b23c064c12571e970a87cd7694 Mon Sep 17 00:00:00 2001 From: Yeji Han Date: Mon, 6 Jul 2026 19:57:26 +0900 Subject: [PATCH] fix(arm): Track exclusive forwarding views precisely Carry the paired load-exclusive post-view separately from the forwarded write view, and join it back only for acquire reads from successful store-exclusive forwarding. This implementation is a weakening from the original Promising model and the Armed Cats paper to the current Arm model. --- ArchSemArm/UMPromising.v | 62 +++++++++++++++++++++++++--------------- ArchSemArm/VMPromising.v | 36 ++++++++++++----------- 2 files changed, 59 insertions(+), 39 deletions(-) diff --git a/ArchSemArm/UMPromising.v b/ArchSemArm/UMPromising.v index d6ab8c70..cb65f82c 100644 --- a/ArchSemArm/UMPromising.v +++ b/ArchSemArm/UMPromising.v @@ -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; + addr : address; + size : N; + view : view + }. +End XclItem. + (** The thread state *) Module TState. Record t := @@ -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 _ := @@ -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. @@ -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 => @@ -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. @@ -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). diff --git a/ArchSemArm/VMPromising.v b/ArchSemArm/VMPromising.v index b394ccf0..9c30effb 100644 --- a/ArchSemArm/VMPromising.v +++ b/ArchSemArm/VMPromising.v @@ -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. @@ -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 _ := @@ -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. @@ -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 => @@ -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. @@ -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).