[RFC] change the resource syntax

[japaric]

Let's try this again.

Summary

Change the declaration syntax of resources from static variables to fields of a
struct.

Current behavior

Today resources are represented in the DSL as static variables. There's a
distinction between static and static mut resources. For the former type one
can only get a shared reference (&-) to the underlying data. For the latter
type one can get a mutable reference( &mut-) to the data but may need to use a
critical section (lock API).

There's also distinction between compile time initialized resources (early
resources) and runtime initialized resources (late resources). The distinction
appears in the declaration syntax: late resources have an initial value of ()
(the unit value) in their declaration.

The following snippet shows the 4 possible types of resources.

#[rtfm::app]
const APP: () = {
    static A: Early = Early::new();
    static B: Late = ();

    static mut C: Early = Early::new();
    static mut D: Late = ();

    // ..
};

Access to resources is controlled using resources lists. Each context declares
the resources it can access in this list.

Below the continuation of the previous snippet that shows the resources lists.

#[rtfm::app]
const APP: () = {
    // ..

    #[task(priority = 1, resources = [A, B, C, D])]
    fn a(cx: a::Context) {
        let a: &Early = cx.resources.A;
        let b: &Late = cx.resources.B;

        cx.resources.C.lock(|c: &mut Early| { /* .. */ });
        cx.resources.D.lock(|d: &mut Late| { /* .. */ });
    }

    #[task(priority = 2, resources = [A, B, C, D])]
    fn b(cx: b::Context) {
        let a: &Early = cx.resources.A;
        let b: &Late = cx.resources.B;

        let c: &mut Early = cx.resources.C;
        let d: &mut Late = cx.resources.D;
    }
};

Proposal

Declaration

A structure named Resources declared within the #[app] module will be used
to declare all the resources in the application. Each field of this struct
is a resource. There is no longer a static / static mut difference at
declaration site.

The #[init] attribute can be used to give an initial (compile-time) value to a
resource. Resources that are not given an initial value are considered late
resources and will be initialized to the values returned by the #[init]
function before interrupts (tasks) are re-enabled.

Example from the previous section ported to the new syntax.

#[rtfm::app]
const APP: () = {
    struct Resources {
        #[init(Early::new())]
        a: Early,

        b: Late,

        #[init(Early::new())]
        c: Early,

        d: Late,
    }

    // ..
};

Access lists

The syntax of resources lists is extended to include shared access: &x.
The current "by value" syntax will now have the meaning of exclusive access.

Resources with only shared access will inherit the properties, requirements
(Sync bound) and API of today's static resources. Resources with only
exclusive access will inherit the properties, requirements and API (lock) of
today's static mut resources.

Continuation of the example ported to the new syntax:

#[rtfm::app]
const APP: () = {
    // ..

    #[task(priority = 1, resources = [&a, &b, c, d])]
    fn a(cx: a::Context) {
        let a: &Early = cx.resources.a;
        let b: &Late = cx.resources.b;

        cx.resources.c.lock(|c: &mut Early| { /* .. */ });
        cx.resources.d.lock(|d: &mut Late| { /* .. */ });
    }

    #[task(priority = 2, resources = [&a, &b, c, d])]
    fn b(cx: b::Context) {
        let a: &Early = cx.resources.a;
        let b: &Late = cx.resources.b;

        let c: &mut Early = cx.resources.c;
        let d: &mut Late = cx.resources.d;
    }
};

LateResources

The LateResources syntax / API is unchanged. Both examples initialize their late resources with the same code, which is shown below:

const APP: () = {
    // ..

    #[init]
    fn init(cx: init::Context) -> init::LateResources {
        init::LateResources { b: Late::new(), d: Late::new() }
    }
};

Restrictions

A single resource cannot appear in the same list twice under different access
modes:

#[task(resources = [x, &x])]
//~^ error: resource `x` appears more than once in the list

A single resource cannot be accessed in different ways (shared and exclusive)
from different tasks.

#[task(resources = [x])]
fn a(cx: a::Context) { /* .. */ }

#[task(resources = [&x])]
//~^ error: shared and exclusive access to the same resource is not allowed
fn b(cx: b::Context) { /* .. */ }

Motivation

1. The current late resource syntax is strange as it would not normally pass the
   type checker in normal Rust.

2. The syntax difference between static and static mut resources is
   artificial, for all resources are lowered down to static mut variables.
   Expressing shared access vs exclusive access in the resources list feels
   more natural and lends itself to API extensions like exclusive-shared locks.

Extensions

These are not part of the main proposal and can be discussed as separated RFCs
but are listed here to show the possibilities.

exclusive-shared locks

This syntax lends itself to implementing exclusive-shared locks (AKA
readers-writer locks) as proposed in RFC #129. The required changes would
involve (a) lifting the second restriction so that shared and exclusive access
to a single resource can be mixed, and (b) adding traits for the two new kinds
of locks:

// crate: rtfm-core
trait LockShared {
    type Data;

    fn lock_shared<R>(&self, f: impl FnOnce(&Self::Data)) -> R;
}

trait LockExclusive: LockShared {
    // (or this could be named `lock`)
    // (or a second method named `lock` that is an alias of this one could be added)
    fn lock_exclusive<R>(&mut self, f: impl FnOnce(&mut Self::Data)) -> R;
}

#[deprecated(note = "use `LockExclusive / lock_exclusive`")]
trait Lock {
    type Data;

    fn lock<R>(&mut self, f: impl FnOnce(&mut Self::Data)) -> R;
}

Example:

#[rtfm::app]
const APP: () = {
    // `Type` must implement the `Sync` trait
    struct Resources {
        x: Type,
        y: AnotherType,
    }

    #[task(priority = 1, resources = [x, y])]
    fn a(cx: a::Context) {
        // BASEPRI is modified (ceiling = 3)
        cx.resources.x.lock_exclusive(|x: &mut Type| { /* .. */ });

        // BASEPRI is *not* modified
        cx.resources.x.lock_shared(|x: &Type| { /* .. */ });

        // BASEPRI is modified (ceiling = 2)
        cx.resources.y.lock_exclusive(|y: &mut AnotherType| { /* .. */ });
    }

    #[task(priority = 2, resources = [&x, y])]
    fn b(cx: b::Context) {
        // no lock required at intermediate priority
        let x: &Type = cx.resources.x;

        let y: &mut AnotherType = cx.resources.y;
    }

    #[task(priority = 3, resources = [&x])]
    fn c(cx: c::Context) {
        let x: &Type = cx.resources.x;
    }
};

[TeXitoi]

I approve this version.

[korken89]

Hi, overall I'm positive but the RFC needs clarification on the following points for completeness:

1. How does the initialization at the end of init look now, are there changes?
2. The definition of shared and exclusive needs updated. To me it sounds as if exclusive means that the resource never needs a lock, but in the example this is not what is shown (only a lock is needed).

---

On the extension, why would a lock_shared be needed? It seems to me that the example is contradictory.
The low priority one needs a lock, sounds good, but does not change BASEPRI, what?
Then any of the other tasks may preempt while x is read in the low priority task. Or is there a detail here that I'm missing?

[japaric]

@korken89

How does the initialization at the end of init look now, are there changes?

It's unchanged. I'll add a note.

The definition of shared and exclusive needs updated

I would explain the resources API like this:

&- is a shared reference. &mut- is an exclusive (or unique) reference.

The Rust aliasing rule states that many shared (&-) references XOR a single exclusive (&mut-) reference to some memory location may exist at any point in time.

The mechanism used to safely share data between tasks is the shared-exclusive lock which has the following API:

• lock_shared: grants shared access (&-) to the underlying data for the span of the closure (critical section).

• lock_exclusive: grants exclusive access (&mut-) to the underlying data for the span of the closure (critical section).

Tasks are given proxies to the shared data, AKA resources, that implement the above API based on what has been specified in the resources access list.

In the resources access list, x indicates that the task needs exclusive access (&mut-) to the data, whereas &x indicates that only shared access (&-) is needed.

The DSL minimizes locks so, for example, the highest priority task that requires exclusive access to a resource directly gets an exclusive reference (&mut-) to the underlying data instead of a resource (proxy).

---

Using other terms like "immutable references" for &- references and "mutable references" for &mut- references or readers-write lock, lock_read and lock_write, IMO, only muddy the explanation with questions like "why can one mutate things through an immutable reference (see Cell / RefCell)?" and "what is even considered a read? The following expression x.lock_read(|f: &File| f.read(&mut buf)) doesn't compile". If there are other suggestions for the terminology, I'm all ears.

On the extension, why would a lock_shared be needed?

lock_shared and lock_exclusive have different signatures: the closure takes a different type of reference (&- vs &mut-) in each API.

lock_shared is needed in the following scenario:

#[task(priority = 1, resources = [&x])]
fn a(cx: a::Context) {
    cx.resources.x.lock_shared(|x: &Type| { /* .. */ });
}

#[task(priority = 2, resources = [x])]
fn b(cx: b::Context) { /* .. */ }

lock_exclusive would give the wrong type of reference (&mut-) if used in a, which wouldn't match with the user specification (&x in the resources list).

The low priority one needs a lock, sounds good, but does not change BASEPRI, what?

Then any of the other tasks may preempt while x is read in the low priority task

That is the intention: tasks b and c are allowed to preempt lock_shared. This results in several shared (&-) references to the data existing at the same time -- this is fine under Rust aliasing rule. Furthermore, the required Sync bound ensures that any mutation done through the shared reference in done in a synchronized fashion (AtomicBool is OK; Cell and RefCell are not); this bound is required precisely because b and c can preempt a at any time.

At the end, whether a lock_* changes BASEPRI or not is an implementation detail (e.g. it doesn't occur with either API when the dynamic priority is already high enough); the contract with the user is that they can only access the underlying data within the closure.

[korken89]

Thanks for the clarification!

On the final note, I think there is something I am missing here.
If the data can be changed while someone is having a & to the data seems like UB to me. What I'm thinking is that lets say the reference is to a struct with multiple fields, one task is reading through & and a higher priority task interrupts in the middle of the read and updates the structure - leaving the reader with half of the old struct and half of the new one in the end.
I think there is something stopping this, but it is not clear to me what as BASEPRI (or any other synchronization primitive) is not touched.
I hope you see my reasoning? Something needs to stop the higher prio task.

[TeXitoi]

The actual behavior is similar to Mutex. The new #129 have a behavior similar to RwLock, allowing to block "only" the tasks needing a write access while locking for read (i.e. allowing the tasks of priority upper that the upper write-asking task). Thus, the resource can't be changed while you're holding a lock_shared resource.

[japaric]

If the data can be changed while someone is having a & to the data seems like UB to me

This is fine is if all mutation happens though a shared reference (&-) and the type implements the Sync trait -- this is shared mutability (AKA "interior mutability); see example below. What's not OK is breaking Rust aliasing rules "many shared references XOR one exclusive reference" but the lock API won't let you do that.

struct Pair {
    x: AtomicU32,
    y: u32,
}

struct Resources {
    pair: Pair,
}

#[task(priority = 1, resources = [pair])]
fn low_prio(cx: low_prio::Context) {
    // BASEPRI is NOT changed = may be preempted by `high_prio`
    cx.resources.pair.lock_shared(|pair: &Pair| {
        // NOTE `pair` is a shared reference (`&-`) to the data

        // read operation = OK
        let x: u32 = pair.x.load(Ordering::Relaxed);

        // read operation = OK
        let y: u32 = *pair.y;

        // RMW operation = OK (because it has retry semantics)
        // (shared mutability or "interior mutability")
        pair.x.fetch_add(1, Ordering::Relaxed);
    });

    // BASEPRI IS changed = may NOT be preempted by `high_prio`
    cx.resources.pair.lock_exclusive(|pair: &mut Pair| {
        // NOTE `pair` is a mutable reference (`&mut-`) to the data

        // write operation = OK (because we have exclusive access)
        pair.x = 0;

        // write operation = OK (because we have exclusive access)
        let y: &mut u32 = pair.y.get_mut();
        *y = 0;
    });
}

#[task(priority = 2, resources = [&pair])]
fn high_prio(cx: high_prio::Context) {
    // NOTE direct shared reference (`&-`) to the data
    let pair: &Pair = cx.resources.pair;

    // read operation = OK
    let x: u32 = pair.x.load(Ordering::Relaxed);

    // read operation = OK
    let y: u32 = *pair.y;

    // write operation = OK (because it's an atomic write)
    // (shared mutability or "interior mutability")
    pair.x.store(0, Ordering::Relaxed);
}

[japaric]

@TeXitoi @korken89 think we can move forward with the syntax change (the main proposal)? We can discuss the shared-exclusive lock extension in a separate RFC.

[korken89]

Yes, it is fine to continue.

I will ponder the extension a bit.

[japaric]

Ok then let's FCP (merge) the main proposal about the syntax change.

• @japaric
• @korken89
• @TeXitoi

[TeXitoi]

OK for me.

[japaric]

The FCP has passed; this RFC is now in the accepted state. Implementation is in PR #205.

[japaric]

Done in PR #205