Commit 4d5c9497 authored by Björn Brandenburg's avatar Björn Brandenburg

model reorg: merge job_preemptable def and validity

parent 7b38326f
......@@ -2,8 +2,8 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
......@@ -3,8 +3,8 @@ Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.model.arrival.arrival_curves.
......
......@@ -3,8 +3,8 @@ Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.analysis.abstract.core.definitions.
......
......@@ -3,9 +3,9 @@ Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
......@@ -164,36 +164,36 @@ Section ModelWithLimitedPreemptions.
(** Recall that file [job.parameters] also defines notion of
preemption poins. And note that
[job.parameters.job_preemption_points] cannot have a
[job.parameter.job_preemption_points] cannot have a
duplicating preemption points. Therefore, we need additional
lemmas to relate [job.parameters.job_preemption_points] and
lemmas to relate [job.parameter.job_preemption_points] and
[limited.job_preemption_points]]. *)
(** First we show that the length of the last non-preemptive
segment of [job.parameters.job_preemption_points] is equal to
segment of [job.parameter.job_preemption_points] is equal to
the length of the last non-empty non-preemptive segment of
[limited.job_preemption_points]. *)
Lemma job_parameters_last_np_to_job_limited:
last0 (distances (parameters.job_preemption_points j)) =
last0 (distances (parameter.job_preemption_points j)) =
last0 (filter (fun x => 0 < x) (distances (job_preemption_points j))).
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
intros; rewrite distances_iota_filtered; eauto.
rewrite -A2 //.
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
Qed.
(** Next we show that the length of the max non-preemptive
segment of [job.parameters.job_preemption_points] is equal to
segment of [job.parameter.job_preemption_points] is equal to
the length of the max non-preemptive segment of
[limited.job_preemption_points]. *)
Lemma job_parameters_max_np_to_job_limited:
max0 (distances (parameters.job_preemption_points j)) =
max0 (distances (parameter.job_preemption_points j)) =
max0 (distances (job_preemption_points j)).
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
intros; rewrite distances_iota_filtered; eauto 2.
rewrite max0_rem0 //.
rewrite -A2 //.
......
......@@ -4,8 +4,8 @@ Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.preemptive.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
......
......@@ -2,8 +2,8 @@ Require Import rt.util.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
(** * Run-to-Completion Threshold *)
......
......@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
......
......@@ -3,8 +3,8 @@ Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
......
......@@ -3,8 +3,8 @@ Require Import rt.util.nondecreasing.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
......@@ -68,7 +68,7 @@ Section FloatingNonPremptiveRegionsModel.
case: (posnP (job_cost j)) => [ZERO|POS].
- split.
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
exists 0; rewrite LE; split; first by apply/andP; split.
......
......@@ -3,8 +3,8 @@ Require Import rt.util.nondecreasing.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.instance.limited.
......@@ -66,7 +66,7 @@ Section LimitedPreemptionsModel.
case: (posnP (job_cost j)) => [ZERO|POS].
- split.
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
exists 0; rewrite LE; split; first by apply/andP; split.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.instance.preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
......
......@@ -7,8 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
......@@ -8,8 +8,8 @@ Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.aggregate.task_arrivals.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.schedule.preemption_time.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Export rt.restructuring.analysis.definitions.no_carry_in.
......
......@@ -7,8 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.schedule.work_conserving.
......
......@@ -7,8 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.schedule.work_conserving.
......
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.parameter.
Require Export rt.restructuring.model.task.preemption.parameters.
(** Definition of a parameter relating a job
......
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.parameter.
(** * Platform for Fully Non-Preemptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
......
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.parameter.
(** * Platform for Fully Premptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
......
......@@ -74,3 +74,69 @@ Section MaxAndLastNonpreemptiveSegment.
job_cost j - (job_last_nonpreemptive_segment j - ε).
End MaxAndLastNonpreemptiveSegment.
(** * Platform with limited preemptions *)
(** In the follwoing, we define properties that any reasonable job preemption
model must satisfy. *)
Section PreemptionModel.
(** Consider any type of jobs... *)
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. *)
Context `{JobPreemptable Job}.
(** Consider any kind of processor state model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
(** ... 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 non-preemptive. *)
Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
job_preemptable j 0.
(** And vice versa, a job cannot remain non-preemptive 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.
End PreemptionModel.
Require Export rt.restructuring.model.preemption.job.parameters.
(** * Platform with limited preemptions *)
(** In the follwoing, we define properties that any reasonable job preemption
model must satisfy. *)
Section PreemptionModel.
(** Consider any type of jobs... *)
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. *)
Context `{JobPreemptable Job}.
(** Consider any kind of processor state model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
(** ... 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 non-preemptive. *)
Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
job_preemptable j 0.
(** And vice versa, a job cannot remain non-preemptive 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.
End PreemptionModel.
Require Export rt.restructuring.model.processor.ideal.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.parameter.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.processor.ideal.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.parameter.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Preemption Time in Ideal Uni-Processor Model *)
......
Require Export rt.util.all.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.parameter.
Require Export rt.restructuring.model.task.concept.
(** * Static information about preemption points *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment