# Library prosa.analysis.facts.behavior.arrivals

Require Export prosa.behavior.all.
Require Export prosa.util.all.
Require Export prosa.model.task.arrivals.

# Arrival Sequence

First, we relate the stronger to the weaker arrival predicates.
Section ArrivalPredicates.
Consider any kinds of jobs with arrival times.
Context {Job : JobType} `{JobArrival Job}.
A job that arrives in some interval `[t1, t2)` certainly arrives before time t2.
Lemma arrived_between_before :
∀ j t1 t2,
arrived_between j t1 t2 →
arrived_before j t2.
A job that arrives before a time t certainly has arrived by time t.
Lemma arrived_before_has_arrived :
∀ j t,
arrived_before j t →
has_arrived j t.
Furthermore, we restate a common hypothesis to make its implication easier to discover.
Lemma consistent_times_valid_arrival :
∀ arr_seq,
valid_arrival_sequence arr_seq → consistent_arrival_times arr_seq.
We restate another common hypothesis to make its implication easier to discover.
Lemma uniq_valid_arrival :
∀ arr_seq,
valid_arrival_sequence arr_seq → arrival_sequence_uniq arr_seq.
End ArrivalPredicates.
In this section, we relate job readiness to has_arrived.
Section Arrived.
Consider any kinds of jobs and any kind of processor state.
Context {Job : JobType} {PState : ProcessorState Job}.
Consider any schedule...
Variable sched : schedule PState.
...and suppose that jobs have a cost, an arrival time, and a notion of readiness.
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context {jr : JobReady Job PState}.
First, we note that readiness models are by definition consistent w.r.t. pending.
Lemma any_ready_job_is_pending :
∀ j t,
job_ready sched j t → pending sched j t.
Next, we observe that a given job must have arrived to be ready...
Lemma ready_implies_arrived :
∀ j t, job_ready sched j t → has_arrived j t.
...and lift this observation also to the level of whole schedules.
Lemma jobs_must_arrive_to_be_ready :
jobs_must_be_ready_to_execute sched → jobs_must_arrive_to_execute sched.
Furthermore, in a valid schedule, jobs must arrive to execute.
Corollary valid_schedule_implies_jobs_must_arrive_to_execute :
∀ arr_seq,
valid_schedule sched arr_seq → jobs_must_arrive_to_execute sched.
Since backlogged jobs are by definition ready, any backlogged job must have arrived.
Corollary backlogged_implies_arrived :
∀ j t,
backlogged sched j t → has_arrived j t.
Similarly, since backlogged jobs are by definition pending, any backlogged job must be incomplete.
Lemma backlogged_implies_incomplete :
∀ j t,
backlogged sched j t → ~~ completed_by sched j t.
Finally, we restate common hypotheses on the well-formedness of schedules to make their implications more easily discoverable. First, on the readiness of scheduled jobs, ...
Lemma job_scheduled_implies_ready :
jobs_must_be_ready_to_execute sched →
∀ j t,
scheduled_at sched j t → job_ready sched j t.
... second, on the origin of scheduled jobs, and ...
Lemma valid_schedule_jobs_come_from_arrival_sequence :
∀ arr_seq,
valid_schedule sched arr_seq →
jobs_come_from_arrival_sequence sched arr_seq.
... third, on the readiness of jobs in valid schedules.
Lemma valid_schedule_jobs_must_be_ready_to_execute :
∀ arr_seq,
valid_schedule sched arr_seq → jobs_must_be_ready_to_execute sched.
End Arrived.
In this section, we establish useful facts about arrival sequence prefixes.
Section ArrivalSequencePrefix.
Consider any kind of tasks and jobs.
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobArrival Job}.
Context `{JobTask Job Task}.
Consider any job arrival sequence.
Variable arr_seq : arrival_sequence Job.
We begin with basic lemmas for manipulating the sequences.
We show that the set of arriving jobs can be split into disjoint intervals.
Lemma arrivals_between_cat :
∀ t1 t t2,
t1 ≤ t →
t ≤ t2 →
arrivals_between arr_seq t1 t2
= arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
We also prove a stronger version of the above lemma in the case of arrivals that satisfy a predicate P.
Lemma arrivals_P_cat :
∀ P t t1 t2,
t1 ≤ t < t2 →
arrivals_between_P arr_seq P t1 t2
= arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2.
The same observation applies to membership in the set of arrived jobs.
Lemma arrivals_between_mem_cat :
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in arrivals_between arr_seq t1 t2
= (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
We observe that we can grow the considered interval without "losing" any arrived jobs, i.e., membership in the set of arrived jobs is monotonic.
Lemma arrivals_between_sub :
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in arrivals_between arr_seq t1 t2 →
j \in arrivals_between arr_seq t1' t2'.
Next, we relate the arrival prefixes with job arrival times.
Section ArrivalTimes.
Assume that job arrival times are consistent.
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
To make the hypothesis and its implication easier to discover, we restate it as a trivial lemma.
Lemma job_arrival_arrives_at :
∀ {j t},
arrives_at arr_seq j t → job_arrival j = t.
Similarly, to simplify subsequent proofs, we restate the H_consistent_arrival_times assumption as a trivial corollary.
Lemma job_arrival_at :
∀ {j t},
j \in arr_seq t → job_arrival j = t.
Next, we prove that if j is a part of the arrival sequence, then the converse of the above also holds.
Lemma job_in_arrivals_at :
∀ j t,
arrives_in arr_seq j →
job_arrival j = t →
j \in arr_seq t.
To begin with actual properties, we observe that any job in the set of all arrivals between time instants t1 and t2 must arrive in the interval `[t1,t2)`.
Lemma job_arrival_between :
∀ {j t1 t2},
j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j < t2.
For convenience, we restate the left bound of the above lemma...
Corollary job_arrival_between_ge :
∀ {j t1 t2},
j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j.
... as well as the right bound separately as corollaries.
Corollary job_arrival_between_lt :
∀ {j t1 t2},
j \in arrivals_between arr_seq t1 t2 → job_arrival j < t2.
Consequently, if we filter the list of arrivals in an interval `[t1,t2)` with an arrival-time threshold less than t1, we are left with an empty list.
Lemma arrivals_between_filter_nil :
∀ t1 t2 t,
t < t1 →
[seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t] = [::].
Furthermore, if we filter the list of arrivals in an interval `[t1,t2)` with an arrival-time threshold less than t2, we can simply discard the tail past the threshold.
Lemma arrivals_between_filter :
∀ t1 t2 t,
t ≤ t2 →
arrivals_between arr_seq t1 t
= [seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t].
Next, we prove that if a job belongs to the prefix (jobs_arrived_before t), then it arrives in the arrival sequence.
Lemma in_arrivals_implies_arrived :
∀ j t1 t2,
j \in arrivals_between arr_seq t1 t2 →
arrives_in arr_seq j.
We also prove a weaker version of the above lemma.
Lemma in_arrseq_implies_arrives :
∀ t j,
j \in arr_seq t →
arrives_in arr_seq j.
Next, we prove that if a job belongs to the prefix (jobs_arrived_between t1 t2), then it indeed arrives between t1 and t2.
Lemma in_arrivals_implies_arrived_between :
∀ j t1 t2,
j \in arrivals_between arr_seq t1 t2 →
arrived_between j t1 t2.
Similarly, if a job belongs to the prefix (jobs_arrived_before t), then it indeed arrives before time t.
Lemma in_arrivals_implies_arrived_before :
∀ j t,
j \in arrivals_before arr_seq t →
arrived_before j t.
Similarly, we prove that if a job from the arrival sequence arrives before t, then it belongs to the sequence (jobs_arrived_before t).
Lemma arrived_between_implies_in_arrivals :
∀ j t1 t2,
arrives_in arr_seq j →
arrived_between j t1 t2 →
j \in arrivals_between arr_seq t1 t2.
Any job in arrivals between time instants t1 and t2 must arrive in the interval `[t1,t2)`.
Lemma job_arrival_between_P :
∀ j P t1 t2,
j \in arrivals_between_P arr_seq P t1 t2 →
t1 ≤ job_arrival j < t2.
Any job j is in the sequence arrivals_between t1 t2 given that j arrives in the interval `[t1,t2)`.
Lemma job_in_arrivals_between :
∀ j t1 t2,
arrives_in arr_seq j →
t1 ≤ job_arrival j →
job_arrival j < t2 →
j \in arrivals_between arr_seq t1 t2.
Next, we prove that if the arrival sequence doesn't contain duplicate jobs, the same applies for any of its prefixes.
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq →
∀ t1 t2, uniq (arrivals_between arr_seq t1 t2).
Also note that there can't by any arrivals in an empty time interval.
Lemma arrivals_between_geq :
∀ t1 t2,
t1 ≥ t2 →
arrivals_between arr_seq t1 t2 = [::].
Conversely, if a job arrives, the considered interval is non-empty.
Corollary arrivals_between_nonempty :
∀ t1 t2 j,
j \in arrivals_between arr_seq t1 t2 → t1 < t2.
Given jobs j1 and j2 in arrivals_between_P arr_seq P t1 t2, the fact that j2 arrives strictly before j1 implies that j2 also belongs in the sequence arrivals_between_P arr_seq P t1 (job_arrival j1).
Lemma arrival_lt_implies_job_in_arrivals_between_P :
∀ (j1 j2 : Job) (P : Job → bool) (t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 →
j2 \in arrivals_between_P arr_seq P t1 t2 →
job_arrival j2 < job_arrival j1 →
j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).
For ease of rewriting, we establish the equivalence between a job's membership in arrivals_between and its membership in arrives_in, subject to constraints on the job's arrival time.
Lemma job_arrival_in_bounds :
∀ (j : Job) (t1 t2 : instant),
(j \in arrivals_between arr_seq t1 t2)
↔ (arrives_in arr_seq j ∧ t1 ≤ job_arrival j < t2).
We observe that, by construction, the sequence of arrivals is sorted by arrival times. To this end, we first define the order relation.
Definition by_arrival_times (j1 j2 : Job) : bool := job_arrival j1 ≤ job_arrival j2.
Trivially, the arrivals at any one point in time are ordered w.r.t. arrival times.
Lemma arrivals_at_sorted :
∀ t,
sorted by_arrival_times (arr_seq t).
By design, the list of arrivals in any interval is sorted.
Lemma arrivals_between_sorted :
∀ t1 t2,
sorted by_arrival_times (arrivals_between arr_seq t1 t2).
End ArrivalTimes.
In the following section, we establish a lemma that allows splitting the arrival sequence by task.
Section ArrivalPartition.
If all jobs stem from tasks in a given task set ts...
Variable ts : seq Task.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
... then we can partition the arrival sequence by task.
Lemma arrivals_between_partitioned_by_task :
∀ t1 t2 j,
(j \in arrivals_between arr_seq t1 t2)
= (j \in \cat_(tsk <- ts) task_arrivals_between arr_seq tsk t1 t2).
End ArrivalPartition.
End ArrivalSequencePrefix.
In this section, we establish a few auxiliary facts about the relation between the property of being scheduled and arrival predicates to facilitate automation.
Section ScheduledImpliesArrives.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Consider any kind of processor state model, ...
Context {PState : ProcessorState Job}.
... any job arrival sequence with consistent arrivals, ....
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
... and any schedule of this arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
... where jobs do not execute before their arrival.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Next, consider a job j ...
Variable j : Job.
... which is scheduled at a time instant t.
Variable t : instant.
Hypothesis H_scheduled_at : scheduled_at sched j t.
Then we show that j arrives in arr_seq.
Lemma arrives_in_jobs_come_from_arrival_sequence :
arrives_in arr_seq j.
Job j has arrived by time instant t.
Lemma arrived_between_jobs_must_arrive_to_execute :
has_arrived j t.
For any future time t', job j arrives before t'.
Lemma arrivals_before_scheduled_at :
∀ t',
t < t' →
j \in arrivals_before arr_seq t'.
Similarly, job j arrives up to time t' for any t' such that t ≤ t'.
Lemma arrivals_up_to_scheduled_at :
∀ t',
t ≤ t' →
j \in arrivals_up_to arr_seq t'.
End ScheduledImpliesArrives.
We add some of the above lemmas to the "Hint Database" basic_rt_facts, so the auto tactic will be able to use them.
Global Hint Resolve
any_ready_job_is_pending
arrivals_before_scheduled_at
arrivals_uniq
arrived_between_implies_in_arrivals
arrived_between_jobs_must_arrive_to_execute
arrives_in_jobs_come_from_arrival_sequence
backlogged_implies_arrived
job_scheduled_implies_ready
jobs_must_arrive_to_be_ready
jobs_must_arrive_to_be_ready
ready_implies_arrived
valid_schedule_implies_jobs_must_arrive_to_execute
valid_schedule_jobs_come_from_arrival_sequence
valid_schedule_jobs_must_be_ready_to_execute
uniq_valid_arrival
consistent_times_valid_arrival
job_arrival_arrives_at
job_in_arrivals_between
: basic_rt_facts.