copilot: A stream DSL for writing embedded C monitors.

[ bsd3, embedded, language, library ] [ Propose Tags ]

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 "fib"
 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.


[Skip to Readme]

Modules

[Last Documentation]

  • Language
    • Language.Copilot
      • Language.Copilot.AdHocC
      • Language.Copilot.Analyser
      • Language.Copilot.AtomToC
      • Language.Copilot.Compiler
      • Language.Copilot.Core
      • Language.Copilot.Dispatch
      • Examples
        • Language.Copilot.Examples.Examples
        • Language.Copilot.Examples.LTLExamples
        • Language.Copilot.Examples.PTLTLExamples
        • Language.Copilot.Examples.StatExamples
      • Language.Copilot.Help
      • Language.Copilot.Interface
      • Language.Copilot.Interpreter
      • Language.Copilot.Language
        • Language.Copilot.Language.Casting
        • Language.Copilot.Language.FunctionCalls
        • Language.Copilot.Language.RandomOps
        • Language.Copilot.Language.Sampling
      • Libs
        • Language.Copilot.Libs.ErrorChks
        • Language.Copilot.Libs.Indexes
        • Language.Copilot.Libs.LTL
        • Language.Copilot.Libs.PTLTL
        • Language.Copilot.Libs.Statistics
        • Language.Copilot.Libs.Vote
      • Language.Copilot.PrettyPrinter
      • Tests
        • Language.Copilot.Tests.Random

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.21, 0.22, 0.23, 0.25, 0.26, 0.27, 0.28, 1.0, 1.0.1, 1.0.2, 2.0, 2.0.1, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.0.6, 2.0.7, 2.0.8, 2.0.9, 2.1.0, 2.1.1, 2.1.2, 2.2.0, 2.2.1, 3.0, 3.0.1, 3.1, 3.2, 3.2.1, 3.3, 3.4, 3.5, 3.6, 3.7, 3.8, 3.9, 3.10, 3.11, 3.12, 3.13, 3.14, 3.15, 3.16, 3.16.1, 3.17, 3.18, 3.18.1, 3.19
Dependencies atom (>=1.0.8), base (>=4.0 && <6), containers (>=0.2.0.1), directory (>=1.0.0.0), filepath (>=1.0.0.0), mtl (>=1.0.0.0), process (>=1.0.0.0), random (>=1.0.0.0) [details]
License BSD-3-Clause
Author Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller
Maintainer Lee Pike <leepike@galois.com>
Category Language, Embedded
Home page http://leepike.github.com/Copilot/
Uploaded by LeePike at 2011-03-08T22:15:15Z
Distributions
Reverse Dependencies 6 direct, 0 indirect [details]
Downloads 26746 total (106 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-28 [all 7 reports]

Readme for copilot-1.0.1

[back to package description]
*******************************************************************************
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.