Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
P
PROSA  Formally Proven Schedulability Analysis
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
2
Issues
2
List
Boards
Labels
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Vedant Chavda
PROSA  Formally Proven Schedulability Analysis
Commits
fa2f1873
Commit
fa2f1873
authored
Apr 01, 2020
by
Marco Maida
🌱
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fixed broken intervals
parent
f645d086
Changes
20
Hide whitespace changes
Inline
Sidebyside
Showing
20 changed files
with
60 additions
and
60 deletions
+60
60
analysis/abstract/abstract_rta.v
analysis/abstract/abstract_rta.v
+2
2
analysis/abstract/abstract_seq_rta.v
analysis/abstract/abstract_seq_rta.v
+8
8
analysis/abstract/definitions.v
analysis/abstract/definitions.v
+3
3
analysis/abstract/ideal_jlfp_rta.v
analysis/abstract/ideal_jlfp_rta.v
+2
2
analysis/abstract/run_to_completion.v
analysis/abstract/run_to_completion.v
+3
3
analysis/abstract/search_space.v
analysis/abstract/search_space.v
+1
1
analysis/definitions/busy_interval.v
analysis/definitions/busy_interval.v
+2
2
analysis/definitions/priority_inversion.v
analysis/definitions/priority_inversion.v
+1
1
analysis/definitions/task_schedule.v
analysis/definitions/task_schedule.v
+2
2
analysis/facts/behavior/service.v
analysis/facts/behavior/service.v
+3
3
analysis/facts/busy_interval/busy_interval.v
analysis/facts/busy_interval/busy_interval.v
+9
9
analysis/facts/busy_interval/carry_in.v
analysis/facts/busy_interval/carry_in.v
+5
5
analysis/facts/busy_interval/priority_inversion.v
analysis/facts/busy_interval/priority_inversion.v
+5
5
analysis/facts/model/ideal_schedule.v
analysis/facts/model/ideal_schedule.v
+2
2
analysis/facts/model/service_of_jobs.v
analysis/facts/model/service_of_jobs.v
+5
5
behavior/arrival_sequence.v
behavior/arrival_sequence.v
+1
1
model/aggregate/service_of_jobs.v
model/aggregate/service_of_jobs.v
+3
3
model/task/arrival/curves.v
model/task/arrival/curves.v
+1
1
model/task/arrivals.v
model/task/arrivals.v
+1
1
results/edf/rta/bounded_pi.v
results/edf/rta/bounded_pi.v
+1
1
No files found.
analysis/abstract/abstract_rta.v
View file @
fa2f1873
...
...
@@ 120,7 +120,7 @@ Section Abstract_RTA.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
Hypothesis
H_job_cost_positive
:
job_cost_positive
j
.
(** Assume we have a busy interval
[t1, t2)
of job j that is bounded by L. *)
(** Assume we have a busy interval
<<[t1, t2)>>
of job j that is bounded by L. *)
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
j
t1
t2
.
...
...
@@ 303,7 +303,7 @@ Section Abstract_RTA.
(** Recall that we consider a busy interval of a job [j], and [j] has arrived [A] time units
after the beginning the busy interval. From basic properties of a busy interval it
follows that job [j] incurs interference at any time instant t ∈
[t1, t1 + A)
.
follows that job [j] incurs interference at any time instant t ∈
<<[t1, t1 + A)>>
.
Therefore [interference_bound_function(tsk, A, A + F)] is at least [A]. *)
Lemma
relative_arrival_le_interference_bound
:
A
<=
interference_bound_function
tsk
A
(
A
+
F
).
...
...
analysis/abstract/abstract_seq_rta.v
View file @
fa2f1873
...
...
@@ 221,7 +221,7 @@ Section Sequential_Abstract_RTA.
Hypothesis
H_j2_from_tsk
:
job_task
j2
=
tsk
.
Hypothesis
H_j1_cost_positive
:
job_cost_positive
j1
.
(** Consider the busy interval
[t1, t2)
of job j1. *)
(** Consider the busy interval
<<[t1, t2)>>
of job j1. *)
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
j1
t1
t2
.
...
...
@@ 242,7 +242,7 @@ Section Sequential_Abstract_RTA.
Qed
.
(** Next we prove that if a job is pending after the beginning
of the busy interval
[t1, t2)
then it arrives after t1. *)
of the busy interval
<<[t1, t2)>>
then it arrives after t1. *)
Lemma
arrives_after_beginning_of_busy_interval
:
forall
t
,
t1
<=
t
>
...
...
@@ 277,7 +277,7 @@ Section Sequential_Abstract_RTA.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
Hypothesis
H_job_cost_positive
:
job_cost_positive
j
.
(** Consider the busy interval
[t1, t2)
of job j. *)
(** Consider the busy interval
<<[t1, t2)>>
of job j. *)
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
j
t1
t2
.
...
...
@@ 291,7 +291,7 @@ Section Sequential_Abstract_RTA.
(** ... and job j is not completed by time (t1 + x). *)
Hypothesis
H_job_j_is_not_completed
:
~~
completed_by
sched
j
(
t1
+
x
).
(** In this section, we show that the cumulative interference of job j in the interval
[t1, t1 + x)
(** In this section, we show that the cumulative interference of job j in the interval
<<[t1, t1 + x)>>
is bounded by the sum of the task workload in the interval [t1, t1 + A + ε) and the cumulative
interference of [j]'s task in the interval [t1, t1 + x). Note that the task workload is computed
only on the interval [t1, t1 + A + ε). Thanks to the hypothesis about sequential tasks, jobs of
...
...
@@ 299,14 +299,14 @@ Section Sequential_Abstract_RTA.
Section
TaskInterferenceBoundsInterference
.
(** We start by proving a simpler analog of the lemma which states that at
any time instant t ∈
[t1, t1 + x)
the sum of [interference j t] and
any time instant t ∈
<<[t1, t1 + x)>>
the sum of [interference j t] and
[scheduled_at j t] is no larger than the sum of [the service received
by jobs of task tsk at time t] and [task_iterference tsk t]. *)
(** Next we consider 4 cases. *)
Section
CaseAnalysis
.
(** Consider an arbitrary time instant t ∈
[t1, t1 + x)
. *)
(** Consider an arbitrary time instant t ∈
<<[t1, t1 + x)>>
. *)
Variable
t
:
instant
.
Hypothesis
H_t_in_interval
:
t1
<=
t
<
t1
+
x
.
...
...
@@ 476,7 +476,7 @@ Section Sequential_Abstract_RTA.
End
Case4
.
(** We use the above case analysis to prove that any time instant
t ∈
[t1, t1 + x)
the sum of [interference j t] and [scheduled_at j t]
t ∈
<<[t1, t1 + x)>>
the sum of [interference j t] and [scheduled_at j t]
is no larger than the sum of [the service received by jobs of task
tsk at time t] and [task_iterference tsk t]. *)
Lemma
interference_plus_sched_le_serv_of_task_plus_task_interference
:
...
...
@@ 547,7 +547,7 @@ Section Sequential_Abstract_RTA.
by
apply
service_of_jobs_le_workload
;
auto
using
ideal_proc_model_provides_unit_service
.
Qed
.
(** Finally, we show that the cumulative interference of job j in the interval
[t1, t1 + x)
(** Finally, we show that the cumulative interference of job j in the interval
<<[t1, t1 + x)>>
is bounded by the sum of the task workload in the interval [t1, t1 + A + ε) and
the cumulative interference of [j]'s task in the interval [t1, t1 + x). *)
Lemma
cumulative_job_interference_le_task_interference_bound
:
...
...
analysis/abstract/definitions.v
View file @
fa2f1873
...
...
@@ 98,7 +98,7 @@ Section AbstractRTADefinitions.
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
(** Based on the definition of quiet time, we say that interval
<<[t1, t2)>>
is
a (potentially unbounded) busyinterval 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 nonquiet. *)
...
...
@@ 107,7 +107,7 @@ Section AbstractRTADefinitions.
quiet_time
j
t1
/\
(
forall
t
,
t1
<
t
<
t2
>
~
quiet_time
j
t
).
(** Next, we say that an interval
[t1, t2)
is a busy interval iff
(** Next, we say that an interval
<<[t1, t2)>>
is a busy interval iff
[t1, t2) is a busyinterval prefix and t2 is a quiet time. *)
Definition
busy_interval
(
j
:
Job
)
(
t1
t2
:
instant
)
:
=
busy_interval_prefix
j
t1
t2
/\
...
...
@@ 205,7 +205,7 @@ Section AbstractRTADefinitions.
(** First, we require [j] to be a job of task [tsk]. *)
arrives_in
arr_seq
j
>
job_task
j
=
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 within the interval
<<[t1, t1 + delta)>>
. *)
busy_interval
j
t1
t2
>
t1
+
delta
<
t2
>
(** Next, we require the IBF to bound the interference only until the job is
...
...
analysis/abstract/ideal_jlfp_rta.v
View file @
fa2f1873
...
...
@@ 271,7 +271,7 @@ Section JLFPInstantiation.
conventional workload, i.e., the one defined with concrete schedule parameters. *)
Section
InstantiatedWorkloadEquivalence
.
(** Let
[t1,t2)
be any time interval. *)
(** Let
<<[t1,t2)>>
be any time interval. *)
Variables
t1
t2
:
instant
.
(** Consider any job j of [tsk]. *)
...
...
@@ 330,7 +330,7 @@ Section JLFPInstantiation.
Hypothesis
H_j_arrives
:
arrives_in
arr_seq
j
.
Hypothesis
H_job_of_tsk
:
job_of_task
tsk
j
.
(** We consider an arbitrary time interval
[t1, t)
that starts with a quiet time. *)
(** We consider an arbitrary time interval
<<[t1, t)>>
that starts with a quiet time. *)
Variable
t1
t
:
instant
.
Hypothesis
H_quiet_time
:
quiet_time_cl
j
t1
.
...
...
analysis/abstract/run_to_completion.v
View file @
fa2f1873
...
...
@@ 65,7 +65,7 @@ Section AbstractRTARunToCompletionThreshold.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
Hypothesis
H_job_cost_positive
:
job_cost_positive
j
.
(** Next, consider any busy interval
[t1, t2)
of job [j]. *)
(** Next, consider any busy interval
<<[t1, t2)>>
of job [j]. *)
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
j
t1
t2
.
...
...
@@ 87,13 +87,13 @@ Section AbstractRTARunToCompletionThreshold.
the total time where job [j] is scheduled inside the busy interval. *)
Section
InterferenceIsComplement
.
(** Consider any subinterval
[t, t + delta)
inside the busy interval [t1, t2). *)
(** Consider any subinterval
<<[t, t + delta)>>
inside the busy interval [t1, t2). *)
Variables
(
t
:
instant
)
(
delta
:
duration
).
Hypothesis
H_greater_than_or_equal
:
t1
<=
t
.
Hypothesis
H_less_or_equal
:
t
+
delta
<=
t2
.
(** We prove that sum of cumulative service and cumulative interference
in the interval
[t, t + delta)
is equal to delta. *)
in the interval
<<[t, t + delta)>>
is equal to delta. *)
Lemma
interference_is_complement_to_schedule
:
service_during
sched
j
t
(
t
+
delta
)
+
cumul_interference
j
t
(
t
+
delta
)
=
delta
.
Proof
.
...
...
analysis/abstract/search_space.v
View file @
fa2f1873
...
...
@@ 58,7 +58,7 @@ Section AbstractRTAReduction.
(** Recall the definition of [ε], which defines the neighborhood of a point in the timeline.
Note that [ε = 1] under discrete time. *)
(** To ensure that the search converges more quickly, we only check values of [A] in the interval
[[0, B)]
for which the interference bound function changes, i.e., every point [x] in which
<<[0, B)>>
for which the interference bound function changes, i.e., every point [x] in which
[interference_bound_function (A  ε, x)] is not equal to [interference_bound_function (A, x)]. *)
Definition
is_in_search_space
A
:
=
A
=
0
\/
...
...
analysis/definitions/busy_interval.v
View file @
fa2f1873
...
...
@@ 40,7 +40,7 @@ Section BusyIntervalJLFP.
completed_by
sched
j_hp
t
.
(** Based on the definition of quiet time, we say that interval
[t1, t_busy)
is a (potentially unbounded) busyinterval prefix
<<[t1, t_busy)>>
is a (potentially unbounded) busyinterval prefix
iff the interval starts with a quiet time where a higher or equal
priority job is released and remains nonquiet. We also require
job j to be released in the interval. *)
...
...
@@ 50,7 +50,7 @@ Section BusyIntervalJLFP.
(
forall
t
,
t1
<
t
<
t_busy
>
~
quiet_time
t
)
/\
t1
<=
job_arrival
j
<
t_busy
.
(** Next, we say that an interval
[t1, t2)
is a busy interval iff
(** Next, we say that an interval
<<[t1, t2)>>
is a busy interval iff
[t1, t2) is a busyinterval prefix and t2 is a quiet time. *)
Definition
busy_interval
(
t1
t2
:
instant
)
:
=
busy_interval_prefix
t1
t2
/\
...
...
analysis/definitions/priority_inversion.v
View file @
fa2f1873
...
...
@@ 46,7 +46,7 @@ Section CumulativePriorityInversion.
else
false
.
(** Then we compute the cumulative priority inversion incurred by
a job within some time interval
[t1, t2)
. *)
a job within some time interval
<<[t1, t2)>>
. *)
Definition
cumulative_priority_inversion
(
t1
t2
:
instant
)
:
=
\
sum_
(
t1
<=
t
<
t2
)
is_priority_inversion
t
.
...
...
analysis/definitions/task_schedule.v
View file @
fa2f1873
...
...
@@ 36,12 +36,12 @@ Section ScheduleOfTask.
Definition
task_service_at
(
t
:
instant
)
:
=
task_scheduled_at
t
.
(** Based on the notion of instantaneous service, we define the
cumulative service received by [tsk] during any interval
[t1, t2)
... *)
cumulative service received by [tsk] during any interval
<<[t1, t2)>>
... *)
Definition
task_service_during
(
t1
t2
:
instant
)
:
=
\
sum_
(
t1
<=
t
<
t2
)
task_service_at
t
.
(** ...and the cumulative service received by [tsk] up to time t2,
i.e., in the interval
[0, t2)
. *)
i.e., in the interval
<<[0, t2)>>
. *)
Definition
task_service
(
t2
:
instant
)
:
=
task_service_during
0
t2
.
End
ScheduleOfTask
.
analysis/facts/behavior/service.v
View file @
fa2f1873
...
...
@@ 53,7 +53,7 @@ Section Composition.
Qed
.
(** Next, we observe that we can look at the service received during an
interval
[t1, t3)
as the sum of the service during [t1, t2) and [t2, t3)
interval
<<[t1, t3)>>
as the sum of the service during [t1, t2) and [t2, t3)
for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of
the two intervals.) *)
Lemma
service_during_cat
:
...
...
@@ 114,7 +114,7 @@ Section Composition.
rewrite
/
service
.
rewrite

service_during_last_plus_before
//.
Qed
.
(** Finally, we deconstruct the service received during an interval
[t1, t3)
(** Finally, we deconstruct the service received during an interval
<<[t1, t3)>>
into the service at a midpoint t2 and the service in the intervals before
and after. *)
Lemma
service_split_at_point
:
...
...
@@ 518,7 +518,7 @@ Section RelationToScheduled.
Hypothesis
H_same_service
:
service
sched
j
t1
=
service
sched
j
t2
.
(** First, we observe that this means that the job receives no service
during
[t1, t2)
... *)
during
<<[t1, t2)>>
... *)
Lemma
constant_service_implies_no_service_during
:
service_during
sched
j
t1
t2
=
0
.
Proof
.
...
...
analysis/facts/busy_interval/busy_interval.v
View file @
fa2f1873
...
...
@@ 68,7 +68,7 @@ Section ExistsBusyIntervalJLFP.
(** Assume that the priority relation is reflexive. *)
Hypothesis
H_priority_is_reflexive
:
reflexive_priorities
.
(** Consider any busy interval
[t1, t2)
of job [j]. *)
(** Consider any busy interval
<<[t1, t2)>>
of job [j]. *)
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
t1
t2
.
...
...
@@ 137,7 +137,7 @@ Section ExistsBusyIntervalJLFP.
Hypothesis
H_priority_is_reflexive
:
reflexive_priorities
.
Hypothesis
H_priority_is_transitive
:
transitive_priorities
.
(** Consider any busy interval prefix
[t1, t2)
. *)
(** Consider any busy interval prefix
<<[t1, t2)>>
. *)
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval_prefix
:
busy_interval_prefix
t1
t2
.
...
...
@@ 216,7 +216,7 @@ Section ExistsBusyIntervalJLFP.
by
exists
jhp
;
apply
SE1
;
rewrite
in_cons
;
apply
/
orP
;
left
.
Qed
.
(** We prove that at any time instant [t] within
[t1, t2)
the processor is not idle. *)
(** We prove that at any time instant [t] within
<<[t1, t2)>>
the processor is not idle. *)
Lemma
not_quiet_implies_not_idle
:
forall
t
,
t1
<=
t
<
t2
>
...
...
@@ 254,7 +254,7 @@ Section ExistsBusyIntervalJLFP.
Hypothesis
H_no_quiet_time
:
forall
t
,
t1
<
t
<=
t1
+
Δ
>
~
quiet_time
t
.
(** For clarity, we introduce a notion of the total service of jobs released in
time interval
[t_beg, t_end)
during the time interval [t1, t1 + Δ). *)
time interval
<<[t_beg, t_end)>>
during the time interval [t1, t1 + Δ). *)
Let
service_received_by_hep_jobs_released_during
t_beg
t_end
:
=
service_of_higher_or_equal_priority_jobs
sched
(
arrivals_between
t_beg
t_end
)
j
t1
(
t1
+
Δ
).
...
...
@@ 289,7 +289,7 @@ Section ExistsBusyIntervalJLFP.
Qed
.
(** Next we prove that the total service within a "nonquiet"
time interval
[t1, t1 + Δ)
is exactly Δ. *)
time interval
<<[t1, t1 + Δ)>>
is exactly Δ. *)
Lemma
no_idle_time_within_non_quiet_time_interval
:
service_of_jobs
sched
predT
(
arrivals_between
0
(
t1
+
Δ
))
t1
(
t1
+
Δ
)
=
Δ
.
Proof
.
...
...
@@ 353,12 +353,12 @@ Section ExistsBusyIntervalJLFP.
Hypothesis
H_priority_is_transitive
:
transitive_priorities
.
(** Next, we recall the notion of workload of all jobs released in a given interval
[t1, t2)
that have higherorequal priority w.r.t the job j being analyzed. *)
<<[t1, t2)>>
that have higherorequal priority w.r.t the job j being analyzed. *)
Let
hp_workload
t1
t2
:
=
workload_of_higher_or_equal_priority_jobs
j
(
arrivals_between
t1
t2
).
(** With regard to the jobs with higherorequal priority that are released
in a given interval
[t1, t2)
, we also recall the service received by these
in a given interval
<<[t1, t2)>>
, we also recall the service received by these
jobs in the same interval [t1, t2). *)
Let
hp_service
t1
t2
:
=
service_of_higher_or_equal_priority_jobs
...
...
@@ 457,7 +457,7 @@ Section ExistsBusyIntervalJLFP.
(** Since the interval is always nonquiet, the processor is always busy
with tasks of higherorequal priority or some lower priority job which was scheduled,
i.e., the sum of service done by jobs with actual arrival time in
[t1, t1 + delta)
i.e., the sum of service done by jobs with actual arrival time in
<<[t1, t1 + delta)>>
and priority inversion equals delta. *)
Lemma
busy_interval_has_uninterrupted_service
:
delta
<=
priority_inversion_bound
+
hp_service
t1
(
t1
+
delta
).
...
...
@@ 628,7 +628,7 @@ Section ExistsBusyIntervalJLFP.
infer that there is a time in which j is pending. *)
Hypothesis
H_positive_cost
:
job_cost
j
>
0
.
(** Therefore there must exists a busy interval
[t1, t2)
that
(** Therefore there must exists a busy interval
<<[t1, t2)>>
that
contains the arrival time of j. *)
Corollary
exists_busy_interval
:
exists
t1
t2
,
...
...
analysis/facts/busy_interval/carry_in.v
View file @
fa2f1873
...
...
@@ 112,11 +112,11 @@ Section ExistsNoCarryIn.
(** Let the priority relation be reflexive. *)
Hypothesis
H_priority_is_reflexive
:
reflexive_priorities
.
(** Recall the notion of workload of all jobs released in a given interval
[t1, t2)
... *)
(** Recall the notion of workload of all jobs released in a given interval
<<[t1, t2)>>
... *)
Let
total_workload
t1
t2
:
=
workload_of_jobs
predT
(
arrivals_between
t1
t2
).
(** ... and total service of jobs within some time interval
[t1, t2)
. *)
(** ... and total service of jobs within some time interval
<<[t1, t2)>>
. *)
Let
total_service
t1
t2
:
=
service_of_jobs
sched
predT
(
arrivals_between
0
t2
)
t1
t2
.
...
...
@@ 155,7 +155,7 @@ Section ExistsNoCarryIn.
Hypothesis
H_no_carry_in
:
no_carry_in
t
.
(** First, recall that the total service is bounded by the total workload. Therefore
the total service of jobs in the interval
[t, t + Δ)
is bounded by Δ. *)
the total service of jobs in the interval
<<[t, t + Δ)>>
is bounded by Δ. *)
Lemma
total_service_is_bounded_by_
Δ
:
total_service
t
(
t
+
Δ
)
<=
Δ
.
Proof
.
...
...
@@ 198,7 +198,7 @@ Section ExistsNoCarryIn.
by
apply
idle_instant_implies_no_carry_in_at_t
.
Qed
.
(** In the second case, the total service within the time interval
[t, t + Δ)
is equal to Δ.
(** In the second case, the total service within the time interval
<<[t, t + Δ)>>
is equal to Δ.
On the other hand, we know that the total workload is lowerbounded by the total service
and upperbounded by Δ. Therefore, the total workload is equal to total service this
implies completion of all jobs by time [t + Δ] and hence no carryin at time [t + Δ]. *)
...
...
@@ 267,7 +267,7 @@ Section ExistsNoCarryIn.
Hypothesis
H_from_arrival_sequence
:
arrives_in
arr_seq
j
.
Hypothesis
H_job_cost_positive
:
job_cost_positive
j
.
(** We show that there must exist a busy interval
[t1, t2)
that
(** We show that there must exist a busy interval
<<[t1, t2)>>
that
contains the arrival time of j. *)
Corollary
exists_busy_interval_from_total_workload_bound
:
exists
t1
t2
,
...
...
analysis/facts/busy_interval/priority_inversion.v
View file @
fa2f1873
...
...
@@ 167,7 +167,7 @@ Section PriorityInversionIsBounded.
Hypothesis
H_j_arrives
:
arrives_in
arr_seq
j
.
Hypothesis
H_job_cost_positive
:
job_cost_positive
j
.
(** Consider any busy interval prefix
[t1, t2)
of job j. *)
(** Consider any busy interval prefix
<<[t1, t2)>>
of job j. *)
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval_prefix
:
busy_interval_prefix
arr_seq
sched
j
t1
t2
.
...
...
@@ 182,7 +182,7 @@ Section PriorityInversionIsBounded.
busy scheduling a job with higher or equal priority. *)
Section
ProcessorBusyWithHEPJobAtPreemptionPoints
.
(** Consider an arbitrary preemption time t ∈
[t1,t2)
. *)
(** Consider an arbitrary preemption time t ∈
<<[t1,t2)>>
. *)
Variable
t
:
instant
.
Hypothesis
H_t_in_busy_interval
:
t1
<=
t
<
t2
.
Hypothesis
H_t_preemption_time
:
preemption_time
sched
t
.
...
...
@@ 497,7 +497,7 @@ Section PriorityInversionIsBounded.
Qed
.
(** Also, we show that lowerpriority jobs that are scheduled inside the
busyinterval prefix
[t1,t2)
must arrive before that interval. *)
busyinterval prefix
<<[t1,t2)>>
must arrive before that interval. *)
Lemma
low_priority_job_arrives_before_busy_interval_prefix
:
forall
jlp
t
,
t1
<=
t
<
t2
>
...
...
@@ 523,7 +523,7 @@ Section PriorityInversionIsBounded.
Qed
.
(** Moreover, we show that lowerpriority jobs that are scheduled
inside the busyinterval prefix
[t1,t2)
must be scheduled
inside the busyinterval prefix
<<[t1,t2)>>
must be scheduled
before that interval. *)
Lemma
low_priority_job_scheduled_before_busy_interval_prefix
:
forall
jlp
t
,
...
...
@@ 662,7 +662,7 @@ Section PriorityInversionIsBounded.
Qed
.
(** Thanks to the fact that the scheduler respects the notion of preemption points
we show that [jlp] is continuously scheduled in time interval
[[t1, t1 + fpt)]
. *)
we show that [jlp] is continuously scheduled in time interval
<<[t1, t1 + fpt)>>
. *)
Lemma
continuously_scheduled_between_preemption_points
:
forall
t'
,
t1
<=
t'
<
t1
+
fpt
>
...
...
analysis/facts/model/ideal_schedule.v
View file @
fa2f1873
...
...
@@ 103,7 +103,7 @@ Section IncrementalService.
Variable
sched
:
schedule
(
ideal
.
processor_state
Job
).
(** As a base case, we prove that if a job j receives service in
some time interval
[t1,t2)
, then there exists a time instant t
some time interval
<<[t1,t2)>>
, then there exists a time instant t
∈ [t1,t2) such that j is scheduled at time t and t is the first
instant where j receives service. *)
Lemma
positive_service_during
:
...
...
@@ 141,7 +141,7 @@ Section IncrementalService.
}
Qed
.
(** Next, we prove that if in some time interval
[t1,t2)
a job j
(** Next, we prove that if in some time interval
<<[t1,t2)>>
a job j
receives k units of service, then there exists a time instant t ∈
[t1,t2) such that j is scheduled at time t and service of job j
within interval [t1,t) is equal to k. *)
...
...
analysis/facts/model/service_of_jobs.v
View file @
fa2f1873
...
...
@@ 70,7 +70,7 @@ Section GenericModelLemmas.
the total service of a set of jobs. *)
Section
ServiceCat
.
(** We show that the total service of jobs released in a time interval
[t1,t2)
(** We show that the total service of jobs released in a time interval
<<[t1,t2)>>
during [t1,t2) is equal to the sum of:
(1) the total service of jobs released in time interval [t1, t) during time [t1, t)
(2) the total service of jobs released in time interval [t1, t) during time [t, t2)
...
...
@@ 100,7 +100,7 @@ Section GenericModelLemmas.
by
move
:
ARR
=>
/
andP
[
N1
N2
]
;
apply
leq_trans
with
t
.
Qed
.
(** We show that the total service of jobs released in a time interval
[t1,t2)
(** We show that the total service of jobs released in a time interval
<<[t1,t2)>>
during [t,t2) is equal to the sum of:
(1) the total service of jobs released in a time interval [t1,t) during [t,t2)
and (2) the total service of jobs released in a time interval [t,t2) during [t,t2). *)
...
...
@@ 154,7 +154,7 @@ Section IdealModelLemmas.
Let
arrivals_between
:
=
arrivals_between
arr_seq
.
Let
completed_by
:
=
completed_by
sched
.
(** We prove that if the total service within some time interval
[[t1,t2)]
(** We prove that if the total service within some time interval
<<[t1,t2)>>
is smaller than [t2t1], then there is an idle time instant t ∈ [[t1,t2)]. *)
Lemma
low_service_implies_existence_of_idle_time
:
forall
t1
t2
,
...
...
@@ 272,10 +272,10 @@ Section IdealModelLemmas.
service, cumulative workload, and completion of jobs. *)
Section
WorkloadServiceAndCompletion
.
(** Consider an arbitrary time interval
[t1, t2)
. *)
(** Consider an arbitrary time interval
<<[t1, t2)>>
. *)
Variables
t1
t2
:
instant
.
(** Let jobs be a set of all jobs arrived during
[t1, t2)
. *)
(** Let jobs be a set of all jobs arrived during
<<[t1, t2)>>
. *)
Let
jobs
:
=
arrivals_between
t1
t2
.
(** Next, we consider some time instant [t_compl]. *)
...
...
behavior/arrival_sequence.v
View file @
fa2f1873
...
...
@@ 109,7 +109,7 @@ Section ArrivalSequencePrefix.
Variable
arr_seq
:
arrival_sequence
Job
.
(** By concatenation, we construct the list of jobs that arrived in the
interval
[t1, t2)
. *)
interval
<<[t1, t2)>>
. *)
Definition
arrivals_between
(
t1
t2
:
instant
)
:
=
\
cat_
(
t1
<=
t
<
t2
)
arrivals_at
arr_seq
t
.
...
...
model/aggregate/service_of_jobs.v
View file @
fa2f1873
...
...
@@ 39,7 +39,7 @@ Section ServiceOfJobs.
\
sum_
(
j
<
jobs

P
j
)
service_at
sched
j
t
.
(** ... and the cumulative service received during the interval
[[t1, t2)]
by jobs that satisfy predicate [P]. *)
<<[t1, t2)>>
by jobs that satisfy predicate [P]. *)
Definition
service_of_jobs
(
t1
t2
:
instant
)
:
=
\
sum_
(
j
<
jobs

P
j
)
service_during
sched
j
t1
t2
.
...
...
@@ 61,7 +61,7 @@ Section ServiceOfJobs.
(** Based on the definition of jobs of higher or equal priority, ... *)
Let
of_higher_or_equal_priority
j_hp
:
=
hep_job
j_hp
j
.
(** ...we define the service received during
[[t1, t2)]
by jobs of higher or equal priority. *)
(** ...we define the service received during
<<[t1, t2)>>
by jobs of higher or equal priority. *)
Definition
service_of_higher_or_equal_priority_jobs
(
t1
t2
:
instant
)
:
=
service_of_jobs
of_higher_or_equal_priority
jobs
t1
t2
.
...
...
@@ 78,7 +78,7 @@ Section ServiceOfJobs.
Variable
jobs
:
seq
Job
.
(** We define the cumulative task service received by the jobs of
task [tsk] within time interval
[[t1, t2)]
. *)
task [tsk] within time interval
<<[t1, t2)>>
. *)
Definition
task_service_of_jobs_in
t1
t2
:
=
service_of_jobs
(
job_of_task
tsk
)
jobs
t1
t2
.
...
...
model/task/arrival/curves.v
View file @
fa2f1873
...
...
@@ 65,7 +65,7 @@ Section ArrivalCurves.
monotone
num_arrivals
leq
.
(** We say that [max_arrivals] is an upper arrival bound for task [tsk]
iff, for any interval
[[t1, t2)]
, [max_arrivals (t2  t1)] bounds the
iff, for any interval
<<[t1, t2)>>
, [max_arrivals (t2  t1)] bounds the
number of jobs of [tsk] that arrive in that interval. *)
Definition
respects_max_arrivals
(
tsk
:
Task
)
(
max_arrivals
:
duration
>
nat
)
:
=
forall
(
t1
t2
:
instant
),
...
...
model/task/arrivals.v
View file @
fa2f1873
...
...
@@ 17,7 +17,7 @@ Section TaskArrivals.
Variable
tsk
:
Task
.
(** First, we construct the list of jobs of task [tsk] that arrive
in a given halfopen interval
[[t1, t2)]
. *)
in a given halfopen interval
<<[t1, t2)>>
. *)
Definition
task_arrivals_between
(
t1
t2
:
instant
)
:
=
[
seq
j
<
arrivals_between
arr_seq
t1
t2

job_task
j
==
tsk
].
...
...
results/edf/rta/bounded_pi.v
View file @
fa2f1873
...
...
@@ 305,7 +305,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
Hypothesis
H_job_cost_positive
:
job_cost_positive
j
.
(** Consider any busy interval
[t1, t2)
of job [j]. *)
(** Consider any busy interval
<<[t1, t2)>>
of job [j]. *)
Variable
t1
t2
:
duration
.
Hypothesis
H_busy_interval
:
definitions
.
busy_interval
sched
interference
interfering_workload
j
t1
t2
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment