Add plenty of text

3 files changed, 135 insertions, 64 deletions

diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/env.mkiv b/env.mkiv
index eb5902d..1d74493 100644
--- a/env.mkiv
+++ b/env.mkiv
@@ -28,7 +28,7 @@
 \setuppapersize[A4][A4]
 
 \definefontfeature[default][default][protrusion=quality,expansion=quality]
-\setupbodyfont[ymhg]
+\setupbodyfont[ymhg,10pt]
 \setupinterlinespace[big]
 \setupindenting[yes,medium,next]
 
@@ -48,7 +48,7 @@
 \setuphead[subsubsection][style={\ita\ss}]
 \setuphead[subsubsubsection][style={\it\ss}]
 
-\setupheads[title,subject,subsubject,section,subsection][color=darkcyan]
+\setupheads[subject,subsubject,section,subsection][color=darkcyan]
 
 \define\PlaceFootnote
   {\inrightmargin{\vtop{\placelocalnotes[footnote][before=,after=]}}}
@@ -67,4 +67,24 @@
 \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,
+  corner=round,
+  framecolor=codeblockborder,
+]
+
+\setupenumeration
+  [OrgListingEnumEmpty]
+  [alternative=empty,
+   before={\blank\startcodeblockbg},
+   after={\stopcodeblockbg\blank},
+   margin=0pt]
+
+\setupvimtyping[OrgBlkSrcCoq][margin=5mm]
+
 \stopenvironment
diff --git a/main.org b/main.org
index fe44cc6..46cfc37 100644
--- a/main.org
+++ b/main.org
@@ -5,23 +5,33 @@
 #+options: syntax:vim toc:nil
 #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v
 
-* Framing the Problem
+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
+of the whole program at the same time.  Instructions that can executed in parallel are therefore
+grouped together.  The scheduler can also optimise for various other goals, such as minimum number
+of clock cycles in the block, or minimum amount of resources used in the block.
 
 /Hyperblocks/ combine multiple basic blocks using predicated execution.  A scheduling algorithm can
-take this hyperblock and parallelise it, taking advantage of independent predicates to schedule
-instructions using the same resource.  Verifying this algorithm requires formalising various
-heuristics, whereas the schedule is easier to check correct.  If the checker is formalised, it can
-be run to check that the schedule is correct.
+then schedule the hyperblock by also analysing instruction predicates, and remove data dependencies
+between operations that have independent predicates.  The question is then how do we integrate this
+algorithm inside of a formally verified compiler.  Verifying the algorithm directly requires
+formalising various heuristics, whereas the schedule is easier to check for correctness after the
+fact.  We can verify the checker and run it to check that the schedule is correct.
 
-** Initialising the file
+This post[fn:1] covers multiple symbolic analysis passes and discusses their correctness arguments.
+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.
 
-We first add a few imports defined at the end of the file[fn:1] to get everything we are going to
-use to define the abstract language.
+* Syntax Definitions
 
-[[#abstr-imports-link][=<<abstr-imports>>=]]
-#+begin_src coq :exports none
-<<abstr-imports>>
-#+end_src
+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
+analysis.
+
+** Quick Overview of Hyperblocks
+
+Hyperblocks are a list of predicated instructions, which contain the
 
 ** Syntax of Symbolic Expressions
 
@@ -31,7 +41,10 @@ main components.  Firstly, we are separating predicate registers ~Pred~ from sta
 Finally, we might have different exit points under different conditions, so we also need to keep
 track under which conditions we exit using ~Exit~.
 
+#+cindex: abstr-imports
 #+begin_src coq
+<<abstr-imports>>
+
 Definition reg := positive.
 
 Inductive resource : Set :=
@@ -53,9 +66,8 @@ general expressions that will be present in those registers.
 - ~Esetpred~ :: A predicate definition by taking a condition with an expression list.
 - ~Eexit~ :: A syntactic exit instruction.
 
-Then, to make recursion over expressions easier, expression_list is also defined
-in the datatype, as that enables mutual recursive definitions over the
-datatypes.
+Then, to make recursion over expressions easier, ~expression_list~ is also defined in the datatype,
+as that enables mutual recursive definitions over the datatypes.
 
 #+begin_src coq
 Inductive expression : Type :=
@@ -78,21 +90,47 @@ with expression_list : Type :=
 The interesting thing to note about this abstract expression type is that it is weakly typed,
 meaning predicates are not any different to standard expressions.  The correctness is therefore
 governed by how the expressions are generated, and to what resource they are assigned to in the
-final expression tree.  Speaking of the tree, we can also define the forest that contains a mapping
-from resource to corresponding expression.
+final expression tree.  We will also need some kind of equality check for these expressions, so we
+can assume that we can implement a decidable check like the following:
+
+#+begin_src coq
+Axiom expression_dec:
+  forall e1 e2: expression, {e1 = e2} + {e1 <> e2}.
+#+end_src
+
+Speaking of the tree, we can also define the forest that contains a mapping from resource to
+corresponding expression.
+
+First, let's define what a predicate is, by reusing a general predicate expression defined in
+=vericert.hls.Predicate=.  The initial version of the predicate will be the same that is used in the
+~SeqBB.t~ syntax, meaning literals are positive numbers.  The two logical operations that are
+allowed are conjunction and disjunction.
 
 #+begin_src coq
 Definition predicate := positive.
 Definition pred_op := @Predicate.pred_op predicate.
+#+end_src
+
+In addition to that, we also want to define a predicated expression.  To make our lives a bit easier
+later on, we first define what a predicated "something" is, and then specialise it to define the
+predicated expression.  This allows us to easily construct our symbolic values later on.  The main
+thing to note is that a predicated expression is a non-empty list of a predicate combined with an
+expression.
+
+#+begin_src coq
 Definition predicated A := NE.non_empty (pred_op * A).
 Definition pred_expr := predicated expression.
+#+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
 <<R_indexed-def>>
 Module Rtree := ITree(R_indexed).
@@ -102,19 +140,59 @@ Definition forest : Type := Rtree.t apred_expr.
 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]].
 
-Finally, lets assume that we have a correct syntactic equality check between two expressions, so
-that we can get a decidable equality check between expressions.
+* First Attempt at Symbolic Analysis
 
-#+begin_src coq
-Axiom expression_dec: forall e1 e2: expression, {e1 = e2} + {e1 <> e2}.
+* Appendix
+:PROPERTIES:
+:APPENDIX:
+:END:
+
+** ~abstr-imports~
+:PROPERTIES:
+:CUSTOM_ID: abstr-imports-link
+:END:
+
+#+cindex: abstr-imports
+#+name: abstr-imports
+#+begin_src coq :tangle no
+Require Import Coq.Logic.Decidable.
+Require Import Coq.Structures.Equalities.
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Floats.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require compcert.verilog.Op.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.HashTree.
+Require Import vericert.hls.Predicate.
+Require Import vericert.common.DecEq.
+Require        vericert.common.NonEmpty.
+
+Module NE := NonEmpty.
+Import NE.NonEmptyNotation.
+
+#[local] Open Scope positive.
+#[local] Open Scope pred_op.
+#[local] Open Scope non_empty_scope.
 #+end_src
 
-** Definition of R_indexed
+** Definition of ~R_indexed~
 :PROPERTIES:
 :CUSTOM_ID: R_indexed-def-link
 :END:
 
-~<<R_indexed-index-def>> ::=~
+*** ~R_indexed-index-def~
+
+#+cindex: R_indexed-index-def
 #+name: R_indexed-index-def
 #+begin_src coq :tangle no
 Definition index (rs: resource) : positive :=
@@ -126,14 +204,20 @@ Definition index (rs: resource) : positive :=
   end.
 #+end_src
 
-~<<R_indexed-injectivity>> ::=~
+*** ~R_indexed-injectivity~
+
+#+cindex: R_indexed-injectivity
 #+name: R_indexed-injectivity
 #+begin_src coq :tangle no
 Lemma index_inj:  forall (x y: t), index x = index y -> x = y.
 Proof. destruct x; destruct y; crush. Qed.
 #+end_src
 
-~<<R_indexed-def>> ::=~
+*** ~R_indexed-def~
+
+#+cindex: R_indexed-def
+#+cindex: R_indexed-index-def
+#+cindex: R_indexed-injectivity
 #+name: R_indexed-def
 #+begin_src coq :tangle no
 Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}.
@@ -146,47 +230,13 @@ Module R_indexed.
   <<R_indexed-injectivity>>
 End R_indexed.
 #+end_src
-* First Attempt at Symbolic Analysis
 
-* Top-level imports
+* Index
 :PROPERTIES:
-:CUSTOM_ID: abstr-imports-link
+:APPENDIX:
 :END:
 
-~<<abstr-imports>> ::=~
-
-#+name: abstr-imports
-#+begin_src coq :tangle no
-Require Import Coq.Logic.Decidable.
-Require Import Coq.Structures.Equalities.
-
-Require Import compcert.backend.Registers.
-Require Import compcert.common.AST.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.common.Memory.
-Require Import compcert.common.Values.
-Require Import compcert.lib.Floats.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-Require compcert.verilog.Op.
-
-Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.GibleSeq.
-Require Import vericert.hls.GiblePar.
-Require Import vericert.hls.Gible.
-Require Import vericert.hls.HashTree.
-Require Import vericert.hls.Predicate.
-Require Import vericert.common.DecEq.
-
-Require symb.NonEmpty.
-
-Module NE := NonEmpty.
-Import NE.NonEmptyNotation.
-
-#[local] Open Scope positive.
-#[local] Open Scope pred_op.
-#[local] Open Scope non_empty_scope.
-#+end_src
+#+toc: cp
 
 * Footnotes