ANN: Copilot 0.22 -- A stream DSL for writing embedded C.
Announcing Copilot 0.22: Can you write a list in Haskell? Then you can write embedded C code using Copilot. Here's a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even numbers: fib :: Streams fib = do "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib") "t" .= even (var "fib") where even :: Spec Word64 -> Spec Bool even w = w `mod` const 2 == const 0 Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin's Atom[1] (thanks Tom!). Copilot was originally developed to write embedded monitors for more complex systems, but it can be used to develop a variety of embedded code. HACKAGE: http://hackage.haskell.org/package/copilot WEBPAGE: http://leepike.github.com/Copilot/ (with more info). PICS/VIDEO of Copilot's maiden flight: http://picasaweb.google.com/105722675808588603973 A PAPER (PDF): http://www.cs.indiana.edu/~lepike/pub_pages/rv2010.html The Copilot Team * Maintainer: Lee Pike (leepike@galois.com), Galois, Inc. * Alwyn Goodloe, National Institute of Aerospace * Robin Morisset, École Normale Supérieure * Sebastian Niller, Technische Universität Ilmenau [1] http://hackage.haskell.org/package/atom
Oh, one thing I should mention is that there are a few Haskell DSLs for generating embedded C now: * Atom http://hackage.haskell.org/package/atom * Feldspar http://hackage.haskell.org/package/feldspar-language * cmonad http://hackage.haskell.org/package/cmonad * Copilot http://hackage.haskell.org/package/copilot * Others? Which to use for what? Most of my experience is with Atom and Copilot. Copilot is a minimalist stream (data-flow) language, as it is focused on monitoring properties rather than more "stateful" tasks. Still, for some data-processing, it's quick and simple, pretty much like writing Haskell lists. The best reference for Copilot's constraints is this paper: http://www.cs.indiana.edu/~lepike/pub_pages/rv2010.html. In our flight-test of a pitot (air-pressure) sensor http://picasaweb.google.com/105722675808588603973, we wrote some of the fault-tolerance and sensor computation in Atom + C, and monitors for properties in Copilot. As mentioned, Copilot actually uses Atom as a "backend" for generating C code. Of course, it's perfectly fine to mix-and-match Atom & Copilot. I know less about Feldspar, but I think the language has higher-level data-structures (e.g., vectors and matrices) and is focused more on DSP than periodic, constant-time/constant-space C code generation. Thoughts from others? Regards, Lee
The best reference for Copilot's constraints is this paper: http://www.cs.indiana.edu/~lepike/pub_pages/rv2010.html.
Non-Haskell programmers should note that paper has a few typos (Lee, please correct me if I'm mistaken). Section 4.1 is where I'm at so far and I see missing backticks (shoulld be `implies`) and missing parenthesis in "drop 2 (var temps)". Cheers, Thomas
The best reference for Copilot's constraints is this paper: http://www.cs.indiana.edu/~lepike/pub_pages/rv2010.html.
Non-Haskell programmers should note that paper has a few typos (Lee, please correct me if I'm mistaken). Section 4.1 is where I'm at so far and I see missing backticks (shoulld be `implies`) and missing parenthesis in "drop 2 (var temps)".
Sorry it wasn't clear in the paper: the language snippets in there aren't intended to be valid Haskell but to respect the BNF grammar given---it's idealized slightly. But yes, it could be a little confusing if using the paper as a language guide. Thanks for pointing that out, Thomas. Regards, Lee
Oh, one thing I should mention is that there are a few Haskell DSLs for generating embedded C now:
* Atom http://hackage.haskell.org/package/atom * Feldspar http://hackage.haskell.org/package/feldspar-language * cmonad http://hackage.haskell.org/package/cmonad * Copilot http://hackage.haskell.org/package/copilot * Others?
ImProve http://hackage.haskell.org/package/improve We are using ImProve for some safety critical code on a hydraulic hybrid shuttle bus. -Tom
2010-09-21 22:32, Lee Pike skrev:
Oh, one thing I should mention is that there are a few Haskell DSLs for generating embedded C now:
* Atom http://hackage.haskell.org/package/atom * Feldspar http://hackage.haskell.org/package/feldspar-language * cmonad http://hackage.haskell.org/package/cmonad * Copilot http://hackage.haskell.org/package/copilot * Others?
From a quick browse of the cmonad package, it seems that it does not generate C code, but is only intended for interpretation in Haskell.
I know less about Feldspar, but I think the language has higher-level data-structures (e.g., vectors and matrices) and is focused more on DSP than periodic, constant-time/constant-space C code generation.
Yes, at the moment, Feldspar can only describe pure functions. The next step is to add data flow (and other forms of coordination) on top of the pure language. / Emil
participants (4)
-
Emil Axelsson -
Lee Pike -
Thomas DuBuisson -
Tom Hawkins