Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
rt-proofs
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Sergey Bozhko
rt-proofs
Commits
3fe76668
Commit
3fe76668
authored
Jul 18, 2019
by
Björn Brandenburg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
add two notions of "all deadlines met" independent of tasks
parent
bffcc219
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
60 additions
and
0 deletions
+60
-0
restructuring/analysis/schedulability.v
restructuring/analysis/schedulability.v
+60
-0
No files found.
restructuring/analysis/schedulability.v
View file @
3fe76668
...
...
@@ -106,3 +106,63 @@ Section Schedulability.
Qed
.
End
Schedulability
.
(** We further define two notions of "all deadlines met" that do not
depend on a task abstraction: one w.r.t. all scheduled jobs in a
given schedule and one w.r.t. all jobs that arrive in a given
arrival sequence. *)
Section
AllDeadlinesMet
.
(* Consider any given type of jobs... *)
Context
{
Job
:
JobType
}
`
{
JobCost
Job
}
`
{
JobDeadline
Job
}
`
{
JobArrival
Job
}.
(* ... any given type of processor states. *)
Context
{
PState
:
eqType
}.
Context
`
{
ProcessorState
Job
PState
}.
(* We say that all deadlines are met if every job scheduled at some
point in the schedule meets its deadline. Note that this is a
relatively weak definition since an "empty" schedule that is idle
at all times trivially satisfies it (since the definition does
not require any kind of work conservation). *)
Definition
all_deadlines_met
(
sched
:
schedule
PState
)
:
=
forall
j
t
,
scheduled_at
sched
j
t
->
job_meets_deadline
sched
j
.
(* To augment the preceding definition, we also define an alternate
notion of "all deadlines met" based on all jobs included in a
given arrival sequence. *)
Section
DeadlinesOfArrivals
.
(* Given an arbitrary job arrival sequence ... *)
Variable
arr_seq
:
arrival_sequence
Job
.
(* ... we say that all arrivals meet their deadline if every job
that arrives at some point in time meets its deadline. Note
that this definition does not preclude the existence of jobs in
a schedule that miss their deadline (e.g., if they stem from
another arrival sequence). *)
Definition
all_deadlines_of_arrivals_met
(
sched
:
schedule
PState
)
:
=
forall
j
,
arrives_in
arr_seq
j
->
job_meets_deadline
sched
j
.
End
DeadlinesOfArrivals
.
(* We observe that the latter definition, assuming a schedule in
which all jobs come from the arrival sequence, implies the former
definition. *)
Lemma
all_deadlines_met_in_valid_schedule
:
forall
arr_seq
sched
,
jobs_come_from_arrival_sequence
sched
arr_seq
->
all_deadlines_of_arrivals_met
arr_seq
sched
->
all_deadlines_met
sched
.
Proof
.
move
=>
arr_seq
sched
FROM_ARR
DL_ARR_MET
j
t
SCHED
.
apply
DL_ARR_MET
.
by
apply
(
FROM_ARR
_
t
).
Qed
.
End
AllDeadlinesMet
.
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