Library prosa.analysis.facts.model.overheads.schedule_change_bound

Require Export prosa.model.task.arrival.curves.
Require Export prosa.analysis.facts.completes_at.
Require Export prosa.analysis.facts.model.overheads.priority_bump.
Require Export prosa.analysis.facts.model.overheads.schedule_change.
Require Export prosa.analysis.facts.model.arrival_curves.

In this file, we prove upper bounds on the total number of schedule changes that can occur within a busy-interval prefix under FIFO, FP, and general JLFP scheduling policies.

Number of Schedule Changes is Bounded by the Number of Arrivals

We begin by proving a set of helper lemmas that relate the number of schedule changes to the number of job arrivals within a given busy-interval prefix.

Section ScheduleChangesBoundedHelper.

Consider any type of jobs.

  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.

  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.

#[local] Existing Instance basic_ready_instance.

Consider any valid arrival sequence...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any explicit-overhead uni-processor schedule without superfluous preemptions.

  Variable sched : schedule (overheads.processor_state Job).
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
  Hypothesis H_work_conserving : work_conserving arr_seq sched.
  Hypothesis H_no_superfluous_preemptions : no_superfluous_preemptions sched.

Consider any valid preemption model.

  Context `{JobPreemptable Job}.
  Hypothesis H_valid_preemption_model :
    valid_preemption_model arr_seq sched.

Assume that the schedule respects the JLFP policy.

Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

Consider any job j that has a positive job cost and is in the arrival sequence.

  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Consider any busy interval prefix [t1, t2) of job j.

Variables t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2.

We define a helper predicate that holds if some job completes at time t.

Let some_job_completes_at (t : instant) :=
has (fun j_any ⇒ completes_at sched j_any t) (arrivals_up_to arr_seq t).

To reason about the number of schedule changes, we first show that any change in the schedule at time t must be caused by either a priority bump or a job completion.

  Local Lemma schedule_change_caused_by_bump_or_completion :
    ∀ (t : instant),
      t > 0 →
      t1 ≤ t < t2 →
      schedule_change sched t →
      priority_bump sched t || some_job_completes_at t.

As a simple corollary, the number of schedule changes in [t1.+1, t) is bounded by the number of time instants in that interval where either a priority bump occurs or some job completes.

Note: The interval starts at t1.+1 because we do not account for a schedule change at the very first instant of a busy interval. Even if such a change occurs, it is not relevant for our later analysis.

  Local Corollary schedule_changes_bounded_by_bumps_or_completions :
    ∀ (t : instant),
      t1 ≤ t ≤ t2 →
      number_schedule_changes sched t1 .+1 t
      ≤ size [seq to <- index_iota t1 .+1 t | priority_bump sched to || some_job_completes_at to ].

LP and HEP completions are bounded

We now turn to bounding the number of "causes" that could lead to schedule changes within a busy interval prefix. In particular, we consider two types of events: (i) priority bumps, and (ii) job completions. We show that the number of such events is also bounded.

Let us first define the total number of low-priority job completions that occur during the interval (t1, t2). Note that completions exactly at t1 are ignored.

  Let lp_completions_during (t1 t2 : instant) :=
    \sum_(t1 .+1 ≤ to < t2 )
      \sum_(jlp <- arrivals_between arr_seq 0 t2 | ~~ hep_job jlp j )
        completes_at sched jlp to.

Similarly, we define the number of higher-or-equal-priority job completions in the same interval.

  Let hep_completions_during (t1 t2 : instant) :=
    \sum_(t1 .+1 ≤ t < t2 )
      \sum_(jhp <- arrivals_between arr_seq t1 t2 | hep_job jhp j )
        completes_at sched jhp t.

Let us fix a time instant t within the busy-interval prefix.

Variable t : instant.
Hypothesis H_t_in_busy_prefix : t1 < t ≤ t2.

When a low-priority job completes, it necessarily triggers a priority bump. Hence, the number of low-priority completions is bounded by the number of instants in which both a priority bump and a job completion occur.

  Local Lemma lp_completions_bounded_by_prio_bumps_completions :
    lp_completions_during t1 t
    ≤ size [seq t <- index_iota t1 .+1 t
           | priority_bump sched t & some_job_completes_at t ].

Under FIFO scheduling, priorities are determined solely by arrival times. Since a job cannot complete before earlier-arriving jobs, no low-priority job can complete while any higher-priority job is incomplete. Hence, low-priority completions cannot occur.

  Local Lemma lp_completions_bounded_by_arrivals :
    policy_is_FIFO JLFP →
    lp_completions_during t1 t = 0.

A higher-or-equal-priority job can complete at most once. Thus, the number of higher-or-equal-priority completions is bounded by the number of such jobs that arrive during the busy-interval prefix.

  Local Lemma hep_completions_bounded_by_arrivals :
    hep_completions_during t1 t
    ≤ size [seq jhp <- arrivals_between arr_seq t1 t | hep_job jhp j ].

Bounding the number of schedule-change causes

Every job completion must be either a higher-or-equal priority or lower-priority job. Thus, the total number of instants in which some job completes is bounded by the number of completions of LP and HEP jobs.

  Local Lemma some_job_completes_bound :
    size [seq to <- index_iota t1 .+1 t | some_job_completes_at to ]
    ≤ hep_completions_during t1 t + lp_completions_during t1 t.

Priority bumps can only be caused by newly arrived higher-or-equal priority jobs. Therefore, the number of time instants with a priority bump is bounded by the number of such jobs.

  Local Lemma priority_bumps_bounded_by_hep_arrivals :
    size [seq to <- index_iota t1 .+1 t | priority_bump sched to ]
    ≤ size [seq jhp <- arrivals_between arr_seq t1 t | hep_job jhp j ].

In the special case of FIFO priority policy, no priority bump can occur within the interval.

  Local Lemma no_priority_bumps_under_fifo :
    policy_is_FIFO JLFP →
    size [seq to <- index_iota t1 .+1 t | priority_bump sched to ] = 0.

Putting bounds together

The number of instants with either a priority bump or a job completion is at most twice the number of jobs that have higher-or-equal priority than j and arrive in [t1, t).

Intuitively, each such job may trigger at most one priority bump and complete once, and these are the only events that can appear in the considered set.

  Local Lemma bumps_and_completions_bounded_by_hep_arrivals :
    size [seq to <- index_iota t1 .+1 t | priority_bump sched to || some_job_completes_at to ]
    ≤ 2 × size [seq jhp <- arrivals_between arr_seq t1 t | hep_job jhp j ].

Under FIFO scheduling, the number of instants with either a priority bump or a job completion is at most the number of higher-or-equal priority jobs (i.e., earlier or equal arrival time) in [t1, t).

This is because, under FIFO, priority bumps cannot occur, and each such job may complete at most once.

  Local Lemma bumps_and_completions_bounded_by_hep_arrivals_fifo :
    policy_is_FIFO JLFP →
    size [seq to <- index_iota t1 .+1 t | priority_bump sched to || some_job_completes_at to ]
    ≤ size [seq jhp <- arrivals_between arr_seq t1 t | hep_job jhp j ].

End ScheduleChangesBoundedHelper.

Number of schedule changes is bounded

In this section, we prove that the number of schedule changes in a busy-interval prefix is bounded under JLFP scheduling.

Section JLFP.

Consider any type of jobs.

  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobPreemptable Job}.

Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.

  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.

#[local] Existing Instance basic_ready_instance.

Consider any valid arrival sequence...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any explicit-overhead uni-processor schedule without superfluous preemptions of this arrival sequence.

Assume that the schedule respects the JLFP policy.

Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

Assume that the preemption model is valid.

Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.

Consider any job j that has a positive job cost and is in the arrival sequence.

  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Consider any busy interval prefix [t1, t2) of job j.

Variables t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2.

Next, consider any type of tasks ...

  Context {Task : TaskType}.
  Context `{MaxArrivals Task}.
  Context `{JobTask Job Task}.

... and an arbitrary task set ts.

Variable ts : seq Task.

Assume that all jobs stem from tasks in this task set.

Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We assume that max_arrivals is a family of arrival curves that constrains the arrival sequence arr_seq.

Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

Consider an interval [t1, t1 + Δ) ⊆ [t1, t2).

Variable Δ : duration.
Hypothesis H_subinterval : t1 + Δ ≤ t2.

The number of schedule changes in the interval [t1 + 1, t1 + Δ) is bounded by twice the total number of job arrivals across all tasks during Δ.

The factor of 2 arises because each arriving job can cause at most one job completion and one priority bump.

  Lemma schedule_changes_bounded_by_total_arrivals_JLFP :
    number_schedule_changes sched t1 .+1 (t1 + Δ)
    ≤ 2 × \sum_(tsk <- ts ) max_arrivals tsk Δ.

End JLFP.

In this section, we prove that the number of schedule changes in a busy-interval prefix is bounded under FP scheduling.

Section FP.

Consider any type of tasks ...

  Context {Task : TaskType}.
  Context `{MaxArrivals Task}.
  Context `{FP : FP_policy Task}.

... and any type of jobs associated with these tasks.

  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.
  Context `{JobPreemptable Job}.

Consider an FP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.

Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
Hypothesis H_priority_is_transitive : transitive_task_priorities FP.

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.

#[local] Existing Instance basic_ready_instance.

Consider any valid arrival sequence...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any explicit-overhead uni-processor schedule without superfluous preemptions of this arrival sequence.

Assume that the schedule respects the FP policy.

Hypothesis H_respects_policy :
respects_FP_policy_at_preemption_point arr_seq sched FP.

Assume that the preemption model is valid.

Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.

Consider any job j that has a positive job cost and is in the arrival sequence.

  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Consider any busy interval prefix [t1, t2) of job j.

Variables t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2.

Next, we consider an arbitrary task set ts ...

Variable ts : seq Task.

... and assume that all jobs stem from tasks in this task set.

Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We assume that max_arrivals is a family of arrival curves that constrains the arrival sequence arr_seq.

Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

Consider an interval [t1, t1 + Δ) ⊆ [t1, t2).

Variable Δ : duration.
Hypothesis H_subinterval : t1 + Δ ≤ t2.

Under FP scheduling, we bound the number of schedule changes in [t1 + 1, t1 + Δ) by twice the number of arrivals of tasks with priority higher than or equal to the task of job j.

As before, each arrival may lead to at most one priority bump and one completion. Furthermore, tasks with lower priority cannot initiate a schedule change.

  Lemma schedule_changes_bounded_by_total_arrivals_FP :
    number_schedule_changes sched t1 .+1 (t1 + Δ)
    ≤ 2 × \sum_(tsk <- ts | hep_task tsk (job_task j)) max_arrivals tsk Δ.

End FP.

In this section, we prove that the number of schedule changes in a busy-interval prefix is bounded under FIFO scheduling.

Section FIFO.

Consider any type of jobs.

  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobPreemptable Job}.

Consider a FIFO priority policy that indicates a higher-or-equal priority relation.

Context {JLFP : JLFP_policy Job}.
Hypothesis H_FIFO : policy_is_FIFO JLFP.

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.

#[local] Existing Instance basic_ready_instance.

Consider any valid arrival sequence...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any explicit-overhead uni-processor schedule without superfluous preemptions of this arrival sequence.

Assume that the schedule respects the JLFP (i.e., FIFO) policy.

Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

Assume that the preemption model is valid.

Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.

Consider any job j that has a positive job cost and is in the arrival sequence.

  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Consider any busy interval prefix [t1, t2) of job j.

Variables t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2.

Next, consider any type of tasks ...

  Context {Task : TaskType}.
  Context `{MaxArrivals Task}.
  Context `{JobTask Job Task}.

... and an arbitrary task set ts.

Variable ts : seq Task.

Assume that all jobs stem from tasks in this task set.

Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We assume that max_arrivals is a family of arrival curves that constrains the arrival sequence arr_seq.

Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

Consider an interval [t1, t1 + Δ) ⊆ [t1, t2).

Variable Δ : duration.
Hypothesis H_subinterval : t1 + Δ ≤ t2.

Under FIFO scheduling, no priority bumps can occur. Thus, the number of schedule changes in [t1 + 1, t1 + Δ) is at most the number of job arrivals during an interval of length Δ.

  Lemma schedule_changes_bounded_by_total_arrivals_FIFO :
    number_schedule_changes sched t1 .+1 (t1 + Δ)
    ≤ \sum_(tsk <- ts ) max_arrivals tsk Δ.

End FIFO.