From e122dbb1d67b6e02adeb6a065c03d74207035ff1 Mon Sep 17 00:00:00 2001
From: Marco Maida <mmaida@mpi-sws.org>
Date: Mon, 9 May 2022 10:04:58 +0000
Subject: [PATCH] introduce "greedy" concrete arrival sequence
This commit defines and adds facts about a concrete arrival sequence in
which tasks release jobs "as quickly as possible" as allowed by their
respective arrival-curve constraints. This maximal arrival sequence is
used in POET to generate assumption-less certificates.
---
.../definitions/maximal_arrival_sequence.v | 88 ++++++
.../facts/maximal_arrival_sequence.v | 266 ++++++++++++++++++
2 files changed, 354 insertions(+)
create mode 100644 implementation/definitions/maximal_arrival_sequence.v
create mode 100644 implementation/facts/maximal_arrival_sequence.v
diff --git a/implementation/definitions/maximal_arrival_sequence.v b/implementation/definitions/maximal_arrival_sequence.v
new file mode 100644
index 000000000..c46090c50
--- /dev/null
+++ b/implementation/definitions/maximal_arrival_sequence.v
@@ -0,0 +1,88 @@
+Require Export prosa.model.task.arrival.curves.
+Require Export prosa.util.supremum.
+
+(** * A Maximal Arrival Sequence *)
+
+(** 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 [max_arrivals] 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 instant without violating the
+ corresponding arrival curve. *)
+ Section NumberOfJobs.
+
+ (** Let [tsk] be any task. *)
+ Variable tsk : Task.
+
+ (** First, we introduce a function that computes the sum of all elements in
+ a given list's 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.
diff --git a/implementation/facts/maximal_arrival_sequence.v b/implementation/facts/maximal_arrival_sequence.v
new file mode 100644
index 000000000..73856ca88
--- /dev/null
+++ b/implementation/facts/maximal_arrival_sequence.v
@@ -0,0 +1,266 @@
+Require Export prosa.analysis.facts.model.task_arrivals.
+Require Export prosa.implementation.definitions.maximal_arrival_sequence.
+
+(** Recall that, given an arrival curve [max_arrivals] and a
+ job-generating function [generate_jobs_at], the function
+ [concrete_arrival_sequence] generates an arrival sequence. In this
+ section, we prove a few properties of this function. *)
+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}.
+
+ (** Consider a task set [ts] with non-duplicate tasks. *)
+ Variable ts : seq Task.
+ Hypothesis H_ts_uniq : uniq ts.
+
+ (** Let [max_arrivals] be a family of valid arrival curves, i.e.,
+ for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+ bound of [tsk], and (2) it is a monotonic function that equals [0]
+ for the empty interval [delta = 0]. *)
+ Context `{MaxArrivals Task}.
+ Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+
+ (** Further assume we are given a function that generates the required number of
+ jobs of a given task at a given instant of time. *)
+ Variable generate_jobs_at : Task -> nat -> instant -> seq Job.
+
+ (** First, we assume that [generate_jobs_at tsk n t] generates [n] jobs. *)
+ Hypothesis H_job_generation_valid_number:
+ forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n.
+
+ (** Second, we assume that [generate_jobs_at tsk n t] generates jobs of task
+ [tsk] that arrive at time [t]. *)
+ Hypothesis H_job_generation_valid_jobs:
+ forall (tsk : Task) (n : nat) (t : instant) (j : Job),
+ (j \in generate_jobs_at tsk n t) ->
+ job_task j = tsk
+ /\ job_arrival j = t
+ /\ job_cost j <= task_cost tsk.
+
+ (** Finally, we assume that all jobs generated by [generate_jobs_at] are unique. *)
+ Hypothesis H_jobs_unique:
+ forall (t1 t2 : instant),
+ uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2).
+
+ (** Assuming such a well-behaved "constructor" [generate_jobs_at], we prove a
+ few validity claims about an arrival sequence generated by
+ [concrete_arrival_sequence]. *)
+ Section ValidityClaims.
+
+ (** We start by showing that the obtained arrival sequence is a set. *)
+ Lemma arr_seq_is_a_set :
+ arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts).
+ Proof.
+ move=> t.
+ move: (H_jobs_unique t t.+1).
+ by rewrite /arrivals_between big_nat1.
+ Qed.
+
+ (** Next, we show that all jobs in the arrival sequence come from [ts]. *)
+ Lemma concrete_all_jobs_from_taskset :
+ all_jobs_from_taskset (concrete_arrival_sequence generate_jobs_at ts) ts.
+ Proof.
+ move=> j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
+ move: (H_job_generation_valid_jobs tsk _ _ _ IN) => [JOB_TASK _].
+ by rewrite JOB_TASK.
+ Qed.
+
+ (** Further, we note that the jobs in the arrival sequence have consistent
+ arrival times. *)
+ Lemma arrival_times_are_consistent :
+ consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts).
+ Proof.
+ move=> j t /mem_bigcat_exists [tsk [TSK_IN IN]].
+ by move: (H_job_generation_valid_jobs tsk _ _ _ IN) => [_ [JOB_ARR _]].
+ Qed.
+
+ (** Lastly, we observe that the jobs in the arrival sequence have valid job
+ costs. *)
+ Lemma concrete_valid_job_cost :
+ arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts).
+ Proof.
+ move=> j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
+ move: (H_job_generation_valid_jobs tsk _ _ _ IN) => [JOB_TASK [_ JOB_COST]].
+ by rewrite /valid_job_cost JOB_TASK.
+ Qed.
+
+ End ValidityClaims.
+
+ (** In this section, we prove a series of facts regarding the maximal arrival
+ sequence, leading up to the main theorem that all arrival-curve
+ constraints are respected. *)
+ Section Facts.
+
+ (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+ Variable tsk : Task.
+ Hypothesis H_tsk_in_ts : tsk \in ts.
+
+ (** First, we show that the arrivals at time [t] are indeed generated by
+ [generate_jobs_at] applied at time [t]. *)
+ Lemma task_arrivals_at_eq_generate_jobs_at:
+ forall t,
+ task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t
+ = generate_jobs_at tsk (max_arrivals_at tsk t) t.
+ Proof.
+ move=> t.
+ rewrite /task_arrivals_at bigcat_filter_eq_filter_bigcat bigcat_seq_uniqK // => tsk0 j INj.
+ apply H_job_generation_valid_jobs in INj.
+ by destruct INj.
+ Qed.
+
+ (** Next, we show that the number of arrivals at time [t] always matches
+ [max_arrivals_at] applied at time [t]. *)
+ Lemma task_arrivals_at_eq:
+ forall t,
+ size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
+ = max_arrivals_at tsk t.
+ Proof.
+ move=> t.
+ rewrite task_arrivals_at_eq_generate_jobs_at //.
+ by apply H_job_generation_valid_number.
+ Qed.
+
+ (** We then generalize the previous result to an arbitrary interval
+ <<[t1,t2)>>. *)
+ Lemma number_of_task_arrivals_eq :
+ forall t1 t2,
+ number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2
+ = \sum_(t1 <= t < t2) max_arrivals_at tsk t.
+ Proof.
+ move=> t1 t2.
+ rewrite /number_of_task_arrivals task_arrivals_between_is_cat_of_task_arrivals_at -size_big_nat.
+ apply eq_big_nat => t RANGE.
+ by apply task_arrivals_at_eq.
+ Qed.
+
+ (** We further show that, starting from an empty prefix and applying
+ [extend_arrival_prefix] [t] times, we end up with a prefix of size
+ [t]... *)
+ Lemma extend_horizon_size :
+ forall t,
+ size (iter t (extend_arrival_prefix tsk) [::]) = t.
+ Proof. by elim=> // t IHt; rewrite size_cat IHt //=; lia. Qed.
+
+ (** ...and that the arrival sequence prefix up to an arbitrary horizon
+ [t] is a sequence of [t+1] elements. *)
+ Lemma prefix_up_to_size :
+ forall t,
+ size (maximal_arrival_prefix tsk t) = t.+1.
+ Proof.
+ by elim=> // t IHt; rewrite /maximal_arrival_prefix /extend_arrival_prefix size_cat IHt //=; lia.
+ Qed.
+
+ (** Next, we prove prefix inclusion for [maximal_arrival_prefix] when the
+ horizon is expanded by one... *)
+ Lemma n_arrivals_at_prefix_inclusion1 :
+ forall t h,
+ t <= h ->
+ nth 0 (maximal_arrival_prefix tsk h) t
+ = nth 0 (maximal_arrival_prefix tsk h.+1) t.
+ Proof.
+ move=> t h LEQ.
+ rewrite /maximal_arrival_prefix //= {3}/extend_arrival_prefix nth_cat prefix_up_to_size.
+ by case: (ltnP t h.+1); lia.
+ Qed.
+
+ (** ...and we generalize the previous result to two arbitrary horizons [h1 <= h2]. *)
+ Lemma n_arrivals_at_prefix_inclusion :
+ forall t h1 h2,
+ t <= h1 <= h2 ->
+ nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.
+ Proof.
+ move=> t h1 h2 /andP[LEQh1 LEQh2].
+ induction h2; [by have -> : h1 = 0; lia |].
+ rewrite leq_eqVlt in LEQh2.
+ move: LEQh2 => /orP [/eqP EQ | LT]; first by rewrite EQ.
+ feed IHh2; first by lia.
+ rewrite -n_arrivals_at_prefix_inclusion1 //.
+ by lia.
+ Qed.
+
+ (** Next, we prove that, for any positive time instant [t], [max_arrivals_at] indeed
+ matches the arrivals of [next_max_arrival] applied at [t-1]. *)
+ Lemma max_arrivals_at_next_max_arrivals_eq:
+ forall t,
+ 0 < t ->
+ max_arrivals_at tsk t
+ = next_max_arrival tsk (maximal_arrival_prefix tsk t.-1).
+ Proof.
+ move => t GT0.
+ move: prefix_up_to_size; rewrite /maximal_arrival_prefix => PUS.
+ rewrite /max_arrivals_at /maximal_arrival_prefix {1}/extend_arrival_prefix nth_cat extend_horizon_size //= ltnn //= subnn //=.
+ by destruct t.
+ Qed.
+
+ (** Given a time instant [t] and and interval [Δ], we show that
+ [max_arrivals_at] applied at time [t] is always less-or-equal to
+ [max_arrivals] applied to [Δ+1], even when each value of
+ [max_arrivals_at] in the interval <<[t-Δ, t)>> is subtracted from it. *)
+ Lemma n_arrivals_at_leq :
+ forall t Δ,
+ Δ <= t ->
+ max_arrivals_at tsk t
+ <= max_arrivals tsk Δ.+1 - \sum_(t - Δ <= i < t) max_arrivals_at tsk i.
+ Proof.
+ move=> t Δ LEQ.
+ move: (H_valid_arrival_curve tsk H_tsk_in_ts) => [ZERO MONO].
+ destruct t.
+ { rewrite unlock //= subn0.
+ rewrite /max_arrivals_at /maximal_arrival_prefix /extend_arrival_prefix
+ /next_max_arrival //= /suffix_sum subn0 unlock subn0.
+ by apply MONO. }
+ { rewrite max_arrivals_at_next_max_arrivals_eq; last by done.
+ rewrite /next_max_arrival /jobs_remaining prefix_up_to_size.
+ simpl (t.+1.-1).
+ destruct supremum eqn:SUP; last by move:(supremum_none _ _ SUP); rewrite map_cons.
+ eapply (supremum_spec _ leqnn leq_total leq_trans _ _ SUP).
+ rewrite /suffix_sum prefix_up_to_size /max_arrivals_at.
+ have -> : \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk i) i =
+ \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i.
+ { apply eq_big_nat => i RANGE.
+ by apply n_arrivals_at_prefix_inclusion; lia. }
+ set f := fun x => max_arrivals _ x.+1 - \sum_(t.+1-x <= i < t.+1) nth 0 (maximal_arrival_prefix _ t) i.
+ have-> : max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i = f Δ by done.
+ apply map_f.
+ by rewrite mem_iota; lia. }
+ Qed.
+
+ End Facts.
+
+ (** Finally, we prove our main result, that is, the proposed maximal arrival
+ sequence instantiation indeed respects all arrival-curve constraints. *)
+ Theorem concrete_is_arrival_curve :
+ taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts.
+ Proof.
+ move=> tsk IN t1 t LEQ.
+ set Δ := t - t1.
+ replace t1 with (t-Δ); last by lia.
+ have LEQd: Δ <= t by lia.
+ generalize Δ LEQd; clear LEQ Δ LEQd.
+ induction t; move => Δ LEQ.
+ { rewrite sub0n.
+ rewrite number_of_task_arrivals_eq //.
+ by vm_compute; rewrite unlock. }
+ { rewrite number_of_task_arrivals_eq //.
+ destruct Δ; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
+ rewrite subSS.
+ specialize (IHt Δ).
+ feed IHt; first by lia.
+ rewrite number_of_task_arrivals_eq // in IHt.
+ rewrite big_nat_recr //=; last by lia.
+ rewrite -leq_subRL; first apply n_arrivals_at_leq; try lia.
+ move: (H_valid_arrival_curve tsk IN) => [ZERO MONO].
+ apply (leq_trans IHt).
+ by apply MONO. }
+ Qed.
+
+End MaximalArrivalSequence.
+
--
GitLab