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.