summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-07-26 20:30:09 +0100
committerYann Herklotz <git@yannherklotz.com>2022-07-26 20:30:09 +0100
commita95b90f9b7a4e1b3cb91a7ed2b2009f97257d6a7 (patch)
tree25e07adffc3505f4b6bb10f51693a69c066791f2
parentf2e52c7397d20610f5439ca5735c15ea2d8dcd6b (diff)
downloadpred-aware-ai-a95b90f9b7a4e1b3cb91a7ed2b2009f97257d6a7.tar.gz
pred-aware-ai-a95b90f9b7a4e1b3cb91a7ed2b2009f97257d6a7.zip
Use org mode instead
-rw-r--r--env.tex21
-rw-r--r--main.org48
-rw-r--r--main.tex17
3 files changed, 57 insertions, 29 deletions
diff --git a/env.tex b/env.tex
index 701dd9c..718d0f6 100644
--- a/env.tex
+++ b/env.tex
@@ -17,25 +17,22 @@
\definefontfeature[default][default][protrusion=quality,expansion=quality]
\setupbodyfont[ymhg]
\setupinterlinespace[big]
+\setupindenting[yes,medium,next]
\setuphead[title][
style={\bfd\ss},
header=empty,
align=center,
- after={\blank[3*line]},
before={\blank[2*line,force]},
]
-\setupindenting[yes,medium]
-
-\setupfootertexts[pagenumber]
-\setupheadertexts[]
-\setupheadertexts[{\sc Yann Herklotz}][{\sc Abstract Interpretation}]
-
-\usemodule[vim]
-\definevimtyping [hlcoq] [syntax=coq]
-\definevimtyping [hlocaml] [syntax=ocaml]
-\definevimtyping [hlverilog] [syntax=verilog]
-\definevimtyping [hlC] [syntax=c,escape=command]
+\setuphead[subject][style={\bfb\ss}]
+\setuphead[subsubject][style={\bfa\ss}]
+\setuphead[subsubsubject][style={\ita\ss}]
+\setuphead[subsubsubsubject][style={\it\ss}]
+\setuphead[section][style={\bfb\ss}]
+\setuphead[subsection][style={\bfa\ss}]
+\setuphead[subsubsection][style={\ita\ss}]
+\setuphead[subsubsubsection][style={\it\ss}]
\stopenvironment
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
diff --git a/main.tex b/main.tex
deleted file mode 100644
index b0e6489..0000000
--- a/main.tex
+++ /dev/null
@@ -1,17 +0,0 @@
-\environment env
-\starttext
-
-\title{Abstract Interpretation}
-
-\input tufte
-\input tufte
-\input tufte
-\input tufte
-
-\input tufte
-\input tufte
-\input tufte
-\input tufte
-\input tufte
-
-\stoptext