summaryrefslogtreecommitdiffstats
path: root/main.org
diff options
context:
space:
mode:
Diffstat (limited to 'main.org')
-rw-r--r--main.org48
1 files changed, 48 insertions, 0 deletions
diff --git a/main.org b/main.org
new file mode 100644
index 0000000..830af60
--- /dev/null
+++ b/main.org
@@ -0,0 +1,48 @@
+#+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