Commit a5393afb authored by Björn Brandenburg's avatar Björn Brandenburg

cleanup the restructured model

improve comments, fix names, move some stuff around
parent d64ab1d1
...@@ -38,8 +38,8 @@ Section Abstract_RTA. ...@@ -38,8 +38,8 @@ Section Abstract_RTA.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched. Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *) (** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_job_cost_le_task_cost: Hypothesis H_valid_job_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. arrivals_have_valid_job_costs arr_seq.
(** Consider a task set ts... *) (** Consider a task set ts... *)
Variable ts : list Task. Variable ts : list Task.
...@@ -402,7 +402,7 @@ Section Abstract_RTA. ...@@ -402,7 +402,7 @@ Section Abstract_RTA.
rewrite addnBA; last by apply PRT1. rewrite addnBA; last by apply PRT1.
rewrite subh1; last by done. rewrite subh1; last by done.
rewrite leq_sub2r // leq_add2l. rewrite leq_sub2r // leq_add2l.
by rewrite -H_job_of_tsk; apply H_job_cost_le_task_cost. by rewrite -H_job_of_tsk; apply H_valid_job_cost.
} }
Qed. Qed.
......
...@@ -45,8 +45,8 @@ Section Sequential_Abstract_RTA. ...@@ -45,8 +45,8 @@ Section Sequential_Abstract_RTA.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched. Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *) (** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_job_cost_le_task_cost: Hypothesis H_valid_job_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. arrivals_have_valid_job_costs arr_seq.
(** Consider an arbitrary task set. *) (** Consider an arbitrary task set. *)
Variable ts : list Task. Variable ts : list Task.
...@@ -611,7 +611,7 @@ Section Sequential_Abstract_RTA. ...@@ -611,7 +611,7 @@ Section Sequential_Abstract_RTA.
rewrite mulnDr mulnC muln1 -addnBA // subnn addn0 mulnC. rewrite mulnDr mulnC muln1 -addnBA // subnn addn0 mulnC.
apply sum_majorant_constant. apply sum_majorant_constant.
move => j' ARR' /eqP TSK2. move => j' ARR' /eqP TSK2.
by rewrite -TSK2; apply H_job_cost_le_task_cost; exists (t1 + A); apply rem_in in ARR'. by rewrite -TSK2; apply H_valid_job_cost; exists (t1 + A); apply rem_in in ARR'.
Qed. Qed.
(** Finally, we use the lemmas above to obtain the bound on (** Finally, we use the lemmas above to obtain the bound on
......
...@@ -36,7 +36,7 @@ Section AbstractRTARunToCompletionThreshold. ...@@ -36,7 +36,7 @@ Section AbstractRTARunToCompletionThreshold.
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
(** Assume that the job costs are no larger than the task costs. *) (** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. Hypothesis H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq.
(** Let [tsk] be any task that is to be analyzed. *) (** Let [tsk] be any task that is to be analyzed. *)
Variable tsk : Task. Variable tsk : Task.
......
Require Export rt.restructuring.model.arrival.arrival_curves. Require Export rt.restructuring.model.task.arrival.curves.
Require Export rt.restructuring.model.priority.classes. Require Export rt.restructuring.model.priority.classes.
(** The following definitions assume ideal uni-processor schedules. This (** The following definitions assume ideal uni-processor schedules. This
......
Require Export rt.restructuring.model.aggregate.task_arrivals. Require Export rt.restructuring.model.task.arrivals.
(** In this file we provide basic properties related to tasks on arrival sequences. *) (** In this file we provide basic properties related to tasks on arrival sequences. *)
Section TaskArrivals. Section TaskArrivals.
......
...@@ -29,8 +29,8 @@ Section ModelWithLimitedPreemptions. ...@@ -29,8 +29,8 @@ Section ModelWithLimitedPreemptions.
(** Next, consider any limited ideal uni-processor schedule of this arrival sequence ... *) (** Next, consider any limited ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_valid_schedule_with_limited_preemptions: Hypothesis H_schedule_respects_preemption_model:
valid_schedule_with_limited_preemptions arr_seq sched. schedule_respects_preemption_model arr_seq sched.
(** ...where jobs do not execute after their completion. *) (** ...where jobs do not execute after their completion. *)
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched. Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
...@@ -204,7 +204,7 @@ Section ModelWithLimitedPreemptions. ...@@ -204,7 +204,7 @@ Section ModelWithLimitedPreemptions.
intros j ARR; repeat split. intros j ARR; repeat split.
{ by apply zero_in_preemption_points. } { by apply zero_in_preemption_points. }
{ by apply job_cost_in_nonpreemptive_points. } { by apply job_cost_in_nonpreemptive_points. }
{ by move => t NPP; apply H_valid_schedule_with_limited_preemptions. } { by move => t NPP; apply H_schedule_respects_preemption_model. }
{ intros t NSCHED SCHED. { intros t NSCHED SCHED.
have SERV: service sched j t = service sched j t.+1. have SERV: service sched j t = service sched j t.+1.
{ rewrite -[service sched j t]addn0 /service /service_during; apply/eqP. { rewrite -[service sched j t]addn0 /service /service_during; apply/eqP.
...@@ -215,7 +215,7 @@ Section ModelWithLimitedPreemptions. ...@@ -215,7 +215,7 @@ Section ModelWithLimitedPreemptions.
rewrite -[job_preemptable _ _]Bool.negb_involutive. rewrite -[job_preemptable _ _]Bool.negb_involutive.
apply/negP; intros CONTR. apply/negP; intros CONTR.
move: NSCHED => /negP NSCHED; apply: NSCHED. move: NSCHED => /negP NSCHED; apply: NSCHED.
apply H_valid_schedule_with_limited_preemptions; first by done. apply H_schedule_respects_preemption_model; first by done.
by rewrite SERV. by rewrite SERV.
} }
Qed. Qed.
......
...@@ -24,7 +24,7 @@ Section FullyNonPreemptiveModel. ...@@ -24,7 +24,7 @@ Section FullyNonPreemptiveModel.
(** Next, consider any non-preemptive ideal uniprocessor schedule of (** Next, consider any non-preemptive ideal uniprocessor schedule of
this arrival sequence ... *) this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched. Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
(** ... where jobs do not execute before their arrival or after completion. *) (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
......
...@@ -22,8 +22,8 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions. ...@@ -22,8 +22,8 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
Variable arr_seq : arrival_sequence Job. Variable arr_seq : arrival_sequence Job.
(** Assume that a job cost cannot be larger than a task cost. *) (** Assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_job_cost_le_task_cost: Hypothesis H_valid_job_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. arrivals_have_valid_job_costs arr_seq.
(** Then, we prove that [task_run_to_completion_threshold] function (** Then, we prove that [task_run_to_completion_threshold] function
defines a valid task's run to completion threshold. *) defines a valid task's run to completion threshold. *)
...@@ -31,10 +31,10 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions. ...@@ -31,10 +31,10 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
forall tsk, valid_task_run_to_completion_threshold arr_seq tsk. forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.
Proof. Proof.
intros; split. intros; split.
- by rewrite /task_run_to_completion_threshold_le_task_cost. - by rewrite /task_rtc_bounded_by_cost.
- intros j ARR TSK. - intros j ARR TSK.
apply leq_trans with (job_cost j); eauto 2 with basic_facts. apply leq_trans with (job_cost j); eauto 2 with basic_facts.
by rewrite-TSK; apply H_job_cost_le_task_cost. by rewrite-TSK; apply H_valid_job_cost.
Qed. Qed.
End TaskRTCThresholdFloatingNonPreemptiveRegions. End TaskRTCThresholdFloatingNonPreemptiveRegions.
......
...@@ -28,8 +28,8 @@ Section TaskRTCThresholdLimitedPreemptions. ...@@ -28,8 +28,8 @@ Section TaskRTCThresholdLimitedPreemptions.
(** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *) (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_valid_schedule_with_limited_preemptions: Hypothesis H_schedule_respects_preemption_model:
valid_schedule_with_limited_preemptions arr_seq sched. schedule_respects_preemption_model arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *) (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
...@@ -39,8 +39,8 @@ Section TaskRTCThresholdLimitedPreemptions. ...@@ -39,8 +39,8 @@ Section TaskRTCThresholdLimitedPreemptions.
Variable ts : seq Task. Variable ts : seq Task.
(** Assume that a job cost cannot be larger than a task cost. *) (** Assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_job_cost_le_task_cost: Hypothesis H_valid_job_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. arrivals_have_valid_job_costs arr_seq.
(** Consider the model with fixed preemption points. I.e., each task (** Consider the model with fixed preemption points. I.e., each task
is divided into a number of non-preemptive segments by inserting is divided into a number of non-preemptive segments by inserting
...@@ -97,7 +97,7 @@ Section TaskRTCThresholdLimitedPreemptions. ...@@ -97,7 +97,7 @@ Section TaskRTCThresholdLimitedPreemptions.
Lemma limited_valid_task_run_to_completion_threshold: Lemma limited_valid_task_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk. valid_task_run_to_completion_threshold arr_seq tsk.
Proof. Proof.
split; first by rewrite /task_run_to_completion_threshold_le_task_cost leq_subr. split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
intros ? ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT]. intros ? ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT].
move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]]. move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
rewrite /job_run_to_completion_threshold /task_run_to_completion_threshold /limited_preemptions rewrite /job_run_to_completion_threshold /task_run_to_completion_threshold /limited_preemptions
...@@ -106,7 +106,7 @@ Section TaskRTCThresholdLimitedPreemptions. ...@@ -106,7 +106,7 @@ Section TaskRTCThresholdLimitedPreemptions.
have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
by eapply job_last_nonpreemptive_segment_positive; eauto using valid_fixed_preemption_points_model_lemma. by eapply job_last_nonpreemptive_segment_positive; eauto using valid_fixed_preemption_points_model_lemma.
have T_RTCT__pos : 0 < task_last_nonpr_segment tsk. have T_RTCT__pos : 0 < task_last_nonpr_segment tsk.
{ unfold lengths_of_task_segments_bound_length_of_job_segments, task_last_nonpr_segment in *. { unfold job_respects_segment_lengths, task_last_nonpr_segment in *.
rewrite last0_nth; apply T6; eauto 2. rewrite last0_nth; apply T6; eauto 2.
have F: 1 <= size (distances (task_preemption_points tsk)). have F: 1 <= size (distances (task_preemption_points tsk)).
{ apply leq_trans with (size (task_preemption_points tsk) - 1). { apply leq_trans with (size (task_preemption_points tsk) - 1).
......
...@@ -28,7 +28,7 @@ Section TaskRTCThresholdFullyNonPreemptive. ...@@ -28,7 +28,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
(** Next, consider any ideal non-preemptive uniprocessor schedule of (** Next, consider any ideal non-preemptive uniprocessor schedule of
this arrival sequence ... *) this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched. Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
(** ... where jobs do not execute before their arrival or after completion. *) (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
...@@ -70,7 +70,7 @@ Section TaskRTCThresholdFullyNonPreemptive. ...@@ -70,7 +70,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
valid_task_run_to_completion_threshold arr_seq tsk. valid_task_run_to_completion_threshold arr_seq tsk.
Proof. Proof.
intros; split. intros; split.
- by unfold task_run_to_completion_threshold_le_task_cost. - by unfold task_rtc_bounded_by_cost.
- intros j ARR TSK. - intros j ARR TSK.
rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive. rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
edestruct (posnP (job_cost j)) as [ZERO|POS]. edestruct (posnP (job_cost j)) as [ZERO|POS].
......
...@@ -21,8 +21,8 @@ Section TaskRTCThresholdFullyPreemptiveModel. ...@@ -21,8 +21,8 @@ Section TaskRTCThresholdFullyPreemptiveModel.
Variable arr_seq : arrival_sequence Job. Variable arr_seq : arrival_sequence Job.
(** ... and assume that a job cost cannot be larger than a task cost. *) (** ... and assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_job_cost_le_task_cost: Hypothesis H_valid_job_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. arrivals_have_valid_job_costs arr_seq.
(** Then, we prove that [task_run_to_completion_threshold] function (** Then, we prove that [task_run_to_completion_threshold] function
defines a valid task's run to completion threshold. *) defines a valid task's run to completion threshold. *)
...@@ -30,10 +30,10 @@ Section TaskRTCThresholdFullyPreemptiveModel. ...@@ -30,10 +30,10 @@ Section TaskRTCThresholdFullyPreemptiveModel.
forall tsk, valid_task_run_to_completion_threshold arr_seq tsk. forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.
Proof. Proof.
intros; split. intros; split.
- by rewrite /task_run_to_completion_threshold_le_task_cost. - by rewrite /task_rtc_bounded_by_cost.
- intros j ARR TSK. - intros j ARR TSK.
apply leq_trans with (job_cost j); eauto 2 with basic_facts. apply leq_trans with (job_cost j); eauto 2 with basic_facts.
by rewrite-TSK; apply H_job_cost_le_task_cost. by rewrite-TSK; apply H_valid_job_cost.
Qed. Qed.
End TaskRTCThresholdFullyPreemptiveModel. End TaskRTCThresholdFullyPreemptiveModel.
......
...@@ -37,7 +37,7 @@ Section FloatingNonPreemptiveRegionsModel. ...@@ -37,7 +37,7 @@ Section FloatingNonPreemptiveRegionsModel.
of this arrival sequence ... *) of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_preemption_aware_schedule: Hypothesis H_preemption_aware_schedule:
valid_schedule_with_limited_preemptions arr_seq sched. schedule_respects_preemption_model arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *) (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
...@@ -58,7 +58,7 @@ Section FloatingNonPreemptiveRegionsModel. ...@@ -58,7 +58,7 @@ Section FloatingNonPreemptiveRegionsModel.
move: (H_valid_model_with_floating_nonpreemptive_regions) => LIM; move: LIM (LIM) => [LIM L] [[BEG [END NDEC]] MAX]. move: (H_valid_model_with_floating_nonpreemptive_regions) => LIM; move: LIM (LIM) => [LIM L] [[BEG [END NDEC]] MAX].
case: (posnP (job_cost j)) => [ZERO|POS]. case: (posnP (job_cost j)) => [ZERO|POS].
- split. - split.
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl. /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2. rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE]. + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
......
...@@ -31,8 +31,8 @@ Section LimitedPreemptionsModel. ...@@ -31,8 +31,8 @@ Section LimitedPreemptionsModel.
(** Next, consider any ideal uni-processor preemption-aware schedule (** Next, consider any ideal uni-processor preemption-aware schedule
of this arrival sequence ... *) of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_valid_schedule_with_limited_preemptions: Hypothesis H_schedule_respects_preemption_model:
valid_schedule_with_limited_preemptions arr_seq sched. schedule_respects_preemption_model arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *) (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
...@@ -57,14 +57,14 @@ Section LimitedPreemptionsModel. ...@@ -57,14 +57,14 @@ Section LimitedPreemptionsModel.
move: (LIM) => [BEG [END NDEC]]; move: (FIX) => [A1 [A2 [A3 [A4 A5]]]]. move: (LIM) => [BEG [END NDEC]]; move: (FIX) => [A1 [A2 [A3 [A4 A5]]]].
case: (posnP (job_cost j)) => [ZERO|POS]. case: (posnP (job_cost j)) => [ZERO|POS].
- split. - split.
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl. /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2. rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE]. + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
exists 0; rewrite LE; split; first by apply/andP; split. exists 0; rewrite LE; split; first by apply/andP; split.
by eapply zero_in_preemption_points; eauto 2. by eapply zero_in_preemption_points; eauto 2.
- split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN). - split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
+ rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment + rewrite /job_respects_max_nonpreemptive_segment
/job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto. /job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
by apply max_of_dominating_seq; intros; apply A5. by apply max_of_dominating_seq; intros; apply A5.
+ exists progr; split; first apply/andP; first split; rewrite ?leq_addr; by done. + exists progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
......
...@@ -28,15 +28,15 @@ Section FullyNonPreemptiveModel. ...@@ -28,15 +28,15 @@ Section FullyNonPreemptiveModel.
(** Next, consider any ideal non-preemptive uni-processor schedule of this arrival sequence... *) (** Next, consider any ideal non-preemptive uni-processor schedule of this arrival sequence... *)
Variable sched : schedule (ideal.processor_state Job). Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched. Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
(** ... where jobs do not execute before their arrival or after completion. *) (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched. Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that a job cost cannot be larger than a task cost. *) (** Assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_job_cost_le_task_cost: Hypothesis H_valid_job_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. arrivals_have_valid_job_costs arr_seq.
(** Then we prove that [fully_nonpreemptive_model] function (** Then we prove that [fully_nonpreemptive_model] function
defines a model with bounded non-preemptive regions.*) defines a model with bounded non-preemptive regions.*)
...@@ -45,7 +45,7 @@ Section FullyNonPreemptiveModel. ...@@ -45,7 +45,7 @@ Section FullyNonPreemptiveModel.
Proof. Proof.
have F: forall n, n = 0 \/ n > 0 by intros n; destruct n; [left | right]. have F: forall n, n = 0 \/ n > 0 by intros n; destruct n; [left | right].
intros j; split. intros j; split.
{ rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment; eauto 2. { rewrite /job_respects_max_nonpreemptive_segment; eauto 2.
erewrite job_max_nps_is_job_cost; eauto 2. erewrite job_max_nps_is_job_cost; eauto 2.
} }
move => progr /andP [_ GE]. move => progr /andP [_ GE].
......
...@@ -37,8 +37,8 @@ Section FullyPreemptiveModel. ...@@ -37,8 +37,8 @@ Section FullyPreemptiveModel.
Proof. Proof.
intros j ARR; split. intros j ARR; split.
- case: (posnP (job_cost j)) => [ZERO|POS]. - case: (posnP (job_cost j)) => [ZERO|POS].
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_0. + by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_0.
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_ε. + by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_ε.
- intros t; exists t; split. - intros t; exists t; split.
+ by apply/andP; split; [ done | rewrite leq_addr]. + by apply/andP; split; [ done | rewrite leq_addr].
+ by done. + by done.
......
...@@ -46,8 +46,8 @@ Section ProofWorkloadBound. ...@@ -46,8 +46,8 @@ Section ProofWorkloadBound.
Hypothesis H_tsk_in_ts : tsk \in ts. Hypothesis H_tsk_in_ts : tsk \in ts.
(** Assume that the job costs are no larger than the task costs. *) (** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_job_cost_le_task_cost : Hypothesis H_valid_job_cost :
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq. arrivals_have_valid_job_costs arr_seq.
(** Next, we assume that all jobs come from the task set. *) (** Next, we assume that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts. Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
...@@ -106,7 +106,7 @@ Section ProofWorkloadBound. ...@@ -106,7 +106,7 @@ Section ProofWorkloadBound.
rewrite /same_task -H_job_of_tsk muln1. rewrite /same_task -H_job_of_tsk muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ. apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto. rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.
by apply H_job_cost_le_task_cost. by apply H_valid_job_cost.
Qed. Qed.
(** As a corollary, we prove that workload of task is no larger the than (** As a corollary, we prove that workload of task is no larger the than
...@@ -149,7 +149,7 @@ Section ProofWorkloadBound. ...@@ -149,7 +149,7 @@ Section ProofWorkloadBound.
rewrite /workload_of_jobs. rewrite /workload_of_jobs.
rewrite muln1 /l /arrivals_between /arrival_sequence.arrivals_between. rewrite muln1 /l /arrivals_between /arrival_sequence.arrivals_between.
apply leq_sum_seq; move => j0 IN0 /eqP EQ. apply leq_sum_seq; move => j0 IN0 /eqP EQ.
by rewrite -EQ; apply H_job_cost_le_task_cost; apply in_arrivals_implies_arrived in IN0. by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
} }
{ rewrite leq_mul2l; apply/orP; right. { rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t). rewrite -{2}[delta](addKn t).
...@@ -183,7 +183,7 @@ Section ProofWorkloadBound. ...@@ -183,7 +183,7 @@ Section ProofWorkloadBound.
rewrite muln1. rewrite muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ. apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite -EQ. rewrite -EQ.
apply H_job_cost_le_task_cost. apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0. by apply in_arrivals_implies_arrived in IN0.
} }
{ rewrite leq_mul2l; apply/orP; right. { rewrite leq_mul2l; apply/orP; right.
...@@ -219,7 +219,7 @@ Section ProofWorkloadBound. ...@@ -219,7 +219,7 @@ Section ProofWorkloadBound.
rewrite muln1. rewrite muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ. apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite -EQ. rewrite -EQ.
apply H_job_cost_le_task_cost. apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0. by apply in_arrivals_implies_arrived in IN0.
} }
{ rewrite leq_mul2l; apply/orP; right. { rewrite leq_mul2l; apply/orP; right.
......
Require Export rt.restructuring.model.schedule.tdma. Require Export rt.restructuring.model.schedule.tdma.
Require Import rt.util.all. Require Import rt.util.all.
From mathcomp Require Import div.
(** In this section, we define the properties of TDMA and prove some basic lemmas. *) (** In this section, we define the properties of TDMA and prove some basic lemmas. *)
Section TDMAFacts. Section TDMAFacts.
...@@ -141,4 +142,4 @@ Section TDMAFacts. ...@@ -141,4 +142,4 @@ Section TDMAFacts.
Qed. Qed.
End TimeSlotOrderFacts. End TimeSlotOrderFacts.
End TDMAFacts. End TDMAFacts.
\ No newline at end of file
...@@ -735,9 +735,9 @@ Section EDFTransformFacts. ...@@ -735,9 +735,9 @@ Section EDFTransformFacts.
(** We begin with the first key property: the resulting schedule is actually (** We begin with the first key property: the resulting schedule is actually
an EDF schedule. *) an EDF schedule. *)
Theorem edf_transform_ensures_edf: Theorem edf_transform_ensures_edf:
is_EDF_schedule sched_edf. EDF_schedule sched_edf.
Proof. Proof.
rewrite /is_EDF_schedule /sched_edf /edf_transform => t. rewrite /EDF_schedule /sched_edf /edf_transform => t.
rewrite /EDF_at //= => j SCHED_j t' j' LE_t_t' SCHED_j' ARR_j'. rewrite /EDF_at //= => j SCHED_j t' j' LE_t_t' SCHED_j' ARR_j'.
move: SCHED_j. move: SCHED_j.
rewrite scheduled_at_def. rewrite scheduled_at_def.
......
Require Export rt.restructuring.model.priority.classes. Require Export rt.restructuring.model.priority.classes.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** * Service Received by Sets of Jobs *)