From e95622e253ba8fb4c29b89e950883102a7e25fb6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 30 Jul 2022 20:11:56 +0100 Subject: Add more text --- env.mkiv | 50 ++++-- main.org | 560 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 590 insertions(+), 20 deletions(-) diff --git a/env.mkiv b/env.mkiv index ee8619f..6eecce9 100644 --- a/env.mkiv +++ b/env.mkiv @@ -67,25 +67,51 @@ \setupfootnotes[align={stretch,verytolerant,hz,hanging,hyphenated}] \setupmargindata[stack=yes] -\definecolor[codeblockcolor][x=EAF5F2] -\definecolor[codeblockborder][x=6AB9A4] \definetextbackground[codeblockbg][ location=paragraph, - background=color, - backgroundcolor=codeblockcolor, - bottomoffset=\bodyfontsize, + topoffset=\bodyfontsize, corner=round, - framecolor=codeblockborder, +] + +\definecolor[codeblockexportcolor][x=EAF5F2] +\definecolor[codeblockexportborder][x=6AB9A4] +\definetextbackground[codeblockexportbg][codeblockbg][ + background=color, + backgroundcolor=codeblockexportcolor, + framecolor=codeblockexportborder, +] + +\definecolor[codeblockexamplecolor][x=F5EBEA] +\definecolor[codeblockexampleborder][x=B96F6A] +\definetextbackground[codeblockexamplebg][codeblockbg][ + background=color, + backgroundcolor=codeblockexamplecolor, + framecolor=codeblockexampleborder, ] \setupenumeration [OrgListingEnumEmpty] [alternative=empty, - before={\blank\startcodeblockbg}, - after={\stopcodeblockbg\blank}, - margin=0pt] + before=, + after=\blank, + margin=0pt, + indentnext=no,] -\setupvimtyping[OrgBlkSrcCoq][margin=5mm] +\setupenumeration + [OrgExampleEnumEmpty] + [indentnext=no,] + +\setupvimtyping[OrgBlkSrcCoq][ + margin=5mm, + before={\startcodeblockexportbg\blank}, + after={\stopcodeblockexportbg}, +] + +\setuptyping[OrgExample][ + margin=5mm, + before={\startcodeblockexamplebg\blank}, + after={\stopcodeblockexamplebg}, +] \setupregister[OrgConcept][ style={\bfa\tt}, @@ -93,4 +119,8 @@ textstyle=tt, ] +\define\OrgTitleContents{} +\setupcombinedlist[content][alternative=c] +\setupsectionblock[frontpart][before=\blank,after=\blank,] + \stopenvironment diff --git a/main.org b/main.org index 17194ef..b45e96f 100644 --- a/main.org +++ b/main.org @@ -2,10 +2,11 @@ #+author: Yann Herklotz #+context_preset: ymhg-article #+context_header_extra: \environment env -#+options: syntax:vim toc:nil +#+options: syntax:vim #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v #+auto_tangle: t +#+context: \noindent One main optimisation in compilers targeting parallel architectures is /instruction scheduling/, where instructions are placed into time-slots statically so that these can be executed in parallel. To make this more manageable, the scheduler takes smaller chunks of code and schedules these instead @@ -24,7 +25,7 @@ This post[fn:1] covers multiple symbolic analysis passes and discusses their cor The general goal is to talk about a realistic implementation and correctness proof inside of Vericert, which uses the CompCert verified C compiler as the front end. -* Syntax Definitions +* Syntax Definition This section will cover some syntax definitions for the various constructs we will use, especially the syntax of a hyperblock and the symbolic expressions that are the result of the symbolic @@ -32,7 +33,35 @@ analysis. ** Quick Overview of Hyperblocks -Hyperblocks are a list of predicated instructions, which contain the +Hyperblocks are a list of predicated instructions, however, there are various ways in which these +predicates can be represented. Early works about predicated execution would have instructions that +are optionally paired with a literal, which can either be a true or false predicate. Then, there is +a predicated set-predicate instruction which defines the value for the predicate. + +#+begin_example +p ::= (b, n) +i ::= (p) instr + | (p) p = c +#+end_example + +However, there are various other possible definitions of this, for example the most general version +would be the following, which is the one we will be using in this file: + +#+begin_example +p ::= (b, n) | p ∨ p | p ∧ p +i ::= (p) instr + | (p) (b, n) = c +#+end_example + +There are also intermediate versions, where one can assign predicates using the set-predicate +operation or have unpredicate set-predicate operations. + +#+begin_example +p ::= (b, n) | p ∨ p | p ∧ p | p ::= (b, n) | p ∨ p | p ∧ p +i ::= (p) instr | i ::= (b, n) instr + | (b, n) = c | | (b, n) = c + | | (b, n) = p +#+end_example ** Syntax of Symbolic Expressions @@ -123,7 +152,22 @@ Definition predicated A := NE.non_empty (pred_op * A). Definition pred_expr := predicated expression. #+end_src -We can then also speak about equivalence between two predicates by +We can then also speak about equivalence between two predicates by using a SAT query, which uses a +formally verified SAT solver. + +#+begin_src coq +Compute sat_pred_simple (Plit (true, 1) ∨ Plit (false, 1)). +(* ==> None *) +#+end_src + +Finally, we will also define what an ~Rtree~ is, which is a mapping from resources to "something". +where ~R_indexed~ is a proof of injectivity from resources into the positives, and is further +defined in the [[R_indexed-def-link][next section]]. + +#+begin_src coq +<> +Module Rtree := ITree(R_indexed). +#+end_src #+begin_src coq Definition apred : Type := expression. @@ -133,23 +177,320 @@ Definition apred_expr := apredicated expression. #+end_src #+cindex: R_indexed-def - #+begin_src coq -<> -Module Rtree := ITree(R_indexed). Definition forest : Type := Rtree.t apred_expr. #+end_src -where ~R_indexed~ is a proof of injectivity from resources into the positives, and is further -defined in the [[R_indexed-def-link][next section]]. +I'll also quickly sneak in some execution semantics for expression trees and some helper functions +for the forest: + +#+cindex: forest-helpers +#+cindex: sem-expr +#+begin_src coq +<> +<> +<> +#+end_src + + +* About Execution Semantics + +The main idea is that given two expressions, if these expressions are equal, that they will also +behave the same. In the following Lemma, ~ictx~ is the execution context (register state, memory +state, etc...) of the input program, and ~octx~ is the execution context of the output program. + +#+begin_src coq :exports none +<> +#+end_src + +#+cindex: lemma-sem-value-det +#+name: lemma-sem-value-det +#+begin_src coq :tangle no +Lemma sem_value_det : + forall e v1 v2, sem_value ictx e v1 -> sem_value octx e v2 -> v1 = v2. +Proof. Abort. (* exercise left to the reader ;) *) +#+end_src + +However, this assumes that ~e~ is actually executable in both contexts, which is not something you +can assume. Instead, the only thing you know is that the input program is executable, so you want +to be able to show that if you have syntactically the same expressions on both sides, that the +output expression is also executable in its context. This means the Lemma should look like the +following: + +#+cindex: lemma-sem-value-det-better +#+name: lemma-sem-value-det-better +#+begin_src coq :tangle no +Lemma sem_value_det_better : + forall e v, sem_value ictx e v -> sem_value octx e v. +Proof. Abort. +#+end_src + +* Naive symbolic execution + +Now, doing /sound/ symbolic execution is a tricky business in the first place. Even without +predicates, you might assume that if you just collect all the possible values that each register can +take, and then get two states that are exactly the same, that this implies they two initial blocks +must execute the same in all cases. However, there are various issues when actually trying to prove +this formally. Semantics often block in cases where execution does not make sense, a common case +being division by zero. + +For the simple case where we are executing linear instructions, we can see how we can write a +function that will contain all possible values of instructions at the end. + +#+begin_src coq +Definition update_no_predicates f i: Rtree.t pred_expr := + match i with + | RBnop => f + | RBop _ op args dst => + f ! (Reg dst) <- + (NE.singleton + (T, (Eop op (to_elist (map (fun x => f ! (Reg x)) args))))) + | _ => f (* Not defining other cases. *) + end. +#+end_src + +The final version of this function will then allow you to prove the equivalence between two basic +blocks according to their semantics. Now let's add predicates to the function and try and do the +same. + +#+begin_src coq :exports none +<> +#+end_src + +#+cindex: update-function-simple-predicate +#+name: update-function-simple-predicate +#+begin_src coq :tangle no +Definition update (fop : Rtree.t pred_expr) (i : instr): Rtree.t pred_expr := + match i with + | RBnop => fop + | RBop p op rl r => + Rtree.set (Reg r) + (app_predicated (Option.default T p) + (get_forest' (Reg r) fop) + (map_predicated + (pred_ret (Eop op)) + (merge (list_translation rl fop)))) fop + | _ => fop (* Still not defining other cases. *) + end. +#+end_src + +Here we can see that the symbolic execution already becomes a bit more complicated, because we now +need to correctly deal with predicated instructions. The final representation is a /non-empty/ list +of /predicated/ symbolic expressions. The reason this representation is convenient instead of a +more recursive structure is that the result of this ~update~ function can just be passed to a SAT +solver, by referring to expressions as numbers. This will tell us that two of these predicated +expression lists are equivalent /iff/ a pair of predicates from each list is equivalent under +satisfiability and their expressions are syntactically equal. -* First Attempt at Symbolic Analysis +** Does This Imply Equivalent Behaviour + +Now the question is if this implies equivalent behaviour, and the answer is it doesn't, because we +don't have good enough execution semantics for the predicates. From the update function, we are +taking predicates directly from the instruction, meaning even if any literals inside of those +predicates are changed using a set-predicate instruction, the predicates will still evaluate to the +same result. + +* Complicating Life a Bit With Abstract Predicates * Appendix :PROPERTIES: :APPENDIX: :END: +** Semantics of Expressions + +*** ~sem-expr~ +:PROPERTIES: +:CUSTOM_ID: sem-expr-link +:END: + +#+cindex: sem-expr +#+name: sem-expr +#+begin_src coq :tangle no +Section SEMANTICS. + +Context {A : Type}. + +Record ctx : Type := mk_ctx { + ctx_is: instr_state; + ctx_sp: val; + ctx_ge: Genv.t A unit; +}. + +Definition ctx_rs ctx := is_rs (ctx_is ctx). +Definition ctx_ps ctx := is_ps (ctx_is ctx). +Definition ctx_mem ctx := is_mem (ctx_is ctx). + +Inductive sem_value : ctx -> expression -> val -> Prop := +| Sbase_reg: + forall r ctx, + sem_value ctx (Ebase (Reg r)) ((ctx_rs ctx) !! r) +| Sop: + forall ctx op args v lv, + sem_val_list ctx args lv -> + Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op lv (ctx_mem ctx) = Some v -> + sem_value ctx (Eop op args) v +| Sload : + forall ctx mexp addr chunk args a v m' lv, + sem_mem ctx mexp m' -> + sem_val_list ctx args lv -> + Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a -> + Memory.Mem.loadv chunk m' a = Some v -> + sem_value ctx (Eload chunk addr args mexp) v +with sem_pred : ctx -> expression -> bool -> Prop := +| Spred: + forall ctx args c lv v, + sem_val_list ctx args lv -> + Op.eval_condition c lv (ctx_mem ctx) = Some v -> + sem_pred ctx (Esetpred c args) v +| Sbase_pred: + forall ctx p, + sem_pred ctx (Ebase (Pred p)) ((ctx_ps ctx) !! p) +with sem_mem : ctx -> expression -> Memory.mem -> Prop := +| Sstore : + forall ctx mexp vexp chunk addr args lv v a m' m'', + sem_mem ctx mexp m' -> + sem_value ctx vexp v -> + sem_val_list ctx args lv -> + Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a -> + Memory.Mem.storev chunk m' a v = Some m'' -> + sem_mem ctx (Estore vexp chunk addr args mexp) m'' +| Sbase_mem : + forall ctx, + sem_mem ctx (Ebase Mem) (ctx_mem ctx) +with sem_exit : ctx -> expression -> option cf_instr -> Prop := +| Sexit : + forall ctx cf, + sem_exit ctx (Eexit cf) (Some cf) +| Sbase_exit : + forall ctx, + sem_exit ctx (Ebase Exit) None +with sem_val_list : ctx -> expression_list -> list val -> Prop := +| Snil : + forall ctx, + sem_val_list ctx Enil nil +| Scons : + forall ctx e v l lv, + sem_value ctx e v -> + sem_val_list ctx l lv -> + sem_val_list ctx (Econs e l) (v :: lv) +. + +Inductive eval_apred (c: ctx): apred_op -> bool -> Prop := +| eval_APtrue : eval_apred c Ptrue true +| eval_APfalse : eval_apred c Pfalse false +| eval_APlit : forall p (b: bool) bres, + sem_pred c p (if b then bres else negb bres) -> + eval_apred c (Plit (b, p)) bres +| eval_APand : forall p1 p2 b1 b2, + eval_apred c p1 b1 -> + eval_apred c p2 b2 -> + eval_apred c (Pand p1 p2) (b1 && b2) +| eval_APor1 : forall p1 p2 b1 b2, + eval_apred c p1 b1 -> + eval_apred c p2 b2 -> + eval_apred c (Por p1 p2) (b1 || b2). + +Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop): + ctx -> apred_expr -> B -> Prop := +| sem_pred_expr_cons_true : + forall ctx e pr p' v, + eval_apred ctx pr true -> + sem ctx e v -> + sem_pred_expr sem ctx ((pr, e) ::| p') v +| sem_pred_expr_cons_false : + forall ctx e pr p' v, + eval_apred ctx pr false -> + sem_pred_expr sem ctx p' v -> + sem_pred_expr sem ctx ((pr, e) ::| p') v +| sem_pred_expr_single : + forall ctx e pr v, + eval_apred ctx pr true -> + sem ctx e v -> + sem_pred_expr sem ctx (NE.singleton (pr, e)) v +. + +Definition collapse_pe (p: apred_expr) : option expression := + match p with + | NE.singleton (APtrue, p) => Some p + | _ => None + end. + +Inductive sem_predset : ctx -> forest -> predset -> Prop := +| Spredset: + forall ctx f rs', + (forall x, sem_pred_expr sem_pred ctx (f # (Pred x)) (rs' !! x)) -> + sem_predset ctx f rs'. + +Inductive sem_regset : ctx -> forest -> regset -> Prop := +| Sregset: + forall ctx f rs', + (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) -> + sem_regset ctx f rs'. + +Inductive sem : ctx -> forest -> instr_state * option cf_instr -> Prop := +| Sem: + forall ctx rs' m' f pr' cf, + sem_regset ctx f rs' -> + sem_predset ctx f pr' -> + sem_pred_expr sem_mem ctx (f # Mem) m' -> + sem_pred_expr sem_exit ctx (f # Exit) cf -> + sem ctx f (mk_instr_state rs' pr' m', cf). + +End SEMANTICS. +#+end_src + +*** ~genv-preserved~ +:PROPERTIES: +:CUSTOM_ID: genv-preserved-link +:END: + +#+cindex: genv-preserved +#+name: genv-preserved +#+begin_src coq :tangle no +Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop := + (forall sp op vl m, Op.eval_operation ge sp op vl m = + Op.eval_operation tge sp op vl m) + /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl = + Op.eval_addressing tge sp addr vl). + +Lemma ge_preserved_same: + forall A B ge, @ge_preserved A B A B ge ge. +Proof. unfold ge_preserved; auto. Qed. +#[local] Hint Resolve ge_preserved_same : core. + +Inductive match_states : instr_state -> instr_state -> Prop := +| match_states_intro: + forall ps ps' rs rs' m m', + (forall x, rs !! x = rs' !! x) -> + (forall x, ps !! x = ps' !! x) -> + m = m' -> + match_states (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). + +Lemma match_states_refl x : match_states x x. +Proof. destruct x; constructor; crush. Qed. + +Lemma match_states_commut x y : match_states x y -> match_states y x. +Proof. inversion 1; constructor; crush. Qed. + +Lemma match_states_trans x y z : + match_states x y -> match_states y z -> match_states x z. +Proof. repeat inversion 1; constructor; crush. Qed. + +#[global] +Instance match_states_Equivalence : Equivalence match_states := + { Equivalence_Reflexive := match_states_refl ; + Equivalence_Symmetric := match_states_commut ; + Equivalence_Transitive := match_states_trans ; }. + +Inductive similar {A B} : @ctx A -> @ctx B -> Prop := +| similar_intro : + forall ist ist' sp ge tge, + ge_preserved ge tge -> + match_states ist ist' -> + similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge). +#+end_src + ** ~abstr-imports~ :PROPERTIES: :CUSTOM_ID: abstr-imports-link @@ -179,13 +520,19 @@ Require Import vericert.hls.HashTree. Require Import vericert.hls.Predicate. Require Import vericert.common.DecEq. Require vericert.common.NonEmpty. +Require Import vericert.common.Monad. Module NE := NonEmpty. Import NE.NonEmptyNotation. +Module OptionExtra := MonadExtra(Option). +Import OptionExtra. +Import OptionExtra.MonadNotation. + #[local] Open Scope positive. #[local] Open Scope pred_op. #[local] Open Scope non_empty_scope. +#[local] Open Scope monad_scope. #+end_src ** Definition of ~R_indexed~ @@ -234,6 +581,199 @@ Module R_indexed. End R_indexed. #+end_src +** Forest helpers + +*** ~forest-helpers~ +:PROPERTIES: +:CUSTOM_ID: forest-helpers-link +:END: + +#+cindex: forest-helpers +#+name: forest-helpers +#+begin_src coq :tangle no +Definition get_forest v (f: forest) := + match Rtree.get v f with + | None => NE.singleton (Ptrue, (Ebase v)) + | Some v' => v' + end. + +Definition get_forest' v (f: Rtree.t pred_expr) := + match Rtree.get v f with + | None => NE.singleton (Ptrue, (Ebase v)) + | Some v' => v' + end. + +Definition get_forest2 v (f: Rtree.t pred_expr) := + match Rtree.get v f with + | None => (Ebase v) + | Some v' => + match v' with + | NE.singleton (_, e) => e + | _ => (Ebase v) (* Just a place-holder. *) + end + end. + +Fixpoint to_elist l := + match l with + | nil => Enil + | a :: b => Econs a (to_elist b) + end. + +Declare Scope forest. + +Notation "a # b" := (get_forest b a) (at level 1) : forest. +Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level) : forest. + +Notation "a ! b" := (get_forest2 b a) (at level 1) : forest. +Notation "a ! b <- c" := (Rtree.set b c a) (at level 1, b at next level) : forest. + +#[local] Open Scope forest. + +Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) := + match p with + | Some p' => if eval_predf pr p' then v else vo + | None => v + end. + +Definition get_pr i := match i with mk_instr_state a b c => b end. + +Definition get_m i := match i with mk_instr_state a b c => c end. + +Definition eval_predf_opt pr p := + match p with Some p' => eval_predf pr p' | None => true end. +#+end_src + +** ~section-abstr-eval~ + +#+cindex: section-abstr-eval +#+name: section-abstr-eval +#+begin_src coq :tangle no +Section ABSTR_EVAL. + Definition fd := GibleSeq.fundef. + Definition tfd := GiblePar.fundef. + + Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx). + + <> + <> +End ABSTR_EVAL. +#+end_src + +** Definition of pred_op version + +#+cindex: predicated-op-defs +#+name: predicated-op-defs +#+begin_src coq :tangle no +Fixpoint list_translation (l : list reg) (f : Rtree.t pred_expr) {struct l} + : list pred_expr := + match l with + | nil => nil + | i :: l => (get_forest' (Reg i) f) :: (list_translation l f) + end. + +Fixpoint replicate {A} (n: nat) (l: A) := + match n with + | O => nil + | S n => l :: replicate n l + end. + +Definition merge''' {A: Type} (x y: option (@Predicate.pred_op A)) := + match x, y with + | Some p1, Some p2 => Some (Pand p1 p2) + | Some p, None | None, Some p => Some p + | None, None => None + end. + +Definition merge'' {A: Type} x := + match x with + | ((a, e), (b, el)) => (@merge''' A a b, Econs e el) + end. + +Definition map_pred_op {A B P: Type} (pf: option (@Predicate.pred_op P) * (A -> B)) + (pa: option (@Predicate.pred_op P) * A): option (@Predicate.pred_op P) * B := + match pa, pf with + | (p, a), (p', f) => (merge''' p p', f a) + end. + +Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := + NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) + (NE.non_empty_prod p1 p2). + +Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A) + : predicated B := NE.map (fun x => (fst x, f (snd x))) p. + +(*map (fun x => (fst x, Econs (snd x) Enil)) pel*) +Definition merge' (pel: pred_expr) (tpel: predicated expression_list) := + predicated_map (uncurry Econs) (predicated_prod pel tpel). + +Fixpoint merge (pel: list pred_expr): predicated expression_list := + match pel with + | nil => NE.singleton (T, Enil) + | a :: b => merge' a (merge b) + end. + +Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A) + : predicated B := + predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa). + +Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A) + : predicated B := + NE.map (fun x => (fst x, (snd x) pa)) pf. + +Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) + (pb: B): predicated C := + NE.map (fun x => (fst x, (snd x) pa pb)) pf. + +Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) + (pa: A) (pb: B) (pc: C): predicated D := + NE.map (fun x => (fst x, (snd x) pa pb pc)) pf. + +Definition predicated_from_opt {A: Type} (p: option apred_op) (a: A) := + match p with + | Some p' => NE.singleton (p', a) + | None => NE.singleton (T, a) + end. + +#[local] Open Scope non_empty_scope. +#[local] Open Scope pred_op. + +Fixpoint NEfold_left {A B} (f: A -> B -> A) (l: NE.non_empty B) (a: A) : A := + match l with + | NE.singleton a' => f a a' + | a' ::| b => NEfold_left f b (f a a') + end. + +Fixpoint NEapp {A} (l m: NE.non_empty A) := + match l with + | NE.singleton a => a ::| m + | a ::| b => a ::| NEapp b m + end. + +Definition app_predicated' {A: Type} (a b: predicated A) := + let negation := ¬ (NEfold_left (fun a b => a ∨ (fst b)) b ⟂) in + NEapp (NE.map (fun x => (negation ∧ fst x, snd x)) a) b. + +Definition app_predicated {A: Type} (p': pred_op) (a b: predicated A) := + NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a) + (NE.map (fun x => (p' ∧ fst x, snd x)) b). + +Definition prune_predicated {A: Type} (a: predicated A) := + NE.filter (fun x => match deep_simplify peq (fst x) with ⟂ => false | _ => true end) + (NE.map (fun x => (deep_simplify peq (fst x), snd x)) a). + +Definition pred_ret {A: Type} (a: A) : predicated A := + NE.singleton (T, a). +#+end_src + +#+cindex: module-pred-op +#+name: module-pred-op +#+begin_src coq :tangle no +Module PredOpVersion. + <> + <> +End PredOpVersion. +#+end_src + * Index :PROPERTIES: :APPENDIX: -- cgit