Home | Research | Enseignement | Prelude

Prelude: programming critical real-time systems

To cite this work, please cite this or this.

Further references available here.

Introduction

Prelude is a high-level language for programming real-time embedded control systems. It is built upon Synchronous Languages (such as Lustre) and inherits their formal properties. It adds real-time primitives to enable the programming of multi-periodic systems. The objective of the language is not to replace other synchronous languages but instead to provide a higher layer of abstraction, on top of classic synchronous languages. It can be considered as a real-time software architecture language that enables to assemble locally mono-periodic synchronous systems into a globally multi-periodic synchronous system.

A complete definition of the language is available in my PhD manuscript (see Chapter 4 mainly). A shorter presentation is available here.

The preludec compiler generates synchronized multi-task C code, that is independent of the target OS. Communication is achieved by a tailor-made buffering communication protocol. The compilation was defined formally and produces completely deterministic code, which respects the real-time semantics of the original program (period, deadlines, release dates and precedences) as well as its functional semantics (respect of variables consumption). The Prelude compiler produces code for either monocore or multicore architectures.

Download

You can either download preludec sources or precompiled binaries. You will need OCaml installed to compile the source distribution, which should be packaged for most Linux distributions, otherwise you can get it from here.

Download preludec, version 1.2:

Sources
Linux-32bits binaries
Linux-64bits binaries
Emacs mode for Prelude (see the documentation in the header of the file)

To compile the code generated by preludec, the simplest way is to install SchedMCore.
You can however use your favorite RTOS instead, following the instructions in the README.

Feedback is welcome and encouraged: Email:julien dot forget at lifl dot fr

Supported features

The following features are supported by the current distribution:

Language features:
- Synchronous semantics;
- Periodicity constraints (through strictly periodic clocks);
- Deadline constraints;
- Strictly periodic clocks and associated transformations: periodic over-sampling (*^), periodic under-sampling (/^), phase offset (~>), clock tail (tail) and clock concatenation (::);
- Classic synchronous operators: delay (fby), Boolean under-sampling (when) and Boolean over-sampling (merge);
- Clocks polymorphism;
- Types polymorphism (à la ML).
Static analyses:
- Typing;
- Clock calculus;
- Causality analysis;
- Deadline calculus.
Muli-threaded C code generation (independent from the target OS);
Code suited for either monocore or multicore artchitectures.

Last changes

Main changes of version 1.2, versus version 1.0:

Clock calculus: fixed type extrusion problems in the clock calculus;
MaRTE OS support has (hopefully just temporarily) been dropped;
SchedMCore support;
Two code generation modes are now available: either with precedence encoding (for monocore) or without (for multicore). If the second mode is used, it is the job of the scheduler to ensure that precedence constraints are respected;
All arrays are now allocated statically in the generated C code;
Added an option to specify the output directory;
Clock calculus performances improved.

Last update: June 30, 2011