Commit ce2cf22c authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add preliminary version of arrival curves

parent 8b622764
This diff is collapsed.
Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence
rt.model.arrival.basic.task_arrival.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div.
(* In this section, we define the notion of arrival curves, which
can be used to reason about the frequency of job arrivals. *)
Module ArrivalCurves.
Import ArrivalSequence TaskArrival.
Section DefiningArrivalCurves.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job -> Task.
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and let tsk be any task to be analyzed. *)
Variable tsk: Task.
(* Recall the job arrivals of tsk in a given interval [t1, t2). *)
Let arrivals_of_tsk := arrivals_of_task_between job_task arr_seq tsk.
Let num_arrivals_of_tsk := num_arrivals_of_task job_task arr_seq tsk.
(* First, we define what constitutes an arrival bound for task tsk. *)
Section ArrivalBound.
(* Let max_arrivals denote any function that takes an interval length and
returns the associated number of job arrivals of tsk.
(This corresponds to the eta+ function in the literature.) *)
Variable max_arrivals: time -> nat.
(* Then, we say that num_arrivals is an arrival bound iff, for any interval [t1, t2),
(num_arrivals (t2 - t1)) bounds the number of jobs of tsk that arrive in that interval. *)
Definition is_arrival_bound :=
forall t1 t2,
t1 <= t2 ->
num_arrivals_of_tsk t1 t2 <= max_arrivals (t2 - t1).
End ArrivalBound.
(* Next, we define the notion of a separation bound for task tsk, i.e., the smallest
interval length in which a certain number of jobs of tsk can be spawned. *)
Section SeparationBound.
(* Let min_length denote any function that takes a number of jobs and
returns an associated interval length.
(This corresponds to the delta- function in the literature.) *)
Variable min_length: nat -> time.
(* Then, we say that min_length is a separation bound iff, for any number of jobs
of tsk, min_separation lower-bounds the minimum interval length in which that number
of jobs can be spawned. *)
Definition is_separation_bound :=
forall t1 t2,
t1 <= t2 ->
min_length (num_arrivals_of_tsk t1 t2) <= t2 - t1.
End SeparationBound.
End DefiningArrivalCurves.
End ArrivalCurves.
\ No newline at end of file
Require Import Coq.Logic.ConstructiveEpsilon.
Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.arrival.curves.bounds.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div.
(* In this section, we show how to convert between arrival bounds and separation bounds. *)
Module ArrivalConversion.
Import ArrivalSequence ArrivalCurves.
(* For simplicity, we redefine some names. *)
Definition linear_search := constructive_indefinite_ground_description_nat.
(* Next, we show how to perform the conversion. *)
Section Conversion.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_task: Job -> Task.
(* Consider any job arrival sequence ...*)
Variable arr_seq: arrival_sequence Job.
(* ...and let tsk be any task to be analyzed. *)
Variable tsk: Task.
(* First, we convert an arrival bound into a separation bound. *)
Section ArrivalToSeparation.
(* Let max_arrivals be any arrival bound of tsk. *)
Variable max_arrivals: time -> nat.
Hypothesis H_is_arrival_bound:
is_arrival_bound job_task arr_seq tsk max_arrivals.
(* Assume that jobs of each task arrive infinitely often. *)
Hypothesis H_jobs_arrive_infinitely_often:
forall j1,
exists j2,
job_task j1 = job_task j2 /\
job_arrival j1 <= job_arrival j2.
(* Next, given any number of job arrivals, we show how to compute the minimum interval
length that can contain all these arrivals.
The computation is done using a linear search for larger values. *)
Section ComputingSeparationBound.
(* Consider any number of job arrivals. *)
Variable num_arrivals: time.
(* Then, we define a predicate that checks whether an interval delta is a separation
bound for this number of arrivals, ... *)
Definition contains_all_arrivals (delta: nat) :=
max_arrivals delta >= num_arrivals.
(* ...which we prove to be decidable (since it is a boolean). *)
Lemma contains_all_arrivals_decidable:
forall delta, {contains_all_arrivals delta} + {~ contains_all_arrivals delta}.
Proof.
by intros delta; apply Bool.bool_dec.
Qed.
(* Next, using the fact that jobs arrive infinitely often, we show that there always
exist an interval delta that contains this number of arrivals, ...*)
Lemma interval_exists:
exists delta, contains_all_arrivals delta.
Proof.
Admitted.
(* ...we run a linear search that looks for this delta. This returns
a value delta and a proof that delta contains all the arrivals. *)
Definition find_delta := linear_search contains_all_arrivals
contains_all_arrivals_decidable
interval_exists.
(* Next, we prove that this linear serch finds the minimum element that
satisfies the property.
(TODO: This proof is optional, just for tightness.
Also, it might require dealing with ConstructiveEpsilon). *)
Lemma find_delta_returns_min: true.
Admitted.
(* To conclude, we define the conversion from arrival bound to separation bound
as this number returned by the linear search. *)
Definition convert_to_separation_bound := proj1_sig find_delta.
End ComputingSeparationBound.
(* Based on the computation above, we prove that any value that is returned is indeed
a separation bound. *)
Lemma conversion_to_separation_bound_is_valid:
is_separation_bound job_task arr_seq tsk convert_to_separation_bound.
Proof.
intros t1 t2 LE.
Admitted.
End ArrivalToSeparation.
(* Next, we convert a separation bound into an arrival bound. *)
Section SeparationToArrival.
(* Let min_length be any separation bound of tsk. *)
Variable min_length: nat -> time.
Hypothesis H_is_separation_bound:
is_separation_bound job_task arr_seq tsk min_length.
(* Then, by computing xxxxxx, ...*)
Definition convert_to_arrival_bound (k: time) := 0. (* TODO: FIX *)
(* ...we transform min_length to obtain an arrival bound. *)
Lemma conversion_to_upper_curve_succeeds:
is_arrival_bound job_task arr_seq tsk convert_to_arrival_bound.
Proof.
Admitted.
End SeparationToArrival.
End Conversion.
End ArrivalConversion.
\ No newline at end of file
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