Generalize ideal aRTA

Merged Sergey Bozhko requested to merge sbozhko/rt-proofs:generalize_aRTA into master

Summary of the changes:

  • Interference and Interfering workload are now type-classes

  • Generalizes aRTA to "multi-stage" aRTA

  • IBF supports arbitrary parameters (not just relative arrival time). IBF parametrised by the relative arrival time is not expressive enough to support restricted-supply analysis. It was generalized to support a larger class of parameters

  • Rename file [run to completion] file into [lower bound on service]. The file was slightly generalized, now it derives a lower bound on any pre-defined amount of service.

  • Generalize instantiations of interference and interfering workload. Now, the definitions do not directly destruct the processor state.

Edited by Sergey Bozhko

Merge request reports