# Library prosa.implementation.facts.ideal_uni.preemption_aware

Require Export prosa.implementation.facts.generic_schedule.

Require Export prosa.implementation.definitions.ideal_uni_scheduler.

Require Export prosa.analysis.facts.model.ideal.schedule.

Require Export prosa.model.schedule.limited_preemptive.

Require Export prosa.implementation.definitions.ideal_uni_scheduler.

Require Export prosa.analysis.facts.model.ideal.schedule.

Require Export prosa.model.schedule.limited_preemptive.

# Properties of the Preemption-Aware Ideal Uniprocessor Scheduler

Consider any type of jobs with costs and arrival times, ...

... in the context of an ideal uniprocessor model.

Suppose we are given a consistent arrival sequence of such jobs, ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.

Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.

... a non-clairvoyant readiness model, ...

Context {RM: JobReady Job (ideal.processor_state Job)}.

Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

... and a preemption model.

For any given job selection policy ...

... consider the schedule produced by the preemption-aware scheduler for
the policy induced by choose_job.

Let schedule := pmc_uni_schedule arr_seq choose_job.

Let policy := allocation_at arr_seq choose_job.

Let policy := allocation_at arr_seq choose_job.

To begin with, we establish that the preemption-aware scheduler does not
induce non-work-conserving behavior.

If choose_job does not voluntarily idle the processor, ...

... then we can establish work-conservation.
First, we observe that allocation_at yields idle_state only if there are
no backlogged jobs.

Lemma allocation_at_idle:

∀ sched t,

allocation_at arr_seq choose_job sched t = idle_state →

jobs_backlogged_at arr_seq sched t = [::].

∀ sched t,

allocation_at arr_seq choose_job sched t = idle_state →

jobs_backlogged_at arr_seq sched t = [::].

As a stepping stone, we observe that the generated schedule is idle at
a time t only if there are no backlogged jobs.

Lemma idle_schedule_no_backlogged_jobs:

∀ t,

is_idle schedule t →

jobs_backlogged_at arr_seq schedule t = [::].

∀ t,

is_idle schedule t →

jobs_backlogged_at arr_seq schedule t = [::].

From the preceding fact, we conclude that the generated schedule is
indeed work-conserving.

The next result establishes that the generated preemption-model-aware
schedule is structurally valid, meaning all jobs stem from the arrival
sequence and only ready jobs are scheduled.

First, any reasonable job selection policy will not create jobs "out
of thin air," i.e., if a job is selected, it was among those given
to choose from.

Second, for the schedule to be valid, we require the notion of readiness
to be consistent with the preemption model: a non-preemptive job remains
ready until (at least) the end of its current non-preemptive section.

Finally, we assume the readiness model to be non-clairvoyant.

For notational convenience, recall the definition of a prefix of the
schedule based on which the next decision is made.

Let sched_prefix t :=

if t is t'.+1 then schedule_up_to policy None t' else empty_schedule idle_state.

if t is t'.+1 then schedule_up_to policy None t' else empty_schedule idle_state.

We begin by showing that any job in the schedule must come from the arrival
sequence used to generate it.

Next, we show that any job selected by the job selection policy must
be ready.

Theorem chosen_job_is_ready:

∀ j t,

choose_job t (jobs_backlogged_at arr_seq (sched_prefix t) t) == Some j →

job_ready schedule j t.

∀ j t,

choose_job t (jobs_backlogged_at arr_seq (sched_prefix t) t) == Some j →

job_ready schedule j t.

Starting from the previous result we show that, at any instant, only
a ready job can be scheduled.

Finally, we show that the generated schedule is valid.

Next, we observe that the resulting schedule is consistent with the
definition of "preemption times".

For notational convenience, recall the definition of a prefix of the
schedule based on which the next decision is made.

Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.

First, we observe that non-preemptive jobs remain scheduled as long as
they are non-preemptive.

Lemma np_job_remains_scheduled:

∀ t,

prev_job_nonpreemptive (prefix t) t →

schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1.

∀ t,

prev_job_nonpreemptive (prefix t) t →

schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1.

From this, we conclude that the predicate used to determine whether the
previously scheduled job is nonpreemptive in the computation of
np_uni_schedule is consistent with the existing notion of a
preemption_time.

Lemma np_consistent:

∀ t,

prev_job_nonpreemptive (prefix t) t →

~~ preemption_time schedule t.

End PreemptionTimes.

∀ t,

prev_job_nonpreemptive (prefix t) t →

~~ preemption_time schedule t.

End PreemptionTimes.

Finally, we establish the main feature: the generated schedule respects
the preemption-model semantics.

As a minimal validity requirement (which is a part of
valid_preemption_model), we require that any job in arr_seq must
start execution to become nonpreemptive.

Hypothesis H_valid_preemption_function :

∀ j,

arrives_in arr_seq j →

job_cannot_become_nonpreemptive_before_execution j.

∀ j,

arrives_in arr_seq j →

job_cannot_become_nonpreemptive_before_execution j.

Second, for the schedule to be valid, we require the notion of readiness
to be consistent with the preemption model: a non-preemptive job remains
ready until (at least) the end of its current non-preemptive section.

Given such a valid preemption model, we establish that the generated
schedule indeed respects the preemption model semantics.