Library rt.restructuring.analysis.basic_facts.preemption.task.preemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.preemption Require Import
valid_model job.instance.preemptive task.instance.preemptive.
From rt.restructuring.analysis.basic_facts.preemption Require Import
job.preemptive.
Platform for Fully Premptive 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 nonpremtive regions.
Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 38)
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 43)
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_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 44) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 67)
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_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 68) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 3 (ID 44) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 68)
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_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 44) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
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 119)
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 + (parameters.job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 120) is:
parameters.job_preemptable j t
----------------------------------------------------------------------------- *)
+ by apply/andP; split; [ done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
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
============================
parameters.job_preemptable j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 38)
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 43)
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_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 44) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 67)
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_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 68) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 3 (ID 44) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 68)
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_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 44) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
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 119)
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 + (parameters.job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 120) is:
parameters.job_preemptable j t
----------------------------------------------------------------------------- *)
+ by apply/andP; split; [ done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
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
============================
parameters.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 47)
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 49)
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 50) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
apply valid_fully_preemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
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.
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_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 47)
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 49)
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 50) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
apply valid_fully_preemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
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.
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.