Skip to content
Snippets Groups Projects
Commit 5cb12571 authored by Kimaya Bedarkar's avatar Kimaya Bedarkar
Browse files

removed assumption job_of_task and restructured proofs

parent 4c867396
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
analysis/facts/model/rbf.v
+ 115
− 103
View file @ 5cb12571
......@@ -54,39 +54,21 @@ Section ProofWorkloadBound.
Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
Let total_rbf := total_request_bound_function ts.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
(** Next, we consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
(** Next, we say that two jobs [j1] and [j2] are in relation
[other_higher_eq_priority], iff [j1] has higher or equal priority than [j2] and
is produced by a different task. *)
Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
(** Next, we recall the notions of total workload of jobs... *)
Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).
(** ...notions of workload of higher or equal priority jobs... *)
Let total_hep_workload t1 t2 :=
workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
(** ... workload of other higher or equal priority jobs... *)
Let total_ohep_workload t1 t2 :=
workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
(** ... and the workload of jobs of the same task as job j. *)
Let task_workload t1 t2 :=
workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).
workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).
(** In this section we prove that the workload of any jobs is
no larger than the request bound function. *)
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
Let total_rbf := total_request_bound_function ts.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
(** In this section, we prove that the workload of any jobs is
no larger than the request bound function. *)
Section WorkloadIsBoundedByRBF.
(** Consider any time t and any interval of length delta. *)
......@@ -99,95 +81,37 @@ Section ProofWorkloadBound.
task_workload t (t + delta)
<= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta).
Proof.
rewrite /task_workload /workload_of_jobs/ number_of_task_arrivals /task_arrivals_between -big_filter /job_of_task.
rewrite // /number_of_task_arrivals -sum1_size big_distrr /= big_filter.
rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs.
rewrite /same_task -H_job_of_tsk muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.
by apply H_valid_job_cost.
destruct (task_arrivals_between arr_seq tsk t (t + delta)) eqn: TASK; unfold task_arrivals_between in TASK.
{ by rewrite -big_filter !TASK !big_nil. }
{ rewrite big_filter.
rewrite big_seq_cond.
rewrite [in X in _ <= X]big_seq_cond.
apply leq_sum.
move => j' /andP [IN TSKj'].
rewrite muln1.
unfold arrivals_have_valid_job_costs, valid_job_cost in H_valid_job_cost.
move : TSKj' => /eqP TSKj'.
rewrite -TSKj'.
apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN. }
Qed.
(** As a corollary, we prove that workload of task is no larger the than
task request bound function. *)
Corollary task_workload_le_task_rbf:
task_workload t (t + delta) <= task_rbf delta.
Proof.
apply leq_trans with
(task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta));
(task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta));
first by apply task_workload_le_num_of_arrivals_times_cost.
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
by apply H_is_arrival_bound; last rewrite leq_addr.
Qed.
(** Next, we prove that total workload of other tasks with higher-or-equal
priority is no larger than the total request bound function. *)
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
Proof.
set l := arrivals_between arr_seq t (t + delta).
apply leq_trans with
(\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{ intros.
rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk && (job_task x != tsk)).
rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
apply leq_sum; move => j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with
(task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
{ rewrite -sum1_size big_distrr /= big_filter.
rewrite /workload_of_jobs.
rewrite muln1 /l /arrivals_between /arrival_sequence.arrivals_between.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
}
{ rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
by apply H_is_arrival_bound; last rewrite leq_addr.
}
Qed.
(** Next, we prove that total workload of tasks with higher-or-equal
priority is no larger than the total request bound function. *)
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) <= total_hep_rbf delta.
Proof.
set l := arrivals_between arr_seq t (t + delta).
apply leq_trans with
(n := \sum_(tsk' <- ts | hep_task tsk' tsk)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{ rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk).
rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
apply leq_sum; move => j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with
(task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
{ rewrite -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{ rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
by apply H_is_arrival_bound; last rewrite leq_addr.
}
by apply H_is_arrival_bound; last rewrite leq_addr.
Qed.
(** Next, we prove that total workload of tasks is no larger than the total
request bound function. *)
Lemma total_workload_le_total_rbf'':
......@@ -224,6 +148,94 @@ Section ProofWorkloadBound.
}
Qed.
(** Next, we consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
(** We say that two jobs [j1] and [j2] are in relation
[other_higher_eq_priority], iff [j1] has higher or equal priority than [j2] and
is produced by a different task. *)
Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
(** Recall the notion of workload of higher or equal priority jobs... *)
Let total_hep_workload t1 t2 :=
workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
(** ... and, workload of other higher or equal priority jobs. *)
Let total_ohep_workload t1 t2 :=
workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
(** We prove that total workload of other tasks with higher-or-equal
priority is no larger than the total request bound function. *)
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
Proof.
set l := arrivals_between arr_seq t (t + delta).
apply leq_trans with
(\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{ intros.
rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk && (job_task x != tsk)).
rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
apply leq_sum; move => j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with
(task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
{ rewrite -sum1_size big_distrr /= big_filter.
rewrite /workload_of_jobs.
rewrite muln1 /l /arrivals_between /arrival_sequence.arrivals_between.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
}
{ rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
by apply H_is_arrival_bound; last rewrite leq_addr.
}
Qed.
(** Next, we prove that total workload of tasks with higher-or-equal
priority is no larger than the total request bound function. *)
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) <= total_hep_rbf delta.
Proof.
set l := arrivals_between arr_seq t (t + delta).
apply leq_trans with
(n := \sum_(tsk' <- ts | hep_task tsk' tsk)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{ rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk).
rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
apply leq_sum; move => j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with
(task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
{ rewrite -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{ rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
by apply H_is_arrival_bound; last rewrite leq_addr.
}
Qed.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
......
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