Building constant-time constant-memory programs for your Arduino with CoPilot

Hard real-time systems are systems that have deadlines that MUST NOT be exceeded no matter what. An example is a nuclear power plant control system, where the specification might prescribe that abnormal situations must be responded to within at most 100 milliseconds. For software systems, this usually means running on a Real Time Operating System for complicated programs or running on a dedicated microcontroller for smaller systems, since consumer grade operating systems such as Windows or MacOS have a variety of background processes that could mess up the timing. Imagine an airplane autopilot being unresponsive because it was too busy running an antivirus program! There are also various techniques that can be applied while writing the program that can ensure every loop through it takes exactly the same time or that the program will always use exactly the same amount of memory every time. Since it is laborious and error-prone to apply these techniques by hand, a variety of tools have been constructed to assist programmers. One such tool is CoPilot, a Haskell DSL that compiles down to C code that is guarantueed to run in constant time and constant memory. It was developed for NASA by Galois and is intended for safety-critical applications.

A few days ago Joey Hess published arduino-copilot, which extends the regular CoPilot language to generate code files for the popular Arduino range of hobbyist microcontrollers. While my personal Arduino contraptions are not quite in need of microsecond accuracy in their main loop, I do thoroughly enjoy overengineering my side projects. I also like writing Haskell better than writing C, but YMMV on that.

How to install

I tried to install arduino-copilot with just cabal install but ran into some incompatibility issues, so I opted for stack instead. Just run stack new arduino-test && cd arduino-test to get a fresh “hello world” project scaffold. Since arduino-copilot is not yet in the stackage resolvers, we’ll have to add it to package.yaml and the extra-deps part of stack.yaml:

-- package.yaml:
dependencies:
- base >= 4.7 && < 5
- arduino-copilot

-- stack.yaml
extra-deps:
- arduino-copilot-1.1.1

Since the copilot libraries are also not in the resolver, stack will complain that they should be in the stack.yaml file as well and will suggest extra lines to add. For me it took a few iterations of progressively adding more and more stuff to the extra-deps section, but eventually stack was happy and everything installed without problems. Once you have it configured, stack run will compile everything and should output something like someFunc to the terminal.

Examples

When you run stack new, it will autogenerate a bunch of files for you. The file we’ll be editing is app/Main.hs. Replace its contents with the following:

{-# LANGUAGE RebindableSyntax #-}
module Main where

import Copilot.Arduino.Uno -- Copilot.Arduino.Nano is also available

main = arduino $ do
  led =: blinking
  delay =: constant 100

There is a little bit to unpack in this example. The first thing to know is that every variable in CoPilot is a stream of values and not a singular point in time. Streams have a type signature indicating which type a value is inside, eg Stream Bool or Stream Word8. The blinking function is a Stream Bool, that switches between True and False on each iteration. The =: operator will bind a Stream to an Output, in this case the onboard LED that every arduino has (usually bound to pin 13). delay is a “magic” output that does not conform to any hardware pin, but it instead sleeps by that many milliseconds. It is fed with the stream constant 100, which is a stream containing the value 100 over and over again. Finally, the whole thing is wrapped with the arduino function, which takes the code and converts it to something that CoPilot understands.

If you run this code with stack run, it will output a .ino file (arduino-test.ino if you used the stack project name from earlier) that contains C code you can open in your Arduino IDE and send to an Arduino to make it blink its LED. (Note: my arduino IDE threw an exception when trying to open the file outright, but just copy-pasting the code into the IDE worked fine.) Not very spectacular so far, but LED blinkers are kinda the “hello world” of Arduino so it makes sense to try that first. A cool feature of CoPilot is that you can simulate the behavior of your program without ever having to touch hardware. Running stack run -- -i 5 should give you output showing the value of each Output on each iteration, like this:

$ stack run -- -i 6
delay:         digitalWrite: 
(100)          (13,false)    
(100)          (13,true)     
(100)          (13,false)    
(100)          (13,true)     
(100)          (13,false)    
(100)          (13,true)  

A program with input is not much more difficult:

main = arduino $ do
  buttonPressed <- readfrom pin8
  led =: buttonPressed || blinking
  delay =: constant 100

This will automatically make sure that pin 8 is set to INPUT mode and read the value of it on each iteration, putting the results in a Stream Bool called buttonPressed. Streams can be manipulated in a variety of ways. All the usual operators on booleans like && and || are implemented pointwise for streams, so the behavior of the above example is that it will blink the LED as long as pin 8 is False. If pin 8 is True, the LED is always on. Streams containing numbers have the same behavior with operators like +, - and *, so (constant 100) + (constant 100) == constant 200. Combining a stream with a scalar non-stream value applies the operation to all elements in the stream, so you can do things like this:

celsiusValues <- ... -- read from some sensor

kelvinValues :: Stream Float
kelvinValues = celsiusValues - 273.15

As a final example, here is a small example of a more complex stream transformation function that takes a Stream Word8 and releases a stream containing the sum of the inputs so far:

-- Sum of inputs
accumulator :: Stream Word8 -> Stream Word8
accumulator vals = n
  where n = [0] ++ n + vals

As you might expect in Haskell, the stream is a lazy data structure and can be defined recursively in terms of itself. You can see its behavior by adding a line of pwm pin3 =: accumulator (constant 2) to the file above. As a fun experiment: can you predict how the accumulator behavior changes if you put in brackets like ([0] ++ n) + vals or like [0] ++ (n + vals)?

Conclusion

To me, defining program behavior in terms of (opeartions on) streams makes a lot of sense for embedded systems. There is a lot of power in the underlying CoPilot library too. With the copilot-theorem package you can even specify and mathematically prove some types of program behavior at compile time, and there are extensions for fault-tolerant voting, stream statistics, temporal logic and many more. It is also literally rocket science, since CoPilot programs are running on at least one spacecraft.

At the same time, it also suffers a little bit because it is what it is; certainly the accumulator example above took me two or three times to get right, for a very simple function. Unlike many other Haskell libraries, it also provides little in the form of type safety: the shape of the library implicitly encourages streams containing simple Bool or Word8 or Float values instead of, for example, more descriptive ThrustInPounds and ThrustInNewtons types. The installation of the libraries themselves is also still more tricky than it could be, but hopefully copilot and arduino-copilot will be included in the stackage resolver soon. Finally, there are some minor bugs in the documentation of arduino-copilot, like delay having type Output MicroSeconds while it actually interprets the argument as milliseconds. These are fairly easily fixed.

I’m planning to play around more with the Arduino ecosystem in the near future and will definitely try to find more projects where I can use arduino-copilot to program my systems. Give it a try!