Library prosa.analysis.facts.preemption.task.preemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.preemption.job.preemptive.
Furthermore, we assume the fully non-preemptive task model.
Platform for Fully Preemptive Model
In this section, we prove that instantiation of functions [job_preemptable and task_max_nonpreemptive_segment] to the fully preemptive model indeed defines a valid preemption model with bounded non-preemptive regions.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of processor state model, ...
... any job arrival sequence, ...
... and any given schedule.
We prove that [fully_preemptive_model] function
defines a model with bounded non-preemptive regions.
Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 634)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros j ARR; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 639)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 640) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 663)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 664) is:
job_respects_max_nonpreemptive_segment j
subgoal 3 (ID 640) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 664)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 640) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 640)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
============================
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- intros t; ∃ t; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 715)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
t : duration
H4 : 0 <= t <= job_cost j
============================
t <= t <= t + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 716) is:
job_preemptable j t
----------------------------------------------------------------------------- *)
+ by apply/andP; split; [ done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 716)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
t : duration
H4 : 0 <= t <= job_cost j
============================
job_preemptable j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 634)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros j ARR; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 639)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 640) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 663)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 664) is:
job_respects_max_nonpreemptive_segment j
subgoal 3 (ID 640) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 664)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 640) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 640)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
============================
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- intros t; ∃ t; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 715)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
t : duration
H4 : 0 <= t <= job_cost j
============================
t <= t <= t + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 716) is:
job_preemptable j t
----------------------------------------------------------------------------- *)
+ by apply/andP; split; [ done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 716)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
ARR : arrives_in arr_seq j
t : duration
H4 : 0 <= t <= job_cost j
============================
job_preemptable j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Which together with lemma [valid_fully_preemptive_model] gives
us the fact that [fully_preemptive_model] defined a valid
preemption model with bounded non-preemptive regions.
Corollary fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 643)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 645)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 646) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
apply valid_fully_preemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 646)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
apply fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyPreemptiveModel.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 643)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 645)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 646) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
apply valid_fully_preemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 646)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
apply fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyPreemptiveModel.
We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Hint Resolve
valid_fully_preemptive_model
fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_facts.
valid_fully_preemptive_model
fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_facts.