Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
RTPROOFS
PROSA  Formally Proven Schedulability Analysis
Commits
6a20581c
Commit
6a20581c
authored
Aug 08, 2022
by
Björn Brandenburg
Browse files
fix spelling and markup issues uncovered by `hunspell`
parent
36bcec43
Pipeline
#70369
failed with stage
in 17 minutes and 52 seconds
Changes
24
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
analysis/abstract/abstract_rta.v
View file @
6a20581c
...
...
@@ 123,7 +123,7 @@ Section Abstract_RTA.
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
j
t1
t2
.
(** Let's define
A
as a relative arrival time of job
j
(with respect to time t1). *)
(** Let's define
[A]
as a relative arrival time of job
[j]
(with respect to time
[
t1
]
). *)
Let
A
:
=
job_arrival
j

t1
.
(** In order to prove that R is a responsetime bound of job j, we use hypothesis H_R_is_maximum.
...
...
@@ 164,7 +164,7 @@ Section Abstract_RTA.
interval remains completed. *)
Section
FixpointOutsideBusyInterval
.
(** By assumption, suppose that t2 is less than or equal to [t1 + A_sp + F_sp]. *)
(** By assumption, suppose that
[
t2
]
is less than or equal to [t1 + A_sp + F_sp]. *)
Hypothesis
H_big_fixpoint_solution
:
t2
<=
t1
+
(
A_sp
+
F_sp
).
(** Then we prove that [job_arrival j + R] is no less than [t2]. *)
...
...
@@ 198,7 +198,7 @@ Section Abstract_RTA.
[t1 + A_sp + F_sp] lies inside the busy interval. *)
Section
FixpointInsideBusyInterval
.
(** So, assume that [t1 + A_sp + F_sp] is less than t2. *)
(** So, assume that [t1 + A_sp + F_sp] is less than
[
t2
]
. *)
Hypothesis
H_small_fixpoint_solution
:
t1
+
(
A_sp
+
F_sp
)
<
t2
.
(** Next, let's consider two other cases: *)
...
...
@@ 221,7 +221,7 @@ Section Abstract_RTA.
Variable
F
:
duration
.
(** (a) the sum of [A_sp] and [F_sp] is equal to the sum of [A] and [F]... *)
Hypothesis
H_Asp_Fsp_eq_A_F
:
A_sp
+
F_sp
=
A
+
F
.
(** (b) [F] is at mo
1
st [F_sp]... *)
(** (b) [F] is at most [F_sp]... *)
Hypothesis
H_F_le_Fsp
:
F
<=
F_sp
.
(** (c) and [A + F] is a solution for the responsetime recurrence for [A]. *)
Hypothesis
H_A_F_fixpoint
:
...
...
analysis/abstract/abstract_seq_rta.v
View file @
6a20581c
...
...
@@ 220,7 +220,7 @@ Section Sequential_Abstract_RTA.
Hypothesis
H_j2_from_tsk
:
job_of_task
tsk
j2
.
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
.
...
...
@@ 241,7 +241,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
>
...
...
@@ 280,14 +280,14 @@ Section Sequential_Abstract_RTA.
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
j
t1
t2
.
(** Let's define
A
as a relative arrival time of job
j
(with respect to time t1). *)
(** Let's define
[A]
as a relative arrival time of job
[j]
(with respect to time
[
t1
]
). *)
Let
A
:
duration
:
=
job_arrival
j

t1
.
(** Consider an arbitrary time x ... *)
Variable
x
:
duration
.
(** ... such that (t1 + x) is inside the busy interval... *)
(** ... such that
[
(t1 + x)
]
is inside the busy interval... *)
Hypothesis
H_inside_busy_interval
:
t1
+
x
<
t2
.
(** ... and job
j
is not completed by time (t1 + x). *)
(** ... 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)>>
...
...
@@ 549,8 +549,8 @@ Section Sequential_Abstract_RTA.
Qed
.
(** 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). *)
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
:
cumul_interference
j
t1
(
t1
+
x
)
<=
(
task_workload_between
t1
(
t1
+
A
+
ε
)

job_cost
j
)
...
...
analysis/abstract/definitions.v
View file @
6a20581c
...
...
@@ 96,7 +96,7 @@ Section AbstractRTADefinitions.
(
forall
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 busyinterval prefix and t2 is a quiet time. *)
<<
[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
/\
quiet_time
j
t2
.
...
...
analysis/abstract/run_to_completion.v
View file @
6a20581c
...
...
@@ 57,9 +57,9 @@ Section AbstractRTARunToCompletionThreshold.
Hypothesis
H_busy_interval
:
busy_interval
j
t1
t2
.
(** First, we prove that job [j] completes by the end of the busy interval.
Note that the busy interval contains the execution of job j, in addition
time instant t2 is a quiet time. Thus by the definition of a quiet time
the job should be completed before time t2. *)
Note that the busy interval contains the execution of job j, in addition
time instant
[
t2
]
is a quiet time. Thus by the definition of a quiet time
the job should be completed before time
[
t2
]
. *)
Lemma
job_completes_within_busy_interval
:
completed_by
sched
j
t2
.
Proof
.
...
...
@@ 74,7 +74,7 @@ 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
.
...
...
analysis/facts/behavior/arrivals.v
View file @
6a20581c
...
...
@@ 275,7 +275,7 @@ Section ArrivalSequencePrefix.
Qed
.
(** Next, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival
[
(jobs_arrived_before t)
]
, then it arrives in the arrival
sequence. *)
Lemma
in_arrivals_implies_arrived
:
forall
j
t1
t2
,
...
...
@@ 291,16 +291,16 @@ Section ArrivalSequencePrefix.
Proof
.
by
move
=>
t
?
?
;
exists
t
.
Qed
.
(** Next, we prove that if a job belongs to the prefix
(jobs_arrived_between t1 t2), then it indeed arrives between t1 and
t2. *)
[
(jobs_arrived_between t1 t2)
]
, then it indeed arrives between
[
t1
]
and
[
t2
]
. *)
Lemma
in_arrivals_implies_arrived_between
:
forall
j
t1
t2
,
j
\
in
arrivals_between
arr_seq
t1
t2
>
arrived_between
j
t1
t2
.
Proof
.
by
move
=>
?
?
?
/
mem_bigcat_nat_exists
[
t0
[/
job_arrival_at
<]].
Qed
.
(** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
then it indeed arrives before time
t
. *)
(** Similarly, if a job belongs to the prefix
[
(jobs_arrived_before t)
]
,
then it indeed arrives before time
[t]
. *)
Lemma
in_arrivals_implies_arrived_before
:
forall
j
t
,
j
\
in
arrivals_before
arr_seq
t
>
...
...
@@ 308,7 +308,7 @@ Section ArrivalSequencePrefix.
Proof
.
by
move
=>
?
?
/
in_arrivals_implies_arrived_between
.
Qed
.
(** Similarly, we prove that if a job from the arrival sequence arrives
before t, then it belongs to the sequence (jobs_arrived_before t). *)
before t, then it belongs to the sequence
[
(jobs_arrived_before t)
]
. *)
Lemma
arrived_between_implies_in_arrivals
:
forall
j
t1
t2
,
arrives_in
arr_seq
j
>
...
...
analysis/facts/behavior/service.v
View file @
6a20581c
...
...
@@ 94,7 +94,7 @@ Section Composition.
Proof
.
move
=>
?
;
exact
:
service_during_last_plus_before
.
Qed
.
(** 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
into the service at a midpoint
[
t2
]
and the service in the intervals before
and after. *)
Lemma
service_split_at_point
:
forall
t1
t2
t3
,
...
...
analysis/facts/model/rbf.v
View file @
6a20581c
...
...
@@ 242,7 +242,7 @@ Section RequestBoundFunctions.
(** Let [max_arrivals] be a family of valid arrival curves, i.e., for any task [tsk] in [ts]
[max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
that equals 0 for the empty interval Δ = 0. *)
that equals 0 for the empty interval
[
Δ = 0
]
. *)
Context
`
{
MaxArrivals
Task
}.
Hypothesis
H_valid_arrival_curve
:
valid_arrival_curve
(
max_arrivals
tsk
).
Hypothesis
H_is_arrival_curve
:
respects_max_arrivals
arr_seq
tsk
(
max_arrivals
tsk
).
...
...
@@ 388,10 +388,10 @@ Section TotalRBFMonotonic.
End
TotalRBFMonotonic
.
(** ** RBFs Equal to Zero for Duration
ε
*)
(** ** RBFs Equal to Zero for Duration
[ε]
*)
(** In the following section, we derive simple properties that follow in
the pathological case of an RBF that yields zero for duration
ε
. *)
the pathological case of an RBF that yields zero for duration
[ε]
. *)
Section
DegenerateTotalRBFs
.
(** Consider a set of tasks characterized by WCETs and arrival curves ... *)
...
...
analysis/facts/preemption/job/preemptive.v
View file @
6a20581c
...
...
@@ 45,7 +45,7 @@ Section FullyPreemptiveModel.
by
rewrite
H1
;
compute
.
Qed
.
(** ... or
ε
when [job_cost j > 0]. *)
(** ... or
[ε]
when [job_cost j > 0]. *)
Lemma
job_max_nps_is_
ε
:
forall
j
,
job_cost
j
>
0
>
...
...
analysis/facts/preemption/rtc_threshold/nonpreemptive.v
View file @
6a20581c
...
...
@@ 47,7 +47,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
by
rewrite
H3
;
compute
.
Qed
.
(** ... and
ε
otherwise. *)
(** ... and
[ε]
otherwise. *)
Fact
job_rtc_threshold_is_
ε
:
forall
j
,
job_cost
j
>
0
>
...
...
analysis/facts/transform/edf_opt.v
View file @
6a20581c
...
...
@@ 97,7 +97,7 @@ Section FindSwapCandidateFacts.
(** Since we are considering a uniprocessor model, only one job is
scheduled at a time. Hence once we know that a job is scheduled
at the time that [find_swap_candidate] returns, we can conclude
that it arrives not later than at time t1. *)
that it arrives not later than at time
[
t1
]
. *)
Corollary
fsc_found_job_arrival
:
forall
j2
,
scheduled_at
sched
j2
(
find_swap_candidate
sched
t1
j1
)
>
...
...
analysis/facts/transform/edf_wc.v
View file @
6a20581c
...
...
@@ 219,7 +219,7 @@ Section FSCWorkConservationLemmas.

by
apply
(
non_idle_swap_maintains_work_conservation_t1
arr_seq
_
_
_
j2
).

case
:
(
boolP
(
t
==
t2
))
=>
[/
eqP
EQ'

/
eqP
NEQ'
].
+
by
apply
(
non_idle_swap_maintains_work_conservation_t2
arr_seq
_
_
_
j1
).
+
case
:
(
boolP
((
t
<=
t1
)

(
t2
<
t
)))
=>
[
NOT_BET

BET
].
(* t <> t2 *)
+
case
:
(
boolP
((
t
<=
t1
)

(
t2
<
t
)))
=>
[
NOT_BET

BET
].
*
move
:
NOT_BET
;
move
/
orP
=>
[]
=>
NOT_BET
.
{
by
apply
(
non_idle_swap_maintains_work_conservation_LEQ_t1
arr_seq
_
_
_
H_range
_
_
H_not_idle
t2_not_idle
j
).
}
{
by
apply
(
non_idle_swap_maintains_work_conservation_GT_t2
arr_seq
_
_
_
H_range
_
_
H_not_idle
t2_not_idle
j
).
}
...
...
analysis/facts/transform/swaps.v
View file @
6a20581c
...
...
@@ 18,11 +18,11 @@ Section SwappedFacts.
Variable
t1
t2
:
instant
.
(** In the following, let [sched'] denote the schedule in which the
allocations at [t1] and [t2] have been swapped. *)
allocations at [t1] and [t2] have been swapped. *)
Let
sched'
:
=
swapped
sched
t1
t2
.
(** First, we note that the trivial case where t1 == t2 is not interesting
because then the two schedules are identical. *)
(** First, we note that the trivial case where
[
t1 == t2
]
is not interesting
because then the two schedules are identical. *)
Lemma
trivial_swap
:
t1
=
t2
>
forall
t
,
...
...
@@ 58,8 +58,8 @@ Section SwappedFacts.
by
rewrite
/
sched'
/
swapped
!
rest_of_schedule_invariant
//.
Qed
.
(** By definition, if a job is scheduled at t2 in the original
schedule, then it is found at t1 in the new schedule. *)
(** By definition, if a job is scheduled at
[
t2
]
in the original
schedule, then it is found at
[
t1
]
in the new schedule. *)
Lemma
swap_job_scheduled_t1
:
forall
j
,
scheduled_at
sched'
j
t1
=
...
...
@@ 72,8 +72,8 @@ Section SwappedFacts.

by
rewrite
ifT
.
Qed
.
(** Similarly, a job scheduled at t1 in the original schedule is
scheduled at t2 after the swap. *)
(** Similarly, a job scheduled at
[
t1
]
in the original schedule is
scheduled at
[
t2
]
after the swap. *)
Lemma
swap_job_scheduled_t2
:
forall
j
,
scheduled_at
sched'
j
t2
=
...
...
@@ 189,11 +189,11 @@ Section SwappedFacts.
service received. *)
(** To avoid dealing with symmetric cases, assume in the following
that t1 and t2 are ordered. *)
that
[
t1
]
and
[
t2
]
are ordered. *)
Hypothesis
H_well_ordered
:
t1
<=
t2
.
(** As another trivial invariant, we observe that nothing has changed
before time t1. *)
before time
[
t1
]
. *)
Lemma
swap_before_invariant
:
forall
t
,
t
<
t1
>
...
...
@@ 205,7 +205,7 @@ Section SwappedFacts.
[
move
:
t_lt_t1

move
:
t_lt_t2
]
;
rewrite
ltnn
.
Qed
.
(** Similarly, nothing has changed after time t2. *)
(** Similarly, nothing has changed after time
[
t2
]
. *)
Lemma
swap_after_invariant
:
forall
t
,
t2
<
t
>
...
...
@@ 217,7 +217,7 @@ Section SwappedFacts.
[
move
:
t1_lt_t

move
:
t2_lt_t
]
;
rewrite
ltnn
.
Qed
.
(** Thus, we observe that, before t1, the two schedules are identical with
(** Thus, we observe that, before
[
t1
]
, the two schedules are identical with
regard to the service received by any job because they are identical. *)
Corollary
service_before_swap_invariant
:
forall
t
,
...
...
@@ 232,7 +232,7 @@ Section SwappedFacts.
by
apply
ltnW
.
Qed
.
(** Likewise, we observe that, *after* t2, the swapped schedule again does not
(** Likewise, we observe that, *after*
[
t2
]
, the swapped schedule again does not
differ with regard to the service received by any job. *)
Lemma
service_after_swap_invariant
:
forall
t
,
...
...
@@ 379,8 +379,8 @@ Section EDFSwap.
(** ...that are ordered. *)
Hypothesis
H_well_ordered
:
t1
<=
t2
.
(** Further, assume that, if there are jobs scheduled at times t1 and t2, then
they either have the same deadline or violate EDF, ... *)
(** Further, assume that, if there are jobs scheduled at times
[
t1
]
and
[
t2
]
, then
they either have the same deadline or violate EDF, ... *)
Hypothesis
H_not_EDF
:
forall
j1
j2
,
scheduled_at
sched
j1
t1
>
...
...
@@ 388,14 +388,14 @@ Section EDFSwap.
job_deadline
j1
>=
job_deadline
j2
.
(** ...and that we don't move idle times or deadline misses earlier,
i.e., if t1 is not an idle time, then neither is t2 and whatever
job is scheduled at time t2 has not yet missed its deadline. *)
i.e., if
[
t1
]
is not an idle time, then neither is
[
t2
]
and whatever
job is scheduled at time
[
t2
]
has not yet missed its deadline. *)
Hypothesis
H_no_idle_time_at_t2
:
forall
j1
,
scheduled_at
sched
j1
t1
>
exists
j2
,
scheduled_at
sched
j2
t2
/\
job_deadline
j2
>
t2
.
(** Consider the schedule obtained from swapping the allocations at times t1 and t2. *)
(** Consider the schedule obtained from swapping the allocations at times
[
t1
]
and
[
t2
]
. *)
Let
sched'
:
=
swapped
sched
t1
t2
.
(** The key property of this transformation is that, for any job that
...
...
@@ 423,7 +423,7 @@ Section EDFSwap.
Qed
.
(** Next, we observe that a swap is unproblematic for the job scheduled at
time t2. *)
time
[
t2
]
. *)
Lemma
moved_earlier_implies_deadline_met
:
scheduled_at
sched
j
t2
>
job_meets_deadline
sched'
j
.
...
...
@@ 453,7 +453,7 @@ Section EDFSwap.
(** From the above case analysis, we conclude that no deadline misses
are introduced in the schedule obtained from swapping the
allocations at times t1 and t2. *)
allocations at times
[
t1
]
and
[
t2
]
. *)
Theorem
edf_swap_no_deadline_misses_introduced
:
forall
j
,
job_meets_deadline
sched
j
>
job_meets_deadline
sched'
j
.
Proof
.
...
...
behavior/arrival_sequence.v
View file @
6a20581c
...
...
@@ 81,16 +81,16 @@ Section ArrivalTimeProperties.
(** Let j be any job. *)
Variable
j
:
Job
.
(** We say that job j has arrived at time
t
iff it arrives at some time t_0
with t_0 <= t. *)
(** We say that job j has arrived at time
[t]
iff it arrives at some time
[
t_0
]
with
[
t_0 <= t
]
. *)
Definition
has_arrived
(
t
:
instant
)
:
=
job_arrival
j
<=
t
.
(** Next, we say that job j arrived before t iff it arrives at some time t_0
with t_0 < t. *)
with t_0 < t. *)
Definition
arrived_before
(
t
:
instant
)
:
=
job_arrival
j
<
t
.
(** Finally, we say that job j arrives between t1 and t2 iff it arrives at
some time
t
with t1 <= t < t2. *)
(** Finally, we say that job j arrives between
[
t1
]
and
[
t2
]
iff it arrives at
some time
[t]
with
[
t1 <= t < t2
]
. *)
Definition
arrived_between
(
t1
t2
:
instant
)
:
=
t1
<=
job_arrival
j
<
t2
.
End
ArrivalTimeProperties
.
...
...
implementation/refinements/arrival_curve.v
View file @
6a20581c
...
...
@@ 15,7 +15,7 @@ Definition get_horizon_of_task (tsk : Task) : duration :=
Definition
get_time_steps_of_task
(
tsk
:
Task
)
:
seq
duration
:
=
time_steps_of
(
get_arrival_curve_prefix
tsk
).
(** ... a function that yields the same time steps, offset by
δ
, ...**)
(** ... a function that yields the same time steps, offset by
[δ]
, ...**)
Definition
time_steps_with_offset
tsk
δ
:
=
[
seq
t
+
δ

t
<
get_time_steps_of_task
tsk
].
(** ... and a generalization of the previous function that repeats the time
...
...
implementation/refinements/task.v
View file @
6a20581c
...
...
@@ 84,7 +84,7 @@ Section Definitions.
Definition
get_time_steps_of_task_T
(
tsk
:
task_T
)
:
seq
T
:
=
time_steps_of_T
(
get_extrapolated_arrival_curve_T
tsk
).
(** ... a function that yields the same time steps, offset by
δ
, ... *)
(** ... a function that yields the same time steps, offset by
[δ]
, ... *)
Definition
time_steps_with_offset_T
tsk
δ
:
=
[
seq
t
+
δ

t
<
get_time_steps_of_task_T
tsk
]%
C
.
...
...
model/schedule/edf.v
View file @
6a20581c
...
...
@@ 7,8 +7,8 @@ Require Export prosa.behavior.all.
"EDF schedule".
Note that the "proper" way to define an EDF schedule in Prosa is to use the
EDF priority policy defined in model.priority.edf and the notion of
prioritycompliant schedules defined in model.schedule.priority_driven, as
EDF priority policy defined in
[
model.priority.edf
]
and the notion of
prioritycompliant schedules defined in
[
model.schedule.priority_driven
]
, as
well as the general notion of workconservation provided in
model.schedule.work_conserving, which will have the benefit of taking into
account issues such as various readiness models (e.g., jitter) and diverse
...
...
model/task/preemption/fully_nonpreemptive.v
View file @
6a20581c
...
...
@@ 30,7 +30,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
(** In the fully nonpreemptive model, no job can be preempted prior to its
completion. In other words, once a job starts running, it is guaranteed
to finish. Thus, we can set the tasklevel runtocompletion threshold
to
ε
. *)
to
[ε]
. *)
Definition
fully_nonpreemptive_rtc_threshold
:
TaskRunToCompletionThreshold
Task
:
=
fun
tsk
:
Task
=>
ε
.
...
...
model/task/preemption/fully_preemptive.v
View file @
6a20581c
...
...
@@ 11,7 +11,7 @@ Section FullyPreemptiveModel.
Context
{
Task
:
TaskType
}.
(** In the fully preemptive model, any job can be preempted at any
time. Thus, the maximal nonpreemptive segment has length at most
ε
time. Thus, the maximal nonpreemptive segment has length at most
[ε]
(i.e., one time unit such as a processor cycle). *)
Definition
fully_preemptive_task_model
:
TaskMaxNonpreemptiveSegment
Task
:
=
fun
tsk
:
Task
=>
ε
.
...
...
results/edf/rta/bounded_pi.v
View file @
6a20581c
...
...
@@ 231,17 +231,17 @@ Section AbstractRTAforEDFwithArrivalCurves.
Hypothesis
H_busy_interval
:
definitions
.
busy_interval
sched
interference
interfering_workload
j
t1
t2
.
(** Let's define A as a relative arrival time of job j (with respect to time t1). *)
(** Let's define A as a relative arrival time of job j (with respect to time
[
t1
]
). *)
Let
A
:
=
job_arrival
j

t1
.
(** Consider an arbitrary
shift Δ
inside the busy interval ... *)
(** Consider an arbitrary
offset [Δ]
inside the busy interval ... *)
Variable
Δ
:
duration
.
Hypothesis
H_
Δ
_in_busy
:
t1
+
Δ
<
t2
.
(** ... and the set of all arrivals between [t1] and [t1 + Δ]. *)
Let
jobs
:
=
arrivals_between
arr_seq
t1
(
t1
+
Δ
).
(** We define a predicate [EDF_from tsk].
P
redicate [EDF_from tsk]
(** We define a predicate [EDF_from tsk].
The p
redicate [EDF_from tsk]
holds true for any job [jo] of task [tsk] such that
[job_deadline jo <= job_deadline j]. *)
Let
EDF_from
(
tsk
:
Task
)
:
=
fun
(
jo
:
Job
)
=>
EDF
jo
j
&&
(
job_task
jo
==
tsk
).
...
...
@@ 355,7 +355,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** Given any job j of task [tsk] that arrives exactly A units after the beginning of
the busy interval, the bound of the total interference incurred by j within an
interval of length
Δ
is equal to [task_rbf (A + ε)  task_cost tsk + IBF_other(A, Δ)]. *)
interval of length
[Δ]
is equal to [task_rbf (A + ε)  task_cost tsk + IBF_other(A, Δ)]. *)
Let
total_interference_bound
tsk
(
A
Δ
:
duration
)
:
=
task_rbf
(
A
+
ε
)

task_cost
tsk
+
IBF_other
A
Δ
.
...
...
results/fixed_priority/rta/bounded_pi.v
View file @
6a20581c
...
...
@@ 199,7 +199,7 @@ Section AbstractRTAforFPwithArrivalCurves.
Recall that in module abstract_seq_RTA hypothesis task_interference_is_bounded_by expects
to receive a function that maps some task t, the relative arrival time of a job j of task t,
and the length of the interval to the maximum amount of interference (for more details see
fi
les limited.abstract_RTA.definitions and limited.abstract_RTA.abstract_seq_rta).
the modu
les
[
limited.abstract_RTA.definitions
]
and
[
limited.abstract_RTA.abstract_seq_rta
]
).
However, in this module we analyze only one task  [tsk], therefore it is “hardcoded”
inside the interference bound function [IBF_other]. Moreover, in case of a model with fixed
...
...
@@ 253,7 +253,7 @@ Section AbstractRTAforFPwithArrivalCurves.
(** Given any job j of task [tsk] that arrives exactly A units after the beginning of
the busy interval, the bound of the total interference incurred by j within an
interval of length
Δ
is equal to [task_rbf (A + ε)  task_cost tsk + IBF_other Δ]. *)
interval of length
[Δ]
is equal to [task_rbf (A + ε)  task_cost tsk + IBF_other Δ]. *)
Let
total_interference_bound
tsk
A
Δ
:
=
task_rbf
(
A
+
ε
)

task_cost
tsk
+
IBF_other
Δ
.
...
...
Prev
1
2
Next
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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