diff --git a/doc/RTFM.md b/doc/RTFM.md index eb874af00cd502c8b4b336e12f56de43335173ed..ec0df640a0701fbc06c9932f79dfae81dc4c1363 100644 --- a/doc/RTFM.md +++ b/doc/RTFM.md @@ -1,2 +1,217 @@ # 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 + +An interrupt will be dispatched iff: +- `i in I` +- `pri(i) >= max(pri(i) in I)` +- `pri(i) > BASEPRI` +- `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. + +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. + +## The 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 handlers (calling the corresponding tasks) + +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. + + + + + + + + + + +