# Library prosa.analysis.abstract.ideal_jlfp_rta

Require Export prosa.analysis.abstract.abstract_seq_rta.

Require Export prosa.analysis.definitions.priority_inversion.

Require Export prosa.analysis.definitions.work_bearing_readiness.

Require Export prosa.analysis.facts.busy_interval.carry_in.

Require Export prosa.analysis.definitions.priority_inversion.

Require Export prosa.analysis.definitions.work_bearing_readiness.

Require Export prosa.analysis.facts.busy_interval.carry_in.

Throughout this file, we assume ideal uni-processor schedules.

Require Import prosa.model.processor.ideal.

Require Export prosa.analysis.facts.busy_interval.ideal.priority_inversion.

Require Export prosa.analysis.facts.busy_interval.ideal.priority_inversion.

# JLFP instantiation of Interference and Interfering Workload for ideal uni-processor.

In this module we instantiate functions Interference and Interfering Workload for an arbitrary JLFP-policy that satisfies the sequential tasks hypothesis. We also prove equivalence of Interference and Interfering Workload to the more conventional notions of service or workload.
Consider any type of tasks ...

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

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Consider any valid arrival sequence with consistent arrivals...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any ideal uni-processor schedule of this arrival sequence...

Variable sched : schedule (ideal.processor_state Job).

Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

... where jobs do not execute before their arrival nor after completion.

Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Assume we have sequential tasks, i.e., jobs of the
same task execute in the order of their arrival.

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

Context `{JLFP_policy Job}.

Hypothesis H_priority_is_reflexive : reflexive_priorities.

Hypothesis H_priority_is_transitive : transitive_priorities.

Hypothesis H_priority_is_reflexive : reflexive_priorities.

Hypothesis H_priority_is_transitive : transitive_priorities.

We also assume that the policy respects sequential tasks, meaning
that later-arrived jobs of a task don't have higher priority than
earlier-arrived jobs of the same task.

Let tsk be any task to be analyzed.

For simplicity, let's define some local names.

Let job_scheduled_at := scheduled_at sched.

Let job_completed_by := completed_by sched.

Let cumulative_task_interference := cumul_task_interference arr_seq sched.

Let job_completed_by := completed_by sched.

Let cumulative_task_interference := cumul_task_interference arr_seq sched.

## Interference and Interfering Workload

In this section, we introduce definitions of interference, interfering workload, and a function that bounds cumulative interference.
Next, we say that job j is incurring interference from another
job with higher or equal priority at time t, if there exists a
job jhp (different from j) with higher or equal priority
that executes at time t.

Definition is_interference_from_another_hep_job (j : Job) (t : instant) :=

if sched t is Some jhp then

another_hep_job jhp j

else false.

if sched t is Some jhp then

another_hep_job jhp j

else false.

Similarly, we say that job j is incurring interference from a
job with higher or equal priority of another task at time t,
if there exists a job jhp (of a different task) with higher or
equal priority that executes at time t.

Definition is_interference_from_hep_job_from_another_task (j : Job) (t : instant) :=

if sched t is Some jhp then

another_task_hep_job jhp j

else false.

if sched t is Some jhp then

another_task_hep_job jhp j

else false.

Now, we define the notion of cumulative interference, called
interfering_workload_of_hep_jobs, that says how many units of
workload are generated by jobs with higher or equal priority
released at time t.

Definition interfering_workload_of_hep_jobs (j : Job) (t : instant) :=

\sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.

\sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.

Instantiation of Interference We say that job j incurs interference at time t iff it
cannot execute due to a higher-or-equal-priority job being
scheduled, or if it incurs a priority inversion.

Definition interference (j : Job) (t : instant) :=

is_priority_inversion j t || is_interference_from_another_hep_job j t.

is_priority_inversion j t || is_interference_from_another_hep_job j t.

Instantiation of Interfering Workload The interfering workload, in turn, is defined as the sum of the
priority inversion function and interfering workload of jobs
with higher or equal priority.

Definition interfering_workload (j : Job) (t : instant) :=

is_priority_inversion j t + interfering_workload_of_hep_jobs j t.

is_priority_inversion j t + interfering_workload_of_hep_jobs j t.

For each of the concepts defined above, we introduce a corresponding cumulative function: (a) cumulative priority inversion...

Definition cumulative_priority_inversion (j : Job) (t1 t2 : instant) :=

\sum_(t1 ≤ t < t2) is_priority_inversion j t.

\sum_(t1 ≤ t < t2) is_priority_inversion j t.

... (b) cumulative interference from other jobs with higher or equal priority...

Let cumulative_interference_from_other_hep_jobs (j : Job) (t1 t2 : instant) :=

\sum_(t1 ≤ t < t2) is_interference_from_another_hep_job j t.

\sum_(t1 ≤ t < t2) is_interference_from_another_hep_job j t.

... (c) and cumulative interference from jobs with higher or equal priority from other tasks...

Definition cumulative_interference_from_hep_jobs_from_other_tasks (j : Job) (t1 t2 : instant) :=

\sum_(t1 ≤ t < t2) is_interference_from_hep_job_from_another_task j t.

\sum_(t1 ≤ t < t2) is_interference_from_hep_job_from_another_task j t.

... (d) cumulative interference...

... (e) cumulative workload from jobs with higher or equal priority...

Let cumulative_interfering_workload_of_hep_jobs (j : Job) (t1 t2 : instant) :=

\sum_(t1 ≤ t < t2) interfering_workload_of_hep_jobs j t.

\sum_(t1 ≤ t < t2) interfering_workload_of_hep_jobs j t.

... (f) and cumulative interfering workload.

Let cumulative_interfering_workload (j : Job) (t1 t2 : instant) :=

\sum_(t1 ≤ t < t2) interfering_workload j t.

\sum_(t1 ≤ t < t2) interfering_workload j t.

Instantiated functions usually do not have any useful lemmas about them. In order to
reuse existing lemmas, we need to prove equivalence of the instantiated functions to
some conventional notions. The instantiations given in this file are equivalent to
service and workload. Further, we prove these equivalences formally.
In order to avoid confusion, we denote the notion of a quiet
time in the

*classical*sense as quiet_time_cl, and the notion of quiet time in the*abstract*sense as quiet_time_ab.
Let quiet_time_cl := busy_interval.quiet_time arr_seq sched.

Let quiet_time_ab := definitions.quiet_time sched interference interfering_workload.

Let quiet_time_ab := definitions.quiet_time sched interference interfering_workload.

Same for the two notions of a busy interval.

Let busy_interval_cl := busy_interval.busy_interval arr_seq sched.

Let busy_interval_ab := definitions.busy_interval sched interference interfering_workload.

Let busy_interval_ab := definitions.busy_interval sched interference interfering_workload.

Before we present the formal proofs of the equivalences, we recall
the notion of workload of higher or equal priority jobs.

Let workload_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=

workload_of_jobs (fun jhp ⇒ another_hep_job jhp j) (arrivals_between arr_seq t1 t2).

workload_of_jobs (fun jhp ⇒ another_hep_job jhp j) (arrivals_between arr_seq t1 t2).

Similarly, we recall notions of service of higher or equal priority jobs from other tasks...

Let service_of_hep_jobs_from_other_tasks (j : Job) (t1 t2 : instant) :=

service_of_jobs sched (fun jhp ⇒ another_task_hep_job jhp j)

(arrivals_between arr_seq t1 t2) t1 t2.

service_of_jobs sched (fun jhp ⇒ another_task_hep_job jhp j)

(arrivals_between arr_seq t1 t2) t1 t2.

... and service of all other jobs with higher or equal priority.

Let service_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=

service_of_jobs sched (fun jhp ⇒ another_hep_job jhp j) (arrivals_between arr_seq t1 t2) t1 t2.

service_of_jobs sched (fun jhp ⇒ another_hep_job jhp j) (arrivals_between arr_seq t1 t2) t1 t2.

## Equivalences

In this section we prove useful equivalences between the definitions obtained by instantiation of definitions from the Abstract RTA module (interference and interfering workload) and definitions corresponding to the conventional concepts.
In the following subsection, we prove properties of the
introduced functions under the assumption that the schedule is
idle.

Consider a time instant t ...

... and assume that the schedule is idle at t.

We prove that in this case: ...
... interference from higher-or-equal priority jobs from
another task is equal to false, ...

Lemma idle_implies_no_hep_task_interference :

∀ j, is_interference_from_hep_job_from_another_task j t = false.

∀ j, is_interference_from_hep_job_from_another_task j t = false.

... and interference for a task is equal to false as well.

Lemma idle_implies_no_task_interference :

∀ upp, task_interference_received_before arr_seq sched interference tsk upp t = false.

End IdleSchedule.

∀ upp, task_interference_received_before arr_seq sched interference tsk upp t = false.

End IdleSchedule.

Next, we prove properties of the introduced functions under
the assumption that the scheduler is not idle.

Consider a job j of task tsk. In this subsection, job
j is deemed to be the main job with respect to which the
functions are computed.

Consider a time instant t.

First, consider a case when

*some*jobs is scheduled at time t.
Under the stated assumptions, we show that the
interference from another higher-or-equal priority job is
equal to the relation another_hep_job.

Lemma interference_ahep_eq_ahep :

is_interference_from_another_hep_job j t = another_hep_job j' j.

End SomeJobIsScheduled.

is_interference_from_another_hep_job j t = another_hep_job j' j.

End SomeJobIsScheduled.

Then there is no interference from higher-or-equal
priority jobs at time t.

Lemma interference_ahep_job_eq_false :

is_interference_from_another_hep_job j t = false.

End JIsScheduled.

is_interference_from_another_hep_job j t = false.

End JIsScheduled.

In the next subsection, we consider a case when a job j'
from the same task (as job j) is scheduled.

Variable j' : Job.

Hypothesis H_j'_tsk : job_of_task tsk j'.

Hypothesis H_j'_sched : scheduled_at sched j' t.

Hypothesis H_j'_tsk : job_of_task tsk j'.

Hypothesis H_j'_sched : scheduled_at sched j' t.

Then we show that interference from higher-or-equal
priority jobs from another task is false.

Similarly, task interference is equal to false, since in
order to incur the task interference, a job from a
distinct task must be scheduled.

Lemma task_interference_eq_false :

∀ upp,

task_interference_received_before arr_seq sched interference tsk upp t = false.

End FromSameTask.

∀ upp,

task_interference_received_before arr_seq sched interference tsk upp t = false.

End FromSameTask.

In the next subsection, we consider a case when a job j'
from a task other than j's task is scheduled.

Variable j' : Job.

Hypothesis H_j'_not_tsk : ~~ job_of_task tsk j'.

Hypothesis H_j'_sched : scheduled_at sched j' t.

Hypothesis H_j'_not_tsk : ~~ job_of_task tsk j'.

Hypothesis H_j'_sched : scheduled_at sched j' t.

We prove that then j incurs higher-or-equal priority
interference from another task iff j' has
higher-or-equal priority than j.

Lemma sched_at_implies_interference_athep_eq_hep :

is_interference_from_hep_job_from_another_task j t = hep_job j' j.

is_interference_from_hep_job_from_another_task j t = hep_job j' j.

Hence, if we assume that j' has higher-or-equal priority, ...

... we will be able to show that j incurs
higher-or-equal priority interference from another task.

Moreover, in this case, task tsk also incurs interference.

Lemma sched_athep_implies_task_interference :

∀ upp,

j \in arrivals_between arr_seq 0 upp →

task_interference_received_before arr_seq sched interference tsk upp t.

End FromDifferentTask.

∀ upp,

j \in arrivals_between arr_seq 0 upp →

task_interference_received_before arr_seq sched interference tsk upp t.

End FromDifferentTask.

Variable j' : Job.

Hypothesis H_j'_sched : scheduled_at sched j' t.

Hypothesis H_j'_lp : ~~ hep_job j' j.

Lemma sched_alp_implies_interference_ahep_false :

is_interference_from_another_hep_job j t = false.

End LowerPriority.

End ScheduledJob.

Hypothesis H_j'_sched : scheduled_at sched j' t.

Hypothesis H_j'_lp : ~~ hep_job j' j.

Lemma sched_alp_implies_interference_ahep_false :

is_interference_from_another_hep_job j t = false.

End LowerPriority.

End ScheduledJob.

We prove that we can split cumulative interference into two
parts: (1) cumulative priority inversion and (2) cumulative
interference from jobs with higher or equal priority.

Lemma cumulative_interference_split :

∀ j t1 t2,

cumulative_interference j t1 t2

= cumulative_priority_inversion j t1 t2

+ cumulative_interference_from_other_hep_jobs j t1 t2.

∀ j t1 t2,

cumulative_interference j t1 t2

= cumulative_priority_inversion j t1 t2

+ cumulative_interference_from_other_hep_jobs j t1 t2.

Similarly, we prove that we can split cumulative interfering
workload into two parts: (1) cumulative priority inversion and
(2) cumulative interfering workload from jobs with higher or
equal priority.

Lemma cumulative_interfering_workload_split :

∀ j t1 t2,

cumul_interfering_workload interfering_workload j t1 t2 =

cumulative_priority_inversion j t1 t2 + cumulative_interfering_workload_of_hep_jobs j t1 t2.

∀ j t1 t2,

cumul_interfering_workload interfering_workload j t1 t2 =

cumulative_priority_inversion j t1 t2 + cumulative_interfering_workload_of_hep_jobs j t1 t2.

Let j be any job of task tsk, and let upp_t be any time
instant after job j's arrival. Then for any time interval
lying before upp_t, the cumulative interference received by
tsk is equal to the sum of the cumulative priority inversion
of job j and the cumulative interference incurred by task
tsk due to other tasks.

Lemma cumulative_task_interference_split :

∀ j t1 t2 upp_t,

arrives_in arr_seq j →

job_of_task tsk j →

j \in arrivals_before arr_seq upp_t →

~~ job_completed_by j t2 →

cumulative_task_interference interference tsk upp_t t1 t2 =

cumulative_priority_inversion j t1 t2 +

cumulative_interference_from_hep_jobs_from_other_tasks j t1 t2.

∀ j t1 t2 upp_t,

arrives_in arr_seq j →

job_of_task tsk j →

j \in arrivals_before arr_seq upp_t →

~~ job_completed_by j t2 →

cumulative_task_interference interference tsk upp_t t1 t2 =

cumulative_priority_inversion j t1 t2 +

cumulative_interference_from_hep_jobs_from_other_tasks j t1 t2.

In this section we prove that the (abstract) cumulative interfering workload is equivalent to
conventional workload, i.e., the one defined with concrete schedule parameters.

Let

`[t1,t2)`

be any time interval.
Variable j : Job.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_of_tsk : job_of_task tsk j.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_of_tsk : job_of_task tsk j.

Then for any job j, the cumulative interfering workload is
equal to the conventional workload.

Lemma cumulative_iw_hep_eq_workload_of_ohep :

cumulative_interfering_workload_of_hep_jobs j t1 t2

= workload_of_other_hep_jobs j t1 t2.

End InstantiatedWorkloadEquivalence.

cumulative_interfering_workload_of_hep_jobs j t1 t2

= workload_of_other_hep_jobs j t1 t2.

End InstantiatedWorkloadEquivalence.

In this section we prove that the (abstract) cumulative interference of jobs with higher or
equal priority is equal to total service of jobs with higher or equal priority.

Variable j : Job.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_of_tsk : job_of_task tsk j.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_of_tsk : job_of_task tsk j.

We consider an arbitrary time interval

`[t1, t)`

that starts with a quiet time.
Then for any job j, the (abstract) instantiated function of interference is
equal to the total service of jobs with higher or equal priority.

Lemma cumulative_i_ohep_eq_service_of_ohep :

cumulative_interference_from_other_hep_jobs j t1 t

= service_of_other_hep_jobs j t1 t.

cumulative_interference_from_other_hep_jobs j t1 t

= service_of_other_hep_jobs j t1 t.

The same applies to the alternative definition of interference.

Lemma cumulative_i_thep_eq_service_of_othep :

cumulative_interference_from_hep_jobs_from_other_tasks j t1 t

= service_of_hep_jobs_from_other_tasks j t1 t.

End InstantiatedServiceEquivalences.

cumulative_interference_from_hep_jobs_from_other_tasks j t1 t

= service_of_hep_jobs_from_other_tasks j t1 t.

End InstantiatedServiceEquivalences.

In this section we prove that the abstract definition of busy interval is equivalent to
the conventional, concrete definition of busy interval for JLFP scheduling.

Consider any job j of tsk.

Variable j : Job.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_of_tsk : job_of_task tsk j.

Hypothesis H_job_cost_positive : job_cost_positive j.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_of_tsk : job_of_task tsk j.

Hypothesis H_job_cost_positive : job_cost_positive j.

To show the equivalence of the notions of busy intervals
we first show that the notions of quiet time are also
equivalent.

Lemma quiet_time_cl_implies_quiet_time_ab:

∀ t, quiet_time_cl j t → quiet_time_ab j t.

Lemma quiet_time_ab_implies_quiet_time_cl:

∀ t, quiet_time_ab j t → quiet_time_cl j t.

The equivalence trivially follows from the lemmas above.

Corollary instantiated_quiet_time_equivalent_quiet_time:

∀ t,

quiet_time_cl j t ↔ quiet_time_ab j t.

∀ t,

quiet_time_cl j t ↔ quiet_time_ab j t.

Based on that, we prove that the concept of busy interval obtained by instantiating the abstract
definition of busy interval coincides with the conventional definition of busy interval.

Lemma instantiated_busy_interval_equivalent_busy_interval:

∀ t1 t2,

busy_interval_cl j t1 t2 ↔ busy_interval_ab j t1 t2.

End BusyIntervalEquivalence.

End Equivalences.

∀ t1 t2,

busy_interval_cl j t1 t2 ↔ busy_interval_ab j t1 t2.

End BusyIntervalEquivalence.

End Equivalences.

In this section we prove some properties about the interference
and interfering workload as defined in this file.

Consider work-bearing readiness.

Context `{@JobReady Job (ideal.processor_state Job) _ _}.

Hypothesis H_work_bearing_readiness : work_bearing_readiness arr_seq sched.

Hypothesis H_work_bearing_readiness : work_bearing_readiness arr_seq sched.

Assume that the schedule is valid and work-conserving.

Note that we differentiate between abstract and classical
notions of work conserving schedule.

Let work_conserving_ab := definitions.work_conserving arr_seq sched interference interfering_workload.

Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.

Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.

We assume that the schedule is a work-conserving schedule in the

*classical*sense, and later prove that the hypothesis about abstract work-conservation also holds.
Assume the scheduling policy under consideration is reflexive.

In this section, we prove the correctness of interference
inside the busy interval, i.e., we prove that if interference
for a job is false then the job is scheduled and vice versa.
This property is referred to as abstract work conservation.

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

Variable j : Job.

Hypothesis H_arrives : arrives_in arr_seq j.

Hypothesis H_job_cost_positive : 0 < job_cost j.

Hypothesis H_arrives : arrives_in arr_seq j.

Hypothesis H_job_cost_positive : 0 < job_cost j.

Let the busy interval of the job be

`[t1,t2)`

.
Consider a time t inside the busy interval of the job.

Lemma scheduled_implies_no_interference :

scheduled_at sched j t → ¬ interference j t.

End Abstract_Work_Conservation.

scheduled_at sched j t → ¬ interference j t.

End Abstract_Work_Conservation.

Using the above two lemmas, we can prove that abstract work conservation
always holds for these instantiations of I and IW.

Next, in order to prove that these definitions of I and IW are consistent
with sequential tasks, we need to assume that the policy under consideration
respects sequential tasks.

We prove that these definitions of I and IW are consistent with sequential
tasks.

Lemma instantiated_interference_and_workload_consistent_with_sequential_tasks :

interference_and_workload_consistent_with_sequential_tasks

arr_seq sched tsk interference interfering_workload.

interference_and_workload_consistent_with_sequential_tasks

arr_seq sched tsk interference interfering_workload.

Since interfering and interfering workload are sufficient to define the busy window,
next, we reason about the bound on the length of the busy window.

Consider an arrival curve.

Consider a set of tasks that respects the arrival curve.

Variable ts : list Task.

Hypothesis H_taskset_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.

Hypothesis H_taskset_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.

Assume that all jobs come from this task set.

Consider a constant L such that...

... L is greater than 0, and...

L is the fixed point of the following equation.

Assume all jobs have a valid job cost.

Then, we prove that L is a bound on the length of the busy window.