maximal_arrival_sequence.v 4.27 KiB
Require Import prosa.model.processor.ideal.
Require Import prosa.model.task.concept.
Require Import prosa.model.task.arrival.curves.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.util.all.
(** In this section, we propose a concrete instantiation of an arrival sequence.
Given an arbitrary arrival curve, the defined arrival sequence tries to
generate as many jobs as possible at any time instant by adopting a greedy
strategy: at each time [t], the arrival sequence contains the maximum possible
number of jobs that does not violate the given arrival curve's constraints. *)
Section MaximalArrivalSequence.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Let [MaxArrivals] denote any function that takes a task and an interval length
and returns the associated number of job arrivals of the task. *)
Context `{MaxArrivals Task}.
(** In this section, we define a procedure that computes the maximal
number of jobs that can be released at a given time instant
without violating the corresponding arrival curve. *)
Section NumberOfJobs.
(** Let [tsk] be any task. *)
Variable tsk : Task.
(** First, we define a function that, given a sequence [xs], keeps
only the last [n] elements. *)
Definition suffix (xs : seq nat) (n : nat) := drop (size xs - n) xs.
(** Next, we introduce a function that computes the sum of the suffix of length [n]. *)
Definition suffix_sum xs n :=
\sum_(size xs - n <= t < size xs) nth 0 xs t.
(** Let the arrival prefix [arr_prefix] be a sequence of natural
numbers where [nth xs t] denotes the number of jobs that
arrive at time [t]. Then, given an arrival curve
[max_arrivals] and an arrival prefix [arr_prefix], we define a
function that computes the number of jobs that can be
additionally released without violating the arrival curve.
The high-level idea is as follows. Let us assume that the length of
the arrival prefix is [Δ]. To preserve the sub-additive property, one
needs to go through all suffixes of the arrival prefix and pick
the minimum. *)
Definition jobs_remaining (arr_prefix : seq nat) :=
supremum leq [seq (max_arrivals tsk Δ.+1 - suffix_sum arr_prefix Δ) | Δ <- iota 0 (size arr_prefix).+1].
(** Further, We define the function [next_max_arrival] to handle a special
case: when the arrival prefix is empty, the function returns the value
of the arrival curve with a window length of [1]. Otherwise, it
returns the number the number of jobs that can additionally be
generated. *)
Definition next_max_arrival (arr_prefix : seq nat) :=
match jobs_remaining arr_prefix with
| None => max_arrivals tsk 1
| Some n => n
end.
(** Next, we define a function that extends by one a given arrival prefix... *)
Definition extend_arrival_prefix (arr_prefix : seq nat) := arr_prefix ++ [:: next_max_arrival arr_prefix ].
(** ... and a function that generates a maximal arrival prefix
of size [t], starting from an empty arrival prefix. *)
Definition maximal_arrival_prefix (t : nat) :=
iter t.+1 extend_arrival_prefix [::].
(** Finally, we define a function that returns the maximal number
of jobs that can be released at time [t]; this definition
assumes that at each time instant prior to time [t] the maximal
number of jobs were released. *)
Definition max_arrivals_at t := nth 0 (maximal_arrival_prefix t) t.
End NumberOfJobs.
(** Consider a function that generates [n] concrete jobs of
the given task at the given time instant. *)
Variable generate_jobs_at : Task -> nat -> instant -> seq Job.
(** The maximal arrival sequence of task set [ts] at time [t] is a
concatenation of sequences of generated jobs for each task. *)
Definition concrete_arrival_sequence (ts : seq Task) (t : instant) :=
\cat_(tsk <- ts) generate_jobs_at tsk (max_arrivals_at tsk t) t.
End MaximalArrivalSequence.