Skip to content

Promise-First Optimization #32

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

Promise-First Optimization #32

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3cc8a0f
Implement Promise-First optimization
febyeji Oct 11, 2025
fbfa855
Add venumerate
febyeji Nov 12, 2025
53d1c39
Simplify promise-first code
febyeji Nov 12, 2025
6d10f9e
Re-add the computational model without promise-free optimization
febyeji Nov 26, 2025
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
120 changes: 87 additions & 33 deletions ArchSem/GenPromising.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,27 +170,38 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
it generic *)
Structure BasicExecutablePM := {
pModel :> PromisingModel;
(** try to compute ALL allowed promises, if that is not possible (not
enough fuel) then fail with error message.

Soundness and completeness proofs are required to show that when not
failing, promise_select effectively computes the allowed_promises
set.*)
promise_select :
enumerate_promises_and_terminal_states :
(* fuel *) nat → (* tid *) nat →
(* termination condition *) (registerMap → bool) →
memoryMap → pModel.(tState) → PromMemory.t pModel.(mEvent) →
Exec.res string pModel.(mEvent);
result string (list pModel.(mEvent) * list pModel.(tState));

promise_select_sound :
∀ fuel tid term initMem ts mem,
∀ ev ∈ (promise_select fuel tid term initMem ts mem),
ev ∈ pModel.(allowed_promises) tid initMem ts mem;
∀ fuel tid term initMem ts mem promises tstates,
Ok (promises, tstates) =
enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
∀ ev ∈ promises, ev ∈ pModel.(allowed_promises) tid initMem ts mem;

promise_select_complete :
∀ fuel tid term initMem ts mem,
¬ Exec.has_error (promise_select fuel tid term initMem ts mem) →
∀ ev ∈ pModel.(allowed_promises) tid initMem ts mem,
ev ∈ promise_select fuel tid term initMem ts mem
∀ fuel tid term initMem ts mem promises tstates,
Ok (promises, tstates) =
enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
∀ ev ∈ pModel.(allowed_promises) tid initMem ts mem, ev ∈ promises;

terminal_state_no_outstanding_promise :
∀ fuel tid term initMem ts mem promises tstates,
Ok (promises, tstates) =
enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
∀ tts ∈ tstates, pModel.(tState_nopromises) tts;

terminal_state_is_terminated :
∀ fuel tid term initMem ts mem promises tstates,
Ok (promises, tstates) =
enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
∀ tts ∈ tstates, term (pModel.(tState_regs) tts);

(* TODO: add terminal_state_is_reachable *)
}.
Arguments BasicExecutablePM : clear implicits.

Expand Down Expand Up @@ -328,10 +339,24 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
Local Notation mEvent := (mEvent prom).
Local Notation t := (t tState mEvent 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.

(** 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.

(** 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 :=
prom.(promise_select) fuel tid (term tid) (initmem st) (tstate tid st) (events st).
'(promises, _) ← mlift $ prom.(enumerate_promises_and_terminal_states)
fuel tid (term tid) (initmem st) (tstate tid st) (events st);
mchoosel promises.

(** Take any promising step for that tid and promise it *)
Definition cpromise_tid (fuel : nat) (tid : fin n)
Expand All @@ -355,20 +380,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
promise ← mchoosel (enum bool);
if (promise : bool) then cpromise_tid fuel tid else run_tid isem prom tid.

(** 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.


(** 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.

(** Computational evaluate all the possible allowed final states according
(** Computationally evaluate all the possible allowed final states according
to the promising model prom starting from st *)
Fixpoint run (fuel : nat) : Exec.t t string final :=
st ← mGet;
Expand All @@ -378,21 +390,63 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
run_step (S fuel);;
run fuel
else mthrow "Could not finish running within the size of the fuel".

(** Computationally evaluate all the possible allowed final states according
to the promising model prom starting from st with promise-first optimization.
The size of fuel should be at least (# of promises) + max(# of instructions) + 1 *)
Fixpoint run_promise_first (fuel : nat) : Exec.t t string final :=
if fuel is S fuel then
st ← mGet;
(* Find out next possible promises or terminating states at the current thread *)
executions ←
vmapM (λ '(tid, ts),
'(promises_per_tid, tstates_per_tid) ←
mlift $ prom.(enumerate_promises_and_terminal_states)
fuel (fin_to_nat tid) (term tid) (initmem st) ts (events st);
mret (map (.,tid) promises_per_tid, tstates_per_tid)
) (venumerate (tstates st));

promise ← mchoosel (enum bool);
if (promise : bool) then
(* Non-deterministically choose the next promise and the tid for pruning *)
let promises_all := List.concat (vmap fst executions) in
'(next_ev, tid) ← mchoosel promises_all;
mSet (λ st, promise_tid prom st tid next_ev);;
run_promise_first fuel
else
(* Compute cartesian products of the possible thread states *)
let tstates_all := cprodn (vmap snd executions) in
let new_finals :=
omap (λ tstates,
let st := Make tstates st.(PState.initmem) st.(PState.events) in
if decide $ terminated prom term st is left pt
then Some (make_final st pt)
else None
) tstates_all in
mchoosel new_finals
else
mthrow "Could not finish running within the size of the fuel".

End CPS.
Arguments to_final_archState {_ _ _}.
End CPState.

(** Create a computational model from an ISA model and promising model *)
(** Create computational models from an ISA model and promising model *)
Definition Promising_to_Modelc (isem : iMon ()) (prom : BasicExecutablePM)
(fuel : nat) : archModel.c ∅ :=
fun n term (initMs : archState n) =>
λ n term (initMs : archState n),
PState.from_archState prom initMs |>
archModel.Res.from_exec
$ CPState.to_final_archState
<$> CPState.run isem prom term fuel.

(* TODO state some soundness lemma between Promising_to_Modelnc and
Promising_Modelc *)
Definition Promising_to_Modelc_pf (isem : iMon ()) (prom : BasicExecutablePM)
(fuel : nat) : archModel.c ∅ :=
λ n term (initMs : archState n),
PState.from_archState prom initMs |>
archModel.Res.from_exec
$ CPState.to_final_archState
<$> CPState.run_promise_first prom term fuel.
Copy link
Collaborator

@tperami tperami Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Promising_to_Modelc should still use run and we should have Promising_to_Modelc_pf as an additional thing, ideally, and tests should run both. Sorry if it wasn't clear

Copy link
Collaborator Author

@febyeji febyeji Nov 25, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, sorry. I will fix it.


End GenPromising.

Expand Down
43 changes: 29 additions & 14 deletions ArchSemArm/UMPromising.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -416,7 +416,7 @@ Definition read_fwd_view (macc : mem_acc) (f : FwdItem.t) :=
Definition read_mem (loc : Loc.t) (vaddr : view) (macc : mem_acc)
(init : Memory.initial) (mem : Memory.t) :
Exec.t TState.t string (view * val) :=
guard_or "Atomic RMV unsupported" (¬ (is_atomic_rmw macc));;
guard_or "Atomic RMW unsupported" (¬ (is_atomic_rmw macc));;
ts ← mGet;
let vbob := ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
(* SC Acquire loads are ordered after Release stores *)
Expand Down Expand Up @@ -457,7 +457,8 @@ Definition read_mem4 (addr : address) (macc : mem_acc) (init : Memory.initial) :
This may mutate memory if no existing promise can be fullfilled *)
Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
(macc : mem_acc) (mem : Memory.t)
(data : val) : Exec.t TState.t string (Memory.t * view * option view):=
(data : val) :
Exec.t TState.t string (Memory.t * view * option view):=
let msg := Msg.make tid loc data in
let is_release := is_rel_acq macc in
ts ← mGet;
Expand Down Expand Up @@ -489,7 +490,7 @@ Definition write_mem_xcl (tid : nat) (loc : Loc.t)
(vdata : view) (macc : mem_acc)
(mem : Memory.t) (data : val)
: Exec.t TState.t string (Memory.t * option view) :=
guard_or "Atomic RMV unsupported" (¬ (is_atomic_rmw macc));;
guard_or "Atomic RMW unsupported" (¬ (is_atomic_rmw macc));;
let xcl := is_exclusive macc in
if xcl then
'(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data;
Expand Down Expand Up @@ -659,11 +660,14 @@ Section ComputeProm.
else
mret res.

Fixpoint runSt_to_termination
(* Run the thread state until termination, collecting certified promises.
Returns true if termination occurs within the given fuel,
false otherwise. *)
Fixpoint run_to_termination_promise
(isem : iMon ())
(fuel : nat)
(base : nat)
: Exec.t (CProm.t * PPState.t TState.t Msg.t IIS.t) string bool :=
(base : nat) :
Exec.t (CProm.t * PPState.t TState.t Msg.t IIS.t) string bool :=
match fuel with
| 0%nat =>
ts ← mget (PPState.state ∘ snd);
Expand All @@ -675,20 +679,26 @@ Section ComputeProm.
if term (TState.reg_map ts) then
mret true
else
runSt_to_termination isem fuel base
run_to_termination_promise isem fuel base
end.

Definition run_to_termination (isem : iMon ())
(fuel : nat)
(ts : TState.t)
(mem : Memory.t)
: Exec.res string Msg.t :=
: result string (list Msg.t * list TState.t) :=
let base := List.length mem in
let res := Exec.results $ runSt_to_termination isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
guard_or ("Could not finish promises within the size of the fuel")%string (∀ r ∈ res, r.2 = true);;
res.*1.*1
|> union_list
|> mchoosel ∘ CProm.proms.
let res_proms := Exec.results $
run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
guard_or ("Out of fuel when searching for new promises")%string
(∀ r ∈ res_proms, r.2 = true);;
let promises := res_proms.*1.*1 |> union_list |> CProm.proms in
let tstates :=
res_proms
|> omap (λ '((cp, st), _),
if is_emptyb (CProm.proms cp) then Some (PPState.state st)
else None) in
mret (promises, tstates).

End ComputeProm.

Expand Down Expand Up @@ -764,12 +774,17 @@ Definition UMPromising_cert_nc isem :=
Program Definition UMPromising_exe' (isem : iMon ())
: BasicExecutablePM :=
{|pModel := UMPromising_cert' isem;
promise_select :=
enumerate_promises_and_terminal_states :=
λ fuel tid term initmem ts mem,
run_to_termination tid initmem term isem fuel ts mem
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.

Definition UMPromising_cert_c isem fuel :=
Promising_to_Modelc isem (UMPromising_exe' isem) fuel.

Definition UMPromising_cert_c_pf isem fuel :=
Promising_to_Modelc_pf isem (UMPromising_exe' isem) fuel.
55 changes: 33 additions & 22 deletions ArchSemArm/VMPromising.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1540,7 +1540,7 @@ Definition run_mem_read (addr : address) (macc : mem_acc) (init : Memory.initial
mret val
else mthrow "Unsupported 8 bytes access".

Definition run_mem_read4 (addr : address) (macc : mem_acc) (init : Memory.initial) :
Definition run_mem_read4 (addr : address) (macc : mem_acc) (init : Memory.initial) :
Exec.t Memory.t string (bv 32) :=
if is_ifetch macc then
let aligned_addr := bv_unset_bit 2 addr in
Expand All @@ -1558,8 +1558,8 @@ Definition run_mem_read4 (addr : address) (macc : mem_acc) (init : Memory.initi

This may mutate memory if no existing promise can be fullfilled *)
Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
(invalidation_time : option nat) (macc : mem_acc)
(data : val) : Exec.t (TState.t * Memory.t) string (view * option view) :=
(invalidation_time : option nat) (macc : mem_acc) (data : val) :
Exec.t (TState.t * Memory.t) string (view * option view) :=
let msg := Msg.make tid loc data in
let is_release := is_rel_acq macc in
'(ts, mem) ← mGet;
Expand All @@ -1585,10 +1585,7 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
mset fst $ TState.update_coh loc time;;
mset fst $ TState.update TState.vwr time;;
mset fst $ TState.update TState.vrel (view_if is_release time);;
match new_promise with
| true => mret (time, Some vpre)
| false => mret (time, None)
end.
mret (time, if (new_promise : bool) then Some vpre else None).

(** Tries to perform a memory write.

Expand Down Expand Up @@ -1896,7 +1893,7 @@ Section RunOutcome.
| _ => mthrow "Unsupported outcome".

Definition run_outcome' (out : outcome) :
Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
run_outcome out |$> fst.

End RunOutcome.
Expand Down Expand Up @@ -1945,11 +1942,14 @@ Section ComputeProm.
else
mret res.

Fixpoint runSt_to_termination
(* Run the thread state until termination, collecting certified promises.
Returns true if termination occurs within the given fuel,
false otherwise. *)
Fixpoint run_to_termination_promise
(isem : iMon ())
(fuel : nat)
(base : nat)
: Exec.t (CProm.t * PPState.t TState.t Ev.t IIS.t) string bool :=
(base : nat) :
Exec.t (CProm.t * PPState.t TState.t Ev.t IIS.t) string bool :=
match fuel with
| 0%nat =>
ts ← mget (PPState.state ∘ snd);
Expand All @@ -1961,20 +1961,26 @@ Section ComputeProm.
if term (TState.reg_map ts) then
mret true
else
runSt_to_termination isem fuel base
run_to_termination_promise isem fuel base
end.

Definition run_to_termination (isem : iMon ())
(fuel : nat)
(ts : TState.t)
(mem : Memory.t)
: Exec.res string Ev.t :=
: result string (list Ev.t * list TState.t) :=
let base := List.length mem in
let res := Exec.results $ runSt_to_termination isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
guard_or ("Could not finish promises within the size of the fuel")%string (∀ r ∈ res, r.2 = true);;
res.*1.*1
|> union_list
|> mchoosel ∘ CProm.proms.
let res_proms := Exec.results $
run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
guard_or ("Out of fuel when searching for new promises")%string
(∀ r ∈ res_proms, r.2 = true);;
let promises := res_proms.*1.*1 |> union_list |> CProm.proms in
let tstates :=
res_proms
|> omap (λ '((cp, st), _),
if is_emptyb (CProm.proms cp) then Some (PPState.state st)
else None) in
mret (promises, tstates).

End ComputeProm.

Expand Down Expand Up @@ -2023,8 +2029,7 @@ Definition allowed_promises_cert (isem : iMon ()) tid (initmem : memoryMap)
TState.prom ts' = []
]}.


Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
{|tState := TState.t;
tState_init := λ tid, TState.init;
tState_regs := TState.reg_map;
Expand All @@ -2040,16 +2045,22 @@ Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
λ initmem, Memory.to_memMap (Memory.initial_from_memMap initmem);
|}.

(** Implement the Executable Promising Model *)

Program Definition VMPromising_exe' (isem : iMon ())
: BasicExecutablePM :=
{|pModel := VMPromising_cert' isem;
promise_select :=
enumerate_promises_and_terminal_states :=
λ fuel tid term initmem ts mem,
run_to_termination tid initmem term isem fuel ts mem
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.

Next Obligation. Admitted.
Next Obligation. Admitted.

Definition VMPromising_cert_c isem fuel :=
Promising_to_Modelc isem (VMPromising_exe' isem) fuel.

Definition VMPromising_cert_c_pf isem fuel :=
Promising_to_Modelc_pf isem (VMPromising_exe' isem) fuel.
Loading