Skip to content

Commit ef69b8d

Browse files
Hodapp87Hodapp87
committed
Travis build 29 on Sun Jun 28 04:34:49 UTC 2015
1 parent 8bfdc91 commit ef69b8d

17 files changed

+1138
-0
lines changed

‎slides/20150609_CincyFP/Example.hs

+108
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
{-# LANGUAGE QuasiQuotes #-}
2+
3+
module Example where
4+
5+
import Language.Atom
6+
import Language.Atom.Unit
7+
import Data.Word
8+
import StringEmbed
9+
10+
main :: IO ()
11+
main = do (sched, _, _, _, _) <- compile "example" atomCfg example
12+
putStrLn $ reportSchedule sched
13+
14+
atomCfg :: Config
15+
atomCfg = defaults { cFuncName = "atom_tick"
16+
, cStateName = "example"
17+
, cCode = prePostCode
18+
, hCode = prePostHeader
19+
, cRuleCoverage = False
20+
}
21+
22+
cHeader = [embedStr|
23+
// ---- This source is automatically generated by Atom ----
24+
#include <stdlib.h>
25+
#include <stdio.h>
26+
#include <unistd.h>
27+
28+
#define WATCHDOG_PERIOD 15
29+
30+
static uint64_t watchdog_deadline = WATCHDOG_PERIOD;
31+
32+
static uint16_t voltage = 0;
33+
34+
void reset_watchdog(void);
35+
void measure_voltage(void);
36+
// End header
37+
|]
38+
39+
cFooter = [embedStr|
40+
// Start footer
41+
int main(void) {
42+
while (true) {
43+
printf("__global_clock = %lu\n", __global_clock);
44+
45+
if (__global_clock > watchdog_deadline) {
46+
printf("Watchdog expired!\n");
47+
exit(1);
48+
}
49+
atom_tick();
50+
usleep(500000);
51+
}
52+
return 0;
53+
}
54+
55+
void reset_watchdog(void) {
56+
printf("Watchdog reset\n");
57+
watchdog_deadline = __global_clock + WATCHDOG_PERIOD;
58+
}
59+
60+
void measure_voltage(void) {
61+
voltage = (rand() + rand()) / 2;
62+
}
63+
// End footer
64+
|]
65+
66+
prePostCode :: [Name] -> [Name] -> [(Name, Type)] -> (String, String)
67+
prePostCode _ _ _ = (cHeader, cFooter)
68+
69+
prePostHeader :: [Name] -> [Name] -> [(Name, Type)] -> (String, String)
70+
prePostHeader _ _ _ =
71+
( "// ---- This header is automatically generated by Atom ----"
72+
, "// ---- End automatically-generated header ----"
73+
)
74+
75+
measureVoltage :: Word16 -> Word16 -> Atom (V Bool)
76+
measureVoltage lower upper = atom "measureVoltage" $ do
77+
let voltage = word16' "voltage"
78+
safeTime = 10
79+
80+
triggered <- bool "voltage_trigger" False
81+
countdown <- timer "threshold"
82+
83+
phase 0 $ atom "measure" $ call "measure_voltage"
84+
phase 1 $ atom "read" $ do
85+
printIntegralE "voltage" $ value voltage
86+
atom "checkLower" $ do
87+
cond (value voltage <. Const lower)
88+
triggered <== true
89+
printStrLn "Voltage under threshold!"
90+
atom "checkUpper" $ do
91+
cond (value triggered &&. value voltage <=. Const upper)
92+
printStrLn "Resetting countdown..."
93+
startTimer countdown safeTime
94+
atom "checkTimer" $ do
95+
cond (value triggered &&. timerDone countdown)
96+
triggered <== false
97+
printStrLn "Voltage back to normal."
98+
99+
return triggered
100+
101+
example :: Atom ()
102+
example = atom "example" $ do
103+
104+
voltage <- period 2 $ measureVoltage 18000 20000
105+
106+
period 15 $ atom "watchdog" $ do call "reset_watchdog"
107+
108+
return ()

‎slides/20150609_CincyFP/Slides.html

+141
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
2+
<html xmlns="http://www.w3.org/1999/xhtml">
3+
<head>
4+
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
5+
<meta http-equiv="Content-Style-Type" content="text/css" />
6+
<meta name="generator" content="pandoc" />
7+
<meta name="author" content="Chris Hodapp" />
8+
<title>Embedded Haskell, part 1: EDSLs &amp; Metaprogramming</title>
9+
<style type="text/css">code{white-space: pre;}</style>
10+
<!-- configuration parameters -->
11+
<meta name="defaultView" content="slideshow" />
12+
<meta name="controlVis" content="hidden" />
13+
<!-- style sheet links -->
14+
<link rel="stylesheet" href="../s5/default/slides.css" type="text/css" media="projection" id="slideProj" />
15+
<link rel="stylesheet" href="../s5/default/outline.css" type="text/css" media="screen" id="outlineStyle" />
16+
<link rel="stylesheet" href="../s5/default/print.css" type="text/css" media="print" id="slidePrint" />
17+
<link rel="stylesheet" href="../s5/default/opera.css" type="text/css" media="projection" id="operaFix" />
18+
<!-- S5 JS -->
19+
<script src="../s5/default/slides.js" type="text/javascript"></script>
20+
</head>
21+
<body>
22+
<div class="layout">
23+
<div id="controls"></div>
24+
<div id="currentSlide"></div>
25+
<div id="header"></div>
26+
<div id="footer">
27+
<h1>CincyFP, 2015-06-09</h1>
28+
<h2>Embedded Haskell, part 1: EDSLs &amp; Metaprogramming</h2>
29+
</div>
30+
</div>
31+
<div class="presentation">
32+
<div class="titleslide slide">
33+
<h1>Embedded Haskell, part 1: EDSLs &amp; Metaprogramming</h1>
34+
<h2>Chris Hodapp</h2>
35+
<h3>CincyFP, 2015-06-09</h3>
36+
</div>
37+
<div id="why-use-haskell-there-at-all" class="slide section level1">
38+
<h1>Why use Haskell there at all?</h1>
39+
<ol class="incremental" style="list-style-type: decimal">
40+
<li>Because you can.</li>
41+
<li>With apologies to Kernighan &amp; Ritchie: Because C is kind of horrid for this. (And with apologies to no one: Because C++ is also a train-wreck.)</li>
42+
<li>Because Haskell has a very powerful type system, and this can work wonders when dealing with embedded systems that are notoriously finicky and fragile.</li>
43+
<li>Because arcane concepts like &quot;functional programming&quot; and &quot;pure functions&quot; and &quot;monads&quot; turn out to be useful for something besides ivory-tower navel-gazing.</li>
44+
</ol>
45+
</div>
46+
<div id="approaches-to-embedded-haskell" class="slide section level1">
47+
<h1>Approaches to embedded Haskell</h1>
48+
<p><em>Disclaimer:</em> I made these categories up, and I'm excluding languages like Cryptol and Idris that only incidentally involve Haskell.</p>
49+
<ul>
50+
<li>Full compilation, reduced runtime approach</li>
51+
<li>Static analysis approach</li>
52+
<li>Compiled EDSL approach (the focus of this presentation)</li>
53+
</ul>
54+
</div>
55+
<div id="full-compilation-reduced-runtime" class="slide section level1">
56+
<h1>Full compilation, reduced runtime</h1>
57+
<p>This compiles Haskell code to run directly on an embedded target. This requires:</p>
58+
<ul>
59+
<li>reducing the fairly heavy Haskell runtime,</li>
60+
<li>optimizing the garbage collection,</li>
61+
<li>making the lazy evaluation less of a pain.</li>
62+
</ul>
63+
<div class="incremental">
64+
<p>Ajhc (<a href="https://github.com/ajhc/ajhc" class="uri">https://github.com/ajhc/ajhc</a>), a JHC-derived compiler from Kiwamu Okabe of METASEPI, is the only example of this I found - it could compile and execute on ARM Cortex-M3/M4. His subsequent switch to the ATS language may be a hint.</p>
65+
</div>
66+
</div>
67+
<div id="static-analysis" class="slide section level1">
68+
<h1>Static analysis</h1>
69+
<p>This uses an existing compiler for certain stages (such as the parsing and type-checking), but a custom back-end to actually produce code. This may adapt or disallow certain constructs.</p>
70+
<p>GHC readily accomodates this by allowing developers to invoke GHC functionality, from Haskell, as a library. (<em>GHCJS</em>, a Haskell to JavaScript compiler, uses this.)</p>
71+
</div>
72+
<div id="static-analysis-examples" class="slide section level1">
73+
<h1>Static analysis examples</h1>
74+
<p><em>CλaSH</em> (<a href="http://www.clash-lang.org/" class="uri">http://www.clash-lang.org/</a>) from Christiaan Baaij uses this to compile a subset of Haskell to VHDL and SystemVerilog. CλaSH disallows certain things: recursive functions, recursive types, side effects, floating-point...</p>
75+
<div class="incremental">
76+
<p><em>Reduceron</em> (<a href="https://github.com/tommythorn/Reduceron" class="uri">https://github.com/tommythorn/Reduceron</a>) is an &quot;FPGA Haskell machine&quot; relying on massively-parallel graph reduction, complete with GC and lazy evaluation.</p>
77+
</div>
78+
<div class="incremental">
79+
<p>Conal Elliott worked with a Silicon Valley startup, <em>Tabula</em>, on massively-parallel execution of Haskell code on a new architecture (<em>Spacetime</em>), using an approach based on Cartesian Closed Categories (<a href="http://conal.net/blog/posts/haskell-to-hardware-via-cccs" class="uri">http://conal.net/blog/posts/haskell-to-hardware-via-cccs</a> &amp; <a href="https://github.com/conal/lambda-ccc/" class="uri">https://github.com/conal/lambda-ccc/</a>).</p>
80+
</div>
81+
</div>
82+
<div id="compiled-edsl" class="slide section level1">
83+
<h1>Compiled EDSL</h1>
84+
<p>This uses an EDSL (embedded domain-specific language) inside of Haskell to direct the process of code generation to a lower-level representation. (Otherwise called: <em>compiling</em>.)</p>
85+
<p>Note that in this case, Haskell code never actually <em>runs</em> on the embedded target. Rather, it uses specifications in the EDSL to build a representation of what <em>will</em> run there - in other words, a sort of metaprogramming.</p>
86+
<p>The code that runs on the target is entirely decoupled from the Haskell runtime.</p>
87+
</div>
88+
<div id="compiled-edsl-examples" class="slide section level1">
89+
<h1>Compiled EDSL: Examples</h1>
90+
<ul class="incremental">
91+
<li>The entire <em>Lava</em> family for circuit design and verification. (Compiles to: VHDL, Verilog, netlist? Reduceron from a few slides ago is implemented in York Lava.)</li>
92+
<li><em>Atom</em> for reactive, hard real-time, synchronous systems. (Compiles to: C)</li>
93+
<li><em>Copilot</em> for stream-oriented, hard real-time systems. (Compiles to: C via Atom &amp; SBV, CBMC model checker)</li>
94+
<li><em>SBV</em> for theorem proving oriented around SMT. (Compiles to: C, various SMT solvers)</li>
95+
<li><em>Ivory</em> for safe systems programming. (Compiles to: C, LLVM(?), CVC4 &amp; ACL2 theorem provers)</li>
96+
</ul>
97+
</div>
98+
<div id="atom-edsl" class="slide section level1">
99+
<h1>Atom EDSL</h1>
100+
<p>The official definition: &quot;Atom is a Haskell EDSL for designing hard realtime embedded software. Based on guarded atomic actions (similar to STM), Atom enables highly concurrent programming without the need for mutex locking. In addition, Atom performs compile-time task scheduling and generates code with deterministic execution time and constant memory use, simplifying the process of timing verification and memory consumption in hard realtime applications. Without mutex locking and run-time task scheduling, Atom eliminates the need and overhead of RTOSes for many embedded applications.&quot;</p>
101+
<p>Short version: Atom is a <em>synchronous language</em>: One specifies rules that apply on specific clock ticks, and all rules are atomic. Feed a specification into Atom, and Atom generates fairly bulletproof, deterministic C code.</p>
102+
</div>
103+
<div id="imaginary-atom-scenario" class="slide section level1">
104+
<h1>Imaginary Atom scenario</h1>
105+
<ol class="incremental" style="list-style-type: decimal">
106+
<li>You have a fairly resource-constrained microcontroller.</li>
107+
<li>It contains a hardware watchdog timer which you must reset every 15 milliseconds.</li>
108+
<li>You must monitor an input voltage. If it ever goes below 1.9 V, then the chip must cease all other operation (aside from resetting the watchdog) until it has stayed above 2.0 V for at least 10 milliseconds.</li>
109+
<li>There is an input button. If it is pressed for at least 50 milliseconds, its respective output pin should be toggled.</li>
110+
<li>There are incidentally 15 other buttons (and respective output pins) that behave the same way.</li>
111+
</ol>
112+
</div>
113+
<div id="my-workflow-for-those-interested" class="slide section level1">
114+
<h1>My workflow, for those interested</h1>
115+
<ul>
116+
<li>Haskell code contains:
117+
<ul>
118+
<li>Specifications in Atom &amp; Ivory</li>
119+
<li>Build targets for Shake (a Haskell-based build system)</li>
120+
</ul></li>
121+
<li>Shake build is responsible for:
122+
<ul>
123+
<li>Generating C code with Atom &amp; Ivory</li>
124+
<li>Compiling &amp; linking C code with GCC</li>
125+
<li>Producing a firmware image and commands for flashing it</li>
126+
</ul></li>
127+
<li>GDB communicates with GDB server</li>
128+
<li>JLink/OpenOCD implements GDB server and communicates with target via SWD</li>
129+
<li>Emacs communicates with GDB, handles Haskell and C code, and handles Shake build</li>
130+
</ul>
131+
</div>
132+
<div id="references-mindless-self-promotion" class="slide section level1">
133+
<h1>References &amp; Mindless Self-Promotion</h1>
134+
<p>Nearly everything that I reference should have a link at: <a href="http://haskellembedded.github.io/pages/links.html" class="uri">http://haskellembedded.github.io/pages/links.html</a></p>
135+
<p>My Atom introduction is at: <a href="http://haskellembedded.github.io/posts/2015-02-17-atom-examples.html" class="uri">http://haskellembedded.github.io/posts/2015-02-17-atom-examples.html</a></p>
136+
<p>In explaining the &quot;How?&quot; and &quot;What?&quot;, I probably ignored much of the &quot;Why?&quot;, and this explains some of that: <a href="http://haskellembedded.github.io/posts/2015-02-06-how-i-got-here.html" class="uri">http://haskellembedded.github.io/posts/2015-02-06-how-i-got-here.html</a></p>
137+
<p>See the <em>#haskell-embedded</em> IRC channel on Freenode to find me (<em>hodapp</em>) and a bunch of other people who are way better at this than I am.</p>
138+
</div>
139+
</div>
140+
</body>
141+
</html>

‎slides/20150609_CincyFP/Slides.md

+104
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
% Embedded Haskell, part 1: EDSLs & Metaprogramming
2+
% Chris Hodapp
3+
% CincyFP, 2015-06-09
4+
5+
# Why use Haskell there at all?
6+
7+
> 1. Because you can.
8+
> 2. With apologies to Kernighan & Ritchie: Because C is kind of horrid for this. (And with apologies to no one: Because C++ is also a train-wreck.)
9+
> 3. Because Haskell has a very powerful type system, and this can work wonders when dealing with embedded systems that are notoriously finicky and fragile.
10+
> 4. Because arcane concepts like "functional programming" and "pure functions" and "monads" turn out to be useful for something besides ivory-tower navel-gazing.
11+
12+
# Approaches to embedded Haskell
13+
14+
*Disclaimer:* I made these categories up, and I'm excluding languages like Cryptol and Idris that only incidentally involve Haskell.
15+
16+
- Full compilation, reduced runtime approach
17+
- Static analysis approach
18+
- Compiled EDSL approach (the focus of this presentation)
19+
20+
# Full compilation, reduced runtime
21+
22+
This compiles Haskell code to run directly on an embedded target. This requires:
23+
24+
- reducing the fairly heavy Haskell runtime,
25+
- optimizing the garbage collection,
26+
- making the lazy evaluation less of a pain.
27+
28+
. . .
29+
30+
Ajhc ([https://github.com/ajhc/ajhc](https://github.com/ajhc/ajhc)), a JHC-derived compiler from Kiwamu Okabe of METASEPI, is the only example of this I found - it could compile and execute on ARM Cortex-M3/M4. His subsequent switch to the ATS language may be a hint.
31+
32+
# Static analysis
33+
34+
This uses an existing compiler for certain stages (such as the parsing and type-checking), but a custom back-end to actually produce code. This may adapt or disallow certain constructs.
35+
36+
GHC readily accomodates this by allowing developers to invoke GHC functionality, from Haskell, as a library. (*GHCJS*, a Haskell to JavaScript compiler, uses this.)
37+
38+
# Static analysis examples
39+
40+
*CλaSH* ([http://www.clash-lang.org/](http://www.clash-lang.org/)) from Christiaan Baaij uses this to compile a subset of Haskell to VHDL and SystemVerilog. CλaSH disallows certain things: recursive functions, recursive types, side effects, floating-point...
41+
42+
. . .
43+
44+
*Reduceron* ([https://github.com/tommythorn/Reduceron](https://github.com/tommythorn/Reduceron)) is an "FPGA Haskell machine" relying on massively-parallel graph reduction, complete with GC and lazy evaluation.
45+
46+
. . .
47+
48+
Conal Elliott worked with a Silicon Valley startup, *Tabula*, on massively-parallel execution of Haskell code on a new architecture (*Spacetime*), using an approach based on Cartesian Closed Categories ([http://conal.net/blog/posts/haskell-to-hardware-via-cccs](http://conal.net/blog/posts/haskell-to-hardware-via-cccs) & [https://github.com/conal/lambda-ccc/](https://github.com/conal/lambda-ccc/)).
49+
50+
# Compiled EDSL
51+
52+
This uses an EDSL (embedded domain-specific language) inside of Haskell to direct the process of code generation to a lower-level representation. (Otherwise called: *compiling*.)
53+
54+
Note that in this case, Haskell code never actually *runs* on the embedded target. Rather, it uses specifications in the EDSL to build a representation of what *will* run there - in other words, a sort of metaprogramming.
55+
56+
The code that runs on the target is entirely decoupled from the Haskell runtime.
57+
58+
# Compiled EDSL: Examples
59+
60+
> - The entire *Lava* family for circuit design and verification. (Compiles to: VHDL, Verilog, netlist? Reduceron from a few slides ago is implemented in York Lava.)
61+
> - *Atom* for reactive, hard real-time, synchronous systems. (Compiles to: C)
62+
> - *Copilot* for stream-oriented, hard real-time systems. (Compiles to: C via Atom & SBV, CBMC model checker)
63+
> - *SBV* for theorem proving oriented around SMT. (Compiles to: C, various SMT solvers)
64+
> - *Ivory* for safe systems programming. (Compiles to: C, LLVM(?), CVC4 & ACL2 theorem provers)
65+
66+
# Atom EDSL
67+
68+
The official definition: "Atom is a Haskell EDSL for designing hard realtime embedded software. Based on guarded atomic actions (similar to STM), Atom enables highly concurrent programming without the need for mutex locking. In addition, Atom performs compile-time task scheduling and generates code with deterministic execution time and constant memory use, simplifying the process of timing verification and memory consumption in hard realtime applications. Without mutex locking and run-time task scheduling, Atom eliminates the need and overhead of RTOSes for many embedded applications."
69+
70+
Short version:
71+
Atom is a *synchronous language*: One specifies rules that apply on specific clock ticks, and all rules are atomic. Feed a specification into Atom, and Atom generates fairly bulletproof, deterministic C code.
72+
73+
# Imaginary Atom scenario
74+
75+
> 1. You have a fairly resource-constrained microcontroller.
76+
> 2. It contains a hardware watchdog timer which you must reset every 15 milliseconds.
77+
> 3. You must monitor an input voltage. If it ever goes below 1.9 V, then the chip must cease all other operation (aside from resetting the watchdog) until it has stayed above 2.0 V for at least 10 milliseconds.
78+
> 4. There is an input button. If it is pressed for at least 50 milliseconds, its respective output pin should be toggled.
79+
> 5. There are incidentally 15 other buttons (and respective output pins) that behave the same way.
80+
81+
# My workflow, for those interested
82+
83+
- Haskell code contains:
84+
- Specifications in Atom & Ivory
85+
- Build targets for Shake (a Haskell-based build system)
86+
87+
- Shake build is responsible for:
88+
- Generating C code with Atom & Ivory
89+
- Compiling & linking C code with GCC
90+
- Producing a firmware image and commands for flashing it
91+
92+
- GDB communicates with GDB server
93+
- JLink/OpenOCD implements GDB server and communicates with target via SWD
94+
- Emacs communicates with GDB, handles Haskell and C code, and handles Shake build
95+
96+
# References & Mindless Self-Promotion
97+
98+
Nearly everything that I reference should have a link at: [http://haskellembedded.github.io/pages/links.html](http://haskellembedded.github.io/pages/links.html)
99+
100+
My Atom introduction is at: [http://haskellembedded.github.io/posts/2015-02-17-atom-examples.html](http://haskellembedded.github.io/posts/2015-02-17-atom-examples.html)
101+
102+
In explaining the "How?" and "What?", I probably ignored much of the "Why?", and this explains some of that: [http://haskellembedded.github.io/posts/2015-02-06-how-i-got-here.html](http://haskellembedded.github.io/posts/2015-02-06-how-i-got-here.html)
103+
104+
See the *#haskell-embedded* IRC channel on Freenode to find me (*hodapp*) and a bunch of other people who are way better at this than I am.

‎slides/20150609_CincyFP/StringEmbed.hs

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
-- Courtesy of:
2+
-- http://techoverflow.net/blog/2014/07/28/using-quasiquotation-for-more-readable-atom-code/
3+
-- Who gives credit to: https://www.fpcomplete.com/user/marcin/template-haskell-101
4+
module StringEmbed(embedStr, embedStrFile) where
5+
6+
import Language.Haskell.TH
7+
import Language.Haskell.TH.Quote
8+
9+
embedStr :: QuasiQuoter
10+
embedStr = QuasiQuoter { quoteExp = stringE,
11+
quotePat = undefined,
12+
quoteDec = undefined,
13+
quoteType = undefined }
14+
15+
embedStrFile :: QuasiQuoter
16+
embedStrFile = quoteFile embedStr

‎slides/20150609_CincyFP/make_slides.sh

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
#!/bin/sh
2+
3+
PANDOC_BIN="${HOME}/.cabal/bin/pandoc"
4+
S5_PATH="../s5/default"
5+
6+
${PANDOC_BIN} -V s5-url:${S5_PATH} -t s5 -s Slides.md -o Slides.html

0 commit comments

Comments
 (0)