# Library prosa.analysis.facts.model.ideal.schedule

Require Export prosa.util.all.

Require Export prosa.model.processor.platform_properties.

Require Export prosa.analysis.facts.behavior.service.

Require Import prosa.model.processor.ideal.

Require Export prosa.model.processor.platform_properties.

Require Export prosa.analysis.facts.behavior.service.

Require Import prosa.model.processor.ideal.

Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances.
In this section we establish the classes to which an ideal schedule belongs.

We assume ideal uni-processor schedules.

Consider any job type and the ideal processor model.

We note that the ideal processor model is indeed a uni-processor
model.

By definition, service_in is the sum of the service received
in total across all cores. In the ideal uniprocessor model,
however, there is only one "core," which is expressed by using
unit as the type of cores. The type unit only has a single
member tt, which serves as a placeholder. Consequently, the
definition of service_in simplifies to a single term of the
sum, the service on the one core, which we note with the
following lemma that relates service_in to service_on.

Furthermore, since the ideal uniprocessor state is represented
by the option Job type, service_in further simplifies to a
simple equality comparison, which we note next.

We observe that the ideal processor model falls into the category
of ideal-progress models, i.e., a scheduled job always receives
service.

The ideal processor model is a unit-service model.

Lemma ideal_proc_model_provides_unit_service:

unit_service_proc_model (processor_state Job).

Lemma scheduled_in_def (j : Job) s :

scheduled_in j s = (s == Some j).

Lemma scheduled_at_def sched (j : Job) t :

scheduled_at sched j t = (sched t == Some j).

Lemma service_in_is_scheduled_in (j : Job) s :

service_in j s = scheduled_in j s.

Lemma service_at_is_scheduled_at sched (j : Job) t :

service_at sched j t = scheduled_at sched j t.

Lemma service_on_def (j : Job) (s : processor_state Job) c :

service_on j s c = (s == Some j).

Lemma service_at_def sched (j : Job) t :

service_at sched j t = (sched t == Some j).

unit_service_proc_model (processor_state Job).

Lemma scheduled_in_def (j : Job) s :

scheduled_in j s = (s == Some j).

Lemma scheduled_at_def sched (j : Job) t :

scheduled_at sched j t = (sched t == Some j).

Lemma service_in_is_scheduled_in (j : Job) s :

service_in j s = scheduled_in j s.

Lemma service_at_is_scheduled_at sched (j : Job) t :

service_at sched j t = scheduled_at sched j t.

Lemma service_on_def (j : Job) (s : processor_state Job) c :

service_on j s c = (s == Some j).

Lemma service_at_def sched (j : Job) t :

service_at sched j t = (sched t == Some j).

Next we prove a lemma which helps us to do a case analysis on
the state of an ideal schedule.

Lemma ideal_proc_model_sched_case_analysis:

∀ (sched : schedule (ideal.processor_state Job)) (t : instant),

is_idle sched t ∨ ∃ j, scheduled_at sched j t.

∀ (sched : schedule (ideal.processor_state Job)) (t : instant),

is_idle sched t ∨ ∃ j, scheduled_at sched j t.

On a similar note, if a scheduler is idle at a time instant t,
then no job can receive service at t.

Lemma ideal_not_idle_implies_sched sched (j : Job) t :

is_idle sched t →

service_at sched j t = 0.

End ScheduleClass.

is_idle sched t →

service_at sched j t = 0.

End ScheduleClass.

# Incremental Service in Ideal Schedule

In the following section we prove a few facts about service in ideal schedule.
(* Note that these lemmas can be generalized to an arbitrary scheduler. *)

Section IncrementalService.

Section IncrementalService.

Consider any job type, ...

... any arrival sequence, ...

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

As a base case, we prove that if a job j receives service in
some time interval

`[t1,t2)`

, then there exists a time instant
`t ∈ [t1,t2)`

such that j is scheduled at time t and t is
the first instant where j receives service.
Lemma positive_service_during:

∀ j t1 t2,

0 < service_during sched j t1 t2 →

∃ t : nat, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = 0.

∀ j t1 t2,

0 < service_during sched j t1 t2 →

∃ t : nat, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = 0.

Furthermore, we observe that, if a job receives some positive
amount of service during an interval

`[t1, t2)`

, then the
interval can't be empty and hence t1 < t2.
Next, we prove that if in some time interval

`[t1,t2)`

a job j
receives k units of service, then there exists a time instant
`t ∈ [t1,t2)`

such that j is scheduled at time t and service
of job j within interval `[t1,t)`

is equal to k.
Lemma incremental_service_during:

∀ j t1 t2 k,

service_during sched j t1 t2 > k →

∃ t, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = k.

End IncrementalService.

∀ j t1 t2 k,

service_during sched j t1 t2 > k →

∃ t, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = k.

End IncrementalService.

# Automation

We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically.
Global Hint Resolve ideal_proc_model_is_a_uniprocessor_model

ideal_proc_model_ensures_ideal_progress

ideal_proc_model_provides_unit_service : basic_rt_facts.

ideal_proc_model_ensures_ideal_progress

ideal_proc_model_provides_unit_service : basic_rt_facts.

We also provide tactics for case analysis on ideal processor state.
The first tactic generates two sub-goals: one with idle processor and
the other with processor executing a job named JobName.

Ltac ideal_proc_model_sched_case_analysis sched t JobName :=

let Idle := fresh "Idle" in

let Sched := fresh "Sched_" JobName in

destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].

let Idle := fresh "Idle" in

let Sched := fresh "Sched_" JobName in

destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].

The second tactic is similar to the first, but it additionally generates
two equalities: sched t = None and sched t = Some j.

Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=

let Idle := fresh "Idle" in

let IdleEq := fresh "Eq" Idle in

let Sched := fresh "Sched_" JobName in

let SchedEq := fresh "Eq" Sched in

destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];

[move: (Idle) ⇒ /eqP IdleEq; rewrite ?IdleEq

| move: (Sched); simpl; move ⇒ /eqP SchedEq; rewrite ?SchedEq].

let Idle := fresh "Idle" in

let IdleEq := fresh "Eq" Idle in

let Sched := fresh "Sched_" JobName in

let SchedEq := fresh "Eq" Sched in

destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];

[move: (Idle) ⇒ /eqP IdleEq; rewrite ?IdleEq

| move: (Sched); simpl; move ⇒ /eqP SchedEq; rewrite ?SchedEq].