backport: fix ceiling analysis bug

[japaric]

This commit fixes a ceiling bug where the ceiling of a ready queue will be
incorrectly computed. The analysis was not including the priority of the system
timer interrupt (SysTick) in the analysis resulting in a priority ceiling
lower than what's required for memory safety which led to data races.

The bug can be observed in the following program:

 #[rtfm::app(device = /* .. */)]
const APP: () = {
    #[init]
    fn init() {
        // ..
    }

    #[task(priority = 2)]
    fn foo(x: i32) {
        // ..
    }

    #[task(priority = 1, spawn = [foo], schedule = [foo])]
    fn bar() {
        // ..
    }

    extern "C" {
        fn EXTI0();
        fn EXTI1();
    }
};

Here the framework chooses a priority of 2 for the SysTick interrupt
(because it matches the priority of the schedule-able task foo).

Both SysTick and bar::Spawn.foo need to access the ready queue (which, in
this case, stores the messages sent to task foo) but the framework doesn't
account for the priority of SysTick (2) and chooses a priority ceiling of
1 for the ready queue (because it matches the priority of task bar which can
spawn foo).

The result is that bar::Spawn.foo modifies the ready queue without a
critical section (because bar's priority matches the priority ceiling of the
ready queue) which is wrong because SysTick (priority = 3) can also modify
the ready queue.

[japaric]

bors try

[bors]

try

Build failed

• continuous-integration/travis-ci/push

[japaric]

bors try

[bors]

try

Build succeeded

• continuous-integration/travis-ci/push