...
  View open merge request
Commits (9)
......@@ -2,5 +2,5 @@
# See https://beyondgrep.com/ for details.
# Ignore misc files generated by the build process
--ignore-file=ext:glob,aux
--ignore-dir=html
\ No newline at end of file
--ignore-file=ext:glob,aux,d,conf,orig
--ignore-dir=html
Require Export prosa.behavior.ready.
Require Export prosa.analysis.definitions.schedule_prefix.
Require Export prosa.model.preemption.parameter.
(** * Properties of Readiness Models *)
(** In this file, we define commonsense properties of readiness models. *)
Section ReadinessModelProperties.
(** For any type of jobs with costs and arrival times... *)
Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
(** ... and any kind of processor model, ... *)
Context {PState: Type} `{ProcessorState Job PState}.
(** ... consider a notion of job readiness. *)
Variable ReadinessModel : JobReady Job PState.
(** First, we define a notion of non-clairvoyance for readiness
models. Intuitively, whether a job is ready or not should depend only on
the past (i.e., prior allocation decisions and job behavior), not on
future events. Formally, we say that the [ReadinessModel] is
non-clairvoyant if a job's readiness at a given time does not vary across
schedules with identical prefixes. That is, given two schedules [sched]
and [sched'], the predicates [job_ready sched j t] and [job_ready sched'
j t] may not differ if [sched] and [sched'] are identical prior to time
[t]. *)
Definition nonclairvoyant_readiness :=
forall sched sched' j h,
identical_prefix sched sched' h ->
forall t,
t <= h ->
job_ready sched j t = job_ready sched' j t.
(** Next, we relate the readiness model to the preemption model. *)
Context `{JobPreemptable Job}.
(** In a preemption-policy-compliant schedule, nonpreemptive jobs must remain
scheduled. Further, in a valid schedule, scheduled jobs must be
ready. Consequently, in a valid preemption-policy-compliant schedule, a
nonpreemptive job must remain ready until at least the end of its
nonpreemptive section. *)
Definition valid_nonpreemptive_readiness :=
forall sched j t,
~~ job_preemptable j (service sched j t) -> job_ready sched j t.
End ReadinessModelProperties.
Require Export prosa.behavior.ready.
(** We define the notion of prefix-equivalence of schedules. *)
Section PrefixDefinition.
(** For any type of jobs... *)
Context {Job : JobType}.
(** ... and any kind of processor model, ... *)
Context {PState: Type} `{ProcessorState Job PState}.
(** ... two schedules share an identical prefix if they are pointwise
identical (at least) up to a fixed horizon. *)
Definition identical_prefix (sched sched' : schedule PState) (horizon : instant) :=
forall t,
t < horizon ->
sched t = sched' t.
End PrefixDefinition.
......@@ -3,6 +3,37 @@ Require Export prosa.util.all.
(** * Arrival Sequence *)
(** First, we relate the stronger to the weaker arrival predicates. *)
Section ArrivalPredicates.
(** Consider any kinds of jobs with arrival times. *)
Context {Job : JobType} `{JobArrival Job}.
(** A job that arrives in some interval [[t1, t2)] certainly arrives before
time [t2]. *)
Lemma arrived_between_before:
forall j t1 t2,
arrived_between j t1 t2 ->
arrived_before j t2.
Proof.
move=> j t1 t2.
now rewrite /arrived_before /arrived_between => /andP [_ CLAIM].
Qed.
(** A job that arrives before a time [t] certainly has arrived by time
[t]. *)
Lemma arrived_before_has_arrived:
forall j t,
arrived_before j t ->
has_arrived j t.
Proof.
move=> j t.
rewrite /arrived_before /has_arrived.
now apply ltnW.
Qed.
End ArrivalPredicates.
(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
......@@ -51,6 +82,16 @@ Section Arrived.
by apply ready_implies_arrived.
Qed.
(** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
Corollary backlogged_implies_arrived:
forall j t,
backlogged sched j t -> has_arrived j t.
Proof.
rewrite /backlogged.
move=> j t /andP [READY _].
now apply ready_implies_arrived.
Qed.
End Arrived.
(** In this section, we establish useful facts about arrival sequence prefixes. *)
......@@ -199,4 +240,4 @@ Section ArrivalSequencePrefix.
End ArrivalTimes.
End ArrivalSequencePrefix.
\ No newline at end of file
End ArrivalSequencePrefix.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.facts.behavior.arrivals.
Require Export prosa.analysis.definitions.readiness.
(** In this file, we establish basic facts about backlogged jobs. *)
Section BackloggedJobs.
(** Consider any kind of jobs with arrival times and costs... *)
Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
(** ... and any kind of processor model, ... *)
Context {PState: Type} `{ProcessorState Job PState}.
(** ... and allow for any notion of job readiness. *)
Context `{JobReady Job PState}.
(** Given an arrival sequence and a schedule ... *)
Variable arr_seq : arrival_sequence Job.
Variable sched: schedule PState.
(** ... with consistent arrival times, ... *)
Hypothesis H_consistent_arrival_times:
consistent_arrival_times arr_seq.
(** ... we observe that any backlogged job is indeed in the set of backlogged
jobs. *)
Lemma mem_backlogged_jobs:
forall j t,
arrives_in arr_seq j ->
backlogged sched j t ->
j \in jobs_backlogged_at arr_seq sched t.
Proof.
move=> j t ARRIVES BACKLOGGED.
rewrite /jobs_backlogged_at /arrivals_up_to.
rewrite mem_filter.
apply /andP; split; first by exact.
apply arrived_between_implies_in_arrivals => //.
rewrite /arrived_between.
apply /andP; split => //.
rewrite ltnS -/(has_arrived _ _).
now apply (backlogged_implies_arrived sched).
Qed.
(** Trivially, it is also the case that any backlogged job comes from the
respective arrival sequence. *)
Lemma backlogged_job_arrives_in:
forall j t,
j \in jobs_backlogged_at arr_seq sched t ->
arrives_in arr_seq j.
Proof.
move=> j t.
rewrite /jobs_backlogged_at mem_filter => /andP [_ IN].
move: IN. rewrite /arrivals_up_to.
now apply in_arrivals_implies_arrived.
Qed.
End BackloggedJobs.
(** In the following section, we make one more crucial assumption: namely, that
the readiness model is non-clairvoyant, which allows us to relate
backlogged jobs in schedules with a shared prefix. *)
Section NonClairvoyance.
(** Consider any kind of jobs with arrival times and costs... *)
Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
(** ... any kind of processor model, ... *)
Context {PState: Type} `{ProcessorState Job PState}.
(** ... and allow for any non-clairvoyant notion of job readiness. *)
Context {RM : JobReady Job PState}.
Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and two schedules ... *)
Variable sched sched': schedule PState.
(** ... with a shared prefix to a fixed horizon. *)
Variable h : instant.
Hypothesis H_shared_prefix: identical_prefix sched sched' h.
(** We observe that a job is backlogged at a time in the prefix in one
schedule iff it is backlogged in the other schedule due to the
non-clairvoyance of the notion of job readiness ... *)
Lemma backlogged_prefix_invariance:
forall t j,
t < h ->
backlogged sched j t = backlogged sched' j t.
Proof.
move=> t j IN_PREFIX.
rewrite /backlogged.
rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //.
rewrite /scheduled_at H_shared_prefix //.
now apply ltnW.
Qed.
(** As a corollary, if we further know that j is not scheduled at time [h],
we can expand the previous lemma to [t <= h]. *)
Corollary backlogged_prefix_invariance':
forall t j,
~~ scheduled_at sched j t ->
~~ scheduled_at sched' j t ->
t <= h ->
backlogged sched j t = backlogged sched' j t.
Proof.
move=> t j NOT_SCHED NOT_SCHED'.
rewrite leq_eqVlt => /orP [/eqP EQ | LT]; last by apply backlogged_prefix_invariance.
rewrite /backlogged.
rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //;
last by rewrite EQ.
now rewrite NOT_SCHED NOT_SCHED'.
Qed.
(** ... and also lift this observation to the set of all backlogged jobs at
any given time in the shared prefix. *)
Lemma backlogged_jobs_prefix_invariance:
forall t,
t < h ->
jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t.
Proof.
move=> t IN_PREFIX.
rewrite /jobs_backlogged_at.
apply eq_filter.
rewrite /eqfun => j.
now apply backlogged_prefix_invariance.
Qed.
End NonClairvoyance.
......@@ -25,8 +25,16 @@ Section ReplaceAtFacts.
t'. *)
Let sched' := replace_at sched t' nstate.
(** We begin with the trivial observation that the schedule doesn't change at
other times. *)
(** We begin with the trivial observation that [replace_at sched t' nstate]
indeed returns [nstate] at time [t']. *)
Lemma replace_at_def:
sched' t' = nstate.
Proof.
rewrite /sched' /replace_at.
now apply ifT.
Qed.
(** Equally trivially, the schedule doesn't change at other times. *)
Lemma rest_of_schedule_invariant:
forall t, t <> t' -> sched' t = sched t.
Proof.
......
......@@ -10,7 +10,8 @@ do
FIND_OPTS+=( ! -path './classic/*' )
;;
--only-classic)
FIND_OPTS+=( ! -path './analysis/*' ! -path './behavior/*' ! -path './model/*' ! -path './results/*')
FIND_OPTS+=( ! -path './analysis/*' ! -path './behavior/*' ! -path './model/*' \
! -path './implementation/*' ! -path './results/*')
;;
*)
echo "Unrecognized option: $1"
......
Require Export prosa.model.preemption.parameter.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.readiness.backlogged.
Require Export prosa.analysis.transform.swap.
(** * Generic Ideal Uniprocessor Scheduler *)
(** In this file, we provide a generic priority-aware scheduler that produces
an ideal uniprocessor schedule for a given arrival sequence. The scheduler
respects nonpreemptive sections and arbitrary readiness models. *)
(** The following definitions assume ideal uniprocessor schedules. *)
Require prosa.model.processor.ideal.
Section UniprocessorSchedule.
(** Consider any type of jobs with costs and arrival times, ... *)
Context {Job : JobType} {JC: JobCost Job} {JA: JobArrival Job}.
(** ... any readiness model, ... *)
Context `{@JobReady Job (ideal.processor_state Job) (ideal.pstate_instance Job) JC JA}.
(** ... any preemption model, and ... *)
Context `{JobPreemptable Job}.
(** ... and any JLDP priority policy. *)
Context `{JLDP_policy Job}.
(** Suppose we are given an arrival sequence of such jobs. *)
Variable arr_seq : arrival_sequence Job.
(** In the following section, we define how the next job to be scheduled is
selected based on a finite schedule prefix. *)
Section JobAllocation.
(** Consider a finite schedule prefix ... *)
Variable sched_prefix : schedule (ideal.processor_state Job).
(** ... that is valid up to time [t - 1]. *)
Variable t : instant.
(** We define a predicate that tests whether the job scheduled at the
previous instant (if [t > 0]) is nonpreemptive (and hence needs to be
continued to be scheduled). *)
Definition prev_job_nonpreemptive : bool:=
match t with
| 0 => false
| S t' => if sched_prefix t' is Some j then
~~job_preemptable j (service sched_prefix j t)
else
false
end.
(** Based on the [prev_job_nonpreemptive] predicate, either the previous
job is continued to be scheduled or (one of) the highest-priority
backlogged (= pending and ready) jobs is selected. *)
Definition allocation_at: option Job :=
if prev_job_nonpreemptive then
sched_prefix t.-1
else
supremum (hep_job_at t) (jobs_backlogged_at arr_seq sched_prefix t).
End JobAllocation.
(** We construct the schedule step by step starting from an "empty" schedule
that is idle at all times as a base case. *)
Definition empty_schedule: schedule (ideal.processor_state Job) := fun _ => None.
(** Next, we define a function that computes a fine schedule prefix up to a
given time horizon [h]. *)
Fixpoint schedule_up_to (h : instant) : schedule (ideal.processor_state Job) :=
let
prefix := if h is S h' then schedule_up_to h' else empty_schedule
in
replace_at prefix h (allocation_at prefix h).
(** Finally, we define the ideal uniprocessor schedule as follows: for a
given point in time [t], we compute the finite prefix up to and including
[t], namely [schedule_up_to t], and then return the job scheduled at time
[t] in that prefix. *)
Definition uni_schedule (t : instant) : ideal.processor_state Job :=
schedule_up_to t t.
End UniprocessorSchedule.
This diff is collapsed.
......@@ -40,5 +40,11 @@ Section WorkConserving.
backlogged sched j t ->
exists j_other, scheduled_at sched j_other t.
(** Related to this, we define the set of all jobs that are backlogged at a
given time [t], i.e., the set of jobs that could be scheduled, and which
a work-conserving scheduler must hence consider. *)
Definition jobs_backlogged_at (t : instant): seq Job :=
[seq j <- arrivals_up_to arr_seq t | backlogged sched j t].
End WorkConserving.
......@@ -49,3 +49,5 @@ bursty
TODO
mathcomp
hyperperiod
pointwise
notational