[RFC] shared access to resources (resources = [&FOO])

[japaric]

Summary

Extend the syntax of the resources field to let the user specify when shared, instead of exclusive (today's default), access to a resource is required. Specifying shared access can reduce the number of required critical sections in some scenarios.

Background

Consider this example:

#[rtfm::app(device = ..)]
const APP: () = {
    // NOTE: `ComplexThing` implements the `Sync` trait
    static mut FOO: ComplexThing = /* .. */;

    // ..

    #[task(priority = 1, resources = [FOO])]
    fn foo() {
       resources.FOO.lock(mutate);
    }

    #[task(priority = 2, resources = [FOO])]
    fn bar() {
       resources.FOO.lock(print);
    }

    #[task(priority = 3, resources = [FOO])]
    fn baz() {
        print(resources.FOO);
    }

    // ..
};

fn mutate(foo: &mut ComplexThing) {
    // ..
}

fn print(foo: &ComplexThing) {
    println!("{}", foo);
}

With the current rules, the task bar needs a critical section to access FOO. However, that critical section is not really needed because task baz cannot modify FOO.

Design

The parser will be modified to accept both $ident and &$ident in lists of resources. The former syntax, which exists today, indicates exclusive access to the resource -- its semantics are unchanged; the latter syntax indicates shared access to the resource.

When shared access is specified the task will receive a shared reference (&_) to the resource data rather than a Mutex proxy.

If shared access is requested from two or more tasks that run at different priorities then the resource type must implement the Sync trait. This is required to prevent types with interior mutability (like Cell and RefCell) from being accessed without a critical section, and potentially modified, from those tasks as that could result in UB.

With the proposed changes our opening example can be updated as follows:

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

    #[task(priority = 1, resources = [FOO])]
    fn foo() {
       resources.FOO.lock(mutate);
    }

    // NOTE: `&FOO` instead of `FOO` in `resources`
    #[task(priority = 2, resources = [&FOO])]
    fn bar() {
        // NOTE: no critical section is needed this time
        let reference: &ComplexThing = resources.FOO;

        print(reference);
    }

    // NOTE: `&FOO` instead of `FOO` in `resources`
    #[task(priority = 3, resources = [&FOO])]
    fn baz() {
        print(resources.FOO);
    }

    // ..
};

Unresolved questions

It's unclear what to do in this scenario, other than raise a compiler error:

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

    #[task(priority = 1, resources = [&FOO])]
    fn foo() { /* .. */ }

    #[task(priority = 2, resources = [FOO])]
    fn bar() { /* .. */ }

No optimization can be applied here. The task foo needs a critical section to access the resource data, in any form, but the lock API doesn't make sense here because that grants an exclusive reference (&mut _) to the data and shared access was requested.

[TeXitoi]

About unresolved question, you can have a usecase:

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

    #[task(priority = 1, resources = [&FOO])]
    fn foo() { /* .. */ }

    #[task(priority = 2, resources = [FOO])]
    fn bar() { /* .. */ }

    #[task(priority = 3, resources = [&FOO])]
    fn baz() { /* .. */ }
}

In this case, a lock in foo must block only until priority 2, priority 3 can still run.

[TeXitoi]

and, supposing lock and lock_shared, you may want to use lock_shared in bar to limit the blocking critical section (as a lock_shared in bar need no critical section).

[TeXitoi]

Of course, lock and lock_mut would be more rustic, but not backward compatible (and thus only for 0.5).

[perlindgren]

... or going back to claim/claim_mut notation.

Notice here, resource access is wait free under RTFM, thus claiming a resource does not have the non deterministic behavior of a traditional mutex lock. Its a very important property for static response time analysis, and other timing related matters.

Best regards

Per

---

Från: Guillaume P. notifications@github.com Skickat: den 12 februari 2019 17:24:10 Till: japaric/cortex-m-rtfm Kopia: Subscribed Ämne: Re: [japaric/cortex-m-rtfm] [RFC] shared access to resources (resources = [&FOO]) (#129)

Of course, lock and lock_mut would be more rustic, but not backward compatible (and thus only for 0.5).

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/japaric/cortex-m-rtfm/issues/129#issuecomment-462827837, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AD5naEJMVn2g8svU1L_6MW0k5s6FVBSdks5vMuqqgaJpZM4Z7PYf.

{"api_version":"1.0","publisher":{"api_key":"05dde50f1d1a384dd78767c55493e4bb","name":"GitHub"},"entity":{"external_key":"github/japaric/cortex-m-rtfm","title":"japaric/cortex-m-rtfm","subtitle":"GitHub repository","main_image_url":"https://github.githubassets.com/images/email/message_cards/header.png","avatar_image_url":"https://github.githubassets.com/images/email/message_cards/avatar.png","action":{"name":"Open in GitHub","url":"https://github.com/japaric/cortex-m-rtfm"}},"updates":{"snippets":[{"icon":"PERSON","message":"@TeXitoi in rtfm-rs/cortex-m-rtfm#129: Of course, lock and lock_mut would be more rustic, but not backward compatible (and thus only for 0.5)."}],"action":{"name":"View Issue","url":"https://github.com/japaric/cortex-m-rtfm/issues/129#issuecomment-462827837"}}} [ { "@context": "http://schema.org", "@type": "EmailMessage", "potentialAction": { "@type": "ViewAction", "target": "https://github.com/japaric/cortex-m-rtfm/issues/129#issuecomment-462827837", "url": "https://github.com/japaric/cortex-m-rtfm/issues/129#issuecomment-462827837", "name": "View Issue" }, "description": "View this Issue on GitHub", "publisher": { "@type": "Organization", "name": "GitHub", "url": "https://github.com" } } ]

[korken89]

Doing this would make the resource API un-symmetric, as the order of priorities and references to resources would create different behavior. I would not do this due to that reason, simply by changing from FOO to &FOO different behavior can arise which would need users to understand the underlying model of RTFM to predict - for those that does not understand it, it will just seem random.

[perlindgren]

Hi folks.

I think symmetry is key here. I will make a separate RFC on that matter.

[tmplt]

This RFC is now two years old. Has it been superseded?

[korken89]

No, just not decided on. I'm not sure how much effort it would be to support this in the codegen.

[tmplt]

Echoing some up-to-date notes from the Matrix channel which may be of use: @korken89 writes:

Technically you can have many & access and &mut access to the same resource The analysis just needs to calculate the correct ceiling value Today we only support & access, and reject the use of both on the same resource

The current implementation (allowing & or &mut access, but not both) is a minimum viable product.