Skip to content

Add "conditional" interference to remove duplication

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

In short, the idea is to add a new notion of "conditional interference" as follows:

  Definition conditional_interference P j t :=
    (P j t) && (interference j t).

  Definition cumul_cond_interference P j t1 t2 :=
    \sum_(t1 <= t < t2) conditional_interference P j t.

Then, job_interference_is_bounded_by can be generalized as follows. Now, we don't have to duplicate and tweak job_interference_is_bounded_by for different situations like sequential tasks (or restricted supply RTA).

    Definition cond_interference_is_bounded_by Cond :=
      forall t1 t2 Δ j,
        arrives_in arr_seq j ->
        job_of_task tsk j ->
        busy_interval j t1 t2 ->
        t1 + Δ < t2 ->
        ~~ completed_by sched j (t1 + Δ) ->
        forall X, P j X -> 
          cumul_cond_interference Cond j t1 (t1 + Δ) <= IBF tsk X Δ.
          (*    ^^^^--new         ^^^^--new                       *)

Specifically, the bound definition from abstract_seq_rta.v

    Definition task_interference_is_bounded_by
               (tIBF : Task -> duration -> duration -> duration) :=
      forall j R t1 t2,
        arrives_in arr_seq j ->
        job_of_task tsk j ->
        t1 + R < t2 ->
        ~~ completed_by sched j (t1 + R) ->
        busy_interval sched j t1 t2 ->
        let offset := job_arrival j - t1 in
        cumul_task_interference tsk t2 t1 (t1 + R) <= tIBF tsk offset R.

becomes

    Definition non_self (j : Job) (t : instant) :=
      ~~ task_scheduled_at arr_seq sched (job_task j) t.

    Definition task_interference_is_bounded_by tIBF := 
      cond_interference_is_bounded_by
        arr_seq sched tsk tIBF (relative_arrival_time_of_job_is_A sched) non_self.

Merge request reports