Library ArchSem.GenPromising
This module define common infrastructure shared between all promising model
In particular it defined the PromisingModel type that can be used to
manipulate promising models in a first order manner.
From ASCommon Require Import Options.
From ASCommon Require Import Common Exec FMon StateT.
Require Import Interface.
Require Import TermModels.
This module define the representation of a promising model memory as
a sequence of events.
The sequence is 1 indexed so that timestamp 0 represent memory as it was
initially.
The current implementation is a list in reverse order but that may change
Definition of the memory numbering. So it can be used with the !! operator
Global Instance lookup_inst : Lookup nat ev t := {
lookup k mem :=
if k =? 0%nat then None
else
let len := List.length mem in
if (k <=? len)%nat then List.nth_error mem (len - k)%nat else None
}.
lookup k mem :=
if k =? 0%nat then None
else
let len := List.length mem in
if (k <=? len)%nat then List.nth_error mem (len - k)%nat else None
}.
Cuts the memory to only what exists before the timestamp, included.
The timestamp can still be computed the same way.
Cuts the memory to only what exists after the timestamp, excluded.
Beware of timestamp computation. If you need the original timestamps,
use cut_after_timestamps
Cuts the memory to only what exists after the timestamp, excluded.
Provide the original timestamps as a additional value.
Fixpoint attach_timestamps (mem : t) : list (ev × nat) :=
match mem with
| [] ⇒ []
| h :: q ⇒
(h, List.length mem) :: attach_timestamps q
end.
Definition cut_after_with_timestamps (v : nat) (mem : t) : list (ev × nat) :=
take (length mem - v) (attach_timestamps mem).
End PM.
Arguments t : clear implicits.
End PromMemory.
#[export] Typeclasses Transparent PromMemory.t.
Module PPState.
Section PPS.
Context {tState : Type}.
Context {mEvent : Type}.
Context {iis_t : Type}.
Record t :=
Make {
state : tState;
mem : PromMemory.t mEvent;
iis : iis_t;
}.
#[global] Instance eta : Settable t :=
settable! @Make <state;mem;iis>.
End PPS.
Arguments t : clear implicits.
End PPState.
Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
(TM : TermModelsT Arch Inter).
Import Arch.
Import Inter.
Import TM.
Module Promising.
match mem with
| [] ⇒ []
| h :: q ⇒
(h, List.length mem) :: attach_timestamps q
end.
Definition cut_after_with_timestamps (v : nat) (mem : t) : list (ev × nat) :=
take (length mem - v) (attach_timestamps mem).
End PM.
Arguments t : clear implicits.
End PromMemory.
#[export] Typeclasses Transparent PromMemory.t.
Module PPState.
Section PPS.
Context {tState : Type}.
Context {mEvent : Type}.
Context {iis_t : Type}.
Record t :=
Make {
state : tState;
mem : PromMemory.t mEvent;
iis : iis_t;
}.
#[global] Instance eta : Settable t :=
settable! @Make <state;mem;iis>.
End PPS.
Arguments t : clear implicits.
End PPState.
Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
(TM : TermModelsT Arch Inter).
Import Arch.
Import Inter.
Import TM.
Module Promising.
This structure defines a promising model that can share common
infrastructure define in this file. This structure allows to define 4
models:
The first one is there for theoretical reason, but it probably can return
UB on any input, but any non-error behavior it exhibits should also be in
the certified version, so it can be useful for sanity checking.
Theoretically the last 3 models are equivalent (up to fuel for the
executable ones).
TODO: Figure out generic properties to relate those 4 models.
- The non-certified non-executable version where any promises can be made as long as they are all fulfilled by the end
- The certified non-executable version where promises can only be made if there is a sequential trace that lead to that promise being fulfilled.
- The direct executable model which explores all interleaving of promising and instruction steps
- The promise-free executable model which does a smarter search based on some commutation properties of steps, namely that instruction step of different thread commute and that a promise step after an instruction step can always be commuted to be before.
The thread state of the model
Initialize the model thread state from architectural state
Get a register map out of a thread state to test the termination
condition and compute a final state
Check if a thread state has no pending promises, which means that it
can be explained with the current memory state
Intra instruction state, reset after each instruction
The type of memory event, any communication between threads must go here
Give the tid that initiated that event
Filter executable promise candidates from a single enumeration run.
The memory does not yet contain the candidates being selected.
The address space this model is built against, we expect non-secure
for Arm here
The handler for instruction effects, applies the effect of a single
outcome to the thread state. If the outcome need one or more event to
be added to memory,it adds them and return the view of those events in
the option, otherwise it returns None
handle_outcome : nat → nat →
memoryMap →
∀ out : outcome,
Exec.t (PPState.t tState mEvent iis) string
(eff_ret out × option nat);
memoryMap →
∀ out : outcome,
Exec.t (PPState.t tState mEvent iis) string
(eff_ret out × option nat);
Update the thread state after emission of a promise. The new promise
has already been added to the memory when calling that function. I'm
not considering that emit_promise can fail or have a non-deterministic
behaviour. TODO: Add support for failure
Hook for extra UB checks to be done before returning a final state,
e.g. BBM checks. Any returned string is an error, [] is success.
Computes the final memory after a certain promising history
memory_snapshot : memoryMap → PromMemory.t mEvent → memoryMap;
}.
#[global] Arguments Model : clear implicits.
End Promising.
Module PState. Section PS.
Context {tState : Type}.
Context {mEvent : Type}.
Context {n : nat}.
Record t :=
Make {
tstates : vec tState n;
initmem : memoryMap;
events : PromMemory.t mEvent;
}.
#[global] Instance set_t : Settable t :=
settable! @Make <tstates;initmem;events>.
Definition tstate tid := ((.!!! tid) ∘ tstates).
#[global] Typeclasses Transparent tstate.
End PS.
Arguments t : clear implicits.
Section PSProm.
Import Promising.
Context (isem : iMon ()).
Context (prom : Model).
Context {n : nat}.
Local Notation tState := prom.(tState).
Local Notation mEvent := prom.(mEvent).
Local Notation t := (t tState mEvent n).
}.
#[global] Arguments Model : clear implicits.
End Promising.
Module PState. Section PS.
Context {tState : Type}.
Context {mEvent : Type}.
Context {n : nat}.
Record t :=
Make {
tstates : vec tState n;
initmem : memoryMap;
events : PromMemory.t mEvent;
}.
#[global] Instance set_t : Settable t :=
settable! @Make <tstates;initmem;events>.
Definition tstate tid := ((.!!! tid) ∘ tstates).
#[global] Typeclasses Transparent tstate.
End PS.
Arguments t : clear implicits.
Section PSProm.
Import Promising.
Context (isem : iMon ()).
Context (prom : Model).
Context {n : nat}.
Local Notation tState := prom.(tState).
Local Notation mEvent := prom.(mEvent).
Local Notation t := (t tState mEvent n).
Check if a thread has finished according to term
Definition terminated_tid (term : terminationCondition n) (ps : t)
(tid : fin n) := ps |> tstate tid |> prom.(tState_regs) |> term tid.
(tid : fin n) := ps |> tstate tid |> prom.(tState_regs) |> term tid.
Check if all thread have finished according to term
Definition terminated (term : terminationCondition n) (ps : t) :=
fforallb (terminated_tid term ps).
fforallb (terminated_tid term ps).
Check if a thread has no outstanding promises
Check if all threads have no outstanding promises
Check if a thread state can be at a valid end
Definition check_valid_end_tid (ps : t) (tid : fin n) :=
prom.(check_valid_end) tid ps.(initmem) (tstate tid ps) ps.(events).
prom.(check_valid_end) tid ps.(initmem) (tstate tid ps) ps.(events).
Check if all thread states can be at a valid end
Definition check_valid_end (ps : t) :=
List.concat (map (check_valid_end_tid ps) (enum (fin n))).
Definition PState_PPState tid (pst : t) :
PPState.t tState mEvent prom.(iis) :=
PPState.Make (tstate tid pst) pst.(events) prom.(iis_init).
Instance PState_PPState_set tid : Setter (PState_PPState tid) :=
λ update_ppst pst,
let ppst := PState_PPState tid pst |> update_ppst in
pst
|> setv (tstate tid) ppst.(PPState.state)
|> setv events ppst.(PPState.mem).
List.concat (map (check_valid_end_tid ps) (enum (fin n))).
Definition PState_PPState tid (pst : t) :
PPState.t tState mEvent prom.(iis) :=
PPState.Make (tstate tid pst) pst.(events) prom.(iis_init).
Instance PState_PPState_set tid : Setter (PState_PPState tid) :=
λ update_ppst pst,
let ppst := PState_PPState tid pst |> update_ppst in
pst
|> setv (tstate tid) ppst.(PPState.state)
|> setv events ppst.(PPState.mem).
Run on instruction in specific thread by tid, allowing new promises
Definition run_tid (tid : fin n) : Exec.t t string () :=
st ← mGet;
let handler out :=
prom.(handle_outcome) n tid (st.(initmem)) out |$> fst in
Exec.liftSt (PState_PPState tid) (cinterp handler isem).
Definition seq_step (tid : fin n) : relation t :=
λ st1 st2, st2 ∈ Exec.success_state_list $ run_tid tid st1.
st ← mGet;
let handler out :=
prom.(handle_outcome) n tid (st.(initmem)) out |$> fst in
Exec.liftSt (PState_PPState tid) (cinterp handler isem).
Definition seq_step (tid : fin n) : relation t :=
λ st1 st2, st2 ∈ Exec.success_state_list $ run_tid tid st1.
Emit a promise from a thread by tid
Definition promise_tid (tid : fin n) (event : mEvent) (st : t) :=
let st := set events (event ::.) st in
set (tstate tid)
(prom.(emit_promise) tid st.(initmem) st.(events) event)
st.
let st := set events (event ::.) st in
set (tstate tid)
(prom.(emit_promise) tid st.(initmem) st.(events) event)
st.
Compute the set of allowed promises by a thread indexed by tid
Definition allowed_promises_tid (certified : bool) (st : t) (tid : fin n)
(ev : mEvent) :
Prop :=
if certified then
prom.(mEvent_tid) ev = tid ∧
∃ st', rtc (seq_step tid) (promise_tid tid ev st) st' ∧
nopromises_tid st' tid
else prom.(mEvent_tid) ev = tid.
(ev : mEvent) :
Prop :=
if certified then
prom.(mEvent_tid) ev = tid ∧
∃ st', rtc (seq_step tid) (promise_tid tid ev st) st' ∧
nopromises_tid st' tid
else prom.(mEvent_tid) ev = tid.
The inductive stepping relation of the promising model
Inductive step (certified : bool) (ps : t) : (t) → Prop :=
| SRun (tid : fin n) (ps' : t) :
(ps', ()) ∈ (run_tid tid ps) → step certified ps ps'
| SPromise (tid : fin n) (event : mEvent) :
allowed_promises_tid certified ps tid event →
step certified ps (promise_tid tid event ps).
Lemma step_promise certified (ps ps' : t) (tid : fin n) (event : mEvent) :
allowed_promises_tid certified ps tid event →
ps' = promise_tid tid event ps →
step certified ps ps'.
Proof using. sauto l:on. Qed.
| SRun (tid : fin n) (ps' : t) :
(ps', ()) ∈ (run_tid tid ps) → step certified ps ps'
| SPromise (tid : fin n) (event : mEvent) :
allowed_promises_tid certified ps tid event →
step certified ps (promise_tid tid event ps).
Lemma step_promise certified (ps ps' : t) (tid : fin n) (event : mEvent) :
allowed_promises_tid certified ps tid event →
ps' = promise_tid tid event ps →
step certified ps ps'.
Proof using. sauto l:on. Qed.
Create an initial promising state from a generic machine state
Definition from_archState (ms: archState n) : t :=
{|tstates :=
fun_to_vec
(λ tid,
prom.(tState_init) tid ms.(archState.memory)
$ ms.(archState.regs) !!! tid);
initmem := ms.(archState.memory);
events := []|}.
{|tstates :=
fun_to_vec
(λ tid,
prom.(tState_init) tid ms.(archState.memory)
$ ms.(archState.regs) !!! tid);
initmem := ms.(archState.memory);
events := []|}.
Convert a promising state to a generic machine state.
This is a lossy conversion
Definition to_archState (ps: t) : archState n :=
{|archState.regs := vmap (prom.(tState_regs)) ps.(tstates);
archState.memory := prom.(memory_snapshot) ps.(initmem) ps.(events);
archState.address_space := prom.(address_space) |}.
End PSProm.
End PState.
{|archState.regs := vmap (prom.(tState_regs)) ps.(tstates);
archState.memory := prom.(memory_snapshot) ps.(initmem) ps.(events);
archState.address_space := prom.(address_space) |}.
End PSProm.
End PState.
Create a non-computational model from an ISA model and promising model
Definition Promising_to_Modelnc (certified : bool) (prom : Promising.Model)
(isem : iMon ()) : archModel.nc ∅ :=
λ n term (initMs : archState n),
{[ mr : archModel.res ∅ n term |
let initPs := PState.from_archState prom initMs in
match mr with
| archModel.Res.FinalState fs _ ⇒
∃ finPs, rtc (PState.step isem prom certified) initPs finPs ∧
PState.to_archState prom finPs = fs ∧
PState.nopromises prom finPs ∧
PState.check_valid_end prom finPs = []
| archModel.Res.Error s ⇒
∃ finPs,
rtc (PState.step isem prom certified) initPs finPs ∧
((∃ tid, Error s ∈ PState.run_tid isem prom tid finPs)
∨
(PState.terminated prom term finPs ∧
PState.nopromises prom finPs ∧
s ∈ PState.check_valid_end prom finPs))
| _ ⇒ False
end]}.
(isem : iMon ()) : archModel.nc ∅ :=
λ n term (initMs : archState n),
{[ mr : archModel.res ∅ n term |
let initPs := PState.from_archState prom initMs in
match mr with
| archModel.Res.FinalState fs _ ⇒
∃ finPs, rtc (PState.step isem prom certified) initPs finPs ∧
PState.to_archState prom finPs = fs ∧
PState.nopromises prom finPs ∧
PState.check_valid_end prom finPs = []
| archModel.Res.Error s ⇒
∃ finPs,
rtc (PState.step isem prom certified) initPs finPs ∧
((∃ tid, Error s ∈ PState.run_tid isem prom tid finPs)
∨
(PState.terminated prom term finPs ∧
PState.nopromises prom finPs ∧
s ∈ PState.check_valid_end prom finPs))
| _ ⇒ False
end]}.
Computational promising state. Right now it the same type as PState.t but
with more methods
Module CPState.
Import Promising.
Include PState.
Section CPS.
Context (isem : iMon ()).
Context (prom : Model).
Context {n : nat}.
Local Notation tState := (tState prom).
Local Notation mEvent := (mEvent prom).
Local Notation iis := (iis prom).
Local Notation t := (t tState mEvent n).
Let mEvent_eq_dec := prom.(mEvent_eq_dec).
Local Existing Instance mEvent_eq_dec.
Section Steps.
Context (term : terminationCondition n).
Import Promising.
Include PState.
Section CPS.
Context (isem : iMon ()).
Context (prom : Model).
Context {n : nat}.
Local Notation tState := (tState prom).
Local Notation mEvent := (mEvent prom).
Local Notation iis := (iis prom).
Local Notation t := (t tState mEvent n).
Let mEvent_eq_dec := prom.(mEvent_eq_dec).
Local Existing Instance mEvent_eq_dec.
Section Steps.
Context (term : terminationCondition n).
The type of final promising state return by run
Definition final := { x : t | terminated prom term x }.
Definition make_final (p : t) := exist (terminated prom term) p.
Definition validate_final (st : t) : Exec.t t string unit :=
guard_discard $ nopromises prom st;;
let errs := check_valid_end prom st in
if errs is [] then
mret ()
else
err ← mchoosel errs;
mthrow err.
Definition make_final (p : t) := exist (terminated prom term) p.
Definition validate_final (st : t) : Exec.t t string unit :=
guard_discard $ nopromises prom st;;
let errs := check_valid_end prom st in
if errs is [] then
mret ()
else
err ← mchoosel errs;
mthrow err.
Convert a final promising state to a generic final state
Program Definition to_final_archState (f : final) :
{s & archState.is_terminated term s} :=
existT (to_archState prom f) _.
Solve All Obligations with
hauto unfold:terminated unfold:archState.is_terminated l:on db:vec, brefl.
Section EnumerateResult.
Context (tid : fin n) (initmem : memoryMap).
Definition run_outcome_with_promise (base : nat) (out : outcome) :
Exec.t (list mEvent × PPState.t tState mEvent iis) string
(eff_ret out) :=
'(res, vpre_opt) ←
Exec.liftSt snd $ prom.(handle_outcome) n tid initmem out;
if vpre_opt is Some vpre then
if decide (vpre ≤ base)%nat then
mem ← mget (PPState.mem ∘ snd);
mset fst (take (length mem - base) mem ++.);;
mret res
else mret res
else
mret res.
{s & archState.is_terminated term s} :=
existT (to_archState prom f) _.
Solve All Obligations with
hauto unfold:terminated unfold:archState.is_terminated l:on db:vec, brefl.
Section EnumerateResult.
Context (tid : fin n) (initmem : memoryMap).
Definition run_outcome_with_promise (base : nat) (out : outcome) :
Exec.t (list mEvent × PPState.t tState mEvent iis) string
(eff_ret out) :=
'(res, vpre_opt) ←
Exec.liftSt snd $ prom.(handle_outcome) n tid initmem out;
if vpre_opt is Some vpre then
if decide (vpre ≤ base)%nat then
mem ← mget (PPState.mem ∘ snd);
mset fst (take (length mem - base) mem ++.);;
mret res
else mret res
else
mret res.
Runs a thread sequentially to termination, collecting all promises
that had to be made. Returns false if it ran out of fuel during
exploration. fuel is the maximum number of instructions to be run.
Fixpoint run_to_termination (fuel : nat) (base : nat) :
Exec.t (list mEvent × PPState.t tState mEvent iis) string bool :=
ts ← mget (PPState.state ∘ snd);
if term tid (prom.(tState_regs) ts) then
mret true
else
match fuel with
| 0%nat ⇒ mret false
| S fuel ⇒
msetv (PPState.iis ∘ snd) prom.(iis_init);;
let handler := run_outcome_with_promise base in
cinterp handler isem;;
run_to_termination fuel base
end.
Record EnumerationResult :=
{
promises : list mEvent;
final_states : list tState;
errors : list string;
out_of_fuel : bool
}.
Exec.t (list mEvent × PPState.t tState mEvent iis) string bool :=
ts ← mget (PPState.state ∘ snd);
if term tid (prom.(tState_regs) ts) then
mret true
else
match fuel with
| 0%nat ⇒ mret false
| S fuel ⇒
msetv (PPState.iis ∘ snd) prom.(iis_init);;
let handler := run_outcome_with_promise base in
cinterp handler isem;;
run_to_termination fuel base
end.
Record EnumerationResult :=
{
promises : list mEvent;
final_states : list tState;
errors : list string;
out_of_fuel : bool
}.
Enumerate all possible executions for a thread in a given memory.
fuel Is the maximum number of instructions to be run for each
thread.
Definition enumerate_results (fuel : nat) (ts : tState)
(mem : PromMemory.t mEvent) : EnumerationResult :=
let base := List.length mem in
let res :=
run_to_termination fuel base
([], PPState.Make ts mem prom.(iis_init))
in
let success_states := Exec.success_state_list res in
let out_of_fuel := bool_decide (∃ r ∈ (Exec.results res).*2, ¬ (r : bool)) in
let promises :=
List.concat ((success_states.*1) ++ (Exec.errors res).*1.*1)
|> remove_dups in
let promises := prom.(filter_promises) n tid mem promises in
let tstates :=
success_states
|> omap (λ '(new_proms, st),
if is_emptyb new_proms then Some (PPState.state st)
else None) in
let errors :=
res |> Exec.errors |>
omap (λ '((new_proms, _), err_msg),
if is_emptyb new_proms then Some err_msg
else None) in
{|promises:=promises;
final_states:=tstates;
errors:=errors;
out_of_fuel:=out_of_fuel|}.
End EnumerateResult.
(mem : PromMemory.t mEvent) : EnumerationResult :=
let base := List.length mem in
let res :=
run_to_termination fuel base
([], PPState.Make ts mem prom.(iis_init))
in
let success_states := Exec.success_state_list res in
let out_of_fuel := bool_decide (∃ r ∈ (Exec.results res).*2, ¬ (r : bool)) in
let promises :=
List.concat ((success_states.*1) ++ (Exec.errors res).*1.*1)
|> remove_dups in
let promises := prom.(filter_promises) n tid mem promises in
let tstates :=
success_states
|> omap (λ '(new_proms, st),
if is_emptyb new_proms then Some (PPState.state st)
else None) in
let errors :=
res |> Exec.errors |>
omap (λ '((new_proms, _), err_msg),
if is_emptyb new_proms then Some err_msg
else None) in
{|promises:=promises;
final_states:=tstates;
errors:=errors;
out_of_fuel:=out_of_fuel|}.
End EnumerateResult.
Get a list of possible promises for a thread by tid
Definition promise_select_tid (fuel : nat) (st : t)
(tid : fin n) : Exec.res string mEvent :=
let (promises, _, _, out_of_fuel) :=
enumerate_results tid (initmem st) fuel (tstate tid st) (events st)
in
if out_of_fuel then
b ← mchoosef bool;
if (b : bool) then mthrow "out of fuel" else mchoosel promises
else mchoosel promises.
(tid : fin n) : Exec.res string mEvent :=
let (promises, _, _, out_of_fuel) :=
enumerate_results tid (initmem st) fuel (tstate tid st) (events st)
in
if out_of_fuel then
b ← mchoosef bool;
if (b : bool) then mthrow "out of fuel" else mchoosel promises
else mchoosel promises.
Take any promising step for that tid and promise it
Definition cpromise_tid (fuel : nat) (tid : fin n) : Exec.t t string () :=
st ← mGet;
ev ← mlift (promise_select_tid fuel st tid);
mSetv (promise_tid prom tid ev st).
st ← mGet;
ev ← mlift (promise_select_tid fuel st tid);
mSetv (promise_tid prom tid ev st).
Run any possible step, this is the most exhaustive and expensive kind of
search but it is obviously correct. If a thread has reached termination
no progress is made in the thread (either instruction running or
promises
Definition run_step (fuel : nat) : Exec.t t string () :=
st ← mGet;
tid ← mchoose n;
if terminated_tid prom term st tid then mdiscard
else
promise ← mchoosel (enum bool);
if (promise : bool) then cpromise_tid fuel tid else run_tid isem prom tid.
st ← mGet;
tid ← mchoose n;
if terminated_tid prom term st tid then mdiscard
else
promise ← mchoosel (enum bool);
if (promise : bool) then cpromise_tid fuel tid else run_tid isem prom tid.
A single transition of the direct promising model: either the current
state is final, or any certified promise or instruction step is taken.
fuel is the maximum number of instruction to run in each thread to
find a certified promise.
Returning None means it was a non-final step
Definition run_transition (fuel : nat) :
Exec.t t string (option {s & archState.is_terminated term s}) :=
st ← mGet;
if decide $ terminated prom term st is left pt then
validate_final st;;
mret (Some (to_final_archState (make_final st pt)))
else
run_step fuel;;
mret None.
Exec.t t string (option {s & archState.is_terminated term s}) :=
st ← mGet;
if decide $ terminated prom term st is left pt then
validate_final st;;
mret (Some (to_final_archState (make_final st pt)))
else
run_step fuel;;
mret None.
A single transition of the promise-first promising model.
It explore executions of all threads collecting promises and either
choose one of them, or, if it's possible to reach a final state without
making any new promises, return that final state.
fuel is the maximum number of instruction to be explored for each
thread.
Returning None means it was a non-final step
Definition run_transition_promise_first (fuel : nat) :
Exec.t t string (option {s & archState.is_terminated term s}) :=
st ← mGet;
let execution_results :=
vmap (λ '(tid, ts),
enumerate_results tid (initmem st) fuel ts (events st)
) (venumerate (tstates st)) in
opt ← mchoosel (seq 0 4);
match opt : nat with
| 0 ⇒
tid ← mchoosef (fin n);
next_ev ← mchoosel (execution_results !!! tid).(promises);
mSet (promise_tid prom tid next_ev);;
mret None
| 1 ⇒
tstates ← mchoosel $ cprodn (vmap final_states execution_results);
let st := Make tstates st.(initmem) st.(events) in
term_proof ← guard_discard $ terminated prom term st;
validate_final st;;
mret (Some (to_final_archState (make_final st term_proof)))
| 2 ⇒
let errs := List.concat (vmap errors execution_results) in
err ← mchoosel errs;
mthrow err
| _ ⇒
if bool_decide (∃ x ∈ map out_of_fuel execution_results, (x : bool)) then
mthrow "Promise first: out of fuel in enumeration"
else mdiscard
end.
End Steps.
Exec.t t string (option {s & archState.is_terminated term s}) :=
st ← mGet;
let execution_results :=
vmap (λ '(tid, ts),
enumerate_results tid (initmem st) fuel ts (events st)
) (venumerate (tstates st)) in
opt ← mchoosel (seq 0 4);
match opt : nat with
| 0 ⇒
tid ← mchoosef (fin n);
next_ev ← mchoosel (execution_results !!! tid).(promises);
mSet (promise_tid prom tid next_ev);;
mret None
| 1 ⇒
tstates ← mchoosel $ cprodn (vmap final_states execution_results);
let st := Make tstates st.(initmem) st.(events) in
term_proof ← guard_discard $ terminated prom term st;
validate_final st;;
mret (Some (to_final_archState (make_final st term_proof)))
| 2 ⇒
let errs := List.concat (vmap errors execution_results) in
err ← mchoosel errs;
mthrow err
| _ ⇒
if bool_decide (∃ x ∈ map out_of_fuel execution_results, (x : bool)) then
mthrow "Promise first: out of fuel in enumeration"
else mdiscard
end.
End Steps.
The promising model as an operational model. Each transition is either a
promise step or a full instruction step of any thread, which means all
the interleavings of promises and instructions are explored.
The required fuel is:
( of promises) + of instructions of all threads + 1
Definition opmodel : opModel n :=
let init _ initSt := from_archState prom initSt in
let step term _ fuel := run_transition term fuel in
opModel.Make n t init step.
let init _ initSt := from_archState prom initSt in
let step term _ fuel := run_transition term fuel in
opModel.Make n t init step.
The promise-first promising model as an operational model.
Transitions are just certified promises until the last transition that
run all threads instructions to the end in one step.
The required fuel is ( of promises) + max( of instructions or 1)
Definition opmodel_pf : opModel n :=
let init _ initSt := from_archState prom initSt in
let step term _ fuel := run_transition_promise_first term fuel in
opModel.Make n t init step.
End CPS.
Arguments to_final_archState {_ _ _}.
End CPState.
let init _ initSt := from_archState prom initSt in
let step term _ fuel := run_transition_promise_first term fuel in
opModel.Make n t init step.
End CPS.
Arguments to_final_archState {_ _ _}.
End CPState.
Create a computational model from an ISA model and promising model.
fuel needed is one per promise and per instruction of any thread + one
for the final transition
Definition Promising_to_Modelc (prom : Promising.Model) (isem : iMon ())
(fuel : nat) : archModel.c ∅ :=
opModel.to_archModel (@CPState.opmodel isem prom) fuel.
(fuel : nat) : archModel.c ∅ :=
opModel.to_archModel (@CPState.opmodel isem prom) fuel.
Create a computational model from an ISA model and promising model, using
the promise-first optimisation
Definition Promising_to_Modelc_pf (prom : Promising.Model) (isem : iMon ())
(fuel : nat) : archModel.c ∅ :=
opModel.to_archModel (@CPState.opmodel_pf isem prom) fuel.
End GenPromising.
Module Type GenPromisingT (Arch : Arch) (Inter : InterfaceT Arch)
(TM : TermModelsT Arch Inter).
Include GenPromising Arch Inter TM.
End GenPromisingT.
(fuel : nat) : archModel.c ∅ :=
opModel.to_archModel (@CPState.opmodel_pf isem prom) fuel.
End GenPromising.
Module Type GenPromisingT (Arch : Arch) (Inter : InterfaceT Arch)
(TM : TermModelsT Arch Inter).
Include GenPromising Arch Inter TM.
End GenPromisingT.