Library probsa.rt.model.assumptions.basic
From prosa.model Require Export task.arrival.sporadic priority.classes processor.platform_properties.
From prosa.analysis Require Export facts.behavior.completion.
From probsa.rt.behavior Require Export arrival_sequence service.
From probsa.rt.model Require Export task.
Local Open Scope nat_scope.
Section CommonAssumptions.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{P : SporadicModel Task}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable (ts : seq Task) (tsk : Task).
Definition arrivals_from_task_set :=
∀ (j : Job) (ω : Ω), arrives_in (arr_seq ω) j → job_task j \in ts.
Definition arrivals_cost_consistent :=
∀ (j : Job) (ω : Ω),
arrives_in (arr_seq ω) j →
isSome (job_cost j ω).
Definition pr_arrival_sequence_uniq :=
∀ (ω : Ω), arrival_sequence_uniq (arr_seq ω).
Definition constrained_deadlines :=
∀ tsk, tsk \in ts → (D tsk ≤ task_min_inter_arrival_time tsk)%nat.
Definition pr_taskset_respects_sporadic_task_model :=
∀ (ω : Ω),
@taskset_respects_sporadic_task_model
Task _ ts Job _ (sample0_arrivals ω) (arr_seq ω).
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Definition pr_jobs_must_arrive_to_execute :=
∀ (ω : Ω),
@jobs_must_arrive_to_execute
_ _ (pr_sched ω) (sample0_arrivals ω).
Definition pr_completed_jobs_dont_execute :=
∀ (ω : Ω),
@completed_jobs_dont_execute
_ _ (pr_sched ω) (sample0_costs ω).
Definition pr_jobs_come_from_arrival_sequence :=
∀ (ω : Ω),
jobs_come_from_arrival_sequence (pr_sched ω) (arr_seq ω).
End CommonAssumptions.
Section ArrivalsConsistentWithDeadlines.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Lemma arrivals_consistent_with_deadlines :
∀ j ω,
arrives_in (arr_seq ω) j →
isSome (job_deadline j ω).
End ArrivalsConsistentWithDeadlines.
Section PrServiceBounded.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
Hypothesis H_pr_completed_jobs_dont_execute : pr_completed_jobs_dont_execute pr_sched.
Lemma pr_service_bounded_by_pr_job_cost :
∀ (j : Job) (t : instant) (ω : Ω),
service (pr_sched ω) j t ≤ odflt 0 (job_cost j ω).
End PrServiceBounded.
Section SchedImpliesArrivalTime.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence pr_sched.
Lemma scheduled_at_implies_exists_arrival_time :
∀ (j : Job) (t : instant) (ω : Ω),
scheduled_at (pr_sched ω) j t →
∃ A, job_arrival j ω = Some A.
End SchedImpliesArrivalTime.
Section SchedImpliesArrivalTime.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_pr_jobs_must_arrive_to_execute : pr_jobs_must_arrive_to_execute pr_sched.
Variable ω : Ω.
Variable (j : Job) (A : instant).
Hypothesis H_j_arrival : job_arrival j ω = Some A.
Variables (t t' : instant) (Δ : duration).
Hypothesis H_t_interval : t ≤ t' < t + Δ.
Hypothesis H_j_scheduled_at : scheduled_at (pr_sched ω) j t'.
Let arrived_between := arrived_between (H := fun j ⇒ odflt0 (job_arrival j) ω).
Lemma scheduled_at_implies_arrived_between :
t ≤ A →
arrived_between j t (t + Δ).
Lemma scheduled_at_implies_arrived_between' :
A < t →
arrived_between j 0 t.
Lemma scheduled_at_implies_arrived_between'' :
odflt0 (job_arrival j) ω ≤ t'.
End SchedImpliesArrivalTime.
From prosa.analysis Require Export facts.behavior.completion.
From probsa.rt.behavior Require Export arrival_sequence service.
From probsa.rt.model Require Export task.
Local Open Scope nat_scope.
Section CommonAssumptions.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{P : SporadicModel Task}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable (ts : seq Task) (tsk : Task).
Definition arrivals_from_task_set :=
∀ (j : Job) (ω : Ω), arrives_in (arr_seq ω) j → job_task j \in ts.
Definition arrivals_cost_consistent :=
∀ (j : Job) (ω : Ω),
arrives_in (arr_seq ω) j →
isSome (job_cost j ω).
Definition pr_arrival_sequence_uniq :=
∀ (ω : Ω), arrival_sequence_uniq (arr_seq ω).
Definition constrained_deadlines :=
∀ tsk, tsk \in ts → (D tsk ≤ task_min_inter_arrival_time tsk)%nat.
Definition pr_taskset_respects_sporadic_task_model :=
∀ (ω : Ω),
@taskset_respects_sporadic_task_model
Task _ ts Job _ (sample0_arrivals ω) (arr_seq ω).
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Definition pr_jobs_must_arrive_to_execute :=
∀ (ω : Ω),
@jobs_must_arrive_to_execute
_ _ (pr_sched ω) (sample0_arrivals ω).
Definition pr_completed_jobs_dont_execute :=
∀ (ω : Ω),
@completed_jobs_dont_execute
_ _ (pr_sched ω) (sample0_costs ω).
Definition pr_jobs_come_from_arrival_sequence :=
∀ (ω : Ω),
jobs_come_from_arrival_sequence (pr_sched ω) (arr_seq ω).
End CommonAssumptions.
Section ArrivalsConsistentWithDeadlines.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Lemma arrivals_consistent_with_deadlines :
∀ j ω,
arrives_in (arr_seq ω) j →
isSome (job_deadline j ω).
End ArrivalsConsistentWithDeadlines.
Section PrServiceBounded.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
Hypothesis H_pr_completed_jobs_dont_execute : pr_completed_jobs_dont_execute pr_sched.
Lemma pr_service_bounded_by_pr_job_cost :
∀ (j : Job) (t : instant) (ω : Ω),
service (pr_sched ω) j t ≤ odflt 0 (job_cost j ω).
End PrServiceBounded.
Section SchedImpliesArrivalTime.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence pr_sched.
Lemma scheduled_at_implies_exists_arrival_time :
∀ (j : Job) (t : instant) (ω : Ω),
scheduled_at (pr_sched ω) j t →
∃ A, job_arrival j ω = Some A.
End SchedImpliesArrivalTime.
Section SchedImpliesArrivalTime.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_pr_jobs_must_arrive_to_execute : pr_jobs_must_arrive_to_execute pr_sched.
Variable ω : Ω.
Variable (j : Job) (A : instant).
Hypothesis H_j_arrival : job_arrival j ω = Some A.
Variables (t t' : instant) (Δ : duration).
Hypothesis H_t_interval : t ≤ t' < t + Δ.
Hypothesis H_j_scheduled_at : scheduled_at (pr_sched ω) j t'.
Let arrived_between := arrived_between (H := fun j ⇒ odflt0 (job_arrival j) ω).
Lemma scheduled_at_implies_arrived_between :
t ≤ A →
arrived_between j t (t + Δ).
Lemma scheduled_at_implies_arrived_between' :
A < t →
arrived_between j 0 t.
Lemma scheduled_at_implies_arrived_between'' :
odflt0 (job_arrival j) ω ≤ t'.
End SchedImpliesArrivalTime.