From a5393afbdd2cb84d741d288eda3a23fa3808906c Mon Sep 17 00:00:00 2001
From: =?UTF8?q?Bj=C3=B6rn=20Brandenburg?=
Date: Mon, 16 Dec 2019 18:23:54 +0100
Subject: [PATCH] cleanup the restructured model
improve comments, fix names, move some stuff around

.../analysis/abstract/abstract_rta.v  6 +
.../analysis/abstract/abstract_seq_rta.v  6 +
.../analysis/abstract/run_to_completion.v  2 +
.../concepts/request_bound_function.v  2 +
.../analysis/facts/behavior/task_arrivals.v  2 +
.../analysis/facts/preemption/job/limited.v  8 +
.../facts/preemption/job/nonpreemptive.v  2 +
.../facts/preemption/rtc_threshold/floating.v  8 +
.../facts/preemption/rtc_threshold/limited.v  12 +
.../preemption/rtc_threshold/nonpreemptive.v  4 +
.../preemption/rtc_threshold/preemptive.v  8 +
.../analysis/facts/preemption/task/floating.v  4 +
.../analysis/facts/preemption/task/limited.v  8 +
.../facts/preemption/task/nonpreemptive.v  8 +
.../facts/preemption/task/preemptive.v  4 +
restructuring/analysis/facts/rbf.v  12 +
restructuring/analysis/facts/tdma.v  3 +
.../analysis/facts/transform/edf_opt.v  4 +
.../model/aggregate/service_of_jobs.v  69 ++
restructuring/model/aggregate/task_arrivals.v  46 
restructuring/model/aggregate/workload.v  54 ++
restructuring/model/arrival/sporadic.v  53 
.../model/preemption/fully_nonpreemptive.v  13 +
.../model/preemption/fully_preemptive.v  13 +
.../model/preemption/limited_preemptive.v  95 ++++
restructuring/model/preemption/parameter.v  168 +++++++
restructuring/model/priority/classes.v  120 ++++++
.../model/priority/deadline_monotonic.v  6 +
restructuring/model/priority/edf.v  5 +
restructuring/model/priority/fifo.v  6 +
.../model/priority/numeric_fixed_priority.v  3 +
restructuring/model/priority/rate_monotonic.v  8 +
restructuring/model/processor/ideal.v  59 +++
.../model/processor/multiprocessor.v  51 ++++
.../model/processor/platform_properties.v  16 +
restructuring/model/processor/spin.v  28 ++
restructuring/model/processor/varspeed.v  27 ++
restructuring/model/readiness/basic.v  8 +
restructuring/model/readiness/jitter.v  26 ++
restructuring/model/readiness/suspension.v  36 +
restructuring/model/schedule/edf.v  55 +++
.../model/schedule/limited_preemptive.v  32 +
restructuring/model/schedule/nonpreemptive.v  23 +
.../model/schedule/preemption_time.v  42 ++
.../model/schedule/priority_driven.v  40 ++
restructuring/model/schedule/tdma.v  70 +++
.../model/schedule/work_conserving.v  30 +
restructuring/model/task/absolute_deadline.v  8 +
.../arrival/curves.v}  98 ++++++
restructuring/model/task/arrival/sporadic.v  68 ++++++
restructuring/model/task/arrivals.v  36 +++
restructuring/model/task/concept.v  154 +++++++
.../task/preemption/floating_nonpreemptive.v  67 +++
.../task/preemption/fully_nonpreemptive.v  39 ++
.../model/task/preemption/fully_preemptive.v  35 +
.../task/preemption/limited_preemptive.v  122 ++++++
.../model/task/preemption/parameters.v  206 +++++++++
restructuring/model/task/sequentiality.v  15 +
restructuring/model/task/suspension/dynamic.v  3 +
restructuring/results/edf/optimality.v  4 +
restructuring/results/edf/rta/bounded_nps.v  4 +
restructuring/results/edf/rta/bounded_pi.v  14 +
.../results/edf/rta/floating_nonpreemptive.v  6 +
.../results/edf/rta/fully_nonpreemptive.v  10 +
.../results/edf/rta/fully_preemptive.v  4 +
.../results/edf/rta/limited_preemptive.v  10 +
.../results/fixed_priority/rta/bounded_nps.v  4 +
.../results/fixed_priority/rta/bounded_pi.v  4 +
.../rta/floating_nonpreemptive.v  6 +
.../fixed_priority/rta/fully_nonpreemptive.v  10 +
.../fixed_priority/rta/fully_preemptive.v  4 +
.../fixed_priority/rta/limited_preemptive.v  12 +
scripts/wordlist.pws  5 +
73 files changed, 1265 insertions(+), 988 deletions()
delete mode 100644 restructuring/model/aggregate/task_arrivals.v
delete mode 100644 restructuring/model/arrival/sporadic.v
rename restructuring/model/{arrival/arrival_curves.v => task/arrival/curves.v} (51%)
create mode 100644 restructuring/model/task/arrival/sporadic.v
create mode 100644 restructuring/model/task/arrivals.v
diff git a/restructuring/analysis/abstract/abstract_rta.v b/restructuring/analysis/abstract/abstract_rta.v
index 3912dd5..9351b30 100644
 a/restructuring/analysis/abstract/abstract_rta.v
+++ b/restructuring/analysis/abstract/abstract_rta.v
@@ 38,8 +38,8 @@ Section Abstract_RTA.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Consider a task set ts... *)
Variable ts : list Task.
@@ 402,7 +402,7 @@ Section Abstract_RTA.
rewrite addnBA; last by apply PRT1.
rewrite subh1; last by done.
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.
diff git a/restructuring/analysis/abstract/abstract_seq_rta.v b/restructuring/analysis/abstract/abstract_seq_rta.v
index 3effc1a..5946e2a 100644
 a/restructuring/analysis/abstract/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/abstract_seq_rta.v
@@ 45,8 +45,8 @@ Section Sequential_Abstract_RTA.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Consider an arbitrary task set. *)
Variable ts : list Task.
@@ 611,7 +611,7 @@ Section Sequential_Abstract_RTA.
rewrite mulnDr mulnC muln1 addnBA // subnn addn0 mulnC.
apply sum_majorant_constant.
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.
(** Finally, we use the lemmas above to obtain the bound on
diff git a/restructuring/analysis/abstract/run_to_completion.v b/restructuring/analysis/abstract/run_to_completion.v
index 822f65c..53597c8 100644
 a/restructuring/analysis/abstract/run_to_completion.v
+++ b/restructuring/analysis/abstract/run_to_completion.v
@@ 36,7 +36,7 @@ Section AbstractRTARunToCompletionThreshold.
Variable sched : schedule (ideal.processor_state Job).
(** 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. *)
Variable tsk : Task.
diff git a/restructuring/analysis/concepts/request_bound_function.v b/restructuring/analysis/concepts/request_bound_function.v
index d70b44f..2dba4e7 100644
 a/restructuring/analysis/concepts/request_bound_function.v
+++ b/restructuring/analysis/concepts/request_bound_function.v
@@ 1,4 +1,4 @@
Require Export rt.restructuring.model.arrival.arrival_curves.
+Require Export rt.restructuring.model.task.arrival.curves.
Require Export rt.restructuring.model.priority.classes.
(** The following definitions assume ideal uniprocessor schedules. This
diff git a/restructuring/analysis/facts/behavior/task_arrivals.v b/restructuring/analysis/facts/behavior/task_arrivals.v
index 74b882b..539c0c4 100644
 a/restructuring/analysis/facts/behavior/task_arrivals.v
+++ b/restructuring/analysis/facts/behavior/task_arrivals.v
@@ 1,4 +1,4 @@
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. *)
Section TaskArrivals.
diff git a/restructuring/analysis/facts/preemption/job/limited.v b/restructuring/analysis/facts/preemption/job/limited.v
index 64de866..4241860 100644
 a/restructuring/analysis/facts/preemption/job/limited.v
+++ b/restructuring/analysis/facts/preemption/job/limited.v
@@ 29,8 +29,8 @@ Section ModelWithLimitedPreemptions.
(** Next, consider any limited ideal uniprocessor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
 Hypothesis H_valid_schedule_with_limited_preemptions:
 valid_schedule_with_limited_preemptions arr_seq sched.
+ Hypothesis H_schedule_respects_preemption_model:
+ schedule_respects_preemption_model arr_seq sched.
(** ...where jobs do not execute after their completion. *)
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
@@ 204,7 +204,7 @@ Section ModelWithLimitedPreemptions.
intros j ARR; repeat split.
{ by apply zero_in_preemption_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.
have SERV: service sched j t = service sched j t.+1.
{ rewrite [service sched j t]addn0 /service /service_during; apply/eqP.
@@ 215,7 +215,7 @@ Section ModelWithLimitedPreemptions.
rewrite [job_preemptable _ _]Bool.negb_involutive.
apply/negP; intros CONTR.
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.
}
Qed.
diff git a/restructuring/analysis/facts/preemption/job/nonpreemptive.v b/restructuring/analysis/facts/preemption/job/nonpreemptive.v
index 8ac8a82..029b0a2 100644
 a/restructuring/analysis/facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/job/nonpreemptive.v
@@ 24,7 +24,7 @@ Section FullyNonPreemptiveModel.
(** Next, consider any nonpreemptive ideal uniprocessor schedule of
this arrival sequence ... *)
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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
diff git a/restructuring/analysis/facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
index bba9d81..e5be78e 100644
 a/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
@@ 22,8 +22,8 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
Variable arr_seq : arrival_sequence Job.
(** Assume that a job cost cannot be larger than a task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Then, we prove that [task_run_to_completion_threshold] function
defines a valid task's run to completion threshold. *)
@@ 31,10 +31,10 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.
Proof.
intros; split.
  by rewrite /task_run_to_completion_threshold_le_task_cost.
+  by rewrite /task_rtc_bounded_by_cost.
 intros j ARR TSK.
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
 by rewriteTSK; apply H_job_cost_le_task_cost.
+ by rewriteTSK; apply H_valid_job_cost.
Qed.
End TaskRTCThresholdFloatingNonPreemptiveRegions.
diff git a/restructuring/analysis/facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
index 0d1606e..7819489 100644
 a/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
@@ 28,8 +28,8 @@ Section TaskRTCThresholdLimitedPreemptions.
(** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
 Hypothesis H_valid_schedule_with_limited_preemptions:
 valid_schedule_with_limited_preemptions arr_seq sched.
+ Hypothesis H_schedule_respects_preemption_model:
+ schedule_respects_preemption_model arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ 39,8 +39,8 @@ Section TaskRTCThresholdLimitedPreemptions.
Variable ts : seq Task.
(** Assume that a job cost cannot be larger than a task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Consider the model with fixed preemption points. I.e., each task
is divided into a number of nonpreemptive segments by inserting
@@ 97,7 +97,7 @@ Section TaskRTCThresholdLimitedPreemptions.
Lemma limited_valid_task_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
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].
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
@@ 106,7 +106,7 @@ Section TaskRTCThresholdLimitedPreemptions.
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.
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.
have F: 1 <= size (distances (task_preemption_points tsk)).
{ apply leq_trans with (size (task_preemption_points tsk)  1).
diff git a/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 335c6df..f1dcc27 100644
 a/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ 28,7 +28,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
(** Next, consider any ideal nonpreemptive uniprocessor schedule of
this arrival sequence ... *)
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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ 70,7 +70,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
valid_task_run_to_completion_threshold arr_seq tsk.
Proof.
intros; split.
  by unfold task_run_to_completion_threshold_le_task_cost.
+  by unfold task_rtc_bounded_by_cost.
 intros j ARR TSK.
rewrite TSK /task_run_to_completion_threshold /fully_nonpreemptive.
edestruct (posnP (job_cost j)) as [ZEROPOS].
diff git a/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
index d8b601f..e2e9b6a 100644
 a/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ 21,8 +21,8 @@ Section TaskRTCThresholdFullyPreemptiveModel.
Variable arr_seq : arrival_sequence Job.
(** ... and assume that a job cost cannot be larger than a task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Then, we prove that [task_run_to_completion_threshold] function
defines a valid task's run to completion threshold. *)
@@ 30,10 +30,10 @@ Section TaskRTCThresholdFullyPreemptiveModel.
forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.
Proof.
intros; split.
  by rewrite /task_run_to_completion_threshold_le_task_cost.
+  by rewrite /task_rtc_bounded_by_cost.
 intros j ARR TSK.
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
 by rewriteTSK; apply H_job_cost_le_task_cost.
+ by rewriteTSK; apply H_valid_job_cost.
Qed.
End TaskRTCThresholdFullyPreemptiveModel.
diff git a/restructuring/analysis/facts/preemption/task/floating.v b/restructuring/analysis/facts/preemption/task/floating.v
index 14bf9d3..e76c730 100644
 a/restructuring/analysis/facts/preemption/task/floating.v
+++ b/restructuring/analysis/facts/preemption/task/floating.v
@@ 37,7 +37,7 @@ Section FloatingNonPreemptiveRegionsModel.
of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ 58,7 +58,7 @@ Section FloatingNonPreemptiveRegionsModel.
move: (H_valid_model_with_floating_nonpreemptive_regions) => LIM; move: LIM (LIM) => [LIM L] [[BEG [END NDEC]] MAX].
case: (posnP (job_cost j)) => [ZEROPOS].
 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.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
diff git a/restructuring/analysis/facts/preemption/task/limited.v b/restructuring/analysis/facts/preemption/task/limited.v
index 2b11f75..88ba4d0 100644
 a/restructuring/analysis/facts/preemption/task/limited.v
+++ b/restructuring/analysis/facts/preemption/task/limited.v
@@ 31,8 +31,8 @@ Section LimitedPreemptionsModel.
(** Next, consider any ideal uniprocessor preemptionaware schedule
of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
 Hypothesis H_valid_schedule_with_limited_preemptions:
 valid_schedule_with_limited_preemptions arr_seq sched.
+ Hypothesis H_schedule_respects_preemption_model:
+ schedule_respects_preemption_model arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ 57,14 +57,14 @@ Section LimitedPreemptionsModel.
move: (LIM) => [BEG [END NDEC]]; move: (FIX) => [A1 [A2 [A3 [A4 A5]]]].
case: (posnP (job_cost j)) => [ZEROPOS].
 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.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
exists 0; rewrite LE; split; first by apply/andP; split.
by eapply zero_in_preemption_points; eauto 2.
 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.
by apply max_of_dominating_seq; intros; apply A5.
+ exists progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
diff git a/restructuring/analysis/facts/preemption/task/nonpreemptive.v b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
index 899a8f9..6278699 100644
 a/restructuring/analysis/facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
@@ 28,15 +28,15 @@ Section FullyNonPreemptiveModel.
(** Next, consider any ideal nonpreemptive uniprocessor schedule of this arrival sequence... *)
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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_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. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Then we prove that [fully_nonpreemptive_model] function
defines a model with bounded nonpreemptive regions.*)
@@ 45,7 +45,7 @@ Section FullyNonPreemptiveModel.
Proof.
have F: forall n, n = 0 \/ n > 0 by intros n; destruct n; [left  right].
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.
}
move => progr /andP [_ GE].
diff git a/restructuring/analysis/facts/preemption/task/preemptive.v b/restructuring/analysis/facts/preemption/task/preemptive.v
index f7ed785..8b17d3c 100644
 a/restructuring/analysis/facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/facts/preemption/task/preemptive.v
@@ 37,8 +37,8 @@ Section FullyPreemptiveModel.
Proof.
intros j ARR; split.
 case: (posnP (job_cost j)) => [ZEROPOS].
 + by rewrite /job_max_nonpreemptive_segment_le_task_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_0.
+ + by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_ε.
 intros t; exists t; split.
+ by apply/andP; split; [ done  rewrite leq_addr].
+ by done.
diff git a/restructuring/analysis/facts/rbf.v b/restructuring/analysis/facts/rbf.v
index 90ee17c..5c5a910 100644
 a/restructuring/analysis/facts/rbf.v
+++ b/restructuring/analysis/facts/rbf.v
@@ 46,8 +46,8 @@ Section ProofWorkloadBound.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Assume that the job costs are no larger than the task costs. *)
 Hypothesis H_job_cost_le_task_cost :
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost :
+ arrivals_have_valid_job_costs arr_seq.
(** Next, we assume that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
@@ 106,7 +106,7 @@ Section ProofWorkloadBound.
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_job_cost_le_task_cost.
+ by apply H_valid_job_cost.
Qed.
(** As a corollary, we prove that workload of task is no larger the than
@@ 149,7 +149,7 @@ Section ProofWorkloadBound.
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_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 {2}[delta](addKn t).
@@ 183,7 +183,7 @@ Section ProofWorkloadBound.
rewrite muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite EQ.
 apply H_job_cost_le_task_cost.
+ apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{ rewrite leq_mul2l; apply/orP; right.
@@ 219,7 +219,7 @@ Section ProofWorkloadBound.
rewrite muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite EQ.
 apply H_job_cost_le_task_cost.
+ apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{ rewrite leq_mul2l; apply/orP; right.
diff git a/restructuring/analysis/facts/tdma.v b/restructuring/analysis/facts/tdma.v
index d7efce6..c951933 100644
 a/restructuring/analysis/facts/tdma.v
+++ b/restructuring/analysis/facts/tdma.v
@@ 1,5 +1,6 @@
Require Export rt.restructuring.model.schedule.tdma.
Require Import rt.util.all.
+From mathcomp Require Import div.
(** In this section, we define the properties of TDMA and prove some basic lemmas. *)
Section TDMAFacts.
@@ 141,4 +142,4 @@ Section TDMAFacts.
Qed.
End TimeSlotOrderFacts.
End TDMAFacts.
\ No newline at end of file
+End TDMAFacts.
diff git a/restructuring/analysis/facts/transform/edf_opt.v b/restructuring/analysis/facts/transform/edf_opt.v
index 8bc9b82..993ac77 100644
 a/restructuring/analysis/facts/transform/edf_opt.v
+++ b/restructuring/analysis/facts/transform/edf_opt.v
@@ 735,9 +735,9 @@ Section EDFTransformFacts.
(** We begin with the first key property: the resulting schedule is actually
an EDF schedule. *)
Theorem edf_transform_ensures_edf:
 is_EDF_schedule sched_edf.
+ EDF_schedule sched_edf.
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'.
move: SCHED_j.
rewrite scheduled_at_def.
diff git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index e3156c1..6e43522 100644
 a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ 1,12 +1,10 @@
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 *)
(** In this file, we define the notion of service received by a set of jobs. *)
+
+(** In this file, we define the notion of service received by a set of
+ jobs. *)
+
Section ServiceOfJobs.
(** Consider any type of tasks ... *)
@@ 15,10 +13,8 @@ Section ServiceOfJobs.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
 Context `{JobArrival Job}.
 Context `{JobCost Job}.
 (** Consider any kind of processor state model, ... *)
+ (** Consider any kind of processor model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
@@ 31,53 +27,30 @@ Section ServiceOfJobs.
(** First, we define the service received by a generic set of jobs. *)
Section ServiceOfSetOfJobs.
 (** Let P be any predicate over jobs, ...*)
 Variable P : Job > bool.
+ (** Let [P] be any computable predicate over jobs, ...*)
+ Variable P : pred Job.
 (** ... and let jobs denote any (finite) set of jobs. *)
+ (** ... and let [jobs] denote any (finite) set of jobs. *)
Variable jobs : seq Job.
 (** Then we define the cumulative service received at
 time t by the jobs that satisfy this predicate ... *)
+ (** We define the cumulative service received at time [t] by
+ jobs in [jobs] that satisfy predicate [P] ... *)
Definition service_of_jobs_at (t : instant) :=
\sum_(j < jobs  P j) service_at sched j t.
 (** ... and the cumulative service received during time
 interval [t1, t2) by the jobs that satisfy the predicate. *)
+ (** ... and the cumulative service received during the interval
+ [[t1, t2)] by jobs that satisfy predicate [P]. *)
Definition service_of_jobs (t1 t2 : instant) :=
\sum_(j < jobs  P j) service_during sched j t1 t2.
End ServiceOfSetOfJobs.
 (** Next, we define the service received by tasks with
 higherorequal priority under a given FP policy. *)
 Section PerTaskPriority.

 (** Consider any FP policy. *)
 Variable higher_eq_priority : FP_policy Task.

 (** Let jobs denote any (finite) set of jobs. *)
 Variable jobs : seq Job.

 (** Let [tsk] be the task to be analyzed. *)
 Variable tsk : Task.

 (** Based on the definition of jobs of higher or equal priority
 (with respect to task [tsk]), ... *)
 Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.

 (** ...we define the service received during [[t1, t2)] by jobs of
 higher or equal priority. *)
 Definition service_of_higher_or_equal_priority_tasks (t1 t2 : instant) :=
 service_of_jobs of_higher_or_equal_priority jobs t1 t2.

 End PerTaskPriority.

 (** Next, we define the service received by jobs with
 higherorequal priority under JLFP policies. *)
+ (** Next, we define the service received by jobs with higher or
+ equal priority under JLFP policies. *)
Section PerJobPriority.
(** Consider any JLDP policy. *)
+ (* [FIXME]: This should be a nameless context declaration! *)
Variable higher_eq_priority : JLFP_policy Job.
(** Let jobs denote any (finite) set of jobs. *)
@@ 87,6 +60,7 @@ Section ServiceOfJobs.
Variable j : Job.
(** Based on the definition of jobs of higher or equal priority, ... *)
+ (* [FIXME]: this should use [hep_job], not the named type class directly. *)
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
(** ...we define the service received during [[t1, t2)] by jobs of higher or equal priority. *)
@@ 95,17 +69,18 @@ Section ServiceOfJobs.
End PerJobPriority.
 (** In this section, we define the notion of workload for sets of jobs. *)
+ (** Finally, we define the notion of cumulative service received by
+ the jobs of a given task. *)
Section ServiceOfTask.
 (** Let [tsk] be the task to be analyzed... *)
+ (** Let [tsk] be the task to be analyzed ... *)
Variable tsk : Task.
 (** ... and let jobs denote any (finite) set of jobs. *)
+ (** ... and let [jobs] denote any (finite) set of jobs. *)
Variable jobs : seq Job.
 (** We define the cumulative task service received by the jobs
 from the task within time interval [[t1, t2)]. *)
+ (** We define the cumulative task service received by the jobs of
+ task [tsk] within time interval [[t1, t2)]. *)
Definition task_service_of_jobs_in t1 t2 :=
service_of_jobs (job_of_task tsk) jobs t1 t2.
diff git a/restructuring/model/aggregate/task_arrivals.v b/restructuring/model/aggregate/task_arrivals.v
deleted file mode 100644
index 4d3c18b..0000000
 a/restructuring/model/aggregate/task_arrivals.v
+++ /dev/null
@@ 1,46 +0,0 @@
Require Export rt.restructuring.model.task.concept.
(** In this file we provide basic definitions related to tasks on arrival sequences. *)
Section TaskArrivals.

 (** Consider any type of job associated with any type of tasks. *)
 Context {Job : JobType}.
 Context {Task : TaskType}.
 Context `{JobTask Job Task}.

 (** Consider any job arrival sequence. *)
 Variable arr_seq : arrival_sequence Job.

 Section Definitions.

 (** Let [tsk] be any task. *)
 Variable tsk : Task.

 (** We define the sequence of jobs of task [tsk] arriving at time t. *)
 Definition task_arrivals_at (t : instant) : seq Job :=
 [seq j < arrivals_at arr_seq t  job_task j == tsk].

 (** By concatenation, we construct the list of jobs of task [tsk]
 that arrived in the interval [[t1, t2)]. *)
 Definition task_arrivals_between (t1 t2 : instant) :=
 [seq j < arrivals_between arr_seq t1 t2  job_task j == tsk].

 (** Based on that, we define the list of jobs of task [tsk] that
 arrived up to time t, ...*)
 Definition task_arrivals_up_to (t : instant) := task_arrivals_between 0 t.+1.

 (** ...and the list of jobs of task [tsk] that arrived strictly
 before time t ... *)
 Definition task_arrivals_before (t : instant) := task_arrivals_between 0 t.

 (** ... and also count the number of job arrivals. *)
 Definition number_of_task_arrivals (t1 t2 : instant) :=
 size (task_arrivals_between t1 t2).

 End Definitions.

 (** We define a predicate for arrival sequences in which all jobs
 come from a given task set. *)
 Definition arrivals_come_from_taskset (ts : seq Task) :=
 forall j, arrives_in arr_seq j > job_task j \in ts.

End TaskArrivals.
\ No newline at end of file
diff git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index 6a3bea2..42815dd 100644
 a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ 1,19 +1,19 @@
Require Export rt.restructuring.model.priority.classes.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+(** * Cumulative Workload of Sets of Jobs *)
(** * Workload of Sets of Jobs *)
(** In this section, we define the notion of workload for sets of jobs. *)
+(** In this module, we define the notion of the cumulative workload of
+ a set of jobs. *)
Section WorkloadOfJobs.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
 (** ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs with execution costs that are
+ associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
 Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any job arrival sequence. *)
@@ 22,52 +22,34 @@ Section WorkloadOfJobs.
(** First, we define the workload for generic sets of jobs. *)
Section WorkloadOfJobs.
 (** Given any predicate over Jobs, ... *)
 Variable P : Job > bool.
+ (** Given any computable predicate on jobs, ... *)
+ Variable P : pred Job.
 (** ... and any (finite) set of jobs. *)
+ (** ... and any (finite) set of jobs, ... *)
Variable jobs : seq Job.
 (** We define the total workload of the jobs that satisfy predicate P. *)
+ (** ... we define the total workload of the jobs that satisfy
+ predicate [P]. *)
Definition workload_of_jobs := \sum_(j < jobs  P j) job_cost j.
End WorkloadOfJobs.
 (** Next, we define the workload of tasks with higher or
 equal priority under FP policies. *)
 Section PerTaskPriority.

 (** Consider any FP policy that indicates whether a task has
 higher or equal priority. *)
 Variable higher_eq_priority : FP_policy Task.

 (** Let [tsk] be the task to be analyzed. *)
 Variable tsk : Task.

 (** Recall the notion of a job of higher or equal priority. *)
 Let of_higher_or_equal_priority j :=
 higher_eq_priority (job_task j) tsk.

 (** Then, we define the workload of all jobs of tasks with
 higherorequal priority than task [tsk]. *)
 Definition workload_of_higher_or_equal_priority_tasks :=
 workload_of_jobs of_higher_or_equal_priority.

 End PerTaskPriority.

 (** Then, we define the workload of jobs with higher or
 equal priority under JLFP policies. *)
+ (** Next, we define the workload of jobs with higher or
+ equal priority under JLFP policies. *)
Section PerJobPriority.
(** Consider any JLFP policy that indicates whether a job has
higher or equal priority. *)
+ (* [FIXME]: should be a context declaration! *)
Variable higher_eq_priority : JLFP_policy Job.
(** Let j be the job to be analyzed. *)
Variable j : Job.
(** Recall the notion of a job of higher or equal priority. *)
 Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
+ Let of_higher_or_equal_priority j_hp :=
+ (* [FIXME]: should be using [hep_job]! *)
+ higher_eq_priority j_hp j.
(** Then, we define the workload of higher or equal priority of all jobs
with higherorequal priority than j. *)
@@ 86,8 +68,8 @@ Section WorkloadOfJobs.
[tsk]. *)
Definition task_workload jobs := workload_of_jobs (job_of_task tsk) jobs.
 (** Next, we recall the definition of the task workload in
 interval [[t1, t2)]. *)
+ (** Finally, we define the task's workload in a given interval [[t1,
+ t2)]. *)
Definition task_workload_between (t1 t2 : instant) :=
task_workload (arrivals_between arr_seq t1 t2).
diff git a/restructuring/model/arrival/sporadic.v b/restructuring/model/arrival/sporadic.v
deleted file mode 100644
index 23b3623..0000000
 a/restructuring/model/arrival/sporadic.v
+++ /dev/null
@@ 1,53 +0,0 @@
Require Export rt.restructuring.model.task.concept.
Section TaskMinInterArrivalTime.
 Context {Task : TaskType}.

 Variable (task_min_inter_arrival_time : duration).

 Definition valid_task_min_inter_arrival_time :=
 task_min_inter_arrival_time > 0.

 Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

 Variable arr_seq : arrival_sequence Job.

 Definition respects_sporadic_task_model (tsk : Task) (d : duration) :=
 forall (j j': Job),
 j <> j' > (** Given two different jobs j and j' ... *)
 arrives_in arr_seq j > (** ...that belong to the arrival sequence... *)
 arrives_in arr_seq j' >
 job_task j = tsk >
 job_task j' = tsk > (** ... and that are spawned by the same task, ... *)
 job_arrival j <= job_arrival j' > (** ... if the arrival of j precedes the arrival of j' ..., *)
 (** then the arrival of j and the arrival of j' are separated by at least one period. *)
 job_arrival j' >= job_arrival j + d.

End TaskMinInterArrivalTime.

(** Definition of a generic type of parameter for task
 minimum inter arrival times *)

Class SporadicModel (Task : TaskType) :=
 task_min_inter_arrival_time : Task > duration.

Section SporadicModel.
 Context {Task : TaskType} `{SporadicModel Task}.

 Variable ts : seq Task.

 Definition valid_taskset_min_inter_arrival_times :=
 forall tsk : Task,
 tsk \in ts >
 task_min_inter_arrival_time tsk > 0.

 Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

 Variable arr_seq : arrival_sequence Job.

 (** Then, we define the sporadic task model as follows.*)
 Definition taskset_respects_sporadic_task_model :=
 forall tsk,
 tsk \in ts >
 respects_sporadic_task_model arr_seq tsk (task_min_inter_arrival_time tsk).

End SporadicModel.
diff git a/restructuring/model/preemption/fully_nonpreemptive.v b/restructuring/model/preemption/fully_nonpreemptive.v
index 95f9000..6915071 100644
 a/restructuring/model/preemption/fully_nonpreemptive.v
+++ b/restructuring/model/preemption/fully_nonpreemptive.v
@@ 1,19 +1,20 @@
Require Export rt.restructuring.model.preemption.parameter.
(** * Platform for Fully NonPreemptive Model *)
+(** * Preemption Model: Fully NonPreemptive Jobs *)
(** In this section, we instantiate [job_preemptable] for the fully
 nonpreemptive model. *)
+ nonpreemptive model, wherein no job can be forcefully preempted at any
+ time. *)
Section FullyNonPreemptiveModel.
 (** Consider any type of jobs. *)
+ (** Consider any type of jobs with execution costs. *)
Context {Job : JobType}.
 Context `{JobCost Job}.

+ Context `{JobCost Job}.
+
(** We say that the model is fully nonpreemptive iff no job
can be preempted until its completion. *)
Global Instance fully_nonpreemptive_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := (ρ == 0)  (ρ == job_cost j)
}.

+
End FullyNonPreemptiveModel.
diff git a/restructuring/model/preemption/fully_preemptive.v b/restructuring/model/preemption/fully_preemptive.v
index da8401b..d982b2d 100644
 a/restructuring/model/preemption/fully_preemptive.v
+++ b/restructuring/model/preemption/fully_preemptive.v
@@ 1,17 +1,18 @@
Require Export rt.restructuring.model.preemption.parameter.
(** * Fully Preemptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
 preemptive model. *)
+(** * Preemption Model: Fully Preemptive Jobs *)
+(** In this section, we instantiate [job_preemptable] for the fully preemptive
+ model, wherein any job may be preempted at any time. This matches the
+ classic Liu & Layland model. *)
Section FullyPreemptiveModel.
(** Consider any type of jobs. *)
Context {Job : JobType}.
 (** In the fully preemptive model any job can be preempted at any time. *)
+ (** In the fully preemptive model, any job can be preempted at any time. *)
Global Program Instance fully_preemptive_model : JobPreemptable Job :=
{
 job_preemptable (j : Job) (ρ : work) := true
+ job_preemptable (_ : Job) (_ : work) := true
}.
End FullyPreemptiveModel.
\ No newline at end of file
+End FullyPreemptiveModel.
diff git a/restructuring/model/preemption/limited_preemptive.v b/restructuring/model/preemption/limited_preemptive.v
index 9af1016..98fdca8 100644
 a/restructuring/model/preemption/limited_preemptive.v
+++ b/restructuring/model/preemption/limited_preemptive.v
@@ 1,58 +1,71 @@
Require Export rt.restructuring.model.preemption.parameter.
(** Definition of a parameter relating a job
 to the sequence of its preemption points. *)
+(** * Job Model Parameter for Preemption Points *)
+
+(** Under the limitedpreemptive preemption model, jobs can be preempted only
+ at a precise set of points during their execution. To allow such fixed,
+ progressdependent preemption points to be specified, we introduce a new
+ job parameter [job_preemption_points] that, for each job, yields the set of
+ progress values at which the job can be preempted by the scheduler. *)
Class JobPreemptionPoints (Job : JobType) :=
{
job_preemption_points : Job > seq work
}.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we instantiate [job_preemptable] for the model
 with limited preemptions and introduce a set of requirements for
 function [job_preemption_points], so it is coherent with limited
 preemptions model. *)
+(** * Preemption Model: LimitedPreemptive Jobs *)
+
+(** Based on the above definition of [job_preemption_points], in the following
+ we instantiate [job_preemptable] for limitedpreemptive jobs and introduce
+ requirements that the function [job_preemption_points] should satisfy to be
+ coherent with the limitedpreemptive preemption model. *)
Section LimitedPreemptions.
 (** Consider any type of jobs. *)
+ (** Consider any type of jobs with arrival times and execution costs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.

 (** In addition, assume the existence of a function that
 maps a job to the sequence of its preemption points. *)
+
+ (** Given each job's preemption points, as determined by
+ [job_preemption_points], ...*)
Context `{JobPreemptionPoints Job}.
 (** In the model with limited preemptions a job can be preempted
 if its progress is equal to one of the preemption points. *)
+ (** ...a job [j] is preemptable at a given point of progress [ρ] iff [ρ] is
+ one of the preemption points of [j]. *)
Global Instance limited_preemptions_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
 }.

 (** Next, we describe some structural properties that
 a sequence of preemption points should satisfy. *)

 (** Consider any arrival sequence. *)
 Variable arr_seq : arrival_sequence Job.

 (** We require the sequence of preemption points to contain the beginning ... *)
 Definition beginning_of_execution_in_preemption_points :=
 forall j, arrives_in arr_seq j > 0 \in job_preemption_points j.

 (** ... and the end of execution for any job j. *)
 Definition end_of_execution_in_preemption_points :=
 forall j, arrives_in arr_seq j > last0 (job_preemption_points j) = job_cost j.

 (** We require the sequence of preemption points to be a nondecreasing sequence. *)
 Definition preemption_points_is_nondecreasing_sequence :=
 forall j, arrives_in arr_seq j > nondecreasing_sequence (job_preemption_points j).

 (** We define a valid joblevel model with limited preemptions
 as a conjunction of the hypotheses above. *)
 Definition valid_limited_preemptions_job_model :=
 beginning_of_execution_in_preemption_points /\
 end_of_execution_in_preemption_points /\
 preemption_points_is_nondecreasing_sequence.

End LimitedPreemptions.
\ No newline at end of file
+ }.
+
+ (** ** Model Validity *)
+
+ (** Next, we introduce some structural properties that a valid sequence of
+ preemption points must satisfy. *)
+ Section ValidLimitedPreemptiveModel.
+
+ (** Consider any arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** We require the sequence of preemption points to contain the beginning ... *)
+ Definition beginning_of_execution_in_preemption_points :=
+ forall j, arrives_in arr_seq j > 0 \in job_preemption_points j.
+
+ (** ... and the end of execution for any job [j] that arrives in the given
+ arrival sequence [arr_seq]. *)
+ Definition end_of_execution_in_preemption_points :=
+ forall j, arrives_in arr_seq j > last0 (job_preemption_points j) = job_cost j.
+
+ (** We further require the sequence of preemption points to be a
+ nondecreasing sequence. *)
+ Definition preemption_points_is_nondecreasing_sequence :=
+ forall j, arrives_in arr_seq j > nondecreasing_sequence (job_preemption_points j).
+
+ (** A job model is considered valid w.r.t. limitedpreemptive preemption
+ model if it satisfies each of the preceding definitions. *)
+ Definition valid_limited_preemptions_job_model :=
+ beginning_of_execution_in_preemption_points /\
+ end_of_execution_in_preemption_points /\
+ preemption_points_is_nondecreasing_sequence.
+
+ End ValidLimitedPreemptiveModel.
+
+End LimitedPreemptions.
diff git a/restructuring/model/preemption/parameter.v b/restructuring/model/preemption/parameter.v
index 0bb7e5c..970d59d 100644
 a/restructuring/model/preemption/parameter.v
+++ b/restructuring/model/preemption/parameter.v
@@ 1,96 +1,100 @@
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
(** * Job Preemptable *)
(** There are many equivalent ways to represent preemption points of a job. *)

(** In Prosa Preemption points are represented with a predicate
 [job_preemptable] which maps a job and its progress to a boolean
 value saying whether this job is preemptable at its current point
 of execution. *)
+(** * JobLevel Preemption Model *)
+(** There are many equivalent ways to represent at which points in time a job
+ is preemptable, i.e., where it can be forced to relinquish the processor on
+ which it is executing. In Prosa, the various preemption models are
+ represented with a single predicate [job_preemptable] that indicates, for
+ given a job and a given degree of progress, whether the job is preemptable
+ at its current point of execution. *)
Class JobPreemptable (Job : JobType) :=
job_preemptable : Job > work > bool.
(** * Derived Parameters *)
(** * Job Maximum and Last Nonpreemptive Segment *)
(** In this section we define the notions of the maximal and the last
+(** * Maximum and Last Nonpreemptive Segment of a Job *)
+(** In the following section we define the notions of the maximal and the last
nonpreemptive segments. *)
Section MaxAndLastNonpreemptiveSegment.
 (** Consider any type of jobs. *)
+ (** Consider any type of jobs with arrival times and execution costs... *)
Context {Job : JobType}.
Context `{JobArrival Job}.
 Context `{JobCost Job}.
Context `{JobCost Job}.
 Context `{JobPreemptable Job}.

 (** It is useful to have a representation of preemption points of a
 job defined as an actual sequence of points where this job can
 be preempted. *)
+
+ (** ... and consider any given preemption model. *)
+ Context `{JobPreemptable Job}.
+
+ (** It is useful to define a representation of the preemption points of a job
+ as an actual sequence of points where this job can be preempted. To this
+ end, we define [job_preemption_points j] as the sequence of all progress
+ values at which job [j] is preemptable, according to
+ [job_preemptable]. *)
Definition job_preemption_points (j : Job) : seq work :=
 [seq ρ:work < range 0 (job_cost j)  job_preemptable j ρ].

 (** Note that the conversion preserves the equivalence. *)
+ [seq ρ : work < range 0 (job_cost j)  job_preemptable j ρ].
+
+ (** We observe that the conversion indeed is an equivalent way of
+ representing the set of preemption points. *)
Remark conversion_preserves_equivalence:
forall (j : Job) (ρ : work),
ρ <= job_cost j >
job_preemptable j ρ <> ρ \in job_preemption_points j.
Proof.
 intros ? ? LE.
+ intros ? ? LE.
case: (posnP (job_cost j)) => [ZEROPOS].
 { unfold job_preemption_points.
+ { unfold job_preemption_points.
split; intros PP.
 move: LE; rewrite ZERO leqn0; move => /eqP EQ; subst.
 by simpl; rewrite PP.
+ by simpl; rewrite PP.
 rewrite ZERO in PP; simpl in PP.
destruct (job_preemptable j 0) eqn:EQ; last by done.
 by move: PP => /orP [/eqP A1 FF]; subst.
+ by move: PP => /orP [/eqP A1 FF]; subst.
}
have F: job_cost j == 0 = false.
{ by apply/eqP/neqP; rewrite lt0n. }
split; intros PP.
all: unfold job_preemption_points in *.
 rewrite mem_filter; apply/andP; split; first by done.
 by rewrite mem_iota subn0 add0n //; apply/andP; split.
  by move: PP; rewrite mem_filter; move => /andP [PP _].
+ by rewrite mem_iota subn0 add0n //; apply/andP; split.
+  by move: PP; rewrite mem_filter; move => /andP [PP _].
Qed.

 (** We define a function that maps a job to the
 sequence of lengths of its nonpreemptive segments. *)
+
+ (** We further define a function that, for a given job, yields the sequence
+ of lengths of its nonpreemptive segments. *)
Definition lengths_of_segments (j : Job) := distances (job_preemption_points j).
 (** Next, we define a function that maps a job to the
 length of the longest nonpreemptive segment of job j. *)
+ (** Next, we define a function that determines the length of a job's longest
+ nonpreemptive segment (or zero if the job is fully preemptive). *)
Definition job_max_nonpreemptive_segment (j : Job) := max0 (lengths_of_segments j).
 (** Similarly, we define a function that maps a job to the
 length of the last nonpreemptive segment. *)
+ (** Similarly, we define a function that yields the length of a job's last
+ nonpreemptive segment (or zero if the job is fully preemptive). *)
Definition job_last_nonpreemptive_segment (j : Job) := last0 (lengths_of_segments j).
 (** We define the notion of job's runtocompletion threshold:
 runtocompletion threshold is the amount of service after which
 a job cannot be preempted until its completion. *)
+ (** * RuntoCompletion Threshold of a Job *)
+
+ (** Finally, we define the notion of a job's runtocompletion threshold: the
+ runtocompletion threshold is the amount of service after which a job
+ cannot be preempted until its completion. *)
Definition job_run_to_completion_threshold (j : Job) :=
job_cost j  (job_last_nonpreemptive_segment j  ε).

End MaxAndLastNonpreemptiveSegment.
(** * Platform with limited preemptions *)
(** In the following, we define properties that any reasonable job
 preemption model must satisfy. *)
+End MaxAndLastNonpreemptiveSegment.
+
+
+(** * Model Validity *)
+(** In the following, we define properties that any reasonable job preemption
+ model must satisfy. *)
Section PreemptionModel.
 (** Consider any type of jobs... *)
+ (** Consider any type of jobs with arrival times and execution costs... *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
 (** ... and the existence of a predicate mapping a job and
 its progress to a boolean value saying whether this job is
 preemptable at its current point of execution. *)
+ (** ... and any preemption model. *)
Context `{JobPreemptable Job}.
 (** Consider any kind of processor state model, ... *)
+ (** Consider any kind of processor model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
@@ 100,43 +104,39 @@ Section PreemptionModel.
(** ... and any given schedule. *)
Variable sched : schedule PState.
 (** In this section, we define the notion of a valid preemption model. *)
 Section ValidPreemptionModel.

 (** We require that a job has to be executed at least one time
 instant in order to reach a nonpreemptive segment. In other
 words, a job must start execution to become nonpreemptive. *)
 Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
 job_preemptable j 0.

 (** And vice versa, a job cannot remain nonpreemptive after its completion. *)
 Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
 job_preemptable j (job_cost j).

 (** Next, if a job j is not preemptive at some time instant t,
 then j must be scheduled at time t. *)
 Definition not_preemptive_implies_scheduled (j : Job) :=
 forall t,
 ~~ job_preemptable j (service sched j t) >
 scheduled_at sched j t.

 (** A job can start its execution only from a preemption point. *)
 Definition execution_starts_with_preemption_point (j : Job) :=
 forall prt,
 ~~ scheduled_at sched j prt >
 scheduled_at sched j prt.+1 >
 job_preemptable j (service sched j prt.+1).

 (** We say that a preemption model is a valid preemption model if
 all the assumptions given above are satisfied for any job. *)
 Definition valid_preemption_model :=
 forall j,
 arrives_in arr_seq j >
 job_cannot_become_nonpreemptive_before_execution j
 /\ job_cannot_be_nonpreemptive_after_completion j
 /\ not_preemptive_implies_scheduled j
 /\ execution_starts_with_preemption_point j.

 End ValidPreemptionModel.
+ (** In the following, we define the notion of a valid preemption model. To
+ begin with, we require that a job has to be executed at least one time
+ instant in order to reach a nonpreemptive segment. In other words, a job
+ must start execution to become nonpreemptive. *)
+ Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
+ job_preemptable j 0.
+
+ (** And vice versa, a job cannot remain nonpreemptive after its completion. *)
+ Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
+ job_preemptable j (job_cost j).
+
+ (** Next, if a job [j] is not preemptable at some time instant [t], then [j]
+ must be scheduled at time [t]. *)
+ Definition not_preemptive_implies_scheduled (j : Job) :=
+ forall t,
+ ~~ job_preemptable j (service sched j t) >
+ scheduled_at sched j t.
+
+ (** A job can start its execution only from a preemption point. *)
+ Definition execution_starts_with_preemption_point (j : Job) :=
+ forall prt,
+ ~~ scheduled_at sched j prt >
+ scheduled_at sched j prt.+1 >
+ job_preemptable j (service sched j prt.+1).
+
+ (** We say that a preemption model is a valid preemption model if
+ all assumptions given above are satisfied for any job. *)
+ Definition valid_preemption_model :=
+ forall j,
+ arrives_in arr_seq j >
+ job_cannot_become_nonpreemptive_before_execution j
+ /\ job_cannot_be_nonpreemptive_after_completion j
+ /\ not_preemptive_implies_scheduled j
+ /\ execution_starts_with_preemption_point j.
End PreemptionModel.
diff git a/restructuring/model/priority/classes.v b/restructuring/model/priority/classes.v
index e0a0708..ca8a406 100644
 a/restructuring/model/priority/classes.v
+++ b/restructuring/model/priority/classes.v
@@ 4,13 +4,19 @@ Require Export rt.util.list.
From mathcomp Require Export seq.
(** Definitions of FP, JLFP and JLDP priority relations. *)
+(** * The FP, JLFP, and JLDP Priority Classes *)
(** In the following, "hep" means "higher or equal priority". We define an FP
 policy as a relation among tasks, ... *)
+(** In this module, we define the three wellknown classes of priority
+ relations: (1) fixedpriority (FP) policies, (2) joblevel fixedpriority
+ (JLFP) polices, and (3) joblevel dynamicpriority (JLDP) policies, where
+ (2) is a subset of (3), and (1) a subset of (2). *)
+
+(** As a convention, we use "hep" to mean "higher or equal priority." *)
+
+(** We define an FP policy as a relation among tasks, ... *)
Class FP_policy (Task: TaskType) := hep_task : rel Task.
(** ... a JLFP policy as a relation among jobs, a ... *)
+(** ... a JLFP policy as a relation among jobs, and ... *)
Class JLFP_policy (Job: JobType) := hep_job : rel Job.
(** ... a JLDP policy as a relation among jobs that may vary over time. *)
@@ 19,88 +25,122 @@ Class JLDP_policy (Job: JobType) := hep_job_at : instant > rel Job.
(** NB: The preceding definitions currently make it difficult to express
priority policies in which the priority of a job at a given time varies
depending on the preceding schedule prefix (e.g., leastlaxity
 first). *)
+ first). That is, there is room for an even more general notion of a
+ scheduledependent JLDP policy, where the priority relation among jobs
+ may vary depending both on time and the schedule prefix prior to a
+ given time. This is left to future work. *)
+
+(** ** Automatic FP ➔ JLFP ➔ JLDP Conversion *)
+
+(** Since there are natural interpretations of FP and JLFP policies as JLFP and
+ JLDP policies, respectively, we define conversions that express these
+ generalizations. In practice, this means that Coq will be able to
+ automatically satisfy a JLDP assumption if a JLFP or FP policy is in
+ scope. *)
(** Since FP policies are also JLFP and JLDP policies, we define
 conversions that express the generalization. *)
+(** First, any FP policy can be interpreted as an JLFP policy by comparing jobs
+ according to the priorities of their respective tasks. *)
Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
`{JobTask Job Task} `{FP_policy Task} : JLFP_policy Job :=
fun j1 j2 => hep_task (job_task j1) (job_task j2).
+(** Second, any JLFP policy implies a JLDP policy that simply ignores the time
+ parameter. *)
Instance JLFP_to_JLDP (Job: JobType) `{JLFP_policy Job} : JLDP_policy Job :=
fun _ j1 j2 => hep_job j1 j2.
+(** ** Properties of Priority Policies *)
+
+(** In the following section, we define key properties of common priority
+ policies that proofs often depend on. *)
+
Section Priorities.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
 (** ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks, ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
+
+ (** .. and assume that jobs have a cost and an arrival time. *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
 (** In this section we define properties of JLDP policy. *)
+ (** In the following section, we define properties of JLDP policies, and by
+ extension also properties of FP and JLFP policies. *)
Section JLDP.
(** Consider any JLDP policy. *)
Context `{JLDP_policy Job}.
 (** We define common properties of the policy. Note that these definitions
 can also be used for JLFP and FP policies *)
+ (** We define what it means for a JLDP policy to be reflexive, transitive,
+ and total. Note that these definitions, although phrased in terms of a
+ given JLDP policy, can also be used for JLFP and FP policies due to the
+ abovedefined conversion instances. *)
+
+ (** A JLDP policy is reflexive if the relation among jobs is reflexive at
+ every point in time. *)
Definition reflexive_priorities := forall t, reflexive (hep_job_at t).
+ (** A JLDP policy is transitive if the relation among jobs is transitive at
+ every point in time. *)
Definition transitive_priorities := forall t, transitive (hep_job_at t).
+ (** A JLDP policy is total if the relation among jobs is total at
+ every point in time. *)
Definition total_priorities := forall t, total (hep_job_at t).
End JLDP.
 (** In this section we define properties of JLFP policy. *)
+ (** Next, we define a property of JLFP policies. *)
Section JLFP.

+
(** Consider any JLFP policy. *)
Context `{JLFP_policy Job}.
 (** Recall that a task is sequential if its jobs are executed in
 the order that they arrive.

 An arbitrary JLFP can violate the sequential tasks hypothesis.
 For example, consider two jobs j1, j2 of the same task such
 that [job_arrival j1 < job_arrival j2]. It is possible that the
 policy will assign a higher priority to the second job [i.e.,
 π(j1) < π(j2)]. But this situation contradicts the sequential
 tasks hypothesis.

 We say that a policy respects sequential tasks if for any two
 jobs j1, j2 from the same task the fact that [job_arrival j1 <=
 job_arrival j2] implies [π(j1) >= π(j2)]. *)
+ (** Recall that jobs of a sequential task are necessarily executed in the
+ order that they arrive.
+
+ An arbitrary JLFP policy, however, can violate the sequential tasks
+ hypothesis. For example, consider two jobs [j1], [j2] of the same task
+ such that [job_arrival j1 < job_arrival j2]. It is possible that a JLFP
+ priority policy [π] will assign a higher priority to the second job [π
+ j2 j1 = true]. But such a situation would contradict the natural
+ execution order of sequential tasks. It is therefore sometimes
+ necessary to restrict the space of JLFP policies to those that assign
+ priorities in a way that is consistent with sequential tasks.
+
+ To this end, we say that a policy respects sequential tasks if, for any
+ two jobs [j1], [j2] of the same task, [job_arrival j1 <= job_arrival j2]
+ implies [π j1 j2 = true]. *)
Definition policy_respects_sequential_tasks :=
forall j1 j2,
job_task j1 == job_task j2 >
job_arrival j1 <= job_arrival j2 >
hep_job j1 j2.

+
End JLFP.
 (** In this section we define properties of FP policy. *)
+ (** Finally, we we define and observe two properties of FP policies. *)
Section FP.

+
(** Consider any FP policy. *)
Context `{FP_policy Task}.
 (** We define whether the policy is antisymmetric over a task set [ts]. *)
+ (** To express the common assumption that task priorities are unique, we
+ define whether the given FP policy is antisymmetric over a task set
+ [ts]. *)
Definition antisymmetric_over_taskset (ts : seq Task) :=
 antisymmetric_over_list hep_task ts.

 (** Note that any FP_policy respects sequential tasks hypothesis,
 meaning that laterarrived jobs of a task don't have higher
 priority than earlierarrived jobs of the same task. *)
+ antisymmetric_over_list hep_task ts.
+
+ (** Further, we observe that any [FP_policy] respects the sequential tasks
+ hypothesis, meaning that laterarrived jobs of a task don't have higher
+ priority than earlierarrived jobs of the same task (assuming that task
+ priorities are reflexive). *)
Remark respects_sequential_tasks :
 reflexive_priorities >
 policy_respects_sequential_tasks.
+ reflexive_priorities > policy_respects_sequential_tasks.
Proof.
move => REFL j1 j2 /eqP EQ LT.
rewrite /hep_job /FP_to_JLFP EQ.
@@ 108,9 +148,9 @@ Section Priorities.
Qed.
End FP.

+
End Priorities.
(** We add the above lemma into a "Hint Database" basic_facts, so Coq
 will be able to apply them automatically. *)
+(** We add the above observation into the "Hint Database" basic_facts, so Coq
+ will be able to apply it automatically. *)
Hint Resolve respects_sequential_tasks : basic_facts.
diff git a/restructuring/model/priority/deadline_monotonic.v b/restructuring/model/priority/deadline_monotonic.v
index ff680b9..6236df7 100644
 a/restructuring/model/priority/deadline_monotonic.v
+++ b/restructuring/model/priority/deadline_monotonic.v
@@ 2,9 +2,9 @@ Require Export rt.restructuring.model.priority.classes.
(** * DeadlineMonotonic FixedPriority Policy *)
(** We define the notion of deadlinemonotonic task priorities, i.e., tasks are
 prioritized in order of their relative deadlines. The DM policy belongs to
 the class of FP policies. *)
+(** We define the notion of deadlinemonotonic task priorities, i.e., the
+ classic FP policy in which tasks are prioritized in order of their relative
+ deadlines. *)
Instance DM (Task : TaskType) `{TaskDeadline Task} : FP_policy Task :=
{
hep_task (tsk1 tsk2 : Task) := task_deadline tsk1 <= task_deadline tsk2
diff git a/restructuring/model/priority/edf.v b/restructuring/model/priority/edf.v
index 16f4709..6aaa625 100644
 a/restructuring/model/priority/edf.v
+++ b/restructuring/model/priority/edf.v
@@ 2,8 +2,9 @@ Require Export rt.restructuring.model.priority.classes.
(** * EDF Priority Policy *)
(** We introduce the notion of EDF priorities, wherein jobs are scheduled in
 order of their urgency. The EDF policy belongs to the class of JLFP
+(** We introduce the classic EDF priority policy, under which jobs are
+ scheduled in order of their urgency, i.e., jobs are ordered according to
+ their absolute deadlines. The EDF policy belongs to the class of JLFP
policies. *)
Instance EDF (Job : JobType) `{JobDeadline Job} : JLFP_policy Job :=
{
diff git a/restructuring/model/priority/fifo.v b/restructuring/model/priority/fifo.v
index 2e16246..67dfb09 100644
 a/restructuring/model/priority/fifo.v
+++ b/restructuring/model/priority/fifo.v
@@ 2,9 +2,9 @@ Require Export rt.restructuring.model.priority.classes.
(** * FIFO Priority Policy *)
(** We define the notion of FIFO priorities, i.e., jobs are prioritized in
 order of their arrival times. The FIFO policy belongs to the class of JLFP
 policies. *)
+(** We define the basic FIFO priority policy, under which jobs are prioritized
+ in order of their arrival times. The FIFO policy belongs to the class of
+ JLFP policies. *)
Instance FIFO (Job : JobType) `{JobArrival Job} : JLFP_policy Job :=
{
hep_job (j1 j2 : Job) := job_arrival j1 <= job_arrival j2
diff git a/restructuring/model/priority/numeric_fixed_priority.v b/restructuring/model/priority/numeric_fixed_priority.v
index 689f61b..c86717b 100644
 a/restructuring/model/priority/numeric_fixed_priority.v
+++ b/restructuring/model/priority/numeric_fixed_priority.v
@@ 5,13 +5,12 @@ Require Export rt.restructuring.model.priority.classes.
(** We define the notion of arbitrary numeric fixed task priorities, i.e.,
tasks are prioritized in order of userprovided numeric priority values,
where numerically smaller values indicate lower priorities (as for instance
 it is the case in POSIX). *)
+ it is the case in Linux). *)
(** First, we define a new task parameter [task_priority] that maps each task
to a numeric priority value. *)
Class TaskPriority (Task : TaskType) := task_priority : Task > nat.

(** Based on this parameter, we define the corresponding FP policy. *)
Instance NumericFP (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
{
diff git a/restructuring/model/priority/rate_monotonic.v b/restructuring/model/priority/rate_monotonic.v
index 3ab5fa7..7d17f26 100644
 a/restructuring/model/priority/rate_monotonic.v
+++ b/restructuring/model/priority/rate_monotonic.v
@@ 1,12 +1,12 @@
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.model.arrival.sporadic.
+Require Export rt.restructuring.model.task.arrival.sporadic.
(** * RateMonotonic FixedPriority Policy *)
(** We define the notion of ratemonotonic task priorities, i.e., tasks are
 prioritized in order of their minimum interarrival times (or periods). The
 RM policy belongs to the class of FP policies. *)
+(** We define the notion of ratemonotonic task priorities for sporadic tasks,
+ i.e., the classic FP policy in which sporadic tasks are prioritized in
+ order of their minimum interarrival times (or periods). *)
Instance RM (Task : TaskType) `{SporadicModel Task} : FP_policy Task :=
{
hep_task (tsk1 tsk2 : Task) := task_min_inter_arrival_time tsk1 <= task_min_inter_arrival_time tsk2
diff git a/restructuring/model/processor/ideal.v b/restructuring/model/processor/ideal.v
index 8d95975..70ceea8 100644
 a/restructuring/model/processor/ideal.v
+++ b/restructuring/model/processor/ideal.v
@@ 1,45 +1,66 @@
From mathcomp Require Import all_ssreflect.
Require Export rt.restructuring.behavior.all.
+(** * The Ideal Uniprocessor Model *)
(** First let us define the notion of an ideal schedule state, as done in Prosa
 so far: either a job is scheduled or the system is idle. *)
+
+(** In this module, we define a central piece of the Prosa model: the notion of
+ an ideal uniprocessor state. The word "ideal" here refers to the complete
+ absence of runtime overheads or any other complications. In an ideal
+ uniprocessor schedule, there are only two possible cases: at a given time,
+ either a specific job is scheduled and makes unitprogress, or the
+ processor is idle. To model this, we simply reuse the standard [option]
+ type from the Coq standard library. *)
Section State.
+ (** Consider any type of jobs. *)
Variable Job: JobType.
+ (** We define the ideal "processor state" as an [option Job], which means
+ that it is either [Some j] (where [j] is a [Job]) or [None] (which we use
+ to indicate an idle instant). *)
Definition processor_state := option Job.
 Global Program Instance pstate_instance : ProcessorState Job (option Job) :=
+ (** Based on this definition, we say that a given job [j] is scheduled in a
+ given state [s] iff [s] is [Some j]. *)
+ Let ideal_scheduled_at (j : Job) (s : processor_state) := s == Some j.
+
+ (** Similarly, we say that a given job [j] receives service in a given state
+ [s] iff [s] is [Some j]. *)
+ Let ideal_service_in (j : Job) (s : processor_state) := s == Some j.
+
+ (** Next, we connect the justdefined notion of an ideal processor state with
+ the generic interface for the processorstate abstraction in Prosa by
+ declaring a socalled instance of the [ProcessorState] typeclass. *)
+ Global Program Instance pstate_instance : ProcessorState Job processor_state :=
{
(** As this is a uniprocessor model, cores are implicitly defined
 as the unit type containing a single element as a placeholder. *)
 scheduled_on j s (_ : unit) := s == Some j;
 service_in j s := s == Some j;
+ as the [unit] type containing a single element as a placeholder. *)
+ scheduled_on j s (_ : unit) := ideal_scheduled_at j s;
+ service_in j s := ideal_service_in j s;
}.
Next Obligation.
 rewrite /nat_of_bool.
 case: ifP H=>//=_/existsP[].
+ rewrite /ideal_service_in /nat_of_bool.
+ case: ifP H =>//= SOME /existsP[].
by exists tt.
Defined.
End State.
(** In this section we define the notion of idleness for ideal uniprocessor. *)
+(** ** Idle Instants *)
+
+(** In this section, we define the notion of idleness for ideal uniprocessor
+ schedules. *)
Section IsIdle.

 (** Consider any type of job. *)
+
+ (** Consider any type of jobs... *)
Context {Job : JobType}.
 Context `{JobArrival Job}.
 Context `{JobCost Job}.

 (** Consider any arrival sequence... *)
Variable arr_seq : arrival_sequence Job.

 (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
+
+ (** ... and any ideal uniprocessor schedule of such jobs. *)
Variable sched : schedule ((*ideal*)processor_state Job).

+
(** We say that the processor is idle at time t iff there is no job being scheduled. *)
Definition is_idle (t : instant) := sched t == None.
End IsIdle.
\ No newline at end of file
+End IsIdle.
diff git a/restructuring/model/processor/multiprocessor.v b/restructuring/model/processor/multiprocessor.v
index cbe33c8..9c13ebc 100644
 a/restructuring/model/processor/multiprocessor.v
+++ b/restructuring/model/processor/multiprocessor.v
@@ 1,22 +1,65 @@
From mathcomp Require Export fintype.
Require Export rt.restructuring.behavior.all.
+(** * Multiprocessor State *)
+
+(** In the following, we define a model of identical multiprocessors, i.e., of
+ processors with multiple cores of identical capabilities. The
+ multiprocessor model is generic in the type of processor state of the
+ cores. That is, it is possible to combine any uniprocessor state (such as
+ the ideal state) with the following generic multiprocessor
+ construction. (In fact, by combining the below multiprocessor model with
+ variable speed processors, it is even possible to obtain a socalled
+ uniform multiprocessor model.)
+
+ NB: For now, the definition serves only to document how this can be done;
+ it is not actually used anywhere in the library. *)
+
Section Schedule.
+ (** Consider any types of jobs... *)
Variable Job: JobType.
+
+ (** ... and consider any type of perprocessor state. *)
Variable processor_state: Type.
Context `{ProcessorState Job processor_state}.
+ (** Given a desired number of processors [num_cpus], we define a finite type
+ of integers from 0 to [num_cpus  1]. The purpose of this definition is
+ to obtain a finite type (i.e., set of values) that can be enumerated in a
+ terminating computation.
+
+ Syntax hint: the ['I_] before [num_cpus] is ssreflect syntax for the
+ finite set of integers from zero to [num_cpus  1]. *)
Definition processor (num_cpus: nat) := 'I_num_cpus.
+ (** Next, for any given number of processors [num_cpus]... *)
Variable num_cpus : nat.
 Definition identical_state := processor num_cpus > processor_state.
+ (** ...we represent the type of the "multiprocessor state" as a function that
+ maps processor IDs (as defined by [processor num_cpus], see above) to the
+ given state on each core. *)
+ Definition multiprocessor_state := processor num_cpus > processor_state.
+
+ (** Based on this notion of multiprocessor state, we say that a given job [j]
+ is currently scheduled on a specific processor [cpu], according to the
+ given multiprocessor state [mps], if [j] is scheduled in the
+ processorlocal state [(mps cpu)]. *)
+ Let multiproc_scheduled_on (j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
+ := scheduled_in j (mps cpu).
+
+ (** The service received by a given job [j] in a given multiprocessor state
+ [mps] is given by the sum of the service received across all individual
+ processors of the multiprocessor. *)
+ Let multiproc_service_in (j : Job) (mps : multiprocessor_state)
+ := \sum_(cpu < num_cpus) service_in j (mps cpu).
 Global Program Instance multiproc_state : ProcessorState Job (identical_state) :=
+ (** Finally, we connect the above definitions with the generic Prosa
+ interface for processor models. *)
+ Global Program Instance multiproc_state : ProcessorState Job multiprocessor_state :=
{
 scheduled_on j s (cpu : processor num_cpus) := scheduled_in j (s cpu);
 service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
+ scheduled_on := multiproc_scheduled_on;
+ service_in := multiproc_service_in
}.
Next Obligation.
move: j s H0.
diff git a/restructuring/model/processor/platform_properties.v b/restructuring/model/processor/platform_properties.v
index 4fe220a..bf5e482 100644
 a/restructuring/model/processor/platform_properties.v
+++ b/restructuring/model/processor/platform_properties.v
@@ 1,23 +1,25 @@
Require Export rt.restructuring.behavior.all.
(** To reason about classes of schedule types / processor models, we define the
 following properties that a processor model might possess. *)
+ following properties that group processor models into classes of similar
+ models. *)
Section ProcessorModels.
 (** Consider any job type and any processor state. Note: we make the
 processor state an explicit variable (rather than implicit
 context) because it is the primary subject of the following
+ (** Consider any job type and any processor state.
+
+ Note: we make the processor state an explicit variable (rather than
+ implicit context) because it is the primary subject of the following
definitions. *)
Context {Job : JobType}.
Variable PState : Type.
Context `{ProcessorState Job PState}.
 (** We say that a processor model provides unit service if no
 job ever receives more than one unit of service at any time. *)
+ (** We say that a processor model provides unit service if no job ever
+ receives more than one unit of service at any time. *)
Definition unit_service_proc_model :=
forall (j : Job) (s : PState), service_in j s <= 1.
(** We say that a processor model offers ideal progress if a scheduled job
 always receives nonzero service. *)
+ always receives nonzero service. *)
Definition ideal_progress_proc_model :=
forall j s, scheduled_in j s > service_in j s > 0.
diff git a/restructuring/model/processor/spin.v b/restructuring/model/processor/spin.v
index 9013e1b..42d2362 100644
 a/restructuring/model/processor/spin.v
+++ b/restructuring/model/processor/spin.v
@@ 1,29 +1,43 @@
From mathcomp Require Import all_ssreflect.
Require Export rt.restructuring.behavior.all.
(** Next we define a processor state that includes the possibility of spinning,
 where spinning jobs do not progress (= don't get service). *)
+(** In the following, we define a processor state that includes the possibility
+ of spinning, where spinning jobs do not progress (= don't get any service).
+
+ NB: For now, the definition serves only to document how this can be done;
+ it is not actually used anywhere in the library. *)
Section State.
+ (** Consider any type of jobs. *)
Variable Job: JobType.
+ (** We define the state of a processor at a given time to be one of three
+ possible cases: either a specific job is scheduled and makes progress
+ [Progress j], a specific job is scheduled but makes not useful progress
+ [Spin j], or the processor is idle [Idle]. *)
Inductive processor_state :=
Idle
 Spin (j : Job)
 Progress (j : Job).
+ (** Next, we define the semantics of the processor state with spinning. *)
Section Service.
+ (** Let [j] denote any job. *)
Variable j : Job.
 Definition scheduled_on (s : processor_state) (_ : unit) : bool :=
+ (** It is scheduled in a given state [s] iff the state is not idle and [j]
+ is the job mentioned in the state. *)
+ Definition spin_scheduled_on (s : processor_state) (_ : unit) : bool :=
match s with
 Idle => false
 Spin j' => j' == j
 Progress j' => j' == j
end.
 Definition service_in (s : processor_state) : nat :=
+ (** In contrast, job [j] receives service only if the given state [s] is
+ [Progress j]. *)
+ Definition spin_service_in (s : processor_state) : nat :=
match s with
 Idle => 0
 Spin j' => 0
@@ 32,10 +46,12 @@ Section State.
End Service.
+ (** Finally, we connect the above definitions with the generic Prosa
+ interface for abstract processor states. *)
Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
{
 scheduled_on := scheduled_on;
 service_in := service_in
+ scheduled_on := spin_scheduled_on;
+ service_in := spin_service_in
}.
Next Obligation.
move: H.
diff git a/restructuring/model/processor/varspeed.v b/restructuring/model/processor/varspeed.v
index 3073edd..4e9967b 100644
 a/restructuring/model/processor/varspeed.v
+++ b/restructuring/model/processor/varspeed.v
@@ 1,26 +1,41 @@
From mathcomp Require Import all_ssreflect.
Require Export rt.restructuring.behavior.all.
(** Next, let us define a schedule with variable execution speed. *)
+(** In the following, we define a model of processors with variable execution
+ speeds.
+
+ NB: For now, the definition serves only to document how this can be done;
+ it is not actually used anywhere in the library. *)
+
Section State.
+ (** Consider any type of jobs. *)
Variable Job: JobType.
+ (** We define the state of a variablespeed processor at a given time to be
+ one of two possible cases: either a specific job is scheduled and
+ progresses with a specific speed, or the processor is idle. *)
Inductive processor_state :=
Idle
 Progress (j : Job) (speed : nat).
+ (** Next, we define the semantics of the variablespeed processor state. *)
Section Service.
+ (** Consider any job [j]. *)
Variable j : Job.
 Definition scheduled_on (s : processor_state) (_ : unit) : bool :=
+ (** Job [j] is scheduled in a given state [s] if [s] is not idle and [j]
+ matches the job recorded in [s]. *)
+ Definition varspeed_scheduled_on (s : processor_state) (_ : unit) : bool :=
match s with
 Idle => false
 Progress j' _ => j' == j
end.
 Definition service_in (s : processor_state) : nat :=
+ (** If it is scheduled in state [s], job [j] receives service proportional
+ to the speed recorded in the state. *)
+ Definition varspeed_service_in (s : processor_state) : nat :=
match s with
 Idle => 0
 Progress j' speed => if j' == j then speed else 0
@@ 28,10 +43,12 @@ Section State.
End Service.
+ (** Finally, we connect the above definitions to the generic Prosa interface
+ for processor states. *)
Global Program Instance pstate_instance : ProcessorState Job processor_state :=
{
 scheduled_on := scheduled_on;
 service_in := service_in
+ scheduled_on := varspeed_scheduled_on;
+ service_in := varspeed_service_in
}.
Next Obligation.
move: H.
diff git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index 9f133b1..5c94fd6 100644
 a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ 1,8 +1,10 @@
Require Export rt.restructuring.behavior.all.
(** We define the readiness indicator function for the classic Liu & Layland
 model without jitter and no selfsuspensions, where jobs are always
 ready. *)
+(** * Liu & Layland Readiness Model *)
+
+(** In this module, we define the notion of job readiness for the classic Liu &
+ Layland model without jitter or selfsuspensions, where pending jobs are
+ simply always ready. *)
Section LiuAndLaylandReadiness.
(** Consider any kind of jobs... *)
diff git a/restructuring/model/readiness/jitter.v b/restructuring/model/readiness/jitter.v
index 6079837..d7579df 100644
 a/restructuring/model/readiness/jitter.v
+++ b/restructuring/model/readiness/jitter.v
@@ 3,12 +3,21 @@ Require Export rt.restructuring.behavior.all.
Require Import rt.util.nat.
(** We define the readiness indicator function for models with release jitter
 (and no selfsuspensions). *)
(** Definition of a generic type of release jitter parameter. *)
+(** * Job Model Parameter for Jobs Exhibiting Release Jitter *)
+
+(** If a job exhibits release jitter, it is not immediately available for
+ execution upon arrival, and can be scheduled only after its release, which
+ occurs some (bounded) time after its arrival. We model this with the
+ [job_jitter] parameter, which maps each job to its jitter duration. *)
+
Class JobJitter (Job : JobType) := job_jitter : Job > duration.
+(** * Readiness of Jobs with Release Jitter *)
+
+(** Based on the job model's jitter parameter, we define the readiness
+ predicate for jogs with release jitter (and no selfsuspensions). *)
+
Section ReadinessOfJitteryJobs.
(** Consider any kind of jobs... *)
Context {Job : JobType}.
@@ 17,15 +26,16 @@ Section ReadinessOfJitteryJobs.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
 (** Suppose jobs have an arrival time, a cost, and a release jitter bound. *)
+ (** Suppose jobs have an arrival time, a cost, and exhibit release jitter. *)
Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.
 (** We say that a job is released at a time after its arrival if the job's
 release jitter has passed. *)
+ (** We say that a job is released at a time [t] after its arrival if the
+ job's release jitter has passed. *)
Definition is_released (j : Job) (t : instant) := job_arrival j + job_jitter j <= t.
 (** A job that experiences jitter is ready only when the jitterinduced delay
 has passed after its arrival and if it is not yet complete. *)
+ (** Based on the predicate [is_released], it is easy to state the notion of
+ readiness for jobs subject to release jitter: a job is ready only if it
+ is released and not yet complete. *)
Global Program Instance jitter_ready_instance : JobReady Job PState :=
{
job_ready sched j t := is_released j t && ~~ completed_by sched j t
diff git a/restructuring/model/readiness/suspension.v b/restructuring/model/readiness/suspension.v
index 998b6f4..b6c2e52 100644
 a/restructuring/model/readiness/suspension.v
+++ b/restructuring/model/readiness/suspension.v
@@ 2,20 +2,21 @@ Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.definitions.progress.
Require Export rt.util.nat.
(** * Job Parameter for Jobs Exhibiting SelfSuspensions *)
+(** * Job Model Parameter for Jobs Exhibiting SelfSuspensions *)
(** We define a job's selfsuspension parameter as follows: after having
received a given number of units of service [rho], a job [j] may either
 selfsuspend for a given duration [d], in which case
 [job_suspension j rho = d], or it may remain ready, in which case
 [job_suspension j rho = 0]. Note that a job may selfsuspend before
 having received any service, which is equivalent to release jitter. *)
+ selfsuspend for a given duration [d], in which case [job_suspension j rho
+ = d], or it may remain ready, in which case [job_suspension j rho =
+ 0]. Note that a job may selfsuspend before having received any service,
+ which is equivalent to release jitter. (Suspensions after a job has
+ completed are meaningless and irrelevant.) *)
Class JobSuspension (Job : JobType) := job_suspension : Job > work > duration.
(** * Readiness of SelfSuspending Jobs *)
(** In the following section, we define the notion of "readiness" for
 selfsuspending jobs. *)
+ selfsuspending jobs based on the justdefined jobmodel parameter. *)
Section ReadinessOfSelfSuspendingJobs.
(** Consider any kind of jobs... *)
Context {Job : JobType}.
@@ 24,20 +25,25 @@ Section ReadinessOfSelfSuspendingJobs.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
 (** Suppose jobs have an arrival time, a cost, and exhibit selfsuspensions. *)
+ (** Suppose jobs have an arrival time, a cost, and that they exhibit
+ selfsuspensions. *)
Context `{JobArrival Job} `{JobCost Job} `{JobSuspension Job}.
 (** We say that a job's last suspension (if any) of length [delay] has
 passed at a given time [t] (i.e., the job is ready again) if the job
 arrived at least [delay] time units ago and has not progressed within
 the last [delay] time units. *)
+ (** We say that a job's last suspension (if any) of length [delay] "has
+ passed" at a given time [t] (i.e., the job is ready again at time [t]) if
+ the job arrived at least [delay] time units ago and has not progressed
+ within the last [delay] time units. In other words, since a
+ selfsuspension can start only when a job progresses (i.e., when it
+ receives some service), if a job has not been making progress in the last
+ [delay] time units, then a selfsuspension of length [delay] has
+ necessarily ended at time [t]. *)
Definition suspension_has_passed (sched : schedule PState) (j : Job) (t : instant) :=
let delay := job_suspension j (service sched j t) in
(job_arrival j + delay <= t) && no_progress_for sched j t delay.
 (** Based on [suspensions_has_passed], we define the readiness model for
 selfsuspending jobs: a job is ready only when it is not selfsuspended
 and if it is not yet complete. *)
+ (** Based on [suspension_has_passed], we state the notion of readiness for
+ selfsuspending jobs: a job [t] is ready at time [t] in a schedule
+ [sched] only if it is not selfsuspended or complete at time [t]. *)
Global Program Instance suspension_ready_instance : JobReady Job PState :=
{
job_ready sched j t := suspension_has_passed sched j t && ~~ completed_by sched j t
@@ 54,7 +60,7 @@ End ReadinessOfSelfSuspendingJobs.
(** * Total Suspension Time of a Job *)
(** Next, we define the notion of a job's cumulative suspension time. *)
+(** Next, we define the notion of a job's cumulative and total suspension times. *)
Section TotalSuspensionTime.
diff git a/restructuring/model/schedule/edf.v b/restructuring/model/schedule/edf.v
index 439fcf2..4d05ba0 100644
 a/restructuring/model/schedule/edf.v
+++ b/restructuring/model/schedule/edf.v
@@ 1,24 +1,48 @@
From mathcomp Require Import ssrnat ssrbool fintype.
Require Export rt.restructuring.behavior.all.
(** In this file, we define what it means to be an "EDF schedule". *)
Section DefinitionOfEDF.
+(** * FullyPreemptive EDF Schedules *)
 (** For any given type of jobs... *)
+(** This module provides an alternative definition of what it means to be an
+ "EDF schedule".
+
+ Note that the "proper" way to define an EDF schedule in Prosa is to use the
+ EDF priority policy defined in model.priority.edf and the notion of
+ prioritycompliant schedules defined in model.schedule.priority_driven, as
+ well as the general notion of workconservation provided in
+ model.schedule.work_conserving, which will have the benefit of taking into
+ account issues such as various readiness models (e.g., jitter) and diverse
+ preemption models (e.g., limitedpreemptive jobs).
+
+ The simpler definition offered in this module is (intentionally) oblivious
+ to (i.e., not compatible with) issues such as nonpreemptive regions or
+ selfsuspensions, and does not imply anything about workconservation. In
+ other words, it implicitly assumes that pending jobs are always ready and
+ at all times preemptable.
+
+ The advantage of this alternative definition is, however, that it is
+ largely selfcontained and fairly simple, following primarily from first
+ principles. This makes it easier to use in certain contexts such as the
+ proof of optimality of EDF. *)
+
+Section AlternativeDefinitionOfEDF.
+
+ (** Consider any type of jobs with arrival times, costs, and deadlines ... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
 (** ... any given type of processor states: *)
+ (** ... and any processor model. *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
 (** We say that a schedule is locally an EDF schedule at a point in
 time [t] if the job scheduled at time [t] has a deadline that is
 earlier than or equal to the deadline of any other job that could
 be scheduled at time t but is scheduled later.
+ (** We say that a schedule is _locally EDFcompliant_ at a given point in
+ time [t] if the job [j] scheduled at time [t] has a deadline that is
+ earlier than or equal to the deadline of any other job [j'] that could be
+ scheduled at time [t] (i.e., arrives at or before time [t]) but is
+ actually scheduled later in the given schedule.
 Note that this simple definition is (intentionally) oblivious to
 (i.e., not compatible with) issues such as nonpreemptive regions
 or selfsuspensions. *)
+ In other words, a schedule is locally EDFcompliant at time [t] if there
+ is no witness of a priority inversion (= an already arrived job with an
+ earlier deadline) at a later point in the schedule. *)
Definition EDF_at (sched: schedule PState) (t: instant) :=
forall (j: Job),
scheduled_at sched j t >
@@ 28,10 +52,13 @@ Section DefinitionOfEDF.
job_arrival j' <= t >
job_deadline j <= job_deadline j'.
 (** A schedule is an EDF schedule if it is locally EDF at every point in time. *)
 Definition is_EDF_schedule (sched: schedule PState) := forall t, EDF_at sched t.
+ (** Based on the notion of a locally EDFcompliant schedule given by
+ [EDF_at], we say that a schedule is (globally) EDFcompliant
+ schedule if it is locally EDFcompliant at every point in
+ time. *)
+ Definition EDF_schedule (sched: schedule PState) := forall t, EDF_at sched t.
End DefinitionOfEDF.
+End AlternativeDefinitionOfEDF.
diff git a/restructuring/model/schedule/limited_preemptive.v b/restructuring/model/schedule/limited_preemptive.v
index a69d30d..3bf9458 100644
 a/restructuring/model/schedule/limited_preemptive.v
+++ b/restructuring/model/schedule/limited_preemptive.v
@@ 1,29 +1,31 @@
Require Export rt.restructuring.model.preemption.parameter.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
+(** * Preemption Model Compliance *)
(** * Schedule with Limited Preemptions *)
(** In this section we introduce the notion of preemptionsaware
 schedule. *)
+(** A preemption model restricts when jobs can be preempted. In this
+ module, we specify the corresponding semantics, i.e., how a valid
+ schedule must be restricted to be compliant with a given
+ preemption model. *)
Section ScheduleWithLimitedPreemptions.
 (** Consider any type of jobs. *)
+ (** Consider any type of jobs, ... *)
Context {Job : JobType}.
 Context `{JobArrival Job}.
 Context `{JobCost Job}.
+
+ (** ... any processor model, ... *)
+ Context {PState : Type} `{ProcessorState Job PState}.
+
+ (** ... and any preemption model. *)
Context `{JobPreemptable Job}.
 (** Consider any arrival sequence. *)
+ (** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
 (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
 Variable sched : schedule (ideal.processor_state Job).
+ (** ... and a schedule of the jobs in the arrival sequence. *)
+ Variable sched : schedule PState.
 (** Based on the definition of the model with preemption points,
 we define a valid schedule with limited preemptions. *)
 Definition valid_schedule_with_limited_preemptions :=
+ (** We say that a schedule respects the preemption model given by
+ [job_preemptable] if nonpreemptable jobs remain scheduled. *)
+ Definition schedule_respects_preemption_model :=
forall j t,
arrives_in arr_seq j >
~~ job_preemptable j (service sched j t) >
diff git a/restructuring/model/schedule/nonpreemptive.v b/restructuring/model/schedule/nonpreemptive.v
index 18320a0..05e1852 100644
 a/restructuring/model/schedule/nonpreemptive.v
+++ b/restructuring/model/schedule/nonpreemptive.v
@@ 1,27 +1,28 @@
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export rt.restructuring.behavior.all.
(** In this section we introduce the notion of a nonpreemptive schedule. *)
+(** * Nonpreemptive Schedules *)
+
+(** In this module, we introduce a simple alternative definition of
+ nonpreemptive schedules. Take also note of the fully nonpreemptive
+ preemption model in model.preemption.fully_nonpreemptive. *)
+
Section NonpreemptiveSchedule.
 (** Consider any type of jobs ... *)
+ (** Consider any type of jobs with execution costs ... *)
Context {Job : JobType}.
 Context `{JobArrival Job}.
Context `{JobCost Job}.
 (** ... and any kind of processor state model. *)
+ (** ... and any kind of processor model. *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
 (** Consider any uniprocessor schedule. *)
 Variable sched : schedule PState.

 (** We define a schedule to be nonpreemptive iff every job remains scheduled until completion. *)
 Definition is_nonpreemptive_schedule :=
+ (** We say that a given schedule is _nonpreemptive_ if every job,
+ once it is scheduled, remains scheduled until completion. *)
+ Definition nonpreemptive_schedule (sched : schedule PState) :=
forall (j : Job) (t t' : instant),
t <= t' >
scheduled_at sched j t >
~~ completed_by sched j t' >
scheduled_at sched j t'.
End NonpreemptiveSchedule.
\ No newline at end of file
+End NonpreemptiveSchedule.
diff git a/restructuring/model/schedule/preemption_time.v b/restructuring/model/schedule/preemption_time.v
index df873a2..8fb1777 100644
 a/restructuring/model/schedule/preemption_time.v
+++ b/restructuring/model/schedule/preemption_time.v
@@ 1,36 +1,36 @@
Require Export rt.restructuring.model.preemption.parameter.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Preemption Times *)
+
+(** The preemption framework defines a generic predicate [job_preemptable] as
+ the interface to various preemption models. Crucially, [job_preemptable]
+ does not depend on the current schedule or the current time, but only on
+ the job's progress, i.e., it indicates the presence or absence of a
+ preemption _point_ in the job's execution. In this section, we define the
+ notion of a preemption _time_ in an ideal uniprocessor schedule base on the
+ progress of the currently scheduled job.
+
+ NB: For legacy reasons, the following definition are currently specific to
+ ideal uniprocessor schedules. Lifting this assumption is future work. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
+Require rt.restructuring.model.processor.ideal.
(** * Preemption Time in Ideal UniProcessor Model *)
(** In this section we define the notion of preemption _time_ for
 ideal uniprocessor model. *)
Section PreemptionTime.
 (** Consider any type of jobs... *)
+ (** Consider any type of jobs, ... *)
Context {Job : JobType}.
 Context `{JobArrival Job}.
 Context `{JobCost Job}.
 (** ... and assume the existence of a function mapping a job and
 its progress to a boolean value saying whether this job is
 preemptable at its current point of execution. *)
+ (** ... any preemption model, ... *)
Context `{JobPreemptable Job}.
 (** Consider any arrival sequence with consistent arrivals. *)
 Variable arr_seq : arrival_sequence Job.
 Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

 (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+ (** ... and any ideal uniprocessor schedule of such jobs. *)
Variable sched : schedule (ideal.processor_state Job).
 Hypothesis H_jobs_come_from_arrival_sequence:
 jobs_come_from_arrival_sequence sched arr_seq.
 (** We say that a time instant t is a preemption time iff the job
 that is currently scheduled at t can be preempted (according to
 the predicate). *)
+ (** We say that a time [t] is a preemption time iff the job that is currently
+ scheduled at [t], if any, can be preempted according to the predicate
+ [job_preemptable] (which encodes the preemption model). An idle instant
+ is always a preemption time. *)
Definition preemption_time (t : instant) :=
if sched t is Some j then
job_preemptable j (service sched j t)
diff git a/restructuring/model/schedule/priority_driven.v b/restructuring/model/schedule/priority_driven.v
index bdee41e..49845a6 100644
 a/restructuring/model/schedule/priority_driven.v
+++ b/restructuring/model/schedule/priority_driven.v
@@ 1,36 +1,49 @@
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.model.schedule.preemption_time.
(** We now define what it means for a schedule to respect a priority
 in the presence of jobs with nonpreemptive segments. *)
(** We only define it for a JLDP policy since the definitions for JLDP
 and JLFP are the same and can be used through the conversions. *)
+(** * PriorityDriven Schedules *)
+
+(** We now define what it means for a schedule to respect a priority in the
+ presence of jobs with nonpreemptive segments. We only specify a
+ definition for JLDP policies since JLFP and FP policies can be used with
+ this definition through the canonical conversions (see
+ model.priority.classes).
+
+ NB: For legacy reasons, the below definition is currently specific to ideal
+ uniprocessor schedules. Removal of this limitation is future work. *)
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require rt.restructuring.model.processor.ideal.
+
Section Priority.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
 Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
+
+ (** Suppose jobs have an arrival time, a cost, ... *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
+
+ (** ... and consider any preemption model and notion of readiness. *)
Context `{JobPreemptable Job}.
Context `{JobReady Job (ideal.processor_state Job)}.
 (** Consider any job arrival sequence... *)
+ (** Given any job arrival sequence... *)
Variable arr_seq : arrival_sequence Job.

 (** ...and any uniprocessor schedule of these jobs. *)
+
+ (** ...and an ideal uniprocessor schedule of these jobs, *)
Variable sched : schedule (ideal.processor_state Job).
 (** We say that a JLDP policy ...*)
+ (** we say that a JLDP policy ...*)
Context `{JLDP_policy Job}.

 (** ...is respected by the schedule iff, at every preemption point,
 a scheduled task has higher (or same) priority than (as) any
 backlogged job. *)
+
+ (** ...is respected by the schedule iff, at every preemption point, the
+ priority of the scheduled job is higher than or equal to the priority of
+ any backlogged job. *)
Definition respects_policy_at_preemption_point :=
forall j j_hp t,
arrives_in arr_seq j >
@@ 40,3 +53,4 @@ Section Priority.
hep_job_at t j_hp j.
End Priority.
+
diff git a/restructuring/model/schedule/tdma.v b/restructuring/model/schedule/tdma.v
index 6175d3d..24ee5d5 100644
 a/restructuring/model/schedule/tdma.v
+++ b/restructuring/model/schedule/tdma.v
@@ 1,37 +1,49 @@
Require Export rt.restructuring.model.task.concept.
Require Export rt.util.seqset.
Require Export rt.util.rel.
From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
+From mathcomp Require Import div.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
+Require rt.restructuring.model.processor.ideal.
(** In this section, we define the TDMA policy.*)
Section TDMAPolicy.
+(** * TDMA Scheduling *)
+
+(** The TDMA scheduling policy is based on two properties.
+ (1) Each task has a fixed, reserved time slot for execution;
+ (2) These time slots are ordered in sequence to form a TDMA cycle, which
+ repeats along the timeline.
+ An example of TDMA schedule is illustrated in the following.
+<<
+ _______________________________
+  s1  s2 s3 s1  s2 s3...
+ >
+ 0 t
+>> *)
 (** The TDMA policy is based on two properties.
 (1) Each task has a fixed, reserved time slot for execution;
 (2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
 An example of TDMA schedule is illustrated in the following.
 ______________________________
  s1  s2 s3 s1  s2 s3...
 >
 0 t
 *)
+(** ** Task Parameter for TDMA Scheduling *)
+
+(** We define the TDMA policy as follows.*)
+Section TDMAPolicy.
Variable Task: eqType.
(** With each task, we associate the duration of the corresponding TDMA slot. *)
Definition TDMA_slot := Task > duration.
 (** Moreover, within each TDMA cycle, task slots are ordered according to some relation.
 (i.e, slot_order slot1 slot2 means that slot1 comes before slot2 in a TDMA cycle) *)
+ (** Moreover, within each TDMA cycle, task slots are ordered according to
+ some relation (i.e, [slot_order slot1 slot2] means that [slot1] comes
+ before [slot2] in a TDMA cycle). *)
Definition TDMA_slot_order := rel Task.
End TDMAPolicy.
+(** We introduce slots and the slot order as task parameters. *)
Class TDMAPolicy (T : TaskType) :=
 { task_time_slot : TDMA_slot T;
 slot_order : TDMA_slot_order T }.
+ {
+ task_time_slot : TDMA_slot T;
+ slot_order : TDMA_slot_order T
+ }.
+
+(** ** TDMA Policy Validity *)
(** First, we define the properties of a valid TDMA policy. *)
Section ValidTDMAPolicy.
@@ 64,7 +76,9 @@ Section ValidTDMAPolicy.
End ValidTDMAPolicy.
(** In this section, we define functions on a TDMA policy *)
+ (** ** TDMA Cycles, Sots, and Offsets *)
+
+(** In this section, we define key TDMA concepts. *)
Section TDMADefinitions.
Context {Task : eqType}.
@@ 79,18 +93,22 @@ Section TDMADefinitions.
Definition TDMA_cycle:=
\sum_(tsk < ts) task_time_slot tsk.
 (** We define the function returning the slot offset for each task:
 i.e., the distance between the start of the TDMA cycle and
 the start of the task time slot *)
+ (** We define the function returning the slot offset for each task: i.e., the
+ distance between the start of the TDMA cycle and the start of the task
+ time slot. *)
Definition task_slot_offset (tsk : Task) :=
\sum_(prev_task < ts  slot_order prev_task tsk && (prev_task != tsk)) task_time_slot prev_task.
 (** The following function tests whether a task is in its time slot at instant t *)
+ (** The following function tests whether a task is in its time slot at
+ instant [t]. *)
Definition task_in_time_slot (tsk : Task) (t:instant):=
((t + TDMA_cycle  (task_slot_offset tsk)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot tsk).
+
End TDMADefinitions.
+(** ** TDMA Schedule Validity *)
+
Section TDMASchedule.
Context {Task : TaskType} {Job : JobType}.
@@ 101,24 +119,24 @@ Section TDMASchedule.
Variable arr_seq : arrival_sequence Job.
(** ..., any uniprocessor ideal schedule ... *)
 Variable sched : schedule (option Job).
+ Variable sched : schedule (ideal.processor_state Job).
(** ... and any sporadic task set. *)
Variable ts: {set Task}.
Context `{TDMAPolicy Task}.
 (** In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t. *)
+ (** In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time [t]. *)
Definition job_in_time_slot (job:Job) (t:instant):=
task_in_time_slot ts (job_task job) t.
(** We say that a TDMA policy is respected by the schedule iff
 1. when a job is scheduled at time t, then the corresponding task
+ 1. when a job is scheduled at time [t], then the corresponding task
is also in its own time slot... *)
Definition sched_implies_in_slot j t:=
scheduled_at sched j t > job_in_time_slot j t.
 (** 2. when a job is backlogged at time t,the corresponding task
+ (** 2. when a job is backlogged at time [t], the corresponding task
isn't in its own time slot or another previous job of the same task is scheduled *)
Definition backlogged_implies_not_in_slot_or_other_job_sched j t:=
backlogged sched j t >
diff git a/restructuring/model/schedule/work_conserving.v b/restructuring/model/schedule/work_conserving.v
index 3f39cd5..6d72faf 100644
 a/restructuring/model/schedule/work_conserving.v
+++ b/restructuring/model/schedule/work_conserving.v
@@ 1,24 +1,25 @@
Require Export rt.restructuring.behavior.all.
(** In this file, we introduce a restrictive definition of work
 conserving schedules. The definition is restrictive because it
 does not yet cover multiprocessor scheduling (there are plans to
 address this in future work). The definition does however cover
 effects such as jitter or selfsuspensions that affect whether a
 job can be scheduled at a given point in time because it is based
 on the general notion of a job being [backlogged] (i.e., ready and
 not executing), which is parametric in any given job readiness
 model. *)
+(** * Definition of Work Conservation *)
+
+(** In this module, we introduce a restrictive definition of workconserving
+ schedules. The definition is restrictive because it does not yet cover
+ multiprocessor scheduling (there are plans to address this in future
+ work). The definition does however cover effects such as jitter or
+ selfsuspensions that affect whether a job can be scheduled at a given
+ point in time because it is based on the general notion of a job being
+ [backlogged] (i.e., ready and not executing), which is parametric in any
+ given job readiness model. *)
Section WorkConserving.
 (** Consider any type of job associated with any type of tasks... *)
+ (** Consider any type of jobs... *)
Context {Job: JobType}.
(** ... with arrival times and costs ... *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
 (** ... and any kind of processor state model. *)
+ (** ... and any kind of processor model. *)
Context {PState: Type}.
Context `{ProcessorState Job PState}.
@@ 29,8 +30,10 @@ Section WorkConserving.
Variable arr_seq : arrival_sequence Job.
Variable sched: schedule PState.
 (** We say that a scheduler is workconserving iff whenever a job j
 is backlogged, the processor is always busy with another job. *)
+ (** ... we say that a scheduler is _workconserving_ iff whenever a job [j]
+ is backlogged, the processor is always busy executing another job
+ [j_other]. Note that this definition is intentionally silent on matters of
+ priority. *)
Definition work_conserving :=
forall j t,
arrives_in arr_seq j >
@@ 38,3 +41,4 @@ Section WorkConserving.
exists j_other, scheduled_at sched j_other t.
End WorkConserving.
+
diff git a/restructuring/model/task/absolute_deadline.v b/restructuring/model/task/absolute_deadline.v
index b32ac00..86cc56f 100644
 a/restructuring/model/task/absolute_deadline.v
+++ b/restructuring/model/task/absolute_deadline.v
@@ 1,6 +1,10 @@
Require Export rt.restructuring.model.task.concept.
(** Given task deadlines and a mapping from jobs to tasks
 we provide a generic definition of job_deadline. *)
+
+(** Given relative task deadlines and a mapping from jobs to tasks, we provide
+ the canonical definition of each job's absolute deadline, i.e.,
+ [job_deadline], as the job's arrival time plus its task's relative
+ deadline. *)
+
Instance job_deadline_from_task_deadline (Job : JobType) (Task : TaskType)
`{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} : JobDeadline Job :=
fun (j : Job) => job_arrival j + task_deadline (job_task j).
diff git a/restructuring/model/arrival/arrival_curves.v b/restructuring/model/task/arrival/curves.v
similarity index 51%
rename from restructuring/model/arrival/arrival_curves.v
rename to restructuring/model/task/arrival/curves.v
index b69fe73..649d3a6 100644
 a/restructuring/model/arrival/arrival_curves.v
+++ b/restructuring/model/task/arrival/curves.v
@@ 1,8 +1,45 @@
Require Export rt.util.rel.
Require Export rt.restructuring.model.aggregate.task_arrivals.
+Require Export rt.restructuring.model.task.arrivals.
(** In this section, we define the notion of arrival curves, which can
 be used to reason about the frequency of job arrivals. *)
+(** * The Arbitrary Arrival Curves Model *)
+
+(** In the following, we define the notion of arbitrary arrival curves, which
+ can be used to reason about the frequency of job arrivals. In contrast to
+ the sporadic task model, the arbitrary arrival curves model is wellsuited
+ to expressing bursty and irregular arrival processes. *)
+
+(** ** Task Parameters for the Arrival Curves Model *)
+
+(** The arrival curves model describes tasks by giving an upper bound and,
+ optionally, a lower bound on the number of new job arrivals during any
+ given interval. These bounds are typically called arrival curves. *)
+
+(** We let [max_arrivals tsk Δ] denote a bound on the maximum number of
+ arrivals of jobs of task [tsk] in any interval of length [Δ]. *)
+Class MaxArrivals (Task : TaskType) := max_arrivals : Task > duration > nat.
+
+(** Conversely, we let [min_arrivals tsk Δ] denote a bound on the minimum
+ number of arrivals of jobs of task [tsk] in any interval of length [Δ]. *)
+Class MinArrivals (Task : TaskType) := min_arrivals : Task > duration > nat.
+
+(** Alternatively, it is also possible to describe arbitrary arrival processes
+ by specifying the minimum and maximum lengths of an interval in which a
+ given number of jobs arrive. Such bounds are typically called minimum and
+ maximumdistance functions. *)
+
+(** We let [min_separation tsk N] denote the minimal length of an interval in
+ which exactly [N] jobs of task [tsk] arrive. *)
+Class MinSeparation (Task : TaskType) := min_separation : Task > nat > duration.
+
+(** Conversely, we let [max_separation tsk N] denote the maximal length of an interval in
+ which exactly [N] jobs of task [tsk] arrive. *)
+Class MaxSeparation (Task : TaskType) := max_separation : Task > nat > duration.
+
+
+(** ** Parameter Semantics *)
+
+(** In the following, we precisely define the semantics of the arrival curves
+ model. *)
Section ArrivalCurves.
(** Consider any type of tasks ... *)
@@ 12,29 +49,30 @@ Section ArrivalCurves.
Context {Job : JobType}.
Context `{JobTask Job Task}.
 (** Consider any job arrival sequence. *)
+ (** Consider any job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
 (** First, we define what constitutes an arrival bound for a task. *)
+ (** *** Definition of Arrival Curves *)
+
+ (** First, what constitutes a valid arrival bound for a task? *)
Section ArrivalCurves.
 (** We say that [num_arrivals] is a valid arrival curve for task
 [tsk] iff [num_arrivals] is a monotonic function that equals 0
 for the empty interval [delta = 0]. *)
+ (** We say that a given curve [num_arrivals] is a valid arrival curve for
+ task [tsk] iff [num_arrivals] is a monotonic function that equals 0 for
+ the empty interval [delta = 0]. *)
Definition valid_arrival_curve (tsk : Task) (num_arrivals : duration > nat) :=
num_arrivals 0 = 0 /\
monotone num_arrivals leq.
 (** We say that [max_arrivals] is an upper arrival bound for task
 [tsk] iff, for any interval [[t1, t2)], [max_arrivals (t2 
 t1)] bounds the number of jobs of [tsk] that arrive in that
 interval. *)
+ (** We say that [max_arrivals] is an upper arrival bound for task [tsk]
+ iff, for any interval [[t1, t2)], [max_arrivals (t2  t1)] bounds the
+ number of jobs of [tsk] that arrive in that interval. *)
Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration > nat) :=
forall (t1 t2 : instant),
t1 <= t2 >
number_of_task_arrivals arr_seq tsk t1 t2 <= max_arrivals (t2  t1).
 (** We define in the same way lower arrival bounds. *)
+ (** We analogously define the lower arrival bound.. *)
Definition respects_min_arrivals (tsk : Task) (min_arrivals : duration > nat) :=
forall (t1 t2 : instant),
t1 <= t2 >
@@ 42,18 +80,21 @@ Section ArrivalCurves.
End ArrivalCurves.
+ (** *** Definition of Minimum Distance Bounds *)
+
+ (** Next, we define the semantics of minimumdistance bounds. *)
Section SeparationBound.
 (** Then, we say that [min_separation] is a lower separation bound
 iff, for any number of jobs of task [tsk], [min_separation]
 lowerbounds the minimum interval length in which that number
 of jobs can be spawned. *)
+ (** We say that a given function [min_separation] is a lower separation
+ bound iff, for any number of jobs of task [tsk], [min_separation]
+ lowerbounds the minimum interval length in which that many jobs can
+ arrive. *)
Definition respects_min_separation (tsk : Task) (min_separation: nat > duration) :=
forall t1 t2,
t1 <= t2 >
min_separation (number_of_task_arrivals arr_seq tsk t1 t2) <= t2  t1.
 (** We define in the same way upper separation bounds. *)
+ (** We analogously define in upper separation bounds. *)
Definition respects_max_separation (tsk : Task) (max_separation: nat > duration):=
forall t1 t2,
t1 <= t2 >
@@ 63,14 +104,11 @@ Section ArrivalCurves.
End ArrivalCurves.
(** We define generic classes for arrival curves *)
Class MaxArrivals (Task : TaskType) := max_arrivals : Task > duration > nat.
Class MinArrivals (Task : TaskType) := min_arrivals : Task > duration > nat.
+(** ** Model Validity *)
Class MaxSeparation (Task : TaskType) := max_separation : Task > nat > duration.

Class MinSeparation (Task : TaskType) := min_separation : Task > nat > duration.
+(** Based on the justestablished semantics, we define the properties of a
+ valid arrival curves model. *)
Section ArrivalCurvesModel.
@@ 84,23 +122,23 @@ Section ArrivalCurvesModel.
(** Consider any job arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
 (** ..and all the classes of arrival curves. *)
+ (** ..and all kinds of arrival and separation curves. *)
Context `{MaxArrivals Task}
`{MinArrivals Task}
`{MaxSeparation Task}
`{MinSeparation Task}.
(** Let [ts] be an arbitrary task set. *)
 Variable ts : seq Task.
+ Variable ts : TaskSet Task.
(** We say that [arrivals] is a valid arrival curve for a task set
if it is valid for any task in the task set *)
Definition valid_taskset_arrival_curve (arrivals : Task > duration > nat) :=
forall (tsk : Task), tsk \in ts > valid_arrival_curve tsk (arrivals tsk).
 (** We say that [max_arrivals] is an arrival bound for a task set
 [ts] iff [max_arrivals] is an arrival bound for any task in
 [ts]. *)
+ (** Finally, we lift the pertask semantics of the respective arrival and
+ separation curves to the entire task set. *)
+
Definition taskset_respects_max_arrivals :=
forall (tsk : Task), tsk \in ts > respects_max_arrivals arr_seq tsk (max_arrivals tsk).
@@ 113,4 +151,4 @@ Section ArrivalCurvesModel.
Definition taskset_respects_min_separation :=
forall (tsk : Task), tsk \in ts > respects_min_separation arr_seq tsk (min_separation tsk).
End ArrivalCurvesModel.
\ No newline at end of file
+End ArrivalCurvesModel.
diff git a/restructuring/model/task/arrival/sporadic.v b/restructuring/model/task/arrival/sporadic.v
new file mode 100644
index 0000000..f2e7f53
 /dev/null
+++ b/restructuring/model/task/arrival/sporadic.v
@@ 0,0 +1,68 @@
+Require Export rt.restructuring.model.task.concept.
+
+(** * The Sporadic Task Model *)
+
+(** In the following, we define the arrival process commonly known as the
+ sporadic task model, where jobs may arrive at any time provided any two
+ jobs of a task are separated by at least the minimum interarrival time (or
+ period) of the task. *)
+
+
+(** ** Task Parameter for the Sporadic Task Model *)
+
+(** Under the sporadic task model, each task is characterized by its minimum
+ interarrival time, which we denote as [task_min_inter_arrival_time]. *)
+
+Class SporadicModel (Task : TaskType) :=
+ task_min_inter_arrival_time : Task > duration.
+
+(** ** Model Validity *)
+
+(** Next, we define the semantics of the sporadic task model. *)
+Section ValidSporadicTaskModel.
+ (** Consider any type of sporadic tasks. *)
+ Context {Task : TaskType} `{SporadicModel Task}.
+
+ (** A valid sporadic task should have a nonzero minimum interarrival
+ time. *)
+ Definition valid_task_min_inter_arrival_time tsk :=
+ task_min_inter_arrival_time tsk > 0.
+
+ (** Further, in the context of a set of such tasks, ... *)
+ Variable ts : TaskSet Task.
+
+ (** ... every task in the set should have a valid interarrival time. *)
+ Definition valid_taskset_inter_arrival_times :=
+ forall tsk : Task,
+ tsk \in ts > valid_task_min_inter_arrival_time tsk.
+
+ (** Next, consider any type of jobs stemming from these tasks ... *)
+ Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
+
+ (** ... and an arbitrary arrival sequence of such jobs. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** We say that a task respects the sporadic task model if the arrivals of
+ its jobs in the arrival sequence are appropriately spaced in time. *)
+ Definition respects_sporadic_task_model (tsk : Task) :=
+ forall (j j': Job),
+ (** Given two different jobs j and j' ... *)
+ j <> j' >
+ (** ...that belong to the arrival sequence... *)
+ arrives_in arr_seq j >
+ arrives_in arr_seq j' >
+ (** ... and that stem from the given task, ... *)
+ job_task j = tsk >
+ job_task j' = tsk >
+ (** ... if the arrival of j precedes the arrival of j' ..., *)
+ job_arrival j <= job_arrival j' >
+ (** then the arrival of j and the arrival of j' are separated by at least
+ one period. *)
+ job_arrival j' >= job_arrival j + task_min_inter_arrival_time tsk.
+
+ (** Based on the above definition, we define the sporadic task model as
+ follows. *)
+ Definition taskset_respects_sporadic_task_model :=
+ forall tsk, tsk \in ts > respects_sporadic_task_model tsk.
+
+End ValidSporadicTaskModel.
diff git a/restructuring/model/task/arrivals.v b/restructuring/model/task/arrivals.v
new file mode 100644
index 0000000..540571a
 /dev/null
+++ b/restructuring/model/task/arrivals.v
@@ 0,0 +1,36 @@
+Require Export rt.restructuring.model.task.concept.
+
+(** In this module, we provide basic definitions concerning the job
+ arrivals of a given task. *)
+
+Section TaskArrivals.
+
+ (** Consider any type of job associated with any type of tasks. *)
+ Context {Job : JobType}.
+ Context {Task : TaskType}.
+ Context `{JobTask Job Task}.
+
+ (** Consider any job arrival sequence ... *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** ... and any task. *)
+ Variable tsk : Task.
+
+ (** First, we construct the list of jobs of task [tsk] that arrive
+ in a given halfopen interval [[t1, t2)]. *)
+ Definition task_arrivals_between (t1 t2 : instant) :=
+ [seq j < arrivals_between arr_seq t1 t2  job_task j == tsk].
+
+ (** Based on that, we define the list of jobs of task [tsk] that
+ arrive up to and including time [t], ...*)
+ Definition task_arrivals_up_to (t : instant) := task_arrivals_between 0 t.+1.
+
+ (** ...and the list of jobs of task [tsk] that arrive strictly
+ before time [t], ... *)
+ Definition task_arrivals_before (t : instant) := task_arrivals_between 0 t.
+
+ (** ... and also count the number of job arrivals. *)
+ Definition number_of_task_arrivals (t1 t2 : instant) :=
+ size (task_arrivals_between t1 t2).
+
+End TaskArrivals.
diff git a/restructuring/model/task/concept.v b/restructuring/model/task/concept.v
index ad82dad..db9044e 100644
 a/restructuring/model/task/concept.v
+++ b/restructuring/model/task/concept.v
@@ 1,126 +1,138 @@
From mathcomp Require Export ssrbool.
Require Export rt.restructuring.behavior.all.

(** Throughout the library we assume that tasks have decidable equality *)
+
+(** * Task Type *)
+
+(** As in case of the job model, we make no assumptions about the structure or
+ type of tasks, i.e., like jobs, we consider tasks to be mathematically
+ opaque objects. We only assume that any type that represents tasks has a
+ decidable equality. *)
Definition TaskType := eqType.
(** Definition of a generic type of parameter relating jobs to tasks *)
+(** * Task Model Core Parameters *)
+
+(** In the following, we define three central parameters of the task model: how
+ jobs map to tasks, deadlines of tasks, and each task's WCET parameter. *)
+
+(** First, we define a jobmodel parameter [job_task] that maps each job to its
+ corresponding task. *)
Class JobTask (Job : JobType) (Task : TaskType) := job_task : Job > Task.
(** Definition of a generic type of parameter for task deadlines *)
+(** Second, we define a taskmodel parameter to express each task's relative
+ deadline. *)
Class TaskDeadline (Task : TaskType) := task_deadline : Task > duration.
(** Definition of a generic type of parameter for task cost *)
+(** Third, we define a taskmodel parameter to express each task's worstcase
+ execution cost (WCET). *)
Class TaskCost (Task : TaskType) := task_cost : Task > duration.
Section SameTask.

 (** For any type of job associated with any type of tasks... *)
 Context {Job : JobType}.
 Context {Task : TaskType}.
 Context `{JobTask Job Task}.

 (** ... we say that two jobs [j1] and [j2] are from the same task iff
 [job_task j1] is equal to [job_task j2], ... *)
 Definition same_task (j1 j2 : Job) := job_task j1 == job_task j2.

 (** ... we also say that job [j] is a job of task [tsk] iff
 [job_task j] is equal to [tsk]. *)
 Definition job_of_task (tsk : Task) (j : Job) := job_task j == tsk.
End SameTask.
+(** * Task Model Validity *)
(** In this section, we introduce properties of a task. *)
Section PropertesOfTask.
+(** In the following section, we introduce properties that a reasonable task
+ model must satisfy. *)
+Section ModelValidity.
 (** Consider any type of tasks. *)
+ (** Consider any type of tasks with WCETs and relative deadlines. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskDeadline Task}.
 (** Next we introduce attributes of a valid sporadic task. *)
 Section ValidTask.

+ (** First, we constrain the possible WCET values of a valid task. *)
+ Section ValidCost.
+
(** Consider an arbitrary task. *)
Variable tsk: Task.

 (** The cost and deadline of the task must be positive. *)
+
+ (** The WCET of the task should be positive. *)
Definition task_cost_positive := task_cost tsk > 0.
 Definition task_deadline_positive := task_deadline tsk > 0.

 (** The task cost cannot be larger than the deadline or the period. *)
 Definition task_cost_le_deadline := task_cost tsk <= task_deadline tsk.

 End ValidTask.

 (** Job of task *)
 Section ValidJobOfTask.

 (** Consider any type of jobs associated with the tasks ... *)
 Context {Job : JobType}.
 Context `{JobTask Job Task}.
 Context `{JobCost Job}.
 Context `{JobDeadline Job}.
 (** Consider an arbitrary job. *)
 Variable j: Job.
+ (** The WCET should not be larger than the deadline, as otherwise the task
+ is trivially infeasible. *)
+ Definition task_cost_at_most_deadline := task_cost tsk <= task_deadline tsk.
 (** The job cost cannot be larger than the task cost. *)
 Definition job_cost_le_task_cost :=
 job_cost j <= task_cost (job_task j).
+ End ValidCost.
 End ValidJobOfTask.
+ (** Second, we relate the cost of a task's jobs to its WCET. *)
+ Section ValidJobCost.
 (** Jobs of task *)
 Section ValidJobsTask.

(** Consider any type of jobs associated with the tasks ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
+ (** ... and consider the cost of each job. *)
Context `{JobCost Job}.

+
+ (** The cost of any job [j] cannot exceed the WCET of its respective
+ task. *)
+ Definition valid_job_cost j :=
+ job_cost j <= task_cost (job_task j).
+
(** ... and any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** The cost of a job from the arrival sequence cannot
be larger than the task cost. *)
 Definition cost_of_jobs_from_arrival_sequence_le_task_cost :=
+ Definition arrivals_have_valid_job_costs :=
forall j,
arrives_in arr_seq j >
 job_cost_le_task_cost j.
+ valid_job_cost j.
+
+ End ValidJobCost.
 End ValidJobsTask.
+End ModelValidity.
End PropertesOfTask.
+(** * Task Sets *)
(** In this section, we introduce properties of a task set. *)
Section PropertesOfTaskSet.
+(** Next, we introduce the notion of a task set and define properties of valid
+ task sets. *)
 (** Consider any type of tasks ... *)
+(** For simplicity, we represent sets of such tasks simply as (finite) sequences of
+ tasks. *)
+Definition TaskSet := seq.
+
+Section ValidTaskSet.
+
+ (** Consider any type of tasks with WCETs ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
+ (** ... as well as their individual execution costs. *)
Context `{JobCost Job}.
 (** ... and any arrival sequence. *)
+ (** Further, consider an arrival sequence of these jobs... *)
Variable arr_seq : arrival_sequence Job.
 (** Consider an arbitrary task set. *)
 Variable ts : seq Task.

 (** Tasks from the task set have a positive cost. *)
 Definition tasks_cost_positive :=
 forall tsk,
 tsk \in ts >
 task_cost_positive tsk.
+ (** ...and the set of tasks that generate them. *)
+ Variable ts : TaskSet Task.
 (** All jobs in the arrival sequence come from the task set. *)
+ (** All jobs in the arrival sequence should come from the task set. *)
Definition all_jobs_from_taskset :=
forall j,
arrives_in arr_seq j >
job_task j \in ts.
End PropertesOfTaskSet.
\ No newline at end of file
+End ValidTaskSet.
+
+(** Finally, for readability, we define two ways in which jobs and tasks
+ relate. *)
+Section SameTask.
+
+ (** For any type of job associated with any type of tasks... *)
+ Context {Job : JobType}.
+ Context {Task : TaskType}.
+ Context `{JobTask Job Task}.
+
+ (** ... we say that two jobs [j1] and [j2] are from the same task iff
+ [job_task j1] is equal to [job_task j2]. *)
+ Definition same_task (j1 j2 : Job) := job_task j1 == job_task j2.
+
+ (** We further say that a job [j] is a job of task [tsk] iff [job_task j] is
+ equal to [tsk]. *)
+ Definition job_of_task (tsk : Task) (j : Job) := job_task j == tsk.
+
+End SameTask.
+
+
diff git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 953f071..bd65347 100644
 a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ 1,59 +1,66 @@
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Platform for Models with Floating NonPreemptive Regions *)
(** In this section, we introduce a set of requirements for function
 [task_max_nonpr_segment], so it is coherent with model with
 floating nonpreemptive regions. *)
Section ModelWithFloatingNonpreemptiveRegions.
+(** * Task Model with Floating NonPreemptive Regions *)
+
+(** In this file, we instantiate the specific task model of (usually)
+ preemptive tasks with "floating" nonpreemptive regions, i.e., with jobs
+ that exhibit nonpreemptive segments of bounded length at unpredictable
+ points during their execution. *)
+
+(** ** Model Validity *)
+
+(** To begin with, we introduce requirements that the function
+ [task_max_nonpr_segment] must satisfy to be coherent with the floating
+ nonpreemptive regions model. *)
+Section ValidModelWithFloatingNonpreemptiveRegions.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
 Context `{TaskCost Task}.
+ (** ... with a bound on the maximum nonpreemptive segment length ... *)
Context `{TaskMaxNonpreemptiveSegment Task}.

 (** ... and any type of jobs associated with these tasks. *)
+
+ (** ... and any type of limitedpreemptive jobs associated with these tasks ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
 Context `{JobArrival Job}.
+ (** ... with execution costs and specific preemption points. *)
Context `{JobCost Job}.
Context `{JobPreemptionPoints Job}.

+
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.

 (** We require [task_max_nonpreemptive_segment (job_task j)] to be
 an upper bound of the length of the max nonpreemptive segment of
 job [j]. *)
 Definition job_max_np_segment_le_task_max_np_segment :=
+
+ (** We require [task_max_nonpreemptive_segment (job_task j)] to be an upper
+ bound of the length of the maximum nonpreemptive segment of job [j]. *)
+ Definition job_respects_task_max_np_segment :=
forall (j : Job),
arrives_in arr_seq j >
job_max_nonpreemptive_segment j <= task_max_nonpreemptive_segment (job_task j).
 (** We define a valid model with floating nonpreemptive regions as the
 model with floating nonpreemptive regions at the tasklevel and
 valid model with limited preemptions at the joblevel. *)
+ (** A model with floating nonpreemptive regions is valid if it is both valid
+ a the job level and jobs respect the upper bound of their task. *)
Definition valid_model_with_floating_nonpreemptive_regions :=
valid_limited_preemptions_job_model arr_seq /\
 job_max_np_segment_le_task_max_np_segment.
+ job_respects_task_max_np_segment.
End ModelWithFloatingNonpreemptiveRegions.
+End ValidModelWithFloatingNonpreemptiveRegions.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
 threshold] for the model with floating nonpreemptive regions. *)
+(** ** RuntoCompletion Threshold *)
+
+(** In this section, we instantiate the tasklevel runtocompletion threshold
+ for the model with floating nonpreemptive regions. *)
Section TaskRTCThresholdFloatingNonPreemptiveRegions.
 (** Consider any type of tasks.*)
+ (** Consider any type of tasks with a WCET bound.*)
Context {Task : TaskType}.
Context `{TaskCost Task}.

 (** In the model with floating nonpreemptive regions, task has to
 static information about the placement of preemption
 points. Thus, the only safe task's run to completion threshold
 is [task cost]. *)
+
+ (** In the model with floating nonpreemptive regions, there is no static
+ information about the placement of preemption points in all jobs, i.e.,
+ it is impossible to predict when exactly a job will be preemptable. Thus,
+ the only safe runtocompletion threshold is [task cost]. *)
Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
 {
+ {
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.
diff git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/restructuring/model/task/preemption/fully_nonpreemptive.v
index becff21..707c2e9 100644
 a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/restructuring/model/task/preemption/fully_nonpreemptive.v
@@ 1,39 +1,40 @@
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Platform for Fully NonPreemptive Model *)
(** In this section, we instantiate function
 [task_max_nonpreemptive_segment] for the fully nonpreemptive
 model. *)
+(** * Fully NonPreemptive Task Model *)
+
+(** In this module, we instantiate the task model in which jobs cannot be
+ preempted once they have commenced execution. *)
Section FullyNonPreemptiveModel.
 (** Consider any type of jobs. *)
+ (** Consider any type of tasks with WCET bounds. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.

 (** In fully nonpreemptive model no job can be preempted until its
 completion. The maximal nonpreemptive segment of a job
 [j] has length [job_cost j] which is bounded by [task_cost tsk].*)
+
+ (** In the fully nonpreemptive model, no job can be preempted until its
+ completion. The maximal nonpreemptive segment of a job [j] has length
+ [job_cost j], which is bounded by [task_cost tsk].*)
Global Program Instance fully_nonpreemptive_model : TaskMaxNonpreemptiveSegment Task :=
{
task_max_nonpreemptive_segment (tsk : Task) := task_cost tsk
}.

+
End FullyNonPreemptiveModel.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
 threshold] for the fully nonpreemptive model. *)
+(** ** RuntoCompletion Threshold *)
+
+(** In this section, we instantiate the tasklevel runtocompletion threshold
+ for the fully nonpreemptive model. *)
Section TaskRTCThresholdFullyNonPreemptive.
(** Consider any type of tasks. *)
 Context {Task : TaskType}.
 Context `{TaskCost Task}.

 (** In fully nonpreemptive model no job can be preempted until its
 completion. Thus, we can set task's run to completion threshold
+ Context {Task : TaskType}.
+
+ (** In the fully nonpreemptive model, no job can be preempted prior to its
+ completion. In other words, once a job starts running, it is guaranteed
+ to finish. Thus, we can set the tasklevel runtocompletion threshold
to ε. *)
Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
 {
+ {
task_run_to_completion_threshold (tsk : Task) := ε
}.
diff git a/restructuring/model/task/preemption/fully_preemptive.v b/restructuring/model/task/preemption/fully_preemptive.v
index 8f658cb..6a4faa3 100644
 a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/restructuring/model/task/preemption/fully_preemptive.v
@@ 1,36 +1,41 @@
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Platform for Fully Preemptive Model *)
(** In this section, we instantiate function
 [task_max_nonpreemptive_segment] for the fully preemptive model. *)
+(** * Fully Preemptive Task Model *)
+
+(** In this module, we instantiate the common task model in which all jobs are
+ always preemptable. *)
+
Section FullyPreemptiveModel.
(** Consider any type of jobs. *)
Context {Task : JobType}.
 (** In the fully preemptive model any job can be preempted at any time. Thus,
 the maximal nonpreemptive segment has length at most ε. *)
+ (** In the fully preemptive model, any job can be preempted at any
+ time. Thus, the maximal nonpreemptive segment has length at most ε
+ (i.e., one time unit such as a processor cycle). *)
Global Program Instance fully_preemptive_model : TaskMaxNonpreemptiveSegment Task :=
 {
+ {
task_max_nonpreemptive_segment (tsk : Task) := ε
}.

+
End FullyPreemptiveModel.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
 threshold] for the fully preemptive model. *)
+(** ** RuntoCompletion Threshold *)
+
+(** Since jobs are always preemptive, there is no offset after which a job is
+ guaranteed to run to completion. *)
+
Section TaskRTCThresholdFullyPreemptiveModel.
 (** Consider any type of tasks. *)
+ (** Consider any type of tasks with WCETs. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
 (** In the fully preemptive model any job can be preempted at any time. Thus,
 the only safe task's run to completion threshold is [task cost]. *)
+ (** In the fully preemptive model, any job can be preempted at any
+ time. Thus, the only safe runtocompletion threshold for a task is its WCET. *)
Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
 {
+ {
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.

+
End TaskRTCThresholdFullyPreemptiveModel.
diff git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index e3ba898..c91d4f2 100644
 a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ 1,109 +1,115 @@
Require Export rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we introduce a set of requirements for function
 [task_preemption_points], so it is coherent with limited
 preemptions model. *)
Section ModelWithFixedPreemptionPoints.
+(** * LimitedPreemptive Task Model *)
 (** Consider any type of tasks ... *)
+(** In this module, we instantiate the task model in which jobs can be
+ preempted only at certain preemption points. *)
+
+(** ** Model Validity *)
+
+(** To begin with, we introduce requirements that the function
+ [task_max_nonpr_segment] must satisfy to be coherent with the
+ limitedpreemptive task model. *)
+Section ValidModelWithFixedPreemptionPoints.
+
+ (** Consider any type of tasks with WCET bounds and given preemption points ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskPreemptionPoints Task}.
 (** ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks, ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
+ (** ... where each job has an arrival time, an execution cost, and some
+ preemption points. *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
 Context `{JobPreemptionPoints Job}.
+ Context `{JobPreemptionPoints Job}.
(** Consider any arrival sequence. *)
 Variable arr_seq : arrival_sequence Job.

 (** Consider an arbitrary task set ts. *)
 Variable ts : list Task.

 (** Next, we describe structural properties that a sequence of
 preemption points of task should satisfy. *)

 (** (1) We require the sequence of preemption points to contain the beginning... *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** Consider an arbitrary task set [ts]. *)
+ Variable ts : TaskSet Task.
+
+ (** First, we describe structural properties that a sequence of preemption
+ points of a task should satisfy. *)
+
+ (** (1) We require the sequence of preemption points to contain the beginning ... *)
Definition task_beginning_of_execution_in_preemption_points :=
forall tsk, tsk \in ts > first0 (task_preemption_points tsk) = 0.
 (** ... and (2) the end of execution for any job j.*)
+ (** ... and (2) the end of execution. *)
Definition task_end_of_execution_in_preemption_points :=
forall tsk, tsk \in ts > last0 (task_preemption_points tsk) = task_cost tsk.
 (** (3) We require the sequence of preemption points
 to be a nondecreasing sequence. *)
 Definition task_preemption_points_is_nondecreasing_sequence :=
+ (** (3) Furthermore, we require the sequence of preemption points to be a
+ nondecreasing sequence. *)
+ Definition nondecreasing_task_preemption_points :=
forall tsk, tsk \in ts > nondecreasing_sequence (task_preemption_points tsk).
 (** (4) Next, we require the number of nonpreemptive segments of a job to be
 equal to the number of nonpreemptive segments of its task. Note that
 some of nonpreemptive segments of a job can have zero length, nonetheless
 the number of segments should match. *)
 Definition job_consists_of_the_same_number_of_segments_as_task :=
+ (** (4) We also require the number of nonpreemptive segments of a job to be
+ equal to the number of nonpreemptive segments of its task. Note that
+ some of nonpreemptive segments of a job can have zero length;
+ nonetheless the number of segments should match. *)
+ Definition consistent_job_segment_count :=
forall j,
 arrives_in arr_seq j >
+ arrives_in arr_seq j >
size (job_preemption_points j) = size (task_preemption_points (job_task j)).
 (** (5) We require lengths of nonpreemptive segments of a job to be bounded
 by lengths of the corresponding segments of its task. *)
 Definition lengths_of_task_segments_bound_length_of_job_segments :=
+ (** (5) We require the lengths of the nonpreemptive segments of a job to be
+ bounded by the lengths of the corresponding segments of its task. *)
+ Definition job_respects_segment_lengths :=
forall j n,
 arrives_in arr_seq j >
+ arrives_in arr_seq j >
nth 0 (distances (job_preemption_points j)) n
<= nth 0 (distances (task_preemption_points (job_task j))) n.

 (** (6) Lastly, we ban empty nonpreemptive segments for tasks. *)
+
+ (** (6) Lastly, we ban empty nonpreemptive segments at the task level. *)
Definition task_segments_are_nonempty :=
forall tsk n,
(tsk \in ts) >
n < size (distances (task_preemption_points tsk)) >
ε <= nth 0 (distances (task_preemption_points tsk)) n.

 (** We define a valid tasklevel model with fixed preemption points
 as a concatenation of the hypotheses above. *)
+
+ (** We define a valid tasklevel model with fixed preemption points as the
+ conjunction of the hypotheses above. *)
Definition valid_fixed_preemption_points_task_model :=
task_beginning_of_execution_in_preemption_points /\
task_end_of_execution_in_preemption_points /\
 task_preemption_points_is_nondecreasing_sequence /\
 job_consists_of_the_same_number_of_segments_as_task /\
 lengths_of_task_segments_bound_length_of_job_segments /\
+ nondecreasing_task_preemption_points /\
+ consistent_job_segment_count /\
+ job_respects_segment_lengths /\
task_segments_are_nonempty.

 (** We define a valid model with fixed preemption points as
 a model with fixed preemptions points at the tasklevel
 and model with limited preemptions at the joblevel. *)
+
+ (** Finally, a model with fixed preemption points is valid if it is both valid
+ a the job and task levels. *)
Definition valid_fixed_preemption_points_model :=
valid_limited_preemptions_job_model arr_seq /\
valid_fixed_preemption_points_task_model.

End ModelWithFixedPreemptionPoints.
+End ValidModelWithFixedPreemptionPoints.
+
+(** ** RuntoCompletion Threshold *)
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
 threshold] for the limited preemptions model. *)
+(** In this section, we instantiate the tasklevel runtocompletion threshold
+ for the task model with fixed preemption points. *)
Section TaskRTCThresholdLimitedPreemptions.

 (** Consider any type of tasks. *)
+
+ (** Consider any type of tasks with WCET bounds and fixed preemption points. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskPreemptionPoints Task}.

 (** In the model with limited preemptions, no job can be preempted after
 a job reaches its last nonpreemptive segment. Thus, we can
 set task's run to completion threshold to [task_cost tsk 
 (task_last_nonpr_seg tsk  ε)] which is always greater than
 [job_cost j  (job_last_nonpr_seg j  ε)]. *)
+
+ (** Given fixed preemption points, no job can be preempted after a job
+ reaches its last nonpreemptive segment. Thus, we can set the tasklevel
+ runtocompletion threshold to [task_cost tsk  (task_last_nonpr_seg tsk  ε)],
+ which safely bounds [job_cost j  (job_last_nonpr_seg j  ε)]. *)
Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
 {
+ {
task_run_to_completion_threshold (tsk : Task) :=
task_cost tsk  (task_last_nonpr_segment tsk  ε)
}.

+
End TaskRTCThresholdLimitedPreemptions.
diff git a/restructuring/model/task/preemption/parameters.v b/restructuring/model/task/preemption/parameters.v
index d1b9edd..151a838 100644
 a/restructuring/model/task/preemption/parameters.v
+++ b/restructuring/model/task/preemption/parameters.v
@@ 1,76 +1,81 @@
Require Export rt.restructuring.model.preemption.parameter.
Require Export rt.restructuring.model.task.concept.
(** * Static information about preemption points *)
(** Definition of a generic type of parameter relating a task
 to the length of the maximum nonpreemptive segment. *)
+(** * Task Preemption Model *)
+
+(** In this module, we define the abstract interface for tasklevel preemption
+ models. Specific preemption models are instantiated in the sibling files in
+ this directory. *)
+
+(** ** PreemptionRelated Task Parameters *)
+
+(** We define three parameters to express the preemption behavior of a given
+ task. *)
+
+(** First, we define [task_max_nonpreemptive_segment] to denote a bound on the
+ maximum length of a task's nonpreemptive segment. *)
Class TaskMaxNonpreemptiveSegment (Task : TaskType) :=
task_max_nonpreemptive_segment : Task > work.
(** Definition of a generic type of parameter relating a task
 to its runtocompletion threshold. *)
+(** Second, [task_run_to_completion_threshold] indicates a progress bound with
+ the interpretation that, once a job of a task [tsk] has received at least
+ [task_run_to_completion_threshold tsk] time units of service, it will
+ remain nonpreemptive until the end and run to completion. *)
Class TaskRunToCompletionThreshold (Task : TaskType) :=
task_run_to_completion_threshold : Task > work.
(** Definition of a generic type of parameter relating task
 to the sequence of its preemption points. *)
+(** Third, the parameter [task_preemption_points] indicates the nonpreemptive
+ segments of a task. Obviously, not all preemption models use this parameter. *)
Class TaskPreemptionPoints (Task : TaskType) :=
task_preemption_points : Task > seq work.
(** We provide a conversion from task preemption points to task max nonpreemptive segment. *)
Instance TaskPreemptionPoints_to_TaskMaxNonpreemptiveSegment_conversion
 (Task : TaskType) `{TaskPreemptionPoints Task} : TaskMaxNonpreemptiveSegment Task :=
 fun tsk => max0 (distances (task_preemption_points tsk)).

(** * Derived Parameters *)
(** * Task Maximum and Last Nonpreemptive Segment *)
(** In this section we define the notions of the maximal and
 the last nonpreemptive segments of a task. *)
+(** ** Derived Properties *)
+(** In this section, we define the notions of the maximal and the last
+ nonpreemptive segments of a task. *)
Section MaxAndLastNonpreemptiveSegment.
 (** Consider any type of tasks. *)
+ (** Consider any type of tasks with fixed preemption points. *)
Context {Task : TaskType}.
 Context `{TaskCost Task}.

 (** In addition, assume the existence of a function that
 maps a job to the sequence of its preemption points. *)
Context `{TaskPreemptionPoints Task}.
 (** Next, we define a function [task_max_nonpr_segment] that
 maps a task to the length of the longest nonpreemptive segment
 of this task. *)
+ (** We define a function [task_max_nonpr_segment] that computes the length of
+ the longest nonpreemptive segment of a given task. *)
Definition task_max_nonpr_segment (tsk : Task) :=
max0 (distances (task_preemption_points tsk)).
 (** Similarly, [task_last_nonpr_segment] is a function that
 maps a job to the length of the last nonpreemptive segment. *)
+ (** Similarly, [task_last_nonpr_segment] is a function that computes the
+ length of the last nonpreemptive segment. *)
Definition task_last_nonpr_segment (tsk : Task) :=
last0 (distances (task_preemption_points tsk)).

+
End MaxAndLastNonpreemptiveSegment.
+(** To avoid having to specify redundant information, we allow Coq to
+ automatically infer a task's maximum nonpreemptive segment length if its
+ preemption points are known. *)
+Instance TaskPreemptionPoints_to_TaskMaxNonpreemptiveSegment_conversion
+ (Task : TaskType) `{TaskPreemptionPoints Task} : TaskMaxNonpreemptiveSegment Task := task_max_nonpr_segment.
+
(** * Validity of a Preemption Model *)
+(** ** Preemption Model Validity *)
Section PreemptionModel.
+(** For analysis purposes, it is important that the distance between any two
+ neighboring preemption points of a job is bounded. We define the validity
+ criterion for the maximum nonpreemptive segment length accordingly. *)
+Section ValidPreemptionModel.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
 Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
 Context `{JobArrival Job}.
Context `{JobCost Job}.
 (** In addition, we assume the existence of a function mapping a
 task to its maximal nonpreemptive segment ... *)
+ (** Suppose we are given the maximum nonpreemptive segment length for each task ... *)
Context `{TaskMaxNonpreemptiveSegment Task}.
 (** ... and the existence of a predicate mapping a job and
 its progress to a boolean value saying whether this job is
 preemptable at its current point of execution. *)
+ (** ... and a joblevel preemption model. *)
Context `{JobPreemptable Job}.
(** Consider any kind of processor state model, ... *)
@@ 83,23 +88,16 @@ Section PreemptionModel.
(** ... and any given schedule. *)
Variable sched : schedule PState.
 (** For analysis purposes, it is important that the distance between
 preemption points of a job is bounded. To ensure that, next we define the
 model with bounded nonpreemptive segment. *)
 Section ModelWithBoundedNonpreemptiveSegments.

 (** First we require that [task_max_nonpreemptive_segment] gives an
 upper bound for values of the function
 [job_max_nonpreemptive_segment]. *)
 Definition job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment (j: Job) :=
 job_max_nonpreemptive_segment j <= task_max_nonpreemptive_segment (job_task j).

 (** Next, we require that all the segments of a job [j] have
 bounded length. I.e., for any progress [ρ] of job [j] there
 exists a preemption point [pp] such that [ρ <= pp <= ρ +
 (job_max_nps j  ε)]. That is, in any time interval of length
 [job_max_nps j], there exists a preemption point which lies
 in this interval. *)
+ (** First we require that [task_max_nonpreemptive_segment] gives an upper
+ bound on values of the function [job_max_nonpreemptive_segment]. *)
+ Definition job_respects_max_nonpreemptive_segment (j: Job) :=
+ job_max_nonpreemptive_segment j <= task_max_nonpreemptive_segment (job_task j).
+
+ (** Next, we require that all segments of a job [j] have bounded length. That
+ is, for any progress [ρ] of job [j], there exists a preemption point [pp]
+ such that [ρ <= pp <= ρ + (job_max_nps j  ε)]. That is, in any time
+ interval of length [job_max_nps j] during which a job is continuously
+ scheduled, there exists a preemption point that lies in this interval. *)
Definition nonpreemptive_regions_have_bounded_length (j : Job) :=
forall (ρ : duration),
0 <= ρ <= job_cost j >
@@ 107,55 +105,52 @@ Section PreemptionModel.
ρ <= pp <= ρ + (job_max_nonpreemptive_segment j  ε) /\
job_preemptable j pp.
 (** We say that the schedule enforces bounded nonpreemptive
 segments iff the predicate [job_preemptable] satisfies the two
 conditions above. *)
 Definition model_with_bounded_nonpreemptive_segments :=
 forall j,
 arrives_in arr_seq j >
 job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
 /\ nonpreemptive_regions_have_bounded_length j.

 (** Finally, we say that the schedule enforces _valid_ bounded
 nonpreemptive segments iff the predicate [job_preemptable]
 defines a valid preemption model which has bounded
 nonpreemptive segments . *)
 Definition valid_model_with_bounded_nonpreemptive_segments :=
 valid_preemption_model arr_seq sched /\
 model_with_bounded_nonpreemptive_segments.

 End ModelWithBoundedNonpreemptiveSegments.

End PreemptionModel.

(** * Task's RuntoCompletion Threshold *)
(** Since a task model may not provide exact information about
 preemption point of a task, task's runtocompletion threshold
 cannot be defined in terms of preemption points of a task (unlike
 job's runtocompletion threshold). Therefore, we can assume the
 existence of a function that maps a task to its runtocompletion
 threshold. In this section we define the notion of a valid
 runtocompletion threshold of a task. *)
+ (** We say that the schedule exhibits bounded nonpreemptive segments iff the
+ predicate [job_preemptable] satisfies the two preceding conditions. *)
+ Definition model_with_bounded_nonpreemptive_segments :=
+ forall j,
+ arrives_in arr_seq j >
+ job_respects_max_nonpreemptive_segment j
+ /\ nonpreemptive_regions_have_bounded_length j.
+
+ (** Finally, we say that the schedule exhibits _valid_ bounded nonpreemptive
+ segments iff the predicate [job_preemptable] defines a valid preemption
+ model and if this model has nonpreemptive segments of bounded length. *)
+ Definition valid_model_with_bounded_nonpreemptive_segments :=
+ valid_preemption_model arr_seq sched /\
+ model_with_bounded_nonpreemptive_segments.
+
+End ValidPreemptionModel.
+
+(** ** RuntoCompletion Threshold Validity *)
+
+(** Since a task model may not provide exact information about the preemption
+ points of a task, a task's runtocompletion threshold generally cannot be
+ defined in terms of the preemption points of a task (unlike a job's
+ runtocompletion threshold, which can always be computed from a job's
+ preemption points). Instead, we require each tasklevel preemption model to
+ specify a task's runtocompletion threshold explicitly. We define its
+ required properties in the following. *)
Section ValidTaskRunToCompletionThreshold.

 (** Consider any type of tasks ... *)
+
+ (** Consider any type of tasks with bounded WCETs ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
 (** ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
+
+ (** ... where each job has an execution cost. *)
Context `{JobCost Job}.
 (** In addition, we assume existence of a function
 mapping jobs to theirs preemption points ... *)
+ (** Suppose we are given a joblevel preemption model ... *)
Context `{JobPreemptable Job}.
 (** ...and a function mapping tasks to theirs
 runtocompletion threshold. *)
+ (** ...and the runtocompletion threshold for each task. *)
Context `{TaskRunToCompletionThreshold Task}.
 (** Consider any kind of processor state model, ... *)
+ (** Further, consider any kind of processor model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
@@ 163,30 +158,27 @@ Section ValidTaskRunToCompletionThreshold.
Variable arr_seq: arrival_sequence Job.
(** ... and any given schedule. *)
 Variable sched: schedule PState.
+ Variable sched: schedule PState.
 (** A task's runtocompletion threshold should be at most the cost of the task. *)
 Definition task_run_to_completion_threshold_le_task_cost tsk :=
+ (** A task's runtocompletion threshold must not exceed the WCET of the
+ task. *)
+ Definition task_rtc_bounded_by_cost tsk :=
task_run_to_completion_threshold tsk <= task_cost tsk.

 (** We say that the runtocompletion threshold of a task [tsk]
 bounds the job runtocompletion threshold iff for any job [j]
 of task [tsk] the job's runtocompletion threshold is less than
 or equal to the task's runtocompletion threshold. *)
 Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
+
+ (** We say that the runtocompletion threshold of a task [tsk] bounds the
+ joblevel runtocompletion threshold iff, for any job [j] of task [tsk],
+ the job's runtocompletion threshold is at most the task's
+ runtocompletion threshold. *)
+ Definition job_respects_task_rtc tsk :=
forall j,
arrives_in arr_seq j >
job_task j = tsk >
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
 (** We say that task_run_to_completion_threshold is a valid task
 runtocompletion threshold for a task [tsk] iff
 [task_run_to_completion_threshold tsk] is (1) no bigger than
 [tsk]'s cost, (2) for any job of task [tsk]
 [job_run_to_completion_threshold] is bounded by
 [task_run_to_completion_threshold]. *)
+ (** Finally, we require that a valid runtocompletion threshold parameter
+ will satisfy the two above definitions. *)
Definition valid_task_run_to_completion_threshold tsk :=
 task_run_to_completion_threshold_le_task_cost tsk /\
 task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk.
+ task_rtc_bounded_by_cost tsk /\
+ job_respects_task_rtc tsk.
End ValidTaskRunToCompletionThreshold.
diff git a/restructuring/model/task/sequentiality.v b/restructuring/model/task/sequentiality.v
index c52d2c9..8afbffb 100644
 a/restructuring/model/task/sequentiality.v
+++ b/restructuring/model/task/sequentiality.v
@@ 1,7 +1,12 @@
Require Export rt.restructuring.model.task.concept.
+
+(** In this module, we give a precise definition of the common notion of
+ "sequential tasks", which is commonly understood to mean that the jobs of a
+ sequential task execute in sequence and in a nonoverlapping fashion. *)
+
Section PropertyOfSequentiality.
 (** Consider any type of job associated with any type of tasks... *)
+ (** Consider any type of jobs stemming from any type of tasks ... *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
@@ 10,15 +15,15 @@ Section PropertyOfSequentiality.
Context `{JobArrival Job}.
Context `{JobCost Job}.
 (** ... and any kind of processor state model. *)
+ (** ... and any kind of processor model. *)
Context {PState: Type}.
Context `{ProcessorState Job PState}.
 (** Given a schedule ... *)
+ (** Given a schedule of such jobs ... *)
Variable sched: schedule PState.
 (** ...we say that tasks are sequential if each task's jobs
 are executed in the order they arrived. *)
+ (** ... we say that the tasks execute sequentially if each task's jobs are
+ executed in arrival order and in a nonoverlapping fashion. *)
Definition sequential_tasks :=
forall (j1 j2: Job) (t: instant),
same_task j1 j2 >
diff git a/restructuring/model/task/suspension/dynamic.v b/restructuring/model/task/suspension/dynamic.v
index 50c3ccd..44d6c5a 100644
 a/restructuring/model/task/suspension/dynamic.v
+++ b/restructuring/model/task/suspension/dynamic.v
@@ 12,7 +12,8 @@ Class TaskTotalSuspension (Task : TaskType) := task_total_suspension : Task > d
(** In the following section, we specify the semantics of the dynamic
selfsuspension model: each job selfsuspends in total no longer than
 specified by its associated task. *)
+ specified by the cumulative selfsuspension bound of its associated
+ task. *)
Section ValidDynamicSuspensions.
diff git a/restructuring/results/edf/optimality.v b/restructuring/results/edf/optimality.v
index 619b703..44e7f68 100644
 a/restructuring/results/edf/optimality.v
+++ b/restructuring/results/edf/optimality.v
@@ 30,7 +30,7 @@ Section Optimality.
exists edf_sched : schedule (ideal.processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
 is_EDF_schedule edf_sched.
+ EDF_schedule edf_sched.
Proof.
move=> [sched [[COME READY] DL_ARR_MET]].
have ARR := jobs_must_arrive_to_be_ready sched READY.
@@ 68,7 +68,7 @@ Section WeakOptimality.
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
 is_EDF_schedule edf_sched /\
+ EDF_schedule edf_sched /\
forall j,
(exists t, scheduled_at any_sched j t) <>
(exists t', scheduled_at edf_sched j t').
diff git a/restructuring/results/edf/rta/bounded_nps.v b/restructuring/results/edf/rta/bounded_nps.v
index b7247ad..1cf857f 100644
 a/restructuring/results/edf/rta/bounded_nps.v
+++ b/restructuring/results/edf/rta/bounded_nps.v
@@ 88,8 +88,8 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
diff git a/restructuring/results/edf/rta/bounded_pi.v b/restructuring/results/edf/rta/bounded_pi.v
index c3c946a..3a744ce 100644
 a/restructuring/results/edf/rta/bounded_pi.v
+++ b/restructuring/results/edf/rta/bounded_pi.v
@@ 85,8 +85,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
Hypothesis H_sequential_tasks : sequential_tasks sched.
(** Assume that a job cost cannot be larger than a task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Consider an arbitrary task set ts. *)
Variable ts : list Task.
@@ 431,10 +431,10 @@ Section AbstractRTAforEDFwithArrivalCurves.
job_cost j0).
{ rewrite big_mkcond [X in _ <= X]big_mkcond //= leq_sum //.
by intros s _; case (job_task s == tsk_o); case (EDF s j). }
 { rewrite /number_of_task_arrivals /task_arrivals.number_of_task_arrivals
+ { rewrite /number_of_task_arrivals /task.arrivals.number_of_task_arrivals
sum1_size big_distrr /= big_filter muln1.
apply leq_sum_seq; move => jo 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.
@@ 519,12 +519,12 @@ Section AbstractRTAforEDFwithArrivalCurves.
+ rewrite big_mkcond [X in _ <= X]big_mkcond //=.
rewrite leq_sum //; intros s _.
by case (EDF s j).
 + rewrite /number_of_task_arrivals /task_arrivals.number_of_task_arrivals
+ + rewrite /number_of_task_arrivals /task.arrivals.number_of_task_arrivals
sum1_size big_distrr /= big_filter.
rewrite muln1.
apply leq_sum_seq; move => j0 IN0 /eqP EQ.
rewrite EQ.
 apply H_job_cost_le_task_cost.
+ apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0.
 unfold V in *; clear V.
set (V := A + ε + D tsk  D tsk_o) in *.
@@ 622,7 +622,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
rewrite /task_rbf /rbf; erewrite task_rbf_0_zero; eauto 2.
rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk).
 by eapply leq_trans; eauto 2;
 rewrite (eqbool_to_eqprop H_job_of_tsk); apply H_job_cost_le_task_cost.
+ rewrite (eqbool_to_eqprop H_job_of_tsk); apply H_valid_job_cost.
 by eapply task_rbf_1_ge_task_cost; eauto using eqbool_to_eqprop.
}
{ apply/andP; split; first by done.
diff git a/restructuring/results/edf/rta/floating_nonpreemptive.v b/restructuring/results/edf/rta/floating_nonpreemptive.v
index 6bf11b5..a7f1ebd 100644
 a/restructuring/results/edf/rta/floating_nonpreemptive.v
+++ b/restructuring/results/edf/rta/floating_nonpreemptive.v
@@ 55,8 +55,8 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
@@ 76,7 +76,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_schedule_with_limited_preemptions:
 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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
diff git a/restructuring/results/edf/rta/fully_nonpreemptive.v b/restructuring/results/edf/rta/fully_nonpreemptive.v
index 30bab00..bd170fe 100644
 a/restructuring/results/edf/rta/fully_nonpreemptive.v
+++ b/restructuring/results/edf/rta/fully_nonpreemptive.v
@@ 46,8 +46,8 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
@@ 63,7 +63,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
(** Next, consider any ideal nonpreemptive uniprocessor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
 Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched.
+ Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
@@ 141,8 +141,8 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
case: (posnP (task_cost tsk)) => [ZEROPOS].
{ intros j ARR TSK.
have ZEROj: job_cost j = 0.
 { move: (H_job_cost_le_task_cost j ARR) => NEQ.
 rewrite /job_cost_le_task_cost TSK ZERO in NEQ.
+ { move: (H_valid_job_cost j ARR) => NEQ.
+ rewrite /valid_job_cost TSK ZERO in NEQ.
by apply/eqP; rewrite leqn0.
}
by rewrite /job_response_time_bound /completed_by ZEROj.
diff git a/restructuring/results/edf/rta/fully_preemptive.v b/restructuring/results/edf/rta/fully_preemptive.v
index e7cc3df..ad7f412 100644
 a/restructuring/results/edf/rta/fully_preemptive.v
+++ b/restructuring/results/edf/rta/fully_preemptive.v
@@ 46,8 +46,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
diff git a/restructuring/results/edf/rta/limited_preemptive.v b/restructuring/results/edf/rta/limited_preemptive.v
index 3892ec5..133b828 100644
 a/restructuring/results/edf/rta/limited_preemptive.v
+++ b/restructuring/results/edf/rta/limited_preemptive.v
@@ 46,8 +46,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Next, we assume we have the model with fixed preemption points.
I.e., each task is divided into a number of nonpreemptive segments
@@ 75,7 +75,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_schedule_with_limited_preemptions:
 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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ 152,8 +152,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
move: (MLP) => [BEGj [ENDj _]].
case: (posnP (task_cost tsk)) => [ZEROPOSt].
{ intros j ARR TSK.
 move: (H_job_cost_le_task_cost _ ARR) => POSt.
 move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
+ move: (H_valid_job_cost _ ARR) => POSt.
+ move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
by rewrite /job_response_time_bound /completed_by Z.
}
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).
diff git a/restructuring/results/fixed_priority/rta/bounded_nps.v b/restructuring/results/fixed_priority/rta/bounded_nps.v
index 0371282..cf4d6dc 100644
 a/restructuring/results/fixed_priority/rta/bounded_nps.v
+++ b/restructuring/results/fixed_priority/rta/bounded_nps.v
@@ 84,8 +84,8 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
diff git a/restructuring/results/fixed_priority/rta/bounded_pi.v b/restructuring/results/fixed_priority/rta/bounded_pi.v
index 28b5752..db9dc4e 100644
 a/restructuring/results/fixed_priority/rta/bounded_pi.v
+++ b/restructuring/results/fixed_priority/rta/bounded_pi.v
@@ 68,8 +68,8 @@ Section AbstractRTAforFPwithArrivalCurves.
Hypothesis H_sequential_tasks : sequential_tasks sched.
(** Assume that a job cost cannot be larger than a task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Consider an arbitrary task set ts. *)
Variable ts : list Task.
diff git a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
index a7121e8..ecc40a7 100644
 a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
@@ 48,8 +48,8 @@ Section RTAforFloatingModelwithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for any task [tsk] in ts
[max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
@@ 67,7 +67,7 @@ Section RTAforFloatingModelwithArrivalCurves.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_schedule_with_limited_preemptions:
 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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
diff git a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
index 8940d2c..50b498a 100644
 a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
@@ 38,8 +38,8 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
@@ 58,7 +58,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
 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. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ 123,8 +123,8 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
move: (posnP (@task_cost _ H tsk)) => [ZEROPOS].
{ intros j ARR TSK.
have ZEROj: job_cost j = 0.
 { move: (H_job_cost_le_task_cost j ARR) => NEQ.
 rewrite /job_cost_le_task_cost TSK ZERO in NEQ.
+ { move: (H_valid_job_cost j ARR) => NEQ.
+ rewrite /valid_job_cost TSK ZERO in NEQ.
by apply/eqP; rewrite leqn0.
}
by rewrite /job_response_time_bound /completed_by ZEROj.
diff git a/restructuring/results/fixed_priority/rta/fully_preemptive.v b/restructuring/results/fixed_priority/rta/fully_preemptive.v
index 3f63abc..34d4e11 100644
 a/restructuring/results/fixed_priority/rta/fully_preemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_preemptive.v
@@ 38,8 +38,8 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
diff git a/restructuring/results/fixed_priority/rta/limited_preemptive.v b/restructuring/results/fixed_priority/rta/limited_preemptive.v
index b821009..735a3dd 100644
 a/restructuring/results/fixed_priority/rta/limited_preemptive.v
+++ b/restructuring/results/fixed_priority/rta/limited_preemptive.v
@@ 39,8 +39,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
 Hypothesis H_job_cost_le_task_cost:
 cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+ Hypothesis H_valid_job_cost:
+ arrivals_have_valid_job_costs arr_seq.
(** First, we assume we have the model with fixed preemption points.
I.e., each task is divided into a number of nonpreemptive segments
@@ 65,8 +65,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
 Hypothesis H_valid_schedule_with_limited_preemptions:
 valid_schedule_with_limited_preemptions arr_seq sched.
+ Hypothesis H_schedule_respects_preemption_model:
+ schedule_respects_preemption_model arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ 130,8 +130,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
move: (MLP) => [BEGj [ENDj _]].
edestruct (posnP (task_cost tsk)) as [ZEROPOSt].
{ intros j ARR TSK.
 move: (H_job_cost_le_task_cost _ ARR) => POSt.
 move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
+ move: (H_valid_job_cost _ ARR) => POSt.
+ move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
by rewrite /job_response_time_bound /completed_by Z.
}
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
diff git a/scripts/wordlist.pws b/scripts/wordlist.pws
index a07fcdf..4ee125d 100644
 a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ 1,6 +1,7 @@
personal_ws1.1 en 0
Prosa
Coq
+ssreflect
typeclass
iff
schedulability
@@ 35,9 +36,13 @@ RTA
IBF
RBF
RBFs
+WCET
+WCETs
Layland
Liu
sequentiality
equalities
extremum
supremum
+runtime
+bursty

GitLab