From 49a2d62e18ae741a0bee6ca8404b261d7780a3eb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 31 Jul 2022 20:23:43 +0100 Subject: Final changes --- Makefile | 4 + main.org | 397 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 387 insertions(+), 14 deletions(-) diff --git a/Makefile b/Makefile index e51f7ff..084f9d0 100644 --- a/Makefile +++ b/Makefile @@ -16,6 +16,10 @@ Main.v: main.org @echo "TANGLE" $< @emacs -batch -find-file main.org -funcall org-babel-tangle +%.pdf: %.mkiv + @echo "CONTEXT" $< + @context $< + Makefile.coq _CoqProject: force @echo "COQMAKE Makefile.coq" @$(COQMAKE) $(COQINCLUDES) $(VS) -o Makefile.coq diff --git a/main.org b/main.org index b45e96f..7758147 100644 --- a/main.org +++ b/main.org @@ -2,8 +2,9 @@ #+author: Yann Herklotz #+context_preset: ymhg-article #+context_header_extra: \environment env -#+options: syntax:vim +#+options: syntax:vim h:2 #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v +#+html_head_extra: #+auto_tangle: t #+context: \noindent @@ -164,21 +165,12 @@ Finally, we will also define what an ~Rtree~ is, which is a mapping from resourc 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]]. +#+cindex: R_indexed-def +#+cindex: apred-type-definitions #+begin_src coq <> Module Rtree := ITree(R_indexed). -#+end_src - -#+begin_src coq -Definition apred : Type := expression. -Definition apred_op := @Predicate.pred_op apred. -Definition apredicated A := NE.non_empty (apred_op * A). -Definition apred_expr := apredicated expression. -#+end_src - -#+cindex: R_indexed-def -#+begin_src coq -Definition forest : Type := Rtree.t apred_expr. +<> #+end_src I'll also quickly sneak in some execution semantics for expression trees and some helper functions @@ -186,13 +178,13 @@ for the forest: #+cindex: forest-helpers #+cindex: sem-expr +#+cindex: genv-preserved #+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 @@ -292,6 +284,218 @@ same result. * Complicating Life a Bit With Abstract Predicates +One solution to the predicate execution problem is to also evaluate predicates symbolically, so that +one can execute them with the starting context as well. This is an obvious extension to the +previous method, and also reuses the symbolic execution that was done for predicates. However, it +definitely does not come for free. Currently we had the following model, which even though the +proof of correctness does not quite pass at the end, had a simple idea for doing the proof. We had +the following definition for predicated expressions, which had a direct representation when doing +the SAT check, as one only has to turn all the expressions into uniquely identifying numbers. + +#+begin_src coq +Definition example_pred_expr: pred_expr := + (Plit (false, 1), Ebase (Reg 2)) + ::| NE.singleton (Plit (true, 1), Ebase (Reg 1)). +#+end_src + +This could be represented using the following formula, where $e_2$ is just a variable which is +paired with the syntactic ~Ebase (Reg 2)~: + +#+begin_export context +\startformula + \neg p_1 \rightarrow e_2 \land p_1 \rightarrow e_1 +\stopformula +#+end_export + +#+begin_export html +\begin{equation} + \neg p_1 \rightarrow e_2 \land p_1 \rightarrow e_1 +\end{equation} +#+end_export + +However, let's now go over how symbolic execution would work with symbolic predicates. + +** Symbolic Execution with Symbolic Predicate + +We can define abstract predicates as the following, defined as a snippet called +~<>~ which was inserted earlier, and we define a forest type like the +following. + +#+cindex: apred-type-definitions +#+name: apred-type-definitions +#+begin_src coq :tangle no +Definition apred : Type := expression. +Definition apred_op := @Predicate.pred_op apred. +Definition apredicated A := NE.non_empty (apred_op * A). +Definition apred_expr := apredicated expression. + +Definition forest : Type := Rtree.t apred_expr. +#+end_src + +We will first define the update function that works with symbolic predicates in the most general +sense, just so that we can guarantee that we now have correct predicates which imply the runtime +equivalence between two predicated expressions. This means that everytime we encounter a predicate, +we will have to evaluate it with the current expressions forest and retrieve the correct value for +each of the literals at this moment in the execution. We have to start by defining a function like +that, starting by just simply turning a /symbolic predicated expression/ into a symbolic predicate, +which is essentially what was done in the previous section, but now with more rich predicates. + +#+begin_src coq +Fixpoint apredicated_to_apred_op + (b: bool) + (a: apredicated expression): apred_op := + match a with + | NE.singleton (p, e) => p → Plit (b, e) + | (p, e) ::| r => + (p → Plit (b, e)) ∧ apredicated_to_apred_op b r + end. +#+end_src + +We then use this function to turn a standard predicated into an abstract predicate. This works as +expected for every case of the predicate syntax, except for the literal case, where we call the +~apredicated_to_apred_op~ function to get a predicate that represents this expression. + +#+begin_src coq +Fixpoint get_pred' (f: forest) (ap: pred_op): apred_op := + match ap with + | Ptrue => Ptrue + | Pfalse => Pfalse + | Plit (a, b) => + apredicated_to_apred_op a (f # (Pred b)) + | Pand a b => Pand (get_pred' f a) (get_pred' f b) + | Por a b => Por (get_pred' f a) (get_pred' f b) + end. +#+end_src + +There is already quite some nesting, because we used to only have predicates externally to +expressions, but now they can be nested as well. As a quick example, the expressions presented in +the previous sections might look like the following in the current representation. + +The following represents the dynamic value that is present in predicate ~Pred 1~, which is the +predicate we were evaluating in the previous section. + +#+begin_src coq +Definition dynamic_esetpred: expression := + Esetpred (Op.Ccomp Clt) + (to_elist ((Ebase (Reg 1)) + :: Ebase (Reg 2) + :: nil)). +#+end_src + +Then, this will be present in the final ~apred_expr~, which contains all the information of the +current values of each of the predicates, including which expression should then hold. + +#+begin_src coq +Definition example_pred_expr2: apred_expr := + ((Ptrue → Plit (false, dynamic_esetpred)), Ebase (Reg 2)) + ::| NE.singleton ((Ptrue → Plit (true, dynamic_esetpred)), + Ebase (Reg 1)). +#+end_src + +When we then want to pass this expression to the SAT solver to reason about the equivalence between +two ~apred_expr~, you might realise that we have to turn each of the expressions into numbers again, +which lands us back at exactly the same expression we already had previously. This was the case +where we were not doing any symbolic analysis of predicates. In the following expression, $e_3$ +refers to the syntactic construct of the ~dynamic_esetpred~ expression. + +#+begin_export context +\startformula + (\top \rightarrow \neg e_3) \rightarrow e_2 \land (\top \rightarrow e_3) \rightarrow e_1 +\stopformula +#+end_export + +#+begin_export html +\begin{equation} + (\top \rightarrow \neg e_3) \rightarrow e_2 \land (\top \rightarrow e_3) \rightarrow e_1 +\end{equation} +#+end_export + +After simplification we get the exact same expression as before, with the only difference being +$p_1$ is now represented as $e_3$, which is not really a distinction. However, the benefit that we +get from this is that we can now correctly identify more complicated input code like predicated +set-predicate instructions. The update function will then look something like the following. + +#+cindex: predicated-functions +#+begin_src coq +<> + +Definition update_wo_exit (fop : forest) (i : instr): forest := + match i with + | RBnop => fop + | RBop p op rl r => + let nv := + app_predicated (get_pred fop p) + (fop # (Reg r)) + (map_predicated (pred_ret (Eop op)) + (merge (list_translation rl fop))) + in + fop # (Reg r) <- nv + | _ => fop + end. +#+end_src + +So this is great, theoretically if two symbolic states are equivalent, then the behaviour should be +the same. However, there is still one last big problem with how predicates are represented. +Now that the semantics of predicates are so rich, and that we go from predicates in the code to +symbolic predicates in the forest, and then finally back to normal predicates with literals now +referring to syntactic expressions, we have to reason about much more detailed semantics. It was +easy to reason about predicates earlier because if they were equivalent under the SAT solver, then +one could deduce that if one is true, the other will also be true. However, now that we have rich +expressions inside of predicates, it means that the execution of predicates can actually block, so +in addition to proving that two predicates are equivalent, one will also have to show that one can +now execute both of these expressions. + +** Dealing with Hyperblock Exits + +One thing that we have not yet addressed is how to deal with exits, from the hyperblock. This can +be done by just remembering a predicate (in this case an abstract predicate), which represents the +condition under which the current position in the code would be reached. This means that if one +hits an exit condition, one will add the condition of taking the exit to the current predicate one +is remembering. A new update function which describes all cases is now presented below, where the +exit has been implemented correctly. + +#+cindex: update-function-rest +#+begin_src coq +Definition update (fop : option (apred_op * forest)) (i : instr) + : option (apred_op * forest) := + do (pred, f) <- fop; + match i with + | RBnop => fop + | RBexit p c => + let new_p := + simplify (get_pred' f (negate (Option.default T p)) ∧ pred) in + do pruned <- + prune_predicated + (app_predicated (get_pred f p ∧ pred) (f # Exit) + (pred_ret (Eexit c))); + Some (new_p, f # Exit <- pruned) + <> + end. +#+end_src + +* A More Sane Proposition + +Finally, I believe that there is a better solution to this problem which avoids the evaluation issue +of predicates from the previous section. The trick is that if we restrict the predicates enough, we +can get back to the first case where proving the correctness of the predicates without any runtime +information and symbolic evaluation, still gives us a proof of semantic correctness. + +The main idea is that we can have the following conditions that restrict the block enough, while +also allowing the scheduler to do anything it would want to do to the instructions. + +1. If a predicate is present within the input hyperblock, it will optionally be present within the + other hyperblock. In practice this could be restricted further because the scheduler does not + change simplify or change the predicate expressions. +2. If a set-predicate operation is present for a predicate, then the same set-predicate operation is + present in the output hyperblock. This is verified by symbolically executing the set predicate + instructions, even though this is not used to replace the predicates of each register. +3. If a set-predicate instruction is not present, then it should also not be present in the output + hyperblock. +4. Finally, if a set-predicate instruction is present, then all instruction that depend on that + predicate need to either come all before or all after that instruction. This will probably be + simplified into stating that set-predicate operations always need to come before instructions + that use the predicate. + * Appendix :PROPERTIES: :APPENDIX: @@ -643,6 +847,121 @@ Definition eval_predf_opt pr p := match p with Some p' => eval_predf pr p' | None => true end. #+end_src +*** ~predicated-functions~ + +#+cindex: predicated-functions +#+name: predicated-functions +#+begin_src coq :tangle no +Fixpoint list_translation (l : list reg) (f : forest) {struct l} + : list apred_expr := + match l with + | nil => nil + | i :: l => (f # (Reg i)) :: (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: apredicated A) (p2: apredicated 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: apredicated A) + : apredicated B := NE.map (fun x => (fst x, f (snd x))) p. + +(*map (fun x => (fst x, Econs (snd x) Enil)) pel*) +Definition merge' (pel: apred_expr) (tpel: apredicated expression_list) := + predicated_map (uncurry Econs) (predicated_prod pel tpel). + +Fixpoint merge (pel: list apred_expr): apredicated expression_list := + match pel with + | nil => NE.singleton (T, Enil) + | a :: b => merge' a (merge b) + end. + +Definition map_predicated {A B} (pf: apredicated (A -> B)) (pa: apredicated A) + : apredicated B := + predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa). + +Definition predicated_apply1 {A B} (pf: apredicated (A -> B)) (pa: A) + : apredicated B := + NE.map (fun x => (fst x, (snd x) pa)) pf. + +Definition predicated_apply2 {A B C} (pf: apredicated (A -> B -> C)) (pa: A) + (pb: B): apredicated C := + NE.map (fun x => (fst x, (snd x) pa pb)) pf. + +Definition predicated_apply3 {A B C D} (pf: apredicated (A -> B -> C -> D)) + (pa: A) (pb: B) (pc: C): apredicated 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. + +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: apredicated 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': apred_op) (a b: apredicated 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: apredicated A) := + NE.filter (fun x => match deep_simplify expression_dec (fst x) with ⟂ => false | _ => true end) + (NE.map (fun x => (deep_simplify expression_dec (fst x), snd x)) a). + +Definition pred_ret {A: Type} (a: A) : apredicated A := + NE.singleton (T, a). + +Definition upd_pred_forest (p: apred_op) (f: forest) := + PTree.map (fun i e => + NE.map (fun (x: apred_op * expression) => + let (pred, expr) := x in + (Pand p pred, expr)) e) f. + +Definition get_pred (f: forest) (ap: option pred_op): apred_op := + get_pred' f (Option.default Ptrue ap). + +Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) := + Option.map simplify (combine_pred a b). +#+end_src + ** ~section-abstr-eval~ #+cindex: section-abstr-eval @@ -774,6 +1093,56 @@ Module PredOpVersion. End PredOpVersion. #+end_src +** Definition of final version + +*** ~update-function-rest~ + +#+cindex: update-function-rest +#+name: update-function-rest +#+begin_src coq :tangle no +| RBop p op rl r => + do pruned <- + prune_predicated + (app_predicated (get_pred f p ∧ pred) + (f # (Reg r)) + (map_predicated (pred_ret (Eop op)) + (merge (list_translation rl f)))); + Some (pred, f # (Reg r) <- pruned) +| RBload p chunk addr rl r => + do pruned <- + prune_predicated + (app_predicated (get_pred f p ∧ pred) + (f # (Reg r)) + (map_predicated + (map_predicated (pred_ret (Eload chunk addr)) + (merge (list_translation rl f))) + (f # Mem))); + Some (pred, f # (Reg r) <- pruned) +| RBstore p chunk addr rl r => + do pruned <- + prune_predicated + (app_predicated (get_pred f p ∧ pred) + (f # Mem) + (map_predicated + (map_predicated + (predicated_apply2 + (map_predicated (pred_ret Estore) + (f # (Reg r))) chunk addr) + (merge (list_translation rl f))) (f # Mem))); + Some (pred, f # Mem <- pruned) +| RBsetpred p' c args p => + do pruned <- + prune_predicated + (app_predicated (get_pred f p' ∧ pred) + (f # (Pred p)) + (map_predicated + (pred_ret (Esetpred c)) + (merge (list_translation args f)))); + Some (pred, f # (Pred p) <- pruned) +#+end_src + +#+context: \page + * Index :PROPERTIES: :APPENDIX: -- cgit