#+title: Formal Predicate Aware Symbolic Execution
#+author: Yann Herklotz
#+context_preset: ymhg-article
#+context_header_extra: \environment env
#+options: syntax:vim toc:nil

* Framing the Problem

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

** Phasellus et tortor eget tellus

*** aroiesntoirensnt

Ornare gravida nec vitae lectus. Vivamus sed velit quis odio sagittis tincidunt. Praesent non
faucibus ante, vel gravida nulla. Phasellus arcu eros, maximus fermentum nisl sed, iaculis pretium
erat. Praesent eu risus vel sapien malesuada faucibus tempor nec mi. Vivamus eu purus tempor,
molestie neque mollis, feugiat orci. Praesent magna diam, condimentum at bibendum posuere, dapibus
vel ipsum. Phasellus ut sapien sit amet enim mollis elementum. Sed vel odio eu lacus interdum
ultrices at sed dolor. Nam maximus tincidunt orci vel egestas. Vivamus scelerisque risus leo,
malesuada tristique ex tempus ullamcorper. Nullam accumsan augue non nisi consectetur luctus. Cras
erat nulla, suscipit et felis sit amet, congue laoreet lorem. Curabitur malesuada neque purus, ut
consectetur nunc condimentum condimentum.

Fusce at orci lorem. Vestibulum tempus mauris eget sapien dictum rutrum. Aenean faucibus massa non
risus consectetur molestie. Curabitur cursus eget nisl sed pellentesque. Nulla facilisi. Suspendisse
at quam eget nisi euismod bibendum et in ex. Morbi facilisis posuere felis non ultrices. Nulla
sodales nunc ultricies, iaculis mi eget, molestie odio.

Nullam ultricies elit sit amet lorem tempor faucibus. Orci varius natoque penatibus et magnis dis
parturient montes, nascetur ridiculus mus. Vestibulum in erat vel nunc dictum suscipit vel non
nulla. Donec imperdiet viverra diam, at pretium lorem aliquet at. Phasellus ornare aliquet magna a
faucibus. Aenean nec eros ut nulla placerat ultricies ac at tortor. In imperdiet turpis mauris, ac
sodales ante rutrum eu.

** oaiernstoiaernst

aoristna risetn oiarstn

#+begin_src c
int main (int x) {
    return x;
}
#+end_src