Skip to content
GitLab
Commit dfe95431 authored by Felix Stutz's avatar Felix Stutz
Browse files

Commented, splitted workload

parent 14cb2cfe
Expand all Hide whitespace changes
Inline Side-by-side
Makefile
View file @ dfe95431
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_jitter.v workload.v
# coq_makefile bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_fp.v workload_guan.v workload_jitter.v workload.v
#
.DEFAULT_GOAL := all
......@@ -103,6 +103,8 @@ VFILES:=bertogna_edf_comp.v\
util_divround.v\
util_lemmas.v\
Vbase.v\
workload_fp.v\
workload_guan.v\
workload_jitter.v\
workload.v
......
bertogna_edf_comp.v
View file @ dfe95431
Require Import Vbase schedule bertogna_edf_theory util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path
workload_fp.
Module ResponseTimeIterationEDF.
Import Schedule ResponseTimeAnalysisEDF.
Import Schedule ResponseTimeAnalysisEDF WorkloadBoundFP.
Section Analysis.
......
bertogna_edf_theory.v
View file @ dfe95431
Require Import Vbase task job task_arrival schedule platform
workload schedulability priority response_time
workload workload_fp schedulability priority response_time
bertogna_fp_theory util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDF.
Export Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime Priority SporadicTaskArrival ResponseTimeAnalysis.
Export Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime Priority SporadicTaskArrival ResponseTimeAnalysis WorkloadBoundFP.
Section InterferenceBoundEDF.
......
bertogna_fp_comp.v
View file @ dfe95431
Require Import Vbase schedule bertogna_fp_theory util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path
workload_fp.
Module ResponseTimeIterationFP.
Import Schedule ResponseTimeAnalysis.
Import Schedule ResponseTimeAnalysis WorkloadBoundFP.
Section Analysis.
......
bertogna_fp_theory.v
View file @ dfe95431
Require Import Vbase task job task_arrival schedule platform workload
Require Import Vbase task job task_arrival schedule platform workload workload_fp
schedulability priority response_time interference
util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeAnalysis.
Export Job SporadicTaskset Schedule Workload Interference Platform Schedulability ResponseTime Priority SporadicTaskArrival.
Export Job SporadicTaskset Schedule Workload Interference Platform Schedulability ResponseTime Priority SporadicTaskArrival WorkloadBoundFP.
Section InterferenceBoundFP.
......
guan_fp_comp.v
View file @ dfe95431
Require Import Vbase job task schedule task_arrival priority workload_jitter
guan_fp_theory util_divround util_lemmas
workload_guan guan_fp_theory util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeIterationFPGuan.
Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisGuan.
Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisGuan WorkloadBoundGuan.
Section Analysis.
......
guan_fp_theory.v
View file @ dfe95431
Require Import Vbase task job task_arrival schedule platform workload
bertogna_fp_theory schedulability priority interference
platform response_time util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
workload_guan bertogna_fp_theory schedulability priority interference
platform response_time util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeAnalysisGuan.
Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival Interference Platform.
Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival Interference Platform WorkloadBoundGuan.
Export Workload ResponseTimeAnalysis.
Section InterferenceBoundGuan.
......
job.v
View file @ dfe95431
......@@ -2,6 +2,8 @@ Require Import task util_lemmas ssrnat ssrbool eqtype.
Module Job.
(*We define valid parameters for different types of jobs ...*)
(*...for a job*)
Section ValidJob.
Context {Job: eqType}.
......@@ -13,6 +15,7 @@ Module Job.
End ValidJob.
(*... for a real time job (with a deadline) ...*)
Section ValidRealtimeJob.
Context {Job: eqType}.
......@@ -31,6 +34,7 @@ Module Job.
End ValidRealtimeJob.
(* ... for a job of a sporadic task ...*)
Section ValidSporadicTaskJob.
Context {sporadic_task: eqType}.
......@@ -56,6 +60,7 @@ Module Job.
End ValidSporadicTaskJob.
(*... for a job of a sporadic task with jitter ...*)
Section ValidSporadicTaskJobWithJitter.
Context {sporadic_task: eqType}.
......
platform.v
View file @ dfe95431
......@@ -69,7 +69,8 @@ Module Platform.
Hypothesis H_invariant_holds :
JLFP_JLDP_scheduling_invariant_holds.
(* The job which is interfering has higher or equal priority to the interfered one. *)
Lemma interfering_job_has_higher_eq_prio :
forall j j_other t,
backlogged job_cost rate sched j t ->
......@@ -103,11 +104,14 @@ Module Platform.
by rewrite ltnn in BUG.
Qed.
(* Assume all jobs are from the taskset ... *)
Hypothesis all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
(* ... and jobs from the same task don't execute in parallel. *)
Hypothesis no_intra_task_parallelism:
jobs_of_same_task_dont_execute_in_parallel job_task sched.
(* If a job isn't scheduled, the processor are busy with interfering tasks. *)
Lemma cpus_busy_with_interfering_tasks :
forall (j: JobIn arr_seq) tsk t,
job_task j = tsk ->
......
priority.v
View file @ dfe95431
......@@ -74,11 +74,12 @@ Module Priority.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
(* Rate-Monotonic and Deadline-Monotonic priority order *)
(* Rate-Monotonic and Deadline-Monotonic as priority order *)
Definition RM (tsk1 tsk2: sporadic_task) := task_period tsk1 <= task_period tsk2.
Definition DM (tsk1 tsk2: sporadic_task) := task_deadline tsk1 <= task_deadline tsk2.
(* Rate-Montonic is a valid FP policy. *)
Lemma rm_is_valid : valid_fp_policy RM.
Proof.
unfold valid_fp_policy, fp_is_reflexive, fp_is_transitive, RM;
......@@ -88,6 +89,7 @@ Module Priority.
[by left | by right; apply ltnW].
Qed.
(* Deadline-Monotonic is a valid FP policy. *)
Lemma dm_is_valid : valid_fp_policy DM.
Proof.
unfold valid_fp_policy, fp_is_reflexive, fp_is_transitive, DM;
......@@ -106,11 +108,13 @@ Module Priority.
Variable job_task: Job -> sporadic_task.
Variable arr_seq: arrival_sequence Job.
Variable num_cpus: nat.
(* We define a function to get from FP to JLDP policy. *)
Definition fp_to_jldp (task_hp: fp_policy sporadic_task) : jldp_policy arr_seq :=
fun (t: time) (jhigh jlow: JobIn arr_seq) =>
task_hp (job_task jhigh) (job_task jlow).
(* With this function, from a valid FP policy comes a valid JLDP policy. *)
Lemma valid_fp_is_valid_jldp :
forall task_hp (FP: valid_fp_policy task_hp),
valid_jldp_policy (fp_to_jldp task_hp).
......
response_time.v
View file @ dfe95431
......@@ -65,6 +65,7 @@ Module ResponseTime.
Hypothesis response_time_bound:
job_has_completed_by j (job_arrival j + R).
(* The service at any time t' after the response time is 0. *)
Lemma service_at_after_job_rt_zero :
forall t',
t' >= job_arrival j + R ->
......@@ -85,6 +86,7 @@ Module ResponseTime.
by rewrite big_nat_recr // /=; apply leq_addl.
Qed.
(* The cumulative service after the response time is 0. *)
Lemma sum_service_after_job_rt_zero :
forall t' t'',
t' >= job_arrival j + R ->
......@@ -112,7 +114,8 @@ Module ResponseTime.
Variable j: JobIn arr_seq.
Hypothesis H_job_of_task: job_task j = tsk.
(* The service at any time t' after the response time is 0. *)
Lemma service_at_after_rt_zero :
forall t',
t' >= job_arrival j + R ->
......@@ -121,6 +124,7 @@ Module ResponseTime.
by ins; apply service_at_after_job_rt_zero with (R := R); [apply response_time_bound |].
Qed.
(* The cumulative service after the response time is 0. *)
Lemma sum_service_after_rt_zero :
forall t' t'',
t' >= job_arrival j + R ->
......@@ -130,86 +134,7 @@ Module ResponseTime.
Qed.
End AllJobs.
(*Section CostAsLowerBound.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_rate_at_most_one :
forall j cpu, rate j cpu <= 1.
Lemma response_time_ge_cost : R >= job_cost j.
Proof.
rename response_time_bound into BOUND.
unfold is_response_time_bound_of_task, job_has_completed_by, completed,
jobs_must_arrive_to_execute in *.
specialize (BOUND j H_job_of_task).
move: BOUND => /eqP BOUND; rewrite -BOUND.
apply leq_trans with (n := service_during rate sched j
(job_arrival j) (job_arrival j + R)).
unfold service; rewrite -> big_cat_nat with (n := job_arrival j);
[by rewrite sum_service_before_arrival // leqnn | by ins | by apply leq_addr].
unfold service_during.
apply leq_trans with (n := \sum_(job_arrival j <= t < job_arrival j + R) 1);
last by rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA // subnn addn0 leqnn.
by apply leq_sum; ins; by apply service_at_le_max_rate.
Qed.
End CostAsLowerBound.*)
End BasicLemmas.
(*Section LowerBoundOfResponseTimeBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
Context {arr_seq: arrival_sequence Job}.
(* Consider any task with at least one job that arrives in this set. *)
Variable tsk: sporadic_task.
Hypothesis job_of_tsk_exists:
exists j: JobIn arr_seq, job_task j = tsk.
(* And assume any valid schedule...*)
Context {num_cpus : nat}.
Variable sched: schedule num_cpus arr_seq.
Variable rate: Job -> processor num_cpus -> nat.
(*... that satisfies the following properties: *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_rate_at_most_one:
forall j cpu, rate j cpu <= 1.
(* ..., and assume that, for any job cost function, R is a
response-time bound of tsk in this schedule. *)
Variable R: time.
Hypothesis response_time_bound:
forall job_cost,
is_response_time_bound_of_task job_cost job_task tsk rate sched R.
(* Then, R cannot be less than the cost of tsk. *)
Lemma response_time_ub_ge_task_cost:
R >= task_cost tsk.
Proof.
unfold job_has_completed_by, completed in *.
rename job_of_tsk_exists into EX; des.
set new_cost := fun (j': Job) => task_cost (job_task j').
apply leq_trans with (n := new_cost j);
first by unfold new_cost; rewrite EX.
by exploit (response_time_ge_cost new_cost job_task tsk sched rate R);
by ins; apply EX.
Qed.
End LowerBoundOfResponseTimeBound.*)
End ResponseTime.
\ No newline at end of file
schedulability.v
View file @ dfe95431
......@@ -20,6 +20,7 @@ Module Schedulability.
Variable j: JobIn arr_seq.
(* Job won't miss its deadline if it is completed by its arrival time plus its (relative) deadline. *)
Definition job_misses_no_deadline :=
completed job_cost rate sched j (job_arrival j + job_deadline j).
......@@ -37,11 +38,13 @@ Module Schedulability.
Variable ts: taskset_of sporadic_task.
Variable tsk: sporadic_task.
(* A task doesn't miss its deadline iff all of its jobs don't miss their deadline. *)
Definition task_misses_no_deadline :=
forall (j: JobIn arr_seq),
job_task j == tsk ->
job_misses_no_deadline rate sched j.
(* Whether a task misses a deadline before a particular time. *)
Definition task_misses_no_deadline_before (t': time) :=
forall (j: JobIn arr_seq),
job_task j == tsk ->
......
schedule.v
View file @ dfe95431
......@@ -5,6 +5,7 @@ Definition time := nat.
Module ArrivalSequence.
(*We define an arrival sequence as a mapping from natural number t to a sequence of jobs*)
Section ArrivalSequenceDef.
Variable Job: eqType. (* Assume any job type with decidable equality *)
......@@ -108,13 +109,13 @@ Module Schedule.
Section ScheduledJobs.
Context {Job: eqType}. (* Assume a job type with decidable equality... *)
Context {Job: eqType}. (* Assume a job type with decidable equality,... *)
Context {arr_seq: arrival_sequence Job}.
Variable job_cost: Job -> nat. (* ...and a cost function. *)
Variable job_cost: Job -> nat. (* ...a cost function, ... *)
Context {num_cpus: nat}.
Variable rate: Job -> processor num_cpus -> nat.
Variable rate: Job -> processor num_cpus -> nat. (*...and a specific rate for each processor *)
Variable sched: schedule num_cpus arr_seq.
Variable j: JobIn arr_seq.
......@@ -123,9 +124,11 @@ Module Schedule.
Definition scheduled (t: time) :=
[exists cpu in 'I_(num_cpus), sched cpu t == Some j].
(* Whether a processor is idle *)
Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
sched cpu t = None.
(* Define the service as rate of the processor the job is scheduled on. *)
Definition service_at (t: time) :=
\sum_(cpu < num_cpus | sched cpu t == Some j) rate j cpu.
......@@ -160,6 +163,7 @@ Module Schedule.
End ScheduledJobs.
(* Let's define how valid schedules can look like. *)
Section ValidSchedules.
Context {Job: eqType}. (* Assume a job type with decidable equality *)
......@@ -184,6 +188,8 @@ Module Schedule.
Definition completed_jobs_dont_execute :=
forall j t, service rate sched j t <= job_cost j.
(* In a valid sporadic schedule, jobs have to be arrived before they executed
and in case they completed, they don't execute any more. *)
Definition valid_sporadic_schedule :=
jobs_must_arrive_to_execute /\ completed_jobs_dont_execute.
......@@ -203,6 +209,7 @@ Module Schedule.
Section Basic.
(* If a job is not scheduled, it won't get service. *)
Lemma not_scheduled_no_service :
forall t,
~~ scheduled sched j t -> service_at rate sched j t = 0.
......@@ -218,6 +225,8 @@ Module Schedule.
by move: SCHED => /eqP SCHED; rewrite SCHED eq_refl.
Qed.
(* If the service during a time interval isn't 0, there will be
a time t in this interval where the service isn't 0. *)
Lemma job_scheduled_during_interval :
forall t1 t2,
service_during rate sched j t1 t2 != 0 ->
......@@ -248,12 +257,16 @@ Module Schedule.
Section MaxRate.
Variable max_rate: nat.
(* There has to be a maximum rate for all processors. *)
Hypothesis there_is_max_rate:
forall j cpu, rate j cpu <= max_rate.
(* One job won't be executed on more than one processor at the same time. *)
Hypothesis no_parallelism:
jobs_dont_execute_in_parallel sched.
(* Service received by jobs is always less than or equal to the maximum rate. *)
Lemma service_at_le_max_rate :
forall t, service_at rate sched j t <= max_rate.
Proof.
......@@ -285,9 +298,12 @@ Module Schedule.
Hypothesis completed_jobs:
completed_jobs_dont_execute job_cost rate sched.
(* Let the rate on each processor be at most 1. *)
Hypothesis max_service_one:
forall j' t, service_at rate sched j' t <= 1.
(* Let the service interval be the interval a job is getting service during.
Then the length of the service interval is less than or equal to the cost of the job. *)
Lemma service_interval_le_cost :
forall t t',
service_during rate sched j t t' <= job_cost j.
......@@ -302,6 +318,7 @@ Module Schedule.
[by apply leq_addl | by ins | by rewrite leqNgt negbT //].
Qed.
(* If a job is completed at time t, it will be completed at every time t' which is later than t. *)
Lemma completion_monotonic :
forall t t',
t <= t' ->
......@@ -322,6 +339,7 @@ Module Schedule.
Hypothesis jobs_must_arrive:
jobs_must_arrive_to_execute sched.
(* The service received by a job at any time t before its arrival time is 0. ... *)
Lemma service_before_arrival_zero :
forall t0 (LT: t0 < job_arrival j),
service_at rate sched j t0 = 0.
......@@ -338,6 +356,7 @@ Module Schedule.
by exploit (ARR i); [by ins | ins]; destruct (sched i t0 == Some j).
Qed.
(* ... That's why the sum of service received by a job before its arrival time is 0, as well. *)
Lemma sum_service_before_arrival :
forall t1 t2 (LT: t2 <= job_arrival j),
\sum_(t1 <= i < t2) service_at rate sched j i = 0.
......@@ -351,6 +370,7 @@ Module Schedule.
by apply leq_trans with (n := t2); ins.
Qed.
(* Hence, you can ignore the service received by a job before its arrival time. *)
Lemma service_before_arrival_eq_service_during :
forall t0 t (LT: t0 <= job_arrival j),
\sum_(t0 <= t < job_arrival j + t) service_at rate sched j t =
......@@ -382,6 +402,7 @@ Module ScheduleOfSporadicTask.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Whether jobs of the same task can't execute in parallel. *)
Definition jobs_of_same_task_dont_execute_in_parallel :=
forall (j j': JobIn arr_seq) t,
job_task j = job_task j' ->
......@@ -415,6 +436,7 @@ Module ScheduleOfTaskWithJitter.
Section BasicLemmas.
(* The arrival time has to be before the jitter *)
Lemma arrival_before_jitter :
jobs_execute_after_jitter ->
jobs_must_arrive_to_execute sched.
......
task.v
View file @ dfe95431
Require Import Vbase util_lemmas ssrnat ssrbool eqtype fintype seq.
Module SporadicTask.
(* Next we define valid parameters for a sporadic task*)
Section BasicTask.
Context {Task: eqType}.
Variable task_cost: Task -> nat.
......@@ -25,29 +25,14 @@ Module SporadicTask.
End BasicTask.
(*Section TaskWithJitter.
Variable sporadic_task_with_jitter: eqType.
Variable task_cost: sporadic_task_with_jitter -> nat.
Variable task_period: sporadic_task_with_jitter -> nat.
Variable task_deadline: sporadic_task_with_jitter -> nat.
Variable task_jitter: sporadic_task_with_jitter -> nat.
Section ValidParameters.
Variable tsk: sporadic_task_with_jitter.
(*...*)
End ValidParameters.
End TaskWithJitter.*)
End SporadicTask.
Module SporadicTaskset.
Export SporadicTask.
(* In this section we define a task set as a sequence of tasks. *)
Section TasksetDefs.
(* Define task set as a sequence of sporadic tasks. *)
Definition taskset_of (T: eqType) := seq T.
Section TasksetProperties.
......
task_arrival.v
View file @ dfe95431
......@@ -14,21 +14,12 @@ Import SporadicTaskset Schedule.
Variable arr_seq: arrival_sequence Job.
Variable job_task: Job -> sporadic_task.
(* TODO: The definition of periodic is wrong. Only the closest
job has arrives period units later. *)
(*Definition periodic_task_model :=
forall j j',
j <> j' -> (* Given two different jobs j and j' such that *)
job_task j = job_task j' -> (* they are from the same task *)
job_arrival j <= job_arrival j' -> (* and arr <= arr' *)
(* then the next jobs arrives 'period' time units later. *)
job_arrival j' = job_arrival j' + task_period (job_task j).*)
(* We define the sporadic task model *)
Definition sporadic_task_model :=
forall (j j': JobIn arr_seq),
j <> j' -> (* Given two different jobs j and j' such that *)
job_task j = job_task j' -> (* they are from the same task *)
job_arrival j <= job_arrival j' -> (* and arr <= arr' *)
j <> j' -> (* Given two different jobs j and j' such that ... *)
job_task j = job_task j' -> (* ...they are from the same task ... *)
job_arrival j <= job_arrival j' -> (* ...and arr <= arr'... *)
(* then the next jobs arrives 'period' time units later. *)
job_arrival j' >= job_arrival j + task_period (job_task j).
......
workload.v
View file @ dfe95431
This diff is collapsed.
workload_fp.v 0 → 100644
View file @ dfe95431
This diff is collapsed.
workload_guan.v 0 → 100644
View file @ dfe95431
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment