@hackage copilot1.0

---

Overview

---

Copilot: A (Haskell DSL) stream language for generating hard real-time C code.

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 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

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 (thanks Tom!). Copilot was originally developed to write embedded monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.

---

Download

---

Please visit http://leepike.github.com/Copilot/ for more information about installing and using Copilot.

The page is also available as index.html in the gh-pages branch of the Copilot repo. In your local repo,

git checkout gh-pages

and you should see index.html.

---

Release notes

---

• Copilot-1.0

  • Language frozen.
  • Added sampling functions and returning arrays.

• Copilot-0.29

  • Refactor Language.hs into submodules.
  • Removed the notion of phases from sampling. That is a compiler-level concern.

• Copilot-0.28

  • Make triggers part of the Copilot language (see example t5 in Examples.hs).

• Copilot-0.27

  • Changed syntax and semantics of the 'send' function (Language.hs) for sending Copilot values on ports. An example is in Example.hs (grep for 'send').

• Copilot-0.26

  • Variables are now specs, not strings. This gives stream expressions a type, so no need for constant functions, monomorphic cast functions, or var annotations in expressions. Examples updated to reflect the change.

• Copilot-0.25

  • Added true, false Specs (Spec Bool)
  • Removed generic const -- unneeded, since Spec instantiates Num.
  • Change casting to only allow casts that (1) are guaranteed not to change the sign and (2) are to a larger type.
  • Removed libs from Copilot.hs. You must import these explicitly.
  • Fixed buts with LTL and ptLTL libraries and examples and added documentation.

• Copilot-0.24

  • Fixed a bug in external array analysis for computing the minimum period size.
  • Added the ability to specify a HW clock for Atom.

• Copilot-0.23

  • All -Wall warnings removed (from importing Copilot.hs).
  • Added support for sampling external array values. (See Examples.hs).
  • Fixed a bug in calling CBMC to ensure it unrolls it's loop. Updated documentation in Help.hs.
  • Other minor stylistic changes and fixes.

• Copilot-0.22: initial release

---

Modifying the Compiler

---

This document is intended as a help for whoever wants to hack the internals of Copilot. It is up-to-date on August 2010, the 17th.

I will first explain what each module does, then where to look to do some simple modifications.

*** Modules ***

Core : Defines all the important data-structures. Especially interestings are :

• Spec, the AST of the streams specifications. Notice that the operators on streams (F, F2, F3) actually holds functions that helps interpreting/compiling them
• Streamable, a type class whose instances are all the possible types of output for a stream
• StreamableMaps, a generic container for holding pairs of key/values, with values of different types

Compiler : Does all the scheduling, and translates a Copilot specification, to an Atom program. More information on its algorithm can be found in the paper "Copilot: A Hard Real-Time Runtime Monitor".

Interpreter : Provides a small interpreter, mostly for checking the compiler against it. Its design is very concise, because all the hard scheduling work is done by the Haskell runtime. The streams are indeed translated to mutually recursives infinite lists, and the lazyness of Haskell spare us from having to schedule their computation. There is no specific code for each operator either, as operators hold the function to be applied to their argument.

Analyser : There are several kinds of restrictions on the inputs accepted by Copilot. Some of them are catched by the Haskell compiler (for example bad typing into a stream specification), but others aren't :

• Bad typing across stream boundaries
• Specifications which doesn't obey the syntax of Copilot (it could have been checked by Haskell too, but would have greatly complicated the Spec type)
• All kinds of properties on the dependency graph of the specification. All these additional restrictions are checked by the Analyser.

PrettyPrinter : Just allows to print the structure of a specification

Tests.Random : Generates random streams and random input values, for easily checking the compiler against the interpreter in an automated way. Currently a bit ugly, would probably have benefited from using the QuickCheck library, rather than the lower-level Random library. All the parameters of the random generation are near the top of the file.

Language : Defines all the different operators of the language. These are defined through a F, F2 or F3 constructor, a function on how to compile them, and a function on how to interpret them. These are also packed in a Operators data structure for use in the random streams generator. Also contains some monomorphic versions of the polymorphic language constructs, to help the type inferer.

AdHocC : A small number of uninteresting functions to output C code. Used by AtomToC.

AtomToC : Adds to the atom-generated code a main function and some initialisation stuff.

Main : "Plumbing" module. Makes the analyser/interpreter/compiler, atom, gcc, and the generated C program interact. Takes its arguments in a very heavy format (not very convenient for fast testing). Warning : it is rather easy to desynchronyze the generated C program and the interpreter with very small modifications (leading to strange bugs).

Interface : Is a wrapper around Main. Writing its argument is usually much easier, thanks to the provided combinators and the reasonable defaults. All it does is translating those into the numerous and verbose arguments Main expects.

Libs.* : As Copilot is embedded in Haskell, it is very easy to write libraries of "macros" that simplify the writing of some specifications. Thus these files, that holds for example functions for easily writing LTL and PTLTL formulas.

Examples.* : Self-explanatory.

*** Simple modifications ***

Add an example : In Examples.Examples, or if related to a library, in Examples.LibraryName

Add some high-level combinator on streams : In a library, in Lib.* Should not call Atom, should only use other combinators and base operators.

Add some operator in the base language : Write in Language.hs, from F, F2 or F3 (see examples) Would be nice to also add to the corresponding Operators set (opsF, opsF2 or opsF3), so that it could be automatically checked. This last point obviously require that the interpreted and compiled semantics are equivalents.

Add some possible types for the streams : Add a new instance of Stremable in Core.hs Add a new record to StreamableMaps in Core.hs Update foldStreamableMaps, mapStreamableMaps, mapStreamableMapsM, and filterStreamableMaps in Core.hs Update foldRandomableMaps in Tests/Random.hs

Authorise a new type to be exchanged by monitors : Add a new instance of Sendable in Core.hs Update foldSendableMaps in Core.hs

Add a new option to Copilot : Add a new field to the Options record in Interface.hs Add a new combinator for that field in Interface.hs Update the baseOptions in Interface.hs Implement it (probably in Main.hs). Update interface in Interface.hs to convey it to the Main.