RTFM update

doc/RTFM.md

@@ -163,16 +163,17 @@ To our aid the Nested Interrupt Vectorized Controller (NVIC) ARM Contex M3 and A
 - 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:
+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`
+- `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.
+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:
 
@@ -214,6 +215,7 @@ Notice here the type `EXTI0::Resources` was not user defined, but rather generat
 
 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:
@@ -228,7 +230,53 @@ The procedural macro `app!` takes a sytem configuration, and performs the follow
     - 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)
+
+
+
 
 Procedural macros in Rust are executed before code generation (causing the argument AST to replaced by a new AST for the remainder of compilation).