Priority inversion check misinterprets priority property and other bugs

[lwrage]

Summary

The priority inversion checker interprets a higher priority property as lower priority. However, the description for Thread_Properties::Priority says "A larger value represents a higher priority."

Steps to Reproduce

1. Load the model below in OSATE
2. Instantiate S.i
3. On the instance model run Analyses -> Timing -> Check Rate Monotonic Priority Assignment
4. There are errors reported even though threads with lower period have higher priority

package Issue1365
public

    system S
    end S;

    system implementation S.i
        subcomponents
            cpu: processor CPU;
            p: process P.i;
        properties
                Actual_Processor_Binding => (reference (cpu));
    end S.i;

    processor CPU
    end CPU;

    process P
    end P;

    process implementation P.i
        subcomponents
            t1: thread T {
                Priority => 3;
                Period => 10ms;
            };
            t2: thread T {
                Priority => 2;
                Period => 20ms;
            };
            t3: thread T {
                Priority => 1;
                Period => 40ms;
            };
    end P.i;

    thread T
        properties
            Dispatch_Protocol => Periodic;
    end T;

end Issue1365;

Environment

• OSATE Version:
• Operating System:

[jjhugues]

The definition in thread_properties.aadl says that in OSATE, but not the standard document. This is also highly dependent on the scheduling policy/RTOS. RTEMS uses the opposite convention.

Please file an errata on AADLv2.2 first to discuss the semantics we want to enforce.

[lwrage]

"A larger value represents a higher priority" is from the standard document. This really is an OSATE bug. The analysis was written before AADLv2.2.

[lwrage]

Rate group handling also has a bug, it only works for the rate group containing the thread with the highest rate. The following priority assignment should be fine (modulo wrong priority order) but reports a priority inversion for t2.

            t0: thread T {
                Priority => 10;
                Period => 10ms;
            };
            t1: thread T {
                Priority => 20;
                Period => 20ms;
            };
            t2: thread T {
                Priority => 15;
                Period => 20ms;
            };

[lwrage]

THe checker allows the same priority for threads with different priorities. That is wrong.