Scheduling behaviour issue

[Simon Wright <simon@pushface.org>]

As some will recall, I've based my Cortex GNAT RTS[1] (for ARM Cortex-M
devices, so far) on FreeRTOS[2].

I've now discovered an unfortunate difference between what the ARM
requires at D.2.3(9)[3] and the way FreeRTOS behaves. What we need is

    A task dispatching point occurs for the currently running task of a
    processor whenever there is a nonempty ready queue for that
    processor with a higher priority than the priority of the running
    task. The currently running task is said to be preempted and it is
    added at the head of the ready queue for its active priority.

but FreeRTOS adds the preempted task at the *tail* of its ready queue
([4], section Prioritized Pre-emptive Scheduling (without Time Slicing),
on page 95 or thereabouts).

I can see that this will make an application less predictable, but I
don't think it'll make a correct application misbehave.

I've been having some trouble thinking of a way to demonstrate the
(mis)behaviour!

[1] https://github.com/simonjwright/cortex-gnat-rts
[2] https://www.freertos.org
[3] http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-D-2-3.html#p9
[4] https://bit.ly/2VK7slM