Commit 49036f00 authored by Sergey Bozhko's avatar Sergey Bozhko

Improve readability of analysis

parent 5fc2e7dd
......@@ -59,11 +59,11 @@ Section BusyIntervalJLFP.
End BusyInterval.
(** In this section we define the computational
version of the notion of quiet time. *)
version of the notion of quiet time. *)
Section DecidableQuietTime.
(** We say that t is a quiet time for j iff every higher-priority job from
the arrival sequence that arrived before t has completed by that time. *)
the arrival sequence that arrived before t has completed by that time. *)
Definition quiet_time_dec (j : Job) (t : instant) :=
all
(fun j_hp => hep_job j_hp j ==> (completed_by sched j_hp t))
......
Require Export prosa.behavior.all.
From mathcomp Require Export eqtype ssrnat.
(** In this section, we introduce properties of a job. *)
Section PropertiesOfJob.
......
Require Export prosa.analysis.definitions.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** * Cumulative Priority Inversion for JLFP-models *)
(** In this module we define the notion of cumulative priority inversion for uni-processor for JLFP schedulers. *)
Section CumulativePriorityInversion.
......
......@@ -6,6 +6,7 @@ Require Export prosa.analysis.facts.behavior.service.
conversely a notion of a lack of progress. *)
Section Progress.
(** Consider any type of jobs with a known cost... *)
Context {Job : JobType}.
Context `{JobCost Job}.
......
......@@ -6,8 +6,6 @@ Require Export prosa.model.priority.classes.
could be generalized in future work. *)
Require Import prosa.analysis.facts.model.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Request Bound Function (RBF) *)
(** We define the notion of a task's request-bound function (RBF), as well as
......@@ -47,7 +45,8 @@ Section TaskWorkloadBoundedByArrivalCurves.
Variable delta : duration.
(** We define the following workload bound for the task. *)
Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.
Definition task_request_bound_function :=
task_cost tsk * max_arrivals tsk delta.
End SingleTask.
......
Require Export prosa.analysis.facts.behavior.completion.
Require Import prosa.model.task.absolute_deadline.
(** * Schedulability *)
(** In the following section we define the notion of schedulable
task. *)
Section Task.
(** Consider any type of tasks, ... *)
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
(** ... any type of jobs associated with these tasks, ... *)
Context {Job: JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobTask Job Task}.
(** ... and any kind of processor state. *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
......@@ -37,43 +47,27 @@ Section Task.
arrives_in arr_seq j ->
job_task j = tsk ->
job_meets_deadline sched j.
End Task.
Section TaskSet.
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Variable ts : {set Task}.
(** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(** ...and any schedule of these jobs. *)
Variable sched: schedule PState.
(** We say that a task set is schedulable if all its tasks are schedulable *)
Definition schedulable_taskset :=
forall tsk, tsk \in ts -> schedulable_task arr_seq sched tsk.
End TaskSet.
Section Schedulability.
(** We can infer schedulability from a response-time bound of a task. *)
(** In this section we infer schedulability from a response-time bound
of a task. *)
Section Schedulability.
(** Consider any type of tasks, ... *)
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{TaskDeadline Task}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
(** ... any type of jobs associated with these tasks, ... *)
Context {Job: JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
(** ... and any kind of processor state. *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
......@@ -112,9 +106,12 @@ End Schedulability.
given schedule and one w.r.t. all jobs that arrive in a given
arrival sequence. *)
Section AllDeadlinesMet.
(** Consider any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
(** ... any given type of processor states. *)
Context {PState: eqType}.
......@@ -151,8 +148,8 @@ Section AllDeadlinesMet.
End DeadlinesOfArrivals.
(** We observe that the latter definition, assuming a schedule in
which all jobs come from the arrival sequence, implies the former
definition. *)
which all jobs come from the arrival sequence, implies the
former definition. *)
Lemma all_deadlines_met_in_valid_schedule:
forall arr_seq sched,
jobs_come_from_arrival_sequence sched arr_seq ->
......
Require Export prosa.model.task.concept.
Require Export prosa.model.processor.ideal.
(** Due to historical reasons this file defines the notion of a schedule of
a task for the ideal uni-processor model. This is not a fundamental limitation
and the notion can be further generalized to an arbitrary model. *)
(** Due to historical reasons this file defines the notion of a
schedule of a task for the ideal uni-processor model. This is not
a fundamental limitation and the notion can be further generalized
to an arbitrary model. *)
Require Export prosa.model.processor.ideal.
(** * Schedule of task *)
(** In this section we define properties of schedule of a task *)
......@@ -22,29 +23,25 @@ Section ScheduleOfTask.
(** Let [sched] be any ideal uni-processor schedule. *)
Variable sched : schedule (ideal.processor_state Job).
Section TaskProperties.
(** Let [tsk] be any task. *)
Variable tsk : Task.
(** Next we define whether a task is scheduled at time [t], ... *)
Definition task_scheduled_at (t : instant) :=
if sched t is Some j then
job_task j == tsk
else false.
(** Let [tsk] be any task. *)
Variable tsk : Task.
(** Next we define whether a task is scheduled at time [t], ... *)
Definition task_scheduled_at (t : instant) :=
if sched t is Some j then
job_task j == tsk
else false.
(** ...which also corresponds to the instantaneous service it receives. *)
Definition task_service_at (t : instant) := task_scheduled_at t.
(** ...which also corresponds to the instantaneous service it receives. *)
Definition task_service_at (t : instant) := task_scheduled_at t.
(** Based on the notion of instantaneous service, we define the
(** Based on the notion of instantaneous service, we define the
cumulative service received by [tsk] during any interval [t1, t2)... *)
Definition task_service_during (t1 t2 : instant) :=
\sum_(t1 <= t < t2) task_service_at t.
Definition task_service_during (t1 t2 : instant) :=
\sum_(t1 <= t < t2) task_service_at t.
(** ...and the cumulative service received by [tsk] up to time t2,
(** ...and the cumulative service received by [tsk] up to time t2,
i.e., in the interval [0, t2). *)
Definition task_service (t2 : instant) := task_service_during 0 t2.
End TaskProperties.
Definition task_service (t2 : instant) := task_service_during 0 t2.
End ScheduleOfTask.
Require Export prosa.behavior.all.
Require Export prosa.util.all.
(** * Arrival Sequence *)
(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
......@@ -11,8 +13,8 @@ Section Arrived.
(** Consider any schedule... *)
Variable sched : schedule PState.
(** ...and suppose that jobs have a cost, an arrival time, and a notion of
readiness. *)
(** ...and suppose that jobs have a cost, an arrival time, and a
notion of readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobReady Job PState}.
......@@ -61,144 +63,140 @@ Section ArrivalSequencePrefix.
(** Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
(** In this section, we prove some lemmas about arrival sequence prefixes. *)
Section Lemmas.
(** We begin with basic lemmas for manipulating the sequences. *)
Section Composition.
(** We begin with basic lemmas for manipulating the sequences. *)
Section Composition.
(** First, we show that the set of arriving jobs can be split
(** First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma arrivals_between_cat:
forall t1 t t2,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
Proof.
unfold arrivals_between; intros t1 t t2 GE LE.
by rewrite (@big_cat_nat _ _ _ t).
Qed.
(** Second, the same observation applies to membership in the set of
Lemma arrivals_between_cat:
forall t1 t t2,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
Proof.
unfold arrivals_between; intros t1 t t2 GE LE.
by rewrite (@big_cat_nat _ _ _ t).
Qed.
(** Second, the same observation applies to membership in the set of
arrived jobs. *)
Lemma arrivals_between_mem_cat:
forall j t1 t t2,
t1 <= t ->
t <= t2 ->
j \in arrivals_between arr_seq t1 t2 =
(j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
Proof.
by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
Qed.
(** Third, we observe that we can grow the considered interval without
Lemma arrivals_between_mem_cat:
forall j t1 t t2,
t1 <= t ->
t <= t2 ->
j \in arrivals_between arr_seq t1 t2 =
(j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
Proof.
by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
Qed.
(** Third, we observe that we can grow the considered interval without
"losing" any arrived jobs, i.e., membership in the set of arrived jobs
is monotonic. *)
Lemma arrivals_between_sub:
forall j t1 t1' t2 t2',
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'.
Proof.
intros j t1 t1' t2 t2' GE1 LE2 IN.
move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
last by rewrite /arrivals_between big_geq // in IN.
rewrite /arrivals_between.
rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
rewrite mem_cat; apply/orP; right.
rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done].
by rewrite mem_cat; apply/orP; left.
Qed.
End Composition.
(** Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes.
(** Assume that job arrival times are consistent. *)
Hypothesis H_consistent_arrival_times:
consistent_arrival_times arr_seq.
(** First, we prove that if a job belongs to the prefix
Lemma arrivals_between_sub:
forall j t1 t1' t2 t2',
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'.
Proof.
intros j t1 t1' t2 t2' GE1 LE2 IN.
move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
last by rewrite /arrivals_between big_geq // in IN.
rewrite /arrivals_between.
rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
rewrite mem_cat; apply/orP; right.
rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done].
by rewrite mem_cat; apply/orP; left.
Qed.
End Composition.
(** Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes.
(** Assume that job arrival times are consistent. *)
Hypothesis H_consistent_arrival_times:
consistent_arrival_times arr_seq.
(** First, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
Lemma in_arrivals_implies_arrived:
forall j t1 t2,
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j.
Proof.
rename H_consistent_arrival_times into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN => [arr [IN _]].
by exists arr.
Qed.
(** Next, we prove that if a job belongs to the prefix
Lemma in_arrivals_implies_arrived:
forall j t1 t2,
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j.
Proof.
rename H_consistent_arrival_times into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN => [arr [IN _]].
by exists arr.
Qed.
(** Next, we prove that if a job belongs to the prefix
(jobs_arrived_between t1 t2), then it indeed arrives between t1 and
t2. *)
Lemma in_arrivals_implies_arrived_between:
forall j t1 t2,
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2.
Proof.
rename H_consistent_arrival_times into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN => [t0 [IN /= LT]].
by apply CONS in IN; rewrite /arrived_between IN.
Qed.
(** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
Lemma in_arrivals_implies_arrived_between:
forall j t1 t2,
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2.
Proof.
rename H_consistent_arrival_times into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN => [t0 [IN /= LT]].
by apply CONS in IN; rewrite /arrived_between IN.
Qed.
(** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
then it indeed arrives before time t. *)
Lemma in_arrivals_implies_arrived_before:
forall j t,
j \in arrivals_before arr_seq t ->
arrived_before j t.
Proof.
intros j t IN.
have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
by rewrite /arrived_between /=.
Qed.
(** Similarly, we prove that if a job from the arrival sequence arrives
Lemma in_arrivals_implies_arrived_before:
forall j t,
j \in arrivals_before arr_seq t ->
arrived_before j t.
Proof.
intros j t IN.
have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
by rewrite /arrived_between /=.
Qed.
(** Similarly, we prove that if a job from the arrival sequence arrives
before t, then it belongs to the sequence (jobs_arrived_before t). *)
Lemma arrived_between_implies_in_arrivals:
forall j t1 t2,
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2.
Proof.
rename H_consistent_arrival_times into CONS.
move => j t1 t2 [a_j ARRj] BEFORE.
have SAME := ARRj; apply CONS in SAME; subst a_j.
by apply mem_bigcat_nat with (j := (job_arrival j)).
Qed.
(** Next, we prove that if the arrival sequence doesn't contain duplicate
Lemma arrived_between_implies_in_arrivals:
forall j t1 t2,
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2.
Proof.
rename H_consistent_arrival_times into CONS.
move => j t1 t2 [a_j ARRj] BEFORE.
have SAME := ARRj; apply CONS in SAME; subst a_j.
by apply mem_bigcat_nat with (j := (job_arrival j)).
Qed.
(** Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq ->
forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
Proof.
rename H_consistent_arrival_times into CONS.
unfold arrivals_up_to; intros SET t1 t2.
apply bigcat_nat_uniq; first by done.
intros x t t' IN1 IN2.
by apply CONS in IN1; apply CONS in IN2; subst.
Qed.
(** Also note there can't by any arrivals in an empty time interval. *)
Lemma arrivals_between_geq:
forall t1 t2,
t1 >= t2 ->
arrivals_between arr_seq t1 t2 = [::].
Proof.
by intros ? ? GE; rewrite /arrivals_between big_geq.
Qed.
End ArrivalTimes.
End Lemmas.
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq ->
forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
Proof.
rename H_consistent_arrival_times into CONS.
unfold arrivals_up_to; intros SET t1 t2.
apply bigcat_nat_uniq; first by done.
intros x t t' IN1 IN2.
by apply CONS in IN1; apply CONS in IN2; subst.
Qed.
(** Also note there can't by any arrivals in an empty time interval. *)
Lemma arrivals_between_geq:
forall t1 t2,
t1 >= t2 ->
arrivals_between arr_seq t1 t2 = [::].
Proof.
by intros ? ? GE; rewrite /arrivals_between big_geq.
Qed.
End ArrivalTimes.
End ArrivalSequencePrefix.
\ No newline at end of file
Require Export prosa.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.behavior.arrivals.
(** In this file, we establish basic facts about job completions. *)
(** * Completion *)
(** In this file, we establish basic facts about job completions. *)
Section CompletionFacts.
(** Consider any job type,...*)
Context {Job: JobType}.
Context `{JobCost Job}.
......@@ -35,8 +37,7 @@ Section CompletionFacts.
Lemma less_service_than_cost_is_incomplete:
forall t,
service sched j t < job_cost j
<->
~~ completed_by sched j t.
<-> ~~ completed_by sched j t.
Proof.
move=> t. by split; rewrite /completed_by; [rewrite -ltnNge // | rewrite ltnNge //].
Qed.
......@@ -45,8 +46,7 @@ Section CompletionFacts.
Lemma incomplete_is_positive_remaining_cost:
forall t,
~~ completed_by sched j t
<->
remaining_cost sched j t > 0.
<-> remaining_cost sched j t > 0.
Proof.
move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
Qed.
......@@ -112,11 +112,10 @@ Section CompletionFacts.
End CompletionFacts.
Section ServiceAndCompletionFacts.
(** In this section, we establish some facts that are really about service,
but are also related to completion and rely on some of the above lemmas.
Hence they are in this file rather than in the service facts file. *)
(** In this section, we establish some facts that are really about service,
but are also related to completion and rely on some of the above lemmas.
Hence they are in this file rather than in the service facts file. *)
Section ServiceAndCompletionFacts.
(** Consider any job type,...*)
Context {Job: JobType}.
......@@ -133,7 +132,7 @@ Section ServiceAndCompletionFacts.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute sched.
(** Let j be any job that is to be scheduled. *)
(** Let [j] be any job that is to be scheduled. *)
Variable j: Job.
(** Assume that a scheduled job receives exactly one time unit of service. *)
......@@ -171,7 +170,7 @@ Section ServiceAndCompletionFacts.
by apply service_at_most_cost.
Qed.
(** We show that the service received by job j in any interval is no larger
(** We show that the service received by job [j] in any interval is no larger
than its cost. *)
Lemma cumulative_service_le_job_cost:
forall t t',
......@@ -183,8 +182,8 @@ Section ServiceAndCompletionFacts.
rewrite /service. rewrite -(service_during_cat sched j 0 t t') // leq_addl //.
Qed.
(** If a job isn't complete at time t, it can't be completed at time (t +
remaining_cost j t - 1). *)
(** If a job isn't complete at time [t], it can't be completed at time [t +
remaining_cost j t - 1]. *)
Lemma job_doesnt_complete_before_remaining_cost:
forall t,
~~ completed_by sched j t ->
......@@ -227,9 +226,9 @@ Section ServiceAndCompletionFacts.
End ServiceAndCompletionFacts.
(** In this section, we establish facts that on jobs with non-zero costs that
must arrive to execute. *)
Section PositiveCost.
(** In this section, we establish facts that on jobs with non-zero costs that
must arrive to execute. *)
(** Consider any type of jobs with cost and arrival-time attributes,...*)
Context {Job: JobType}.
......@@ -243,11 +242,11 @@ Section PositiveCost.
(** ...and a given schedule. *)
Variable sched: schedule PState.
(** Let j be any job that is to be scheduled. *)
(** Let [j] be any job that is to be scheduled. *)
Variable j: Job.
(** We assume that job j has positive cost, from which we can