#+title: Formal Predicate Aware Symbolic Execution
#+author: Yann Herklotz
#+context_preset: ymhg-article
#+context_header_extra: \environment env
#+options: syntax:vim toc:nil
#+property: header-args:coq :noweb no-export :padline yes :tangle Main.v
#+auto_tangle: t

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

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.

* Syntax Definitions

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

Let us first define what a resource is in our symbolic expressions.  We want to keep track of four
main components.  Firstly, we are separating predicate registers ~Pred~ from standard registers
~Reg~.  Then, we also want to track memory, which can be done using a single global memory ~Mem~.
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 :=
| Reg : reg -> resource
| Pred : reg -> resource
| Mem : resource
| Exit : resource.
#+end_src

We can then create expressions that mimic the expressions defined in RTLBlock
and RTLPar, which use expressions instead of registers as their inputs and
outputs.  This means that we can accumulate all the results of the operations as
general expressions that will be present in those registers.

- ~Ebase~ :: the starting value of the register.
- ~Eop~ :: Some arithmetic operation on a number of registers.
- ~Eload~ :: A load from a memory location into a register.
- ~Estore~ :: A store from a register to a memory location.
- ~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.

#+begin_src coq
Inductive expression : Type :=
| Ebase : resource -> expression
| Eop : Op.operation -> expression_list -> expression
| Eload :
    AST.memory_chunk -> Op.addressing ->
    expression_list -> expression -> expression
| Estore :
    expression -> AST.memory_chunk ->
    Op.addressing -> expression_list ->
    expression -> expression
| Esetpred : Op.condition -> expression_list -> expression
| Eexit : cf_instr -> expression
with expression_list : Type :=
| Enil : expression_list
| Econs : expression -> expression_list -> expression_list.
#+end_src

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.[fn:2] 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

We can then also speak about equivalence between two predicates by

#+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).
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]].

* First Attempt at Symbolic Analysis

* 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~
:PROPERTIES:
:CUSTOM_ID: R_indexed-def-link
:END:

*** ~R_indexed-index-def~

#+cindex: R_indexed-index-def
#+name: R_indexed-index-def
#+begin_src coq :tangle no
Definition index (rs: resource) : positive :=
  match rs with
  | Reg r => xO (xO r)
  | Pred r => xI (xI r)
  | Mem => 1
  | Exit => 2
  end.
#+end_src

*** ~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~

#+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}.
Proof. decide equality; apply Pos.eq_dec. Defined.

Module R_indexed.
  Definition t := resource.
  Definition eq := resource_eq.
  <<R_indexed-index-def>>
  <<R_indexed-injectivity>>
End R_indexed.
#+end_src

* Index
:PROPERTIES:
:APPENDIX:
:END:

#+toc: cp

* Footnotes

[fn:2] We can see that predicates are actually not needed in the semantics of any other
expressions.  It might therefore be better to create a separate ~predicate_expression~ which will
only set predicates based on a condition.

[fn:1] This post uses noweb syntax to specify pieces of code defined elsewhere, and will link to
those pieces of code directly.