Backseat Driving: Copilot UpdatesPosted: November 20, 2010 | |
A lot has been going on since the announcement of Copilot, a Haskell DSL for generating hard real-time C monitors. We’ve presented Copilot a few times, including at Runtime Verification 2010, at a Galois Technical Seminar (video of the talk is here), and at a recent NASA Technical Interchange.
Copilot has had five releases since we originally open-sourced the project. Recent work has focused on making the language more straightforward and improving Copilot libraries. But first, let me remind you how to use Copilot: you can compile specs to hard real-time C code, you can interpret them, you can model-check them, and you can generate specs to test the compiler and interpreter—you can see a bit about usage here.
For example, here’s a Copilot specification that generates the Fibonacci sequence (over
Word64s) and tests for even numbers:
fib :: Streams fib = do let f = varW64 "f" let t = varB "t" f .= [0,1] ++ f + (drop 1 f) t .= even f where even :: Spec Word64 -> Spec Bool even w' = w' `mod` 2 == 0
Notice that lists look almost exactly like Haskell lists.
What about something a little more complicated? Consider the property:
If the temperature rises more than 2.3 degrees within 2 seconds, then the engine has been shut off.
We might use a Copilot specification like the following to express it, assuming that
shutoff are C variables being sampled at phases 1 and 2 respectively, and the period of execution is 1 second:
engine :: Streams engine = do -- external vars let temp = extF "temp" 1 let shutoff = extB "shutoff" 2 -- Copilot vars let temps = varF "temps" let overTemp = varB "overTemp" let trigger = varB "trigger" -- Copilot specification temps .= [0, 0, 0] ++ temp overTemp .= drop 2 temps > 2.3 + temps trigger .= overTemp ==> shutoff
Here’s something that I think shows why you want to write your DSLs in Haskell: Haskell gives you a macro language for your DSL… for free. For example, consider the following (more complicated) property:
“If the engine temperature exeeds 250 degrees, then the engine is shut off within one second, and in the 0.1 second following the shutoff, the cooler is engaged and remains engaged.”
We can more succinctly specify this property using past-time linear temporal logic (ptLTL). There’s a Copilot library for writing those kind of specs, which can be interspersed with normal Copilot streams—the ptLTL specs are highlighted in blue below. Again, assume a period of execution of 1 second:
engine :: Streams engine = do -- external vars let engineTemp = extW8 "engineTemp" 1 let engineOff = extB "engineOff" 1 let coolerOn = extB "coolerOn" 1 -- Copilot vars let cnt = varW8 "cnt" let temp = varB "temp" let cooler = varB "cooler" let off = varB "off" let monitor = varB "monitor" -- Copilot specification temp `ptltl` (alwaysBeen (engineTemp > 250)) cnt .=  ++ mux (temp && cnt < 10) (cnt + 1) cnt off .= cnt >= 10 ==> engineOff cooler `ptltl` (coolerOn `since` engineOff) monitor .= off && cooler
Today, I finished updating another feature of Copilot: the ability to send stream values over ports to other components in a distributed system. We had an implementation of this, but it was a bit hacky. Hopefully, it’s a bit less hacky now. For example, consider the following specification:
distrib :: Streams distrib = do -- Copilot vars let a = varW8 "a" let b = varB "b" -- Copilot spec a .= [0,1] ++ a + 1 b .= mod a 2 == 0 -- send commands send "portA" (port 2) a 1 send "portB" (port 1) b 2
The blue commands are send commands. For example, the first command says, “call the C function
portA(str, num), where argument
str is the value of stream
num is port number 1.” The port number says who to send it to.
These are just a few of the recent updates. We’re still working on Copilot, so let me know if you have questions or comments.