Skip to content
  • Kimaya Bedarkar's avatar
    aRTA clean-up · 98612039
    Kimaya Bedarkar authored and Björn Brandenburg's avatar Björn Brandenburg committed
    * The lemmas concerning the correctness of interference and interfering
      workload for JLFP policies are independent of specific scheduling
      policies. Therefore, these lemmas have been proved in the
      `ideal_jlfp_rta` for any general `JLFP` policies satisfying certain
      conditions.
    * The precondition `job_of_task j tsk` in the work-conservation
      definition was unnecessary. This has been removed.
    * Two new lemmas have been added to the global facts database. This led
      to the simplification of some proofs.
    * Fixed one broken comment in `model.task.sequentiality`.
    * Simplified one proof in `ideal_jlfp_rta` since it kept breaking due to
      use of auto-generated names. This required creating one new file -
      `analysis.facts.busy_interval.quiet_time`. Currently, this file
      contains just one lemma that is used in the `ideal_jlfp_rta` file.
    98612039