Library ArchSemArm.UMPromising
From ASCommon Require Import Options.
From ASCommon Require Import Common Exec FMon StateT.
From ArchSem Require Import GenPromising.
Require Import ArmInst.
#[local] Open Scope stdpp.
The goal of this module is to define an User-mode promising model
with mixed-size support on top of the new interface
A message in the promising model memory. size is a field (not a
parameter) so that Msg.t is a plain Set and all messages
can live in one list.
Module Msg.
Record t :=
make {
size : N;
tid : nat;
addr : address;
val : bv (8 × size);
}.
#[global] Instance eq_dec : EqDecision t.
Proof. intros [] []. decide_eq. Defined.
Record t :=
make {
size : N;
tid : nat;
addr : address;
val : bv (8 × size);
}.
#[global] Instance eq_dec : EqDecision t.
Proof. intros [] []. decide_eq. Defined.
Extracts a byte from a message
Definition read_byte (a : address) (msg : t) : option (bv 8) :=
if decide (addr_in_range (addr msg) (size msg) a) then
let offset := Z.to_N (bv_unsigned a - bv_unsigned (addr msg)) in
Some (bv_get_byte 8 offset (val msg))
else None.
End Msg.
if decide (addr_in_range (addr msg) (size msg) a) then
let offset := Z.to_N (bv_unsigned a - bv_unsigned (addr msg)) in
Some (bv_get_byte 8 offset (val msg))
else None.
End Msg.
A view is just a natural
Definition view := nat.
#[export] Typeclasses Transparent view.
Bind Scope nat_scope with view.
Global Hint Transparent view : core.
Global Hint Unfold view : core.
Module Memory.
Import PromMemory.
#[export] Typeclasses Transparent view.
Bind Scope nat_scope with view.
Global Hint Transparent view : core.
Global Hint Unfold view : core.
Module Memory.
Import PromMemory.
The promising memory: a list of events
Definition t : Type := t Msg.t.
#[export] Typeclasses Transparent t.
Definition cut_after : nat → t → t := @cut_after Msg.t.
Definition cut_before : nat → t → t := @cut_before Msg.t.
#[export] Typeclasses Transparent t.
Definition cut_after : nat → t → t := @cut_after Msg.t.
Definition cut_before : nat → t → t := @cut_before Msg.t.
Reads the last write covering a byte location. Returns the byte value
and the timestamp of the write. Timestamp is 0 if reading from initial
memory.
Fixpoint read_last (addr : address) (init : memoryMap) (mem : t) : option (bv 8 × nat) :=
match mem with
| [] ⇒ init !! addr |$> (., 0%nat)
| msg :: mem' ⇒
if Msg.read_byte addr msg is Some byte then
Some (byte, List.length mem)
else read_last addr init mem'
end.
match mem with
| [] ⇒ init !! addr |$> (., 0%nat)
| msg :: mem' ⇒
if Msg.read_byte addr msg is Some byte then
Some (byte, List.length mem)
else read_last addr init mem'
end.
Reads from initial memory and fail, if the memory has been overwritten
this will fail.
This is mainly for instruction fetching in this model
Definition read_initial (addr : address) (init : memoryMap) (mem : t) : option (bv 8) :=
match read_last addr init mem with
| Some (v, 0%nat) ⇒ Some v
| _ ⇒ None
end.
match read_last addr init mem with
| Some (v, 0%nat) ⇒ Some v
| _ ⇒ None
end.
Reads size bytes starting at addr from the memory state at
timestamp tread. Returns each byte paired with its actual
write-timestamp twrite, or None if any byte is unmapped.
Definition read_from (addr : address) (size : N) (tread : nat)
(init : memoryMap) (mem : t) : option (list (bv 8 × nat)) :=
let snap := cut_before tread mem in
for a in addr_range addr size do
read_last a init snap
end.
(init : memoryMap) (mem : t) : option (list (bv 8 × nat)) :=
let snap := cut_before tread mem in
for a in addr_range addr size do
read_last a init snap
end.
Transforms an initial memory map and a promising memory history back
to a memoryMap
Definition to_memMap (init : memoryMap) (mem : t) : memoryMap :=
foldr (λ msg mm, mem_insert_bv (Msg.addr msg) (Msg.val msg) mm) init mem.
foldr (λ msg mm, mem_insert_bv (Msg.addr msg) (Msg.val msg) mm) init mem.
Promises a write and adds it at the end of memory
Definition promise (msg : Msg.t) : Exec.t t string view :=
mSet (cons msg);;
mem ← mGet;
mret (List.length mem).
mSet (cons msg);;
mem ← mGet;
mret (List.length mem).
Returns a view among a promise set that correspond to a message. The
oldest matching view is taken. This is because it can be proven that
taking a more recent view, will make the previous promises unfulfillable
and thus the corresponding executions would be discarded. TODO prove it.
Definition fulfill (msg : Msg.t) (prom : list view) (mem : t) : option view :=
prom |> filter (λ t, mem !! t = Some msg)
|> reverse
|> head.
prom |> filter (λ t, mem !! t = Some msg)
|> reverse
|> head.
Checks that no write overlapping addr, addr+size) has been made by any
thread other than [tid] in between [tread] and [twrite]
Definition exclusive (tid : nat) (addr : address) (size : N)
(tread : nat) (twrite : nat) (mem : t) : Prop :=
∀ msg ∈ (cut_after tread (cut_before (twrite - 1)%nat mem)),
addr_overlap addr size (Msg.addr msg) (Msg.size msg) →
Msg.tid msg = tid.
#[global] Instance exclusive_dec tid addr size tread twrite mem :
Decision (exclusive tid addr size tread twrite mem).
Proof. unfold exclusive. apply _. Defined.
End Memory.
Import (hints) Memory.
Module FwdItem.
Record t :=
make {
time : nat;
view : view;
xcl_view : option nat
(tread : nat) (twrite : nat) (mem : t) : Prop :=
∀ msg ∈ (cut_after tread (cut_before (twrite - 1)%nat mem)),
addr_overlap addr size (Msg.addr msg) (Msg.size msg) →
Msg.tid msg = tid.
#[global] Instance exclusive_dec tid addr size tread twrite mem :
Decision (exclusive tid addr size tread twrite mem).
Proof. unfold exclusive. apply _. Defined.
End Memory.
Import (hints) Memory.
Module FwdItem.
Record t :=
make {
time : nat;
view : view;
xcl_view : option nat
Implements the new [R];rmw;rfi;[A|Q] rule in aob.
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) :=
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.
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.
Record t :=
make {
time : nat;
addr : address;
size : N;
view : view
}.
End XclItem.
The thread state
Module TState.
Record t :=
make {
prom : list view;
regs : dmap reg (λ reg, reg_type reg × view)%type;
coh : gmap address view;
vrd : view;
vwr : view;
vdmbst : view;
vdmb : view;
vcap : view;
visb : view;
vacq : view;
vrel : view;
fwdb : gmap address FwdItem.t;
xclb : option XclItem.t;
}.
#[global] Instance eta : Settable _ :=
settable! make <prom;regs;coh;vrd;vwr;vdmbst;vdmb;vcap;visb;vacq;vrel;fwdb;xclb>.
Definition init (mem : memoryMap) (iregs : registerMap) :=
({|
prom := [];
regs := dmap_map (λ _ v, (v, 0%nat)) iregs;
coh := ∅;
vrd := 0;
vwr := 0;
vdmbst := 0;
vdmb := 0;
vcap := 0;
visb := 0;
vacq := 0;
vrel := 0;
fwdb := ∅;
xclb := None
|})%nat.
Record t :=
make {
prom : list view;
regs : dmap reg (λ reg, reg_type reg × view)%type;
coh : gmap address view;
vrd : view;
vwr : view;
vdmbst : view;
vdmb : view;
vcap : view;
visb : view;
vacq : view;
vrel : view;
fwdb : gmap address FwdItem.t;
xclb : option XclItem.t;
}.
#[global] Instance eta : Settable _ :=
settable! make <prom;regs;coh;vrd;vwr;vdmbst;vdmb;vcap;visb;vacq;vrel;fwdb;xclb>.
Definition init (mem : memoryMap) (iregs : registerMap) :=
({|
prom := [];
regs := dmap_map (λ _ v, (v, 0%nat)) iregs;
coh := ∅;
vrd := 0;
vwr := 0;
vdmbst := 0;
vdmb := 0;
vcap := 0;
visb := 0;
vacq := 0;
vrel := 0;
fwdb := ∅;
xclb := None
|})%nat.
Extracts a plain register map from the thread state without views.
This is used to decide if a thread has terminated, and to observe the
results of the model
Sets the value of a register
Definition set_reg (reg : reg) (rv : reg_type reg × view) (ts : t) : option t :=
if decide (is_Some (dmap_lookup reg ts.(regs))) then
Some $ set regs (dmap_insert reg rv) ts
else None.
if decide (is_Some (dmap_lookup reg ts.(regs))) then
Some $ set regs (dmap_insert reg rv) ts
else None.
Sets the coherence view of an address
Updates the coherence view of an address by taking the max of the new
view and of the existing value
Definition update_coh (addr : address) (v : view) (ts : t) : t :=
set_coh addr (max v (ts.(coh) !!! addr)) ts.
set_coh addr (max v (ts.(coh) !!! addr)) ts.
Updates the coherence view for a list of (address, view) pairs.
Definition update_cohs (avs : list (address × view)) (ts : t) : t :=
foldr (λ '(a, v), update_coh a v) ts avs.
foldr (λ '(a, v), update_coh a v) ts avs.
Updates the forwarding database for an address.
Sets the same FwdItem for every byte address in a write range.
Definition set_fwdbs (addrs : list address)
(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.
(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) (vpost : view) : t → t :=
setv xclb (Some (XclItem.make time addr size vpost)).
setv xclb (Some (XclItem.make time addr size vpost)).
Clears the exclusive database, to mark a store exclusive
Updates a view that from the state, by taking the max of new value and
the current value.
For example `update rmax vnew t` does t.rmax <- max t.rmax vnew
Updates two view in the same way as update. Purely for convenience
Definition update2 (acc1 acc2 : t → view) {_: Setter acc1} {_: Setter acc2}
(v : view) : t → t :=
(update acc1 v) ∘ (update acc2 v).
(v : view) : t → t :=
(update acc1 v) ∘ (update acc2 v).
Adds a promise to the promise set
Definition promise (v : view) : t → t := set prom (v ::.).
Definition no_promises_until (v : view) (ts : t) : Prop :=
∀ p ∈ ts.(prom), (v < p)%nat.
#[global] Instance Decision_no_promises_until (v : view) (ts : t) :
Decision (no_promises_until v ts).
Proof. unfold_decide. Defined.
End TState.
Definition no_promises_until (v : view) (ts : t) : Prop :=
∀ p ∈ ts.(prom), (v < p)%nat.
#[global] Instance Decision_no_promises_until (v : view) (ts : t) :
Decision (no_promises_until v ts).
Proof. unfold_decide. Defined.
End TState.
Intra instruction state for propagating views inside an instruction
Module IIS.
Record t :=
make {
strict : view;
rmw_read : option (nat × bool);
}.
#[global] Instance eta : Settable _ :=
settable! make <strict;rmw_read>.
Definition init : t := make 0 None.
Record t :=
make {
strict : view;
rmw_read : option (nat × bool);
}.
#[global] Instance eta : Settable _ :=
settable! make <strict;rmw_read>.
Definition init : t := make 0 None.
Add a new view to the IIS
Reads an instruction from initial memory. Returns the size-byte
instruction word as a bv (8 × size) formed by concatenating the
bytes in addr_range addr size. Fails if size is not 4, or
if any byte in the range has been overwritten by a later write.
Definition read_imem (addr : address) (init : memoryMap)
(mem : Memory.t) : Exec.res string (bv 32) :=
bytes ← othrow "Modified instruction memory" $
for a in addr_range addr 4 do
Memory.read_initial a init mem
end;
mret (bv_of_bytes 32 bytes).
(mem : Memory.t) : Exec.res string (bv 32) :=
bytes ← othrow "Modified instruction memory" $
for a in addr_range addr 4 do
Memory.read_initial a init mem
end;
mret (bv_of_bytes 32 bytes).
Returns all interesting timestamp when reading range addr, addr+size) with
minimum view [vpre]. Those are [vpre] itself and any later timestamp that
contain an overlapping write event
Definition read_candidates (addr : address) (size : N) (vpre : view)
(mem : Memory.t) : list nat :=
PromMemory.cut_after_with_timestamps vpre mem
|> omap (λ '(msg, t),
if decide (addr_overlap addr size (Msg.addr msg) (Msg.size msg))
then Some t else None)
|> cons vpre.
(mem : Memory.t) : list nat :=
PromMemory.cut_after_with_timestamps vpre mem
|> omap (λ '(msg, t),
if decide (addr_overlap addr size (Msg.addr msg) (Msg.size msg))
then Some t else None)
|> cons vpre.
Per-byte forwarding. Forwarding fires when fwdb !! addr has an entry fwd
with fwd.time > tread, which means there is a more recent po-previous
write that hasn't been propagated yet. In that case we replace the
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) :
Exec.res string (option (bv 8 × view × nat)) :=
match fwdb !! addr with
| Some fwd ⇒
if (tread <? fwd.(FwdItem.time))%nat then
msg ← othrow "Failed to retrieve forwarded message" (mem !! fwd.(FwdItem.time));
byte' ← othrow "Failed to read a byte from the message" (Msg.read_byte addr msg);
mret (Some (byte', FwdItem.read_fwd_view macc fwd, fwd.(FwdItem.time)))
else mret None
| None ⇒ mret None
end.
(tread : nat) (addr : address) :
Exec.res string (option (bv 8 × view × nat)) :=
match fwdb !! addr with
| Some fwd ⇒
if (tread <? fwd.(FwdItem.time))%nat then
msg ← othrow "Failed to retrieve forwarded message" (mem !! fwd.(FwdItem.time));
byte' ← othrow "Failed to read a byte from the message" (Msg.read_byte addr msg);
mret (Some (byte', FwdItem.read_fwd_view macc fwd, fwd.(FwdItem.time)))
else mret None
| None ⇒ mret None
end.
Performs a multi-byte memory read. This involves multiple steps:
- Computing the minimum view
- Picking an interesting timestamp tread with read_candidates
- Reading main memory at tread with Memory.read_from
- Applying forwarding (read_fwd)
- Do a coherence check
- Update all the views that should be updated
- If exclusive, set the exclusive database
- If atomic RMW, remember this read for the matching write
Definition read_mem (addr : address) (size : N) (macc : mem_acc) (init : memoryMap) :
Exec.t (PPState.t TState.t Msg.t IIS.t) string (bv (8 × size)) :=
ts ← mget PPState.state;
vaddr ← mget (IIS.strict ∘ PPState.iis);
guard_discard (TState.no_promises_until vaddr ts);;
let addrs := addr_range addr size in
let vbob := ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
⊔ view_if (is_rel_acq_rcsc macc) ts.(TState.vrel) in
let vpre := vaddr ⊔ vbob in
mem ← mget PPState.mem;
tread ← mchoosel (read_candidates addr size vpre mem);
( if is_atomic_rmw macc
then msetv (IIS.rmw_read ∘ PPState.iis) (Some (tread, is_rel_acq macc))
else mret ());;
raw_bytes ← othrow "Memory read of unmapped bytes" $
Memory.read_from addr size tread init mem;
fwd_bytes ← mlift $
for (addr, (byte, twrite)) in zip addrs raw_bytes do
read_fwd ts.(TState.fwdb) macc mem tread addr
|$> default (byte, tread, twrite)
end;
let bytes := fwd_bytes.*1.*1 in
let read_views := fwd_bytes.*1.*2 in
let twrites := fwd_bytes.*2 in
guard_discard (∀ '(a,t) ∈ zip addrs twrites, (ts.(TState.coh) !!! a ≤ t)%nat);;
let res := bv_of_bytes (8 × size) bytes in
let vreads := foldr max 0%nat read_views in
let vpost := vpre ⊔ vreads in
mset PPState.state $ TState.update_cohs (zip addrs twrites);;
mset PPState.state $ TState.update TState.vrd vpost;;
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 vpost
else mret ());;
mset PPState.iis $ IIS.add vpost;;
mret res.
Exec.t (PPState.t TState.t Msg.t IIS.t) string (bv (8 × size)) :=
ts ← mget PPState.state;
vaddr ← mget (IIS.strict ∘ PPState.iis);
guard_discard (TState.no_promises_until vaddr ts);;
let addrs := addr_range addr size in
let vbob := ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
⊔ view_if (is_rel_acq_rcsc macc) ts.(TState.vrel) in
let vpre := vaddr ⊔ vbob in
mem ← mget PPState.mem;
tread ← mchoosel (read_candidates addr size vpre mem);
( if is_atomic_rmw macc
then msetv (IIS.rmw_read ∘ PPState.iis) (Some (tread, is_rel_acq macc))
else mret ());;
raw_bytes ← othrow "Memory read of unmapped bytes" $
Memory.read_from addr size tread init mem;
fwd_bytes ← mlift $
for (addr, (byte, twrite)) in zip addrs raw_bytes do
read_fwd ts.(TState.fwdb) macc mem tread addr
|$> default (byte, tread, twrite)
end;
let bytes := fwd_bytes.*1.*1 in
let read_views := fwd_bytes.*1.*2 in
let twrites := fwd_bytes.*2 in
guard_discard (∀ '(a,t) ∈ zip addrs twrites, (ts.(TState.coh) !!! a ≤ t)%nat);;
let res := bv_of_bytes (8 × size) bytes in
let vreads := foldr max 0%nat read_views in
let vpost := vpre ⊔ vreads in
mset PPState.state $ TState.update_cohs (zip addrs twrites);;
mset PPState.state $ TState.update TState.vrd vpost;;
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 vpost
else mret ());;
mset PPState.iis $ IIS.add vpost;;
mret res.
Performs a memory write for a thread tid at addr:
- First attempt to fulfill an existing promises, or add a new one otherwise
- Compute the minimum view of the write
- Discard if the write is not compatible with that view or coherence checks
- Discard if the write is supposed to be atomic, but other writes intervened
- Update all the views that should be updated
- Set the forwarding database
- If a new promise was added, return its minimum view, otherwise None
Definition write_mem (tid : nat) (addr : address) (size : N) (macc : mem_acc)
(data : bv (8 × size)) :
Exec.t (PPState.t TState.t Msg.t IIS.t) string (option view) :=
let msg := Msg.make size tid addr data in
let is_release := is_rel_acq macc in
let addrs := addr_range addr size in
ts ← mget PPState.state;
mem ← mget PPState.mem;
'((time, new_promise) : nat × bool) ←
match Memory.fulfill msg (TState.prom ts) mem with
| Some time ⇒ mret (time, false)
| None ⇒
time ← Exec.liftSt PPState.mem $ Memory.promise msg;
mret (time, true)
end;
'(read_acquire : bool) ←
(if is_atomic_rmw macc then
rmw_read_opt ← mget (IIS.rmw_read ∘ PPState.iis);
'(tread, read_acquire) ← othrow "RMW write without a read" rmw_read_opt;
guard_discard' (Memory.exclusive tid addr size tread time mem);;
msetv (IIS.rmw_read ∘ PPState.iis) None;;
mret read_acquire
else mret false);
let vbob :=
ts.(TState.vdmbst) ⊔ ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
⊔ view_if is_release (ts.(TState.vrd) ⊔ ts.(TState.vwr)) in
vdata ← mget (IIS.strict ∘ PPState.iis);
let vpre := vdata ⊔ ts.(TState.vcap) ⊔ vbob in
guard_discard (vpre < time ∧ ∀ a ∈ addrs, ts.(TState.coh) !!! a < time)%nat;;
mset (TState.prom ∘ PPState.state) $ filter (λ t, t ≠ time);;
mset PPState.state $ TState.update_cohs (map (., time) addrs);;
mset PPState.state $ TState.update TState.vwr time;;
mset PPState.state $ TState.update TState.vrel (view_if is_release time);;
( if (is_atomic_rmw macc && is_rel_acq macc && read_acquire)
then mset PPState.state $ TState.update TState.vacq time
else mret ());;
fwd_xcl_view ← if is_exclusive macc then
match TState.xclb ts with
| None ⇒ mdiscard
| Some xcl ⇒
mset PPState.state $ TState.clear_xclb;;
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
mdiscard
end
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).
(data : bv (8 × size)) :
Exec.t (PPState.t TState.t Msg.t IIS.t) string (option view) :=
let msg := Msg.make size tid addr data in
let is_release := is_rel_acq macc in
let addrs := addr_range addr size in
ts ← mget PPState.state;
mem ← mget PPState.mem;
'((time, new_promise) : nat × bool) ←
match Memory.fulfill msg (TState.prom ts) mem with
| Some time ⇒ mret (time, false)
| None ⇒
time ← Exec.liftSt PPState.mem $ Memory.promise msg;
mret (time, true)
end;
'(read_acquire : bool) ←
(if is_atomic_rmw macc then
rmw_read_opt ← mget (IIS.rmw_read ∘ PPState.iis);
'(tread, read_acquire) ← othrow "RMW write without a read" rmw_read_opt;
guard_discard' (Memory.exclusive tid addr size tread time mem);;
msetv (IIS.rmw_read ∘ PPState.iis) None;;
mret read_acquire
else mret false);
let vbob :=
ts.(TState.vdmbst) ⊔ ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
⊔ view_if is_release (ts.(TState.vrd) ⊔ ts.(TState.vwr)) in
vdata ← mget (IIS.strict ∘ PPState.iis);
let vpre := vdata ⊔ ts.(TState.vcap) ⊔ vbob in
guard_discard (vpre < time ∧ ∀ a ∈ addrs, ts.(TState.coh) !!! a < time)%nat;;
mset (TState.prom ∘ PPState.state) $ filter (λ t, t ≠ time);;
mset PPState.state $ TState.update_cohs (map (., time) addrs);;
mset PPState.state $ TState.update TState.vwr time;;
mset PPState.state $ TState.update TState.vrel (view_if is_release time);;
( if (is_atomic_rmw macc && is_rel_acq macc && read_acquire)
then mset PPState.state $ TState.update TState.vacq time
else mret ());;
fwd_xcl_view ← if is_exclusive macc then
match TState.xclb ts with
| None ⇒ mdiscard
| Some xcl ⇒
mset PPState.state $ TState.clear_xclb;;
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
mdiscard
end
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).
Runs an outcome in the promising model while doing the correct view tracking
and computation. This can mutate memory because it will append a write at
the end of memory the corresponding event was not already promised.
Section RunOutcome.
Context (tid : nat) (initmem : memoryMap).
Equations run_outcome (out : outcome) :
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out × option view) :=
| RegWrite reg racc val ⇒
guard_or "Non trivial reg access types unsupported" (racc = None);;
vreg ← mget (IIS.strict ∘ PPState.iis);
vreg' ←
(if reg =? pc_reg
then
ts ← mget PPState.state;
guard_discard (TState.no_promises_until vreg ts);;
mset PPState.state $ TState.update TState.vcap vreg;;
mret 0%nat
else mret vreg);
ts ← mget PPState.state;
nts ← othrow "Register isn't mapped, can't write" $
TState.set_reg reg (val, vreg') ts;
msetv PPState.state nts;;
mret ((), None)
| RegRead reg racc ⇒
guard_or "Non trivial reg access types unsupported" (racc = None);;
ts ← mget PPState.state;
'(val, view) ← othrow "Register isn't mapped can't read" $
dmap_lookup reg ts.(TState.regs);
mset PPState.iis $ IIS.add view;;
mret (val, None)
| MemRead (MemReq.make macc addr addr_space size 0) ⇒
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
if is_ifetch macc then
size_4 ← guard_or "Ifetch read of size other than 4" (size = 4)%N;
mem ← mget PPState.mem;
opcode ← mlift $ read_imem addr initmem mem;
mret (Ok (ctrans _ opcode, 0%bv), None)
else if is_explicit macc then
val ← read_mem addr size macc initmem;
mret (Ok (val, 0%bv), None)
else mthrow "Read is not explicit nor ifetch"
| MemRead _ ⇒ mthrow "Memory read with tags unsupported"
| MemWriteAddrAnnounce _ ⇒
vaddr ← mget (IIS.strict ∘ PPState.iis);
ts ← mget PPState.state;
guard_discard (TState.no_promises_until vaddr ts);;
mset PPState.state $ TState.update TState.vcap vaddr;;
mret ((), None)
| MemWrite (MemReq.make macc addr addr_space size 0) val tags ⇒
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
guard_or "Only explicit writes are supported" (is_explicit macc);;
vpre_opt ← write_mem tid addr size macc val;
mret (Ok (), vpre_opt)
| MemWrite _ _ _ ⇒ mthrow "Memory write with tags unsupported"
| Barrier (Barrier_DMB dmb) ⇒
ts ← mget PPState.state;
match dmb.(DxB_types) with
| MBReqTypes_All ⇒
let vpost := ts.(TState.vrd) ⊔ ts.(TState.vwr) in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmb vpost
| MBReqTypes_Reads ⇒
let vpost := ts.(TState.vrd) in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmb vpost
| MBReqTypes_Writes ⇒
let vpost := ts.(TState.vwr) in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmbst vpost
end;;
mret ((), None)
| Barrier (Barrier_DSB dsb) ⇒
ts ← mget PPState.state;
let vpost :=
match dsb.(DxB_types) with
| MBReqTypes_All ⇒ ts.(TState.vrd) ⊔ ts.(TState.vwr)
| MBReqTypes_Reads ⇒ ts.(TState.vrd)
| MBReqTypes_Writes ⇒ ts.(TState.vwr)
end in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmb vpost;;
mret ((), None)
| Barrier (Barrier_ISB ()) ⇒
ts ← mget PPState.state;
let vpost := TState.vcap ts in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.visb vpost;;
mret ((), None)
| GenericFail s ⇒ mthrow ("Instruction failure: " ++ s)%string
| _ ⇒ mthrow "Unsupported outcome".
Solve Obligations with lia.
Definition run_outcome' (out : outcome) :
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
run_outcome out |$> fst.
End RunOutcome.
Context (tid : nat) (initmem : memoryMap).
Equations run_outcome (out : outcome) :
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out × option view) :=
| RegWrite reg racc val ⇒
guard_or "Non trivial reg access types unsupported" (racc = None);;
vreg ← mget (IIS.strict ∘ PPState.iis);
vreg' ←
(if reg =? pc_reg
then
ts ← mget PPState.state;
guard_discard (TState.no_promises_until vreg ts);;
mset PPState.state $ TState.update TState.vcap vreg;;
mret 0%nat
else mret vreg);
ts ← mget PPState.state;
nts ← othrow "Register isn't mapped, can't write" $
TState.set_reg reg (val, vreg') ts;
msetv PPState.state nts;;
mret ((), None)
| RegRead reg racc ⇒
guard_or "Non trivial reg access types unsupported" (racc = None);;
ts ← mget PPState.state;
'(val, view) ← othrow "Register isn't mapped can't read" $
dmap_lookup reg ts.(TState.regs);
mset PPState.iis $ IIS.add view;;
mret (val, None)
| MemRead (MemReq.make macc addr addr_space size 0) ⇒
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
if is_ifetch macc then
size_4 ← guard_or "Ifetch read of size other than 4" (size = 4)%N;
mem ← mget PPState.mem;
opcode ← mlift $ read_imem addr initmem mem;
mret (Ok (ctrans _ opcode, 0%bv), None)
else if is_explicit macc then
val ← read_mem addr size macc initmem;
mret (Ok (val, 0%bv), None)
else mthrow "Read is not explicit nor ifetch"
| MemRead _ ⇒ mthrow "Memory read with tags unsupported"
| MemWriteAddrAnnounce _ ⇒
vaddr ← mget (IIS.strict ∘ PPState.iis);
ts ← mget PPState.state;
guard_discard (TState.no_promises_until vaddr ts);;
mset PPState.state $ TState.update TState.vcap vaddr;;
mret ((), None)
| MemWrite (MemReq.make macc addr addr_space size 0) val tags ⇒
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
guard_or "Only explicit writes are supported" (is_explicit macc);;
vpre_opt ← write_mem tid addr size macc val;
mret (Ok (), vpre_opt)
| MemWrite _ _ _ ⇒ mthrow "Memory write with tags unsupported"
| Barrier (Barrier_DMB dmb) ⇒
ts ← mget PPState.state;
match dmb.(DxB_types) with
| MBReqTypes_All ⇒
let vpost := ts.(TState.vrd) ⊔ ts.(TState.vwr) in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmb vpost
| MBReqTypes_Reads ⇒
let vpost := ts.(TState.vrd) in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmb vpost
| MBReqTypes_Writes ⇒
let vpost := ts.(TState.vwr) in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmbst vpost
end;;
mret ((), None)
| Barrier (Barrier_DSB dsb) ⇒
ts ← mget PPState.state;
let vpost :=
match dsb.(DxB_types) with
| MBReqTypes_All ⇒ ts.(TState.vrd) ⊔ ts.(TState.vwr)
| MBReqTypes_Reads ⇒ ts.(TState.vrd)
| MBReqTypes_Writes ⇒ ts.(TState.vwr)
end in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.vdmb vpost;;
mret ((), None)
| Barrier (Barrier_ISB ()) ⇒
ts ← mget PPState.state;
let vpost := TState.vcap ts in
guard_discard (TState.no_promises_until vpost ts);;
mset PPState.state $ TState.update TState.visb vpost;;
mret ((), None)
| GenericFail s ⇒ mthrow ("Instruction failure: " ++ s)%string
| _ ⇒ mthrow "Unsupported outcome".
Solve Obligations with lia.
Definition run_outcome' (out : outcome) :
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
run_outcome out |$> fst.
End RunOutcome.
Import Promising.
Definition UMPromising : Promising.Model :=
{|tState := TState.t;
tState_init := λ tid, TState.init;
tState_regs := TState.reg_map;
tState_nopromises := is_emptyb ∘ TState.prom;
iis := IIS.t;
iis_init := IIS.init;
address_space := PAS_NonSecure;
mEvent := Msg.t;
mEvent_tid := Msg.tid;
filter_promises := λ _ _ _ promises, promises;
handle_outcome := λ _ tid initmem, run_outcome tid initmem;
emit_promise := λ tid initmem mem msg, TState.promise (length mem);
check_valid_end := λ _ _ _ _, [];
memory_snapshot := Memory.to_memMap;
|}.
Definition UMPromising_nocert :=
Promising_to_Modelnc false UMPromising.
Definition UMPromising_cert :=
Promising_to_Modelnc true UMPromising.
Definition UMPromising_exe := Promising_to_Modelc UMPromising.
Definition UMPromising_pf := Promising_to_Modelc_pf UMPromising.
Definition UMPromising_opmodel (isem : iMon ()) (n : nat) : opModel n :=
CPState.opmodel isem UMPromising.
Definition UMPromising_opmodel_pf (isem : iMon ()) (n : nat) : opModel n :=
CPState.opmodel_pf isem UMPromising.