# Real Time For the Masses
Real Time For the Masses is a set of programming models and tools geared towards developing systems with analytical properties, with respect e.g., memory requirements, response time, safety and security.
## History
### RTFM-core
The RTFM-core model offers a static task and resource model for device level modelling, implementation and analysis. The original model has been implemented as a coordination language, embedded and extending the C language with a set of RTFM primiteves.
For single core deployment, the input program is analysed under the Stack Resource Policy. The RTFM-core compiler generates code with inlined scheduling and resource managent primives offering the following key properties:
- Efficeint statcic priority preemtive scheduling, using the underlying interrupt hardware
- Race-free execution (each resource is exclusively accessed)
- Deadlock-free execution
- Schedulability test and response time analysing using a plethora of known methods
Related publications:
- [Real-time for the masses: Step 1: programming API and static priority SRP kernel primitives](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A1005680&c=23&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
- [RTFM-core: Language and Implementation](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A1013248&c=11&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
- [RTFM-RT: a threaded runtime for RTFM-core towards execution of IEC 61499](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A1001553&c=12&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
- [Abstract Timers and their Implementation onto the ARM Cortex-M family of MCUs](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A1013030&c=4&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
- [Safe tasks: run time verification of the RTFM-lang model of computation](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A1037297&c=6&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
- [Well formed Control-flow for Critical Sections in RTFM-core](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A1013317&c=13&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
### RTFM-cOOre
An object oriented model offering a component based abstraction. RTFM-cOOre models can be compiled to RTFM-core for further analysis and target code generation. The language is a mere proof of concept, used by students of the course in Compiler Construction at LTU. The RTFM-cOOre language undertakes the computational model of Concurrent Reactive Objects similarly to the functional Timber language, its C-code implementation (TinyTimber) and the CRC/CRO IDE below.
Related publications:
- [Timber](http://www.timber-lang.org/)
- [TinyTimber, Reactive Objects in C for Real-Time Embedded Systems](http://ieeexplore.ieee.org/document/4484933/)
- [An IDE for component-based design of embedded real-time software](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A1013957&c=26&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
- [RTFM-lang static semantics for systems with mixed criticality](http://ltu.diva-portal.org/smash/record.jsf?dswid=-6547&pid=diva2%3A987559&c=19&searchType=RESEARCH&language=en&query=&af=%5B%5D&aq=%5B%5B%7B%22personId%22%3A%22pln%22%7D%5D%5D&aq2=%5B%5B%5D%5D&aqe=%5B%5D&noOfRows=50&sortOrder=dateIssued_sort_desc&sortOrder2=title_sort_asc&onlyFullText=false&sf=all)
- [RTFM-core: course in compiler construction](http://ltu.diva-portal.org/smash/record.jsf?faces-redirect=true&aq2=%5B%5B%5D%5D&af=%5B%5D&searchType=SIMPLE&sortOrder2=title_sort_asc&query=&language=sv&pid=diva2%3A1068636&aq=%5B%5B%5D%5D&sf=all&aqe=%5B%5D&sortOrder=author_sort_asc&onlyFullText=false&noOfRows=50&dswid=-6339)
### RTFM in Rust
A major drawback of the RTFM-core model relies in the dependency to C code for the implementation of tasks (risking to break the safety of memory accesses and introduce race conditions). While the RTFM-cOOre model lifts this dependency, developing and maintaining a fully fledged language and accomyanying compiler is a daunting task. Instead, we took the rout of the systems programming language offering the memory saftey required and more it turned out.
- first attempt:
Resource protection by scope and `Deref`. Without going into details, a proof of concept was implemented. However feasibible, the approach was dropped in favour of using closures, as seen in RTFM-v1 and RTFM-v2 below.
- second attempt:
At this time Japaric came into play, bringing Rust coding ninja skillz. [RTFM-v1](http://blog.japaric.io/fearless-concurrency/). The approach allows the user to enter resource ceilings manually and uses the Rust type system to verify their soundness. The approach is fairly complicated, and writing generic code requires explicit type bounds.
- current implmentetaion.
In [RTFM-v2](http://blog.japaric.io/rtfm-v2/), A system model is given declaratively (by the `app!` procedural macro). During compilation the system model is analysed, resource ceilings derived and code generated accordingly. This simplifies programming, and generics can be expressed more succintly.
The RTFM-v2 implmentation provides a subset of the original RTFM-core language. The RTFM-core model offers offsed based scheduling, a taks may trigger the asynchronous execution of a sub-task, with optional timing offset, priority assignment and payload. The `rtfm-core` compiler analyses the system model and statically allocates buffers and generates code for sending and receiving payloads. This has not been implmendend the RTFM-v2 framework. However, similar bahavior can be programmatically achieved by manually triggering tasks (`rtfm::set_pending`), and using `arm-core systic`/`device timers` to give timing offsets. Payloads can be safely implmented using *channels* (unprotected *single writer, single readerafter writer* buffers)
- current work and future implmentations.
One can think of extending the RTFM-v2 API with channels, and synthsize buffers, send/receive code and timer managament. (Suitable Masters theisis.)
The CRC/CRO model has been implemented as a proof of concept. Unlike the RTFM-cOOre model, RTFM-CRC direcly generates target code (i.e., it does NOT compile to RTFM-v2). RTFM-CRC is in a prototype stage, implemented so far:
- A system level `Sys` AST (abstact syntax tree) is derived from CRC (components)/ CRO (object) descriptions (given in separtate text files following a Rust struct like syntax for each componet and object)
- The `Sys` AST is analysed and resources, and task set dirived. From that resource ceilings are derived.
- Resources (objcets) and resource ceilings are synthesized.
- Message buffers and messeage passing primintives are synthesized (assuming each message/port being a single buffer)
Not implemented:
- There is no automatic support for messages with offesets (for the puprose of demontastration a mockup is passible by hand written code)
# RTFM-v2 breakdown
In this section a behind the scenes breakdown of the RTFM-v2 is provided.
---
## Task/resource model
The RTFM-v2 mode defines a system in terms of a set of tasks and resources, in compliance to the Stack Resource policy for task with static priorirties and single unit resources.
### Tasks and Resouces
- `t` in a task, with priority `pri(t)`, during exection a task may `claim` the access of resorces in a nested (LIFO) fashion.
- `r` is a singe unit resource (i.e., `r` can be eiter *locked* or *free*), `ceil(r)` denotes the ceiling of the resource computed as the maximum priority of any task claiming `r`
Example: assume a system with three tasks `t1, t2, t3` and two resorces `low, high`:
- `t1`, `pri(t1) = 1`, claiming both `low, high`
- `t2`, `pri(t2) = 2`, claiming `low`
- `t3`, `pri(t3) = 3`, claiming `high`
This renders the resources.
- `low`, `ceil(low) = max(pri(t1), pri(t2)) = 2`
- `high`, `ceil(high) = max(pri(t1), pri(t3)) = 3`
---
### System Ceiling and Current running task
- `sc` is the current system ceiling, set to the maximum ceiling of currently held resources
- `st` is the currently running task
Example:
Assume we currently run the task `t1` having claimed both resources `low` and `high`
- `sc = max(ceil(low), ceil(high)) = max(2, 3) = 3`
- `st = t1`
---
### Execution semantics
- `P` is the set of requested (pended), but not yet dispatched tasks
A task `t` can only be dispatched (scheduled for execution) iff:
- `t in P`
- `pri(t) >= max(pri(tn)), tn in P`
- `pri(t) > sc`
- `pri(t) > pri(st)`
Example1:
Assume we are currently running task `t1` at the point `low` is held. At this point both `t2` and `t3` are requested for execution (becomes pending).
- `sc = max(ceil(low)) = max(2) = 2`
- `sp = pri(t1) = 1`
- `P = {t2, p3}`
Following the dispatch rule, for `t2`:
- `t2 in P` =>
`t2 in {t2, t3}` => OK
- `pri(t2) >= max(pri(tn)), tn in P` =>
`2 >= max(2, 3)` => FAIL
The scheduling condition for `t2` is not met.
Following the dispatch rule, for `t3`:
- `t3 in P` =>
`t3 in {t2, t3}` => OK
- `pri(t3) >= max(pri(tn)), tn in P` =>
`3 >= max(2, 3)` OK =>
- `pri(t3) > sc` =>
`3 > 2` OK =>
- `pri(t3) > pri(t1)` =>
`3 > 1` OK
All conditions hold, and task `t3` will be dispatched.
Example 3:
Assume we are currently running task `t1` at the point both `low` and `high` are held. At this point both `t2` and `t3` are requested for execution (becomes pending).
In this case both `t2` and `t3` fails meeting the dispatch rules. Details left to the reader as an excercise.
Notice, due to the dispatch condition, a task may never preempt itself.
---
## RTFM on Bare Metal ARM Contex M3 and Above
To our aid the Nested Interrupt Vectorized Controller (NVIC) ARM Contex M3 and Above implements the following:
- tracks the `pri(i)`, for each interrupt handler `i`
- tracks the set of pended interrupts `I`
- tracks the `si` (the currently running interrupt handler)
- the `BASEPRI` register, a base priority for dispatching interrupts
- the `PRIMASK` register, a global interrupt enable.
An interrupt will be dispatched iff (for details see [Core Registers](http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0552a/CHDBIBGJ.html)):
- `i in I`
- `pri(i) >= max(pri(i) in I)`
- `pri(i) > BASEPRI && !PRIMASK`
- `pri(i) > pri(si)`
Mapping:
We map each task `t` to an interrupt `i` with `pri(i) = pri(t)`. Assume `BASEPRI` is set to `sc` system ceiling. Assume `PRIMASK == false`.
Exercises:
- Show for the two examles that the NVIC will dispatch `i3` for the above Example 2, while not dispatch any interrupt for abave Example 3.
- Show that an interrupt cannot preempt itself.
Notice, under the Stack Resource Policy, there is an additional dispatch rule, on a tie among pending tasks priorties, the one with the oldest time for request has priority. This rule cannot be enforced directly by the NVIC. However, it can be shown that this restriction does not invalidate soundness, it only affects the response time calculation.
---
## Overall design
Code is split into three partitions,
- the generic `cortex-m-rtfm` library,
- the user code, and
- the *glue* code generated from the `app!` macro.
---
### `cortex-m-rtfm` library
The library implements an *unsafe* `claim<T, R, F>` method, `T` being a referernce to the resource data (can be either `&` or `&mut`), `R` the return type, and `F: FnOnce(T, &mut Threshold) -> R` the closure to execute within the `claim`. Claim cannot be directy accessed from *safe* user code instead a *safe* API `claim/claim_mut` is offered by the generated code. (The API is implemented by a *trait* approach.)
---
### User code
```rust
fn exti0(
t: &mut Threshold,
EXTI0::Resources { mut LOW, mut HIGH }: EXTI0::Resources,
)
```
`t` is the initial `Threshold`, used for the resource protection mechanism (as seen later the parameter will be opted out by the compiler in `--release` mode, yet been the logic behind the parameter will be taken into account.)
`EXTI0::Resources { mut LOW, mut HIGH }: EXTI0::Resources` gives access to the the resources, `LOW` and `HIGH`. Technically, we *destruct* the given parameter (of type `EXTI0::Resource`) into its fields (`mut LOW`, `mut HIGH`).
Notice here the type `EXTI0::Resources` was not user defined, but rather generated by the `app!` macro.
The `LOW`/`HIGH` arguments gives you *safe* access to the corresponding resources through the *safe* API (`claim/claim_mut`).
---
### Generated code (app! macro)
The procedural macro `app!` takes a sytem configuration, and performs the following:
- `Sys` AST creation after syntactic check
- A mapping from tasks to interrupts
- Resource ceiling computation according to the RTFM SRP model
- Generation of code for:
- task to interrupt bindings, and initialization code enabling corresponding interrupts
- static memory allocation and initialization for Resources
- Generation of structures for task parameters
- Interrupt entry points (calling the corresponding tasks)
### Invariants and key properties
Key properties include:
- Race-free execution (each resource is exclusively accessed)
- Deadlock-free execution
Both rely on the RTFM (SRP based) execution model, and a correct implementation thereof. A key component here is the implementation of `claim` in the `cortex-m-rtfm` library.
```rust
pub unsafe fn claim<T, R, F>(
data: T,
ceiling: u8,
_nvic_prio_bits: u8,
t: &mut Threshold,
f: F,
) -> R
where
F: FnOnce(T, &mut Threshold) -> R,
{
if ceiling > t.value() {
let max_priority = 1 << _nvic_prio_bits;
if ceiling == max_priority {
atomic(t, |t| f(data, t))
} else {
let old = basepri::read();
let hw = (max_priority - ceiling) << (8 - _nvic_prio_bits);
basepri::write(hw);
let ret = f(data, &mut Threshold::new(ceiling));
basepri::write(old);
ret
}
} else {
f(data, t)
}
}
```
As seen, the implmentation is fairly simple. `ceiling` here is the resource ceiling for the static data `T`, and `t` is the current `Threshold`. If `ceiling <= t.value()` we can directly access it by executing the closure (`f(dada, t)`), else we need to *claim* the resource before access. Claiming has two cases:
- `ceiling == max_priority` => here we cannot protect the resource by setting `BASEPRI` (masking priorities), and instead use `atomic` (which executes the closure `|t| f(data, t)` with globally disabled interrupts ( `PRIMASK = true`)
- `ceiling != max_priority` => here we store the current system ceiling, (`old = basepri::read())`, set the new system ceiling `basepri::write(hw)` execute the closure `ret = f(data, &mut Threshold::new(ceiling))`, restore the system ceiling, `basepri::write(old)` and return the result `ret`. The `PRIMASK` and `BASEPRI` regeisters are located in the `Private Peripheral Bus` memory region, which is `Strongly-ordered` (meaning that accesses are executed in program order). I.e. the next instruction following `basepri::write(hw)` (inside the `claim`) will be protected by the raised system ceiling. [Arm doc - memory barriers](https://static.docs.arm.com/dai0321/a/DAI0321A_programming_guide_memory_barriers_for_m_profile.pdf)
Race freness at this level can be argued from:
- Each *resource* is associated a *ceiling according to SRP
- Accessing a *resource* from *safe* user code can only be done through the `Resource::claim/claim_mut` trait, calling the library `claim`
Procedural macros in Rust are executed before code generation (causing the argument AST to replaced by a new AST for the remainder of compilation).
The intermediate code (AST after expansion) can be exported by the `cargo` sub-command `export`.
> cargo export examples nested > expanded.rs
or
> xargo export examples nested > expanded.rs
Let us study the `nested` example in detail.
```rust
app! {
device: stm32f40x,
resources: {
static LOW: u64 = 0;
static HIGH: u64 = 0;
},
tasks: {
EXTI0: {
path: exti0,
priority: 1,
resources: [LOW, HIGH],
},
EXTI1: {
path: exti1,
priority: 2,
resources: [LOW],
},
EXTI2: {
path: exti2,
priority: 3,
resources: [HIGH],
},
},
}
```
The intermediate AST defines the following `main` function.
```rust
fn main() {
let init: fn(stm32f40x::Peripherals, init::Resources) = init;
rtfm::atomic(unsafe { &mut rtfm::Threshold::new(0) }, |_t| unsafe {
let _late_resources =
init(stm32f40x::Peripherals::all(), init::Resources::new());
let nvic = &*stm32f40x::NVIC.get();
let prio_bits = stm32f40x::NVIC_PRIO_BITS;
let hw = ((1 << prio_bits) - 3u8) << (8 - prio_bits);
nvic.set_priority(stm32f40x::Interrupt::EXTI2, hw);
nvic.enable(stm32f40x::Interrupt::EXTI2);
let prio_bits = stm32f40x::NVIC_PRIO_BITS;
let hw = ((1 << prio_bits) - 1u8) << (8 - prio_bits);
nvic.set_priority(stm32f40x::Interrupt::EXTI0, hw);
nvic.enable(stm32f40x::Interrupt::EXTI0);
let prio_bits = stm32f40x::NVIC_PRIO_BITS;
let hw = ((1 << prio_bits) - 2u8) << (8 - prio_bits);
nvic.set_priority(stm32f40x::Interrupt::EXTI1, hw);
nvic.enable(stm32f40x::Interrupt::EXTI1);
});
let idle: fn() -> ! = idle;
idle();
}
```
Essentially, the generated code initates the peripheral and resource bindings in an `atomic` section (with the interrupts disabled). The code also sets the interrupt priorities and enables the interrupts.
```rust
pub struct _initResources<'a> {
pub LOW: &'a mut rtfm::Static<u64>,
pub HIGH: &'a mut rtfm::Static<u64>,
}
#[allow(unsafe_code)]
mod init {
pub use stm32f40x::Peripherals;
pub use _initResources as Resources;
#[allow(unsafe_code)]
impl<'a> Resources<'a> {
pub unsafe fn new() -> Self {
Resources {
LOW: ::rtfm::Static::ref_mut(&mut ::_LOW),
HIGH: ::rtfm::Static::ref_mut(&mut ::_HIGH),
}
}
}
}
static mut _HIGH: u64 = 0;
static mut _LOW: u64 = 0;
mod _resource {
#[allow(non_camel_case_types)]
pub struct HIGH {
_0: (),
}
#[allow(unsafe_code)]
impl HIGH {
pub unsafe fn new() -> Self {
HIGH { _0: () }
}
}
#[allow(non_camel_case_types)]
pub struct LOW {
_0: (),
}
#[allow(unsafe_code)]
impl LOW {
pub unsafe fn new() -> Self {
LOW { _0: () }
}
}
}
```
The allocation of memory for the system resources is done using (global) `static mut`, with resource names prepended by `_`. Resources can only by accessed from user code through the `Resource` wrapping, initialized at run time.
In Rust a `mod` provides a *name space*, thus the statically allocated `HIGH` and `LOW` structs are accessed under the names `_resource::HIGH`, `_resource::LOW` respectively.
Code is generated for binding the user API `RES::claim`/`RES::claim_mut` to the library implementation of `claim`. For `claim` the reference is passed as `rtfm::Static::ref_(&_HIGH)`, while for `claim_mut` the reference is passed as `rtfm::Static::ref_mut(&_HIGH)`. Recall here that `_HIGH` is the actual resource allocation.
Similarly code is generated for each resource.
```rust
unsafe impl rtfm::Resource for _resource::HIGH {
type Data = u64;
fn claim<R, F>(&self, t: &mut rtfm::Threshold, f: F) -> R
where
F: FnOnce(&rtfm::Static<u64>, &mut rtfm::Threshold) -> R,
{
unsafe {
rtfm::claim(
rtfm::Static::ref_(&_HIGH),
3u8,
stm32f40x::NVIC_PRIO_BITS,
t,
f,
)
}
}
fn claim_mut<R, F>(&mut self, t: &mut rtfm::Threshold, f: F) -> R
where
F: FnOnce(&mut rtfm::Static<u64>, &mut rtfm::Threshold) -> R,
{
unsafe {
rtfm::claim(
rtfm::Static::ref_mut(&mut _HIGH),
3u8,
stm32f40x::NVIC_PRIO_BITS,
t,
f,
)
}
}
}
```
The `rtfm::Resource` *triat* and `rtfm::Static` type are given through the `rtfm_core` crate.
```rust
pub unsafe trait Resource {
/// The data protected by the resource
type Data: Send;
/// Claims the resource data for the span of the closure `f`. For the
/// duration of the closure other tasks that may access the resource data
/// are prevented from preempting the current task.
fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
where
F: FnOnce(&Static<Self::Data>, &mut Threshold) -> R;
/// Mutable variant of `claim`
fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
where
F: FnOnce(&mut Static<Self::Data>, &mut Threshold) -> R;
}
unsafe impl<T> Resource for Static<T>
where
T: Send,
{
type Data = T;
fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
where
F: FnOnce(&Static<Self::Data>, &mut Threshold) -> R,
{
f(self, t)
}
fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
where
F: FnOnce(&mut Static<Self::Data>, &mut Threshold) -> R,
{
f(self, t)
}
}
/// Preemption threshold token
///
/// The preemption threshold indicates the priority a task must have to preempt
/// the current context. For example a threshold of 2 indicates that only
/// interrupts / exceptions with a priority of 3 or greater can preempt the
/// current context
pub struct Threshold {
value: u8,
_not_send: PhantomData<*const ()>,
}
impl Threshold {
/// Creates a new `Threshold` token
///
/// This API is meant to be used to create abstractions and not to be
/// directly used by applications.
pub unsafe fn new(value: u8) -> Self {
Threshold {
value,
_not_send: PhantomData,
}
}
/// Creates a `Threshold` token with maximum value
///
/// This API is meant to be used to create abstractions and not to be
/// directly used by applications.
pub unsafe fn max() -> Self {
Self::new(u8::MAX)
}
/// Returns the value of this `Threshold` token
pub fn value(&self) -> u8 {
self.value
}
}
```