Library prosa.analysis.abstract.definitions
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Throughout this file, we assume ideal uni-processor schedules.
Definitions for Abstract Response-Time Analysis
In this module, we propose a set of definitions for the general framework for response-time analysis (RTA) of uni-processor scheduling of real-time tasks with arbitrary arrival models.
In this section, we introduce all the abstract notions required by the analysis.
Consider any type of job associated with any type of tasks...
... with arrival times and costs.
Consider any kind of processor state model.
Consider any arrival sequence...
... and any schedule of this arrival sequence.
Let [tsk] be any task that is to be analyzed
For simplicity, let's define some local names.
Recall that a job [j] is pending_earlier_and_at a time instant [t] iff job
[j] arrived before time [t] and is still not completed by time [t].
We are going to introduce two main variables of the analysis:
(a) interference, and (b) interfering workload.
a) Interference Execution of a job may be postponed by the environment and/or the system due to different
factors (preemption by higher-priority jobs, jitter, black-out periods in hierarchical
scheduling, lack of budget, etc.), which we call interference.
Besides, note that even the subsequent activation of a task can suffer from interference at
the beginning of its busy interval (despite the fact that this job hasn’t even arrived
at that moment!). Thus, it makes more sense (at least for the current busy-interval
analysis) to think about interference of a job as any interference within the
corresponding busy interval, and not after release of the job.
Based on that, assume a predicate that expresses whether a job [j] under consideration
incurs interference at a given time [t] (in the context of the schedule under consideration).
This will be used later to upper-bound job [j]'s response time. Note that a concrete
realization of the function may depend on the schedule, but here we do not require this
for the sake of simplicity and generality.
b) Interfering Workload In addition to interference, the analysis assumes that at any time [t], we know an upper
bound on the potential cumulative interference that can be incurred in the future by any
job (i.e., the total remaining potential delays). Based on that, assume a function
interfering_workload that indicates for any job [j], at any time [t], the amount of potential
interference for job [j] that is introduced into the system at time [t]. This function will be
later used to upper-bound the length of the busy window of a job.
One example of workload function is the "total cost of jobs that arrive at time [t] and
have higher-or-equal priority than job j". In some task models, this function expresses
the amount of the potential interference on job [j] that "arrives" in the system at time [t].
In order to bound the response time of a job, we must to consider the cumulative
interference and cumulative interfering workload.
Definition cumul_interference j t1 t2 := \sum_(t1 ≤ t < t2) interference j t.
Definition cumul_interfering_workload j t1 t2 := \sum_(t1 ≤ t < t2) interfering_workload j t.
Definition cumul_interfering_workload j t1 t2 := \sum_(t1 ≤ t < t2) interfering_workload j t.
Definition of Busy Interval Further analysis will be based on the notion of a busy interval. The overall idea of the
busy interval is to take into account the workload that cause a job under consideration to
incur interference. In this section, we provide a definition of an abstract busy interval.
We say that time instant [t] is a quiet time for job [j] iff two conditions hold.
First, the cumulative interference at time [t] must be equal to the cumulative
interfering workload, to indicate that the potential interference seen so far
has been fully "consumed" (i.e., there is no more higher-priority work or other
kinds of delay pending). Second, job [j] cannot be pending at any time earlier
than [t] _and_ at time instant [t] (i.e., either it was pending earlier but is no
longer pending now, or it was previously not pending and may or may not be
released now), to ensure that the busy window captures the execution of job [j].
Definition quiet_time (j : Job) (t : instant) :=
cumul_interference j 0 t = cumul_interfering_workload j 0 t ∧
~~ job_pending_earlier_and_at j t.
cumul_interference j 0 t = cumul_interfering_workload j 0 t ∧
~~ job_pending_earlier_and_at j t.
Based on the definition of quiet time, we say that interval [t1, t2) is
a (potentially unbounded) busy-interval prefix w.r.t. job [j] iff the
interval (a) contains the arrival of job j, (b) starts with a quiet
time and (c) remains non-quiet.
Definition busy_interval_prefix (j : Job) (t1 t2 : instant) :=
t1 ≤ job_arrival j < t2 ∧
quiet_time j t1 ∧
(∀ t, t1 < t < t2 → ¬ quiet_time j t).
t1 ≤ job_arrival j < t2 ∧
quiet_time j t1 ∧
(∀ t, t1 < t < t2 → ¬ quiet_time j t).
Next, we say that an interval [t1, t2) is a busy interval iff
[t1, t2) is a busy-interval prefix and t2 is a quiet time.
Definition busy_interval (j : Job) (t1 t2 : instant) :=
busy_interval_prefix j t1 t2 ∧
quiet_time j t2.
busy_interval_prefix j t1 t2 ∧
quiet_time j t2.
Note that the busy interval, if it exists, is unique.
Lemma busy_interval_is_unique:
∀ j t1 t2 t1' t2',
busy_interval j t1 t2 →
busy_interval j t1' t2' →
t1 = t1' ∧ t2 = t2'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 632)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
============================
forall (j : Job) (t1 t2 t1' t2' : instant),
busy_interval j t1 t2 -> busy_interval j t1' t2' -> t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
Proof.
intros ? ? ? ? ? BUSY BUSY'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 639)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
have EQ: t1 = t1'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 642)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 = t1'
subgoal 2 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 642)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 = t1'
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 699)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 == t1'
----------------------------------------------------------------------------- *)
apply/negPn/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 799)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
CONTR : t1 != t1'
============================
False
----------------------------------------------------------------------------- *)
move: BUSY ⇒ [[IN [QT1 NQ]] _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 833)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY' : busy_interval j t1' t2'
CONTR : t1 != t1'
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
============================
False
----------------------------------------------------------------------------- *)
move: BUSY' ⇒ [[IN' [QT1' NQ']] _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 867)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
CONTR : t1 != t1'
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
============================
False
----------------------------------------------------------------------------- *)
move: CONTR; rewrite neq_ltn; move ⇒ /orP [LT|GT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 916)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
False
subgoal 2 (ID 917) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 916)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
False
----------------------------------------------------------------------------- *)
apply NQ with t1'; try done; clear NQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 942)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
t1 < t1' < t2
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 969)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
t1' < t2
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [_ T1] /andP [T2 _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1052)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
QT1 : quiet_time j t1
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
T1 : job_arrival j < t2
T2 : t1' <= job_arrival j
============================
t1' < t2
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 917)
subgoal 1 (ID 917) is:
False
subgoal 2 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 917)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
GT : t1' < t1
============================
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 917)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
GT : t1' < t1
============================
False
----------------------------------------------------------------------------- *)
apply NQ' with t1; try done; clear NQ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1081)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
GT : t1' < t1
============================
t1' < t1 < t2'
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1108)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
GT : t1' < t1
============================
t1 < t2'
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [T1 _] /andP [_ T2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1191)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT1' : quiet_time j t1'
GT : t1' < t1
T1 : t1 <= job_arrival j
T2 : job_arrival j < t2'
============================
t1 < t2'
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
subgoal 1 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
subgoal 1 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
EQ : t1 = t1'
============================
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
subst t1'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1201)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
have EQ: t2 = t2'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1204)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t2 = t2'
subgoal 2 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1204)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t2 = t2'
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1261)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t2 == t2'
----------------------------------------------------------------------------- *)
apply/negPn/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1361)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
CONTR : t2 != t2'
============================
False
----------------------------------------------------------------------------- *)
move: BUSY ⇒ [[IN [_ NQ]] QT2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1395)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY' : busy_interval j t1 t2'
CONTR : t2 != t2'
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
============================
False
----------------------------------------------------------------------------- *)
move: BUSY' ⇒ [[IN' [_ NQ']] QT2'].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1429)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
CONTR : t2 != t2'
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
============================
False
----------------------------------------------------------------------------- *)
move: CONTR; rewrite neq_ltn; move ⇒ /orP [LT|GT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1478)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
False
subgoal 2 (ID 1479) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1478)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
False
----------------------------------------------------------------------------- *)
apply NQ' with t2; try done; clear NQ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1504)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
t1 < t2 < t2'
----------------------------------------------------------------------------- *)
apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1530)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
t1 < t2
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [_ T1] /andP [T2 _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1614)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
QT2' : quiet_time j t2'
LT : t2 < t2'
T1 : job_arrival j < t2
T2 : t1 <= job_arrival j
============================
t1 < t2
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1479)
subgoal 1 (ID 1479) is:
False
subgoal 2 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1479)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1479)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
False
----------------------------------------------------------------------------- *)
apply NQ with t2'; try done; clear NQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1643)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
t1 < t2' < t2
----------------------------------------------------------------------------- *)
apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1669)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
t1 < t2'
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [T1 _] /andP [_ T2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1753)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
QT2 : quiet_time j t2
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
T1 : t1 <= job_arrival j
T2 : job_arrival j < t2'
============================
t1 < t2'
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1206)
subgoal 1 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1206)
subgoal 1 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1206)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
EQ : t2 = t2'
============================
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
by subst t2'.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BusyInterval.
∀ j t1 t2 t1' t2',
busy_interval j t1 t2 →
busy_interval j t1' t2' →
t1 = t1' ∧ t2 = t2'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 632)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
============================
forall (j : Job) (t1 t2 t1' t2' : instant),
busy_interval j t1 t2 -> busy_interval j t1' t2' -> t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
Proof.
intros ? ? ? ? ? BUSY BUSY'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 639)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
have EQ: t1 = t1'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 642)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 = t1'
subgoal 2 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 642)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 = t1'
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 699)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
============================
t1 == t1'
----------------------------------------------------------------------------- *)
apply/negPn/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 799)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
CONTR : t1 != t1'
============================
False
----------------------------------------------------------------------------- *)
move: BUSY ⇒ [[IN [QT1 NQ]] _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 833)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY' : busy_interval j t1' t2'
CONTR : t1 != t1'
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
============================
False
----------------------------------------------------------------------------- *)
move: BUSY' ⇒ [[IN' [QT1' NQ']] _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 867)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
CONTR : t1 != t1'
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
============================
False
----------------------------------------------------------------------------- *)
move: CONTR; rewrite neq_ltn; move ⇒ /orP [LT|GT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 916)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
False
subgoal 2 (ID 917) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 916)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
False
----------------------------------------------------------------------------- *)
apply NQ with t1'; try done; clear NQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 942)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
t1 < t1' < t2
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 969)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
============================
t1' < t2
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [_ T1] /andP [T2 _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1052)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
QT1 : quiet_time j t1
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
LT : t1 < t1'
T1 : job_arrival j < t2
T2 : t1' <= job_arrival j
============================
t1' < t2
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 917)
subgoal 1 (ID 917) is:
False
subgoal 2 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 917)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
GT : t1' < t1
============================
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 917)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
NQ' : forall t : nat, t1' < t < t2' -> ~ quiet_time j t
GT : t1' < t1
============================
False
----------------------------------------------------------------------------- *)
apply NQ' with t1; try done; clear NQ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1081)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
GT : t1' < t1
============================
t1' < t1 < t2'
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1108)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
IN : t1 <= job_arrival j < t2
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
IN' : t1' <= job_arrival j < t2'
QT1' : quiet_time j t1'
GT : t1' < t1
============================
t1 < t2'
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [T1 _] /andP [_ T2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1191)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
QT1 : quiet_time j t1
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT1' : quiet_time j t1'
GT : t1' < t1
T1 : t1 <= job_arrival j
T2 : job_arrival j < t2'
============================
t1 < t2'
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
subgoal 1 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
subgoal 1 (ID 644) is:
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t1', t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1' t2'
EQ : t1 = t1'
============================
t1 = t1' /\ t2 = t2'
----------------------------------------------------------------------------- *)
subst t1'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1201)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
have EQ: t2 = t2'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1204)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t2 = t2'
subgoal 2 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1204)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t2 = t2'
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1261)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
============================
t2 == t2'
----------------------------------------------------------------------------- *)
apply/negPn/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1361)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
CONTR : t2 != t2'
============================
False
----------------------------------------------------------------------------- *)
move: BUSY ⇒ [[IN [_ NQ]] QT2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1395)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY' : busy_interval j t1 t2'
CONTR : t2 != t2'
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
============================
False
----------------------------------------------------------------------------- *)
move: BUSY' ⇒ [[IN' [_ NQ']] QT2'].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1429)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
CONTR : t2 != t2'
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
============================
False
----------------------------------------------------------------------------- *)
move: CONTR; rewrite neq_ltn; move ⇒ /orP [LT|GT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1478)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
False
subgoal 2 (ID 1479) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1478)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
False
----------------------------------------------------------------------------- *)
apply NQ' with t2; try done; clear NQ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1504)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
t1 < t2 < t2'
----------------------------------------------------------------------------- *)
apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1530)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
QT2' : quiet_time j t2'
LT : t2 < t2'
============================
t1 < t2
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [_ T1] /andP [T2 _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1614)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
QT2' : quiet_time j t2'
LT : t2 < t2'
T1 : job_arrival j < t2
T2 : t1 <= job_arrival j
============================
t1 < t2
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1479)
subgoal 1 (ID 1479) is:
False
subgoal 2 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1479)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1479)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
NQ : forall t : nat, t1 < t < t2 -> ~ quiet_time j t
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
False
----------------------------------------------------------------------------- *)
apply NQ with t2'; try done; clear NQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1643)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
t1 < t2' < t2
----------------------------------------------------------------------------- *)
apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1669)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
IN : t1 <= job_arrival j < t2
QT2 : quiet_time j t2
IN' : t1 <= job_arrival j < t2'
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
============================
t1 < t2'
----------------------------------------------------------------------------- *)
move: IN IN' ⇒ /andP [T1 _] /andP [_ T2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1753)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
QT2 : quiet_time j t2
NQ' : forall t : nat, t1 < t < t2' -> ~ quiet_time j t
QT2' : quiet_time j t2'
GT : t2' < t2
T1 : t1 <= job_arrival j
T2 : job_arrival j < t2'
============================
t1 < t2'
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1206)
subgoal 1 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1206)
subgoal 1 (ID 1206) is:
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1206)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
tsk : Task
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_pending_earlier_and_at := pending_earlier_and_at sched
: Job -> instant -> bool
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
j : Job
t1, t2, t2' : instant
BUSY : busy_interval j t1 t2
BUSY' : busy_interval j t1 t2'
EQ : t2 = t2'
============================
t1 = t1 /\ t2 = t2'
----------------------------------------------------------------------------- *)
by subst t2'.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BusyInterval.
In this section, we introduce some assumptions about the
busy interval that are fundamental for the analysis.
We say that a schedule is "work_conserving" iff for any job [j] from task [tsk] and
at any time [t] within a busy interval, there are only two options:
either (a) interference(j, t) holds or (b) job [j] is scheduled at time [t].
Definition work_conserving :=
∀ j t1 t2 t,
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
busy_interval j t1 t2 →
t1 ≤ t < t2 →
¬ interference j t ↔ job_scheduled_at j t.
∀ j t1 t2 t,
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
busy_interval j t1 t2 →
t1 ≤ t < t2 →
¬ interference j t ↔ job_scheduled_at j t.
Next, we say that busy intervals of task [tsk] are bounded by [L] iff, for any job [j] of task
[tsk], there exists a busy interval with length at most L. Note that the existence of such a
bounded busy interval is not guaranteed if the schedule is overloaded with work.
Therefore, in the later concrete analyses, we will have to introduce an additional
condition that prevents overload.
Definition busy_intervals_are_bounded_by L :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + L ∧
busy_interval j t1 t2.
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + L ∧
busy_interval j t1 t2.
Although we have defined the notion of cumulative interference of a job, it cannot be used in
a response-time analysis because of the variability of job parameters. To address this
issue, we define the notion of an interference bound. Note that according to the definition of
a work conserving schedule, interference does _not_ include execution of a job itself. Therefore,
an interference bound is not obliged to take into account the execution of this job. We say that
the job interference is bounded by an interference_bound_function ([IBF]) iff for any job [j] of
task [tsk] the cumulative interference incurred by [j] in the sub-interval [t1, t1 + delta) of busy
interval [t1, t2) does not exceed [interference_bound_function(tsk, A, delta)], where [A] is a
relative arrival time of job [j] (with respect to time [t1]).
Definition job_interference_is_bounded_by (interference_bound_function: Task → duration → duration → duration) :=
Let's examine this definition in more detail.
∀ t1 t2 delta j,
First, we require [j] to be a job of task [tsk].
Next, we require the IBF to bound the interference only within the interval [t1, t1 + delta).
Next, we require the IBF to bound the interference only until the job is
completed, after which the function can behave arbitrarily.
And finally, the IBF function might depend not only on the length
of the interval, but also on the relative arrival time of job [j] (offset). While the first three conditions are needed for discarding excessive cases, offset adds
flexibility to the IBF, which is important, for instance, when analyzing EDF scheduling.
let offset := job_arrival j - t1 in
cumul_interference j t1 (t1 + delta) ≤ interference_bound_function tsk offset delta.
End BusyIntervalProperties.
End Definitions.
End AbstractRTADefinitions.
cumul_interference j t1 (t1 + delta) ≤ interference_bound_function tsk offset delta.
End BusyIntervalProperties.
End Definitions.
End AbstractRTADefinitions.