The RT-SEC should be an opt-in extension to the RISC-V RT specification.
Problem/Motivation:
Rust RTIC fuses static guarantees provided by the Rust language with properties of Stack Resource Based scheduling, the former brings memory safety, and freedom from undefined behavior, while the latter ensures race- and deadlock-free execution, single stack sharing, bounded priority inversion. RTIC produces an efficient binary leveraging on the underling hardware (Hippomenes in this case), to perform accelerated scheduling:
task dispatch, entry/exit latency and overhead is zero, and
single cycle resource claim/release (aka lock/unlock).
To ensure memory safety, the Rust compiler performs lifetime analysis and asserts freedom from mutable aliasing. In cases analysis is out of reach, the compiler injects code performing run-time verification that panics in favor of running into undefined behavior. Thus at run-time the generated code either runs under defined (memory safe) behavior or halts with a panic (indicating the type of violation and source code location).
Great, we now have what we all been waiting for, or ....
Not really, the Rust memory safety guarantees may be violated by introducing explicit unsafe code. Luckily, the need for such unsafe code is limited to cases:
de-referencing RAW pointers (needed under the hood for accessing underlying HW)
calling into non-Rust code (e.g., inline assembly or external code)
calling other unsafe code.
Proposed solution:
Hardware support to mitigate safety issues in case of unsafe Rust. (As a complement to static/formal verification of unsafe Rust code.)
Thus, the per-task set of reachable regions can be collected and used for both static and run-time (dynamic) validation. This issue will cover both:
A) stack isolation (under SRP all tasks execute on a shared stack). By denying access to memory region above the sp at dispatch we can ensure total separation of task-local variables. (Assuming stack grows downwards towards lower addresses.)
B) resource validation. By denying access outside of the per-task computed set of regions, tasks are ensured to only access intended memory. Notice, peripherals are not memory mapped, but rather mapped trough CSRs, where the CSR address is a part of the inlined assembly instruction. Thus, we have two open problems here.
a) Howto obtain the intended address.
b) Howto enforce protection.
Implementation:
Hippomenes has the goal to ensure singly cycle execution, with zero cycle latency of interrupt (task) dispatch. Thus the implementation must be able to validate memory accesses with zero-latency. A reasonable approach is to introduce a task id, and let the MPU resolve address validity accordingly. (Similar techniques are found in TLBs). In the aforementioned publication, a two stage lookup approach is presented, where region matching is done in parallel, followed by a selection process. For FPGA solutions, the MPU configuration can be synthesized, while for ASIC, MPU tables need to dynamic (static ram). In case of extreme safety requirements, MPU configuration should be synthesized. (But then resources are fixed in location and size, thus only business logic around may be changed.)
Workflow in suggested order:
The implementation of A). A can be implemented without prior passes.
Static ram based MPU. Proof of concept with manual configuration through a set of CSR registers.
Integration with RTIC as a pass for generating setup information for the init task to populate MPU tables.
Integration with RTIC as a pass for generating application specific MPU configuration.
Stretch goal: CSR space protection (this is green field research).
This tracking issue will be used as a basis for an upcoming Master's thesis at LTU.
The RT-SEC should be an opt-in extension to the RISC-V RT specification.
Problem/Motivation:
Rust RTIC fuses static guarantees provided by the Rust language with properties of Stack Resource Based scheduling, the former brings memory safety, and freedom from undefined behavior, while the latter ensures race- and deadlock-free execution, single stack sharing, bounded priority inversion. RTIC produces an efficient binary leveraging on the underling hardware (Hippomenes in this case), to perform accelerated scheduling:
To ensure memory safety, the Rust compiler performs lifetime analysis and asserts freedom from mutable aliasing. In cases analysis is out of reach, the compiler injects code performing run-time verification that panics in favor of running into undefined behavior. Thus at run-time the generated code either runs under defined (memory safe) behavior or halts with a panic (indicating the type of violation and source code location).
Great, we now have what we all been waiting for, or ....
Not really, the Rust memory safety guarantees may be violated by introducing explicit unsafe code. Luckily, the need for such unsafe code is limited to cases:
Proposed solution:
Hardware support to mitigate safety issues in case of unsafe Rust. (As a complement to static/formal verification of unsafe Rust code.)
Due the RTIC modelling framework, system state is represented by means of typed
resourcesmanaged by the framework. Thus by static analysis ofresources, the range of underlying or referred addresses can be computed Static and Dynamic Memory Protection using Type-Based Memory Layout in Rust.Thus, the per-task set of reachable regions can be collected and used for both static and run-time (dynamic) validation. This issue will cover both:
spat dispatch we can ensure total separation of task-local variables. (Assuming stack grows downwards towards lower addresses.)Implementation:
Hippomenes has the goal to ensure singly cycle execution, with zero cycle latency of interrupt (task) dispatch. Thus the implementation must be able to validate memory accesses with zero-latency. A reasonable approach is to introduce a task id, and let the MPU resolve address validity accordingly. (Similar techniques are found in TLBs). In the aforementioned publication, a two stage lookup approach is presented, where region matching is done in parallel, followed by a selection process. For FPGA solutions, the MPU configuration can be synthesized, while for ASIC, MPU tables need to dynamic (static ram). In case of extreme safety requirements, MPU configuration should be synthesized. (But then resources are fixed in location and size, thus only business logic around may be changed.)
Workflow in suggested order:
inittask to populate MPU tables.This tracking issue will be used as a basis for an upcoming Master's thesis at LTU.