Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
rtproofs
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
rtproofs
Commits
edaa526b
Commit
edaa526b
authored
May 24, 2019
by
Maxime Lesourd
Committed by
Björn Brandenburg
Jun 05, 2019
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Indentation in facts
parent
73ea8320
Changes
3
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
25 additions
and
21 deletions
+25
21
behavior/facts/arrivals.v
behavior/facts/arrivals.v
+1
2
behavior/facts/completion.v
behavior/facts/completion.v
+11
12
behavior/facts/ideal_schedule.v
behavior/facts/ideal_schedule.v
+13
7
No files found.
behavior/facts/arrivals.v
View file @
edaa526b
From
rt
.
behavior
.
arrival
Require
Export
arrival_sequence
.
From
rt
.
util
Require
Import
all
.
(* In this section, we establish useful facts about arrival sequence prefixes. *)
Section
ArrivalSequencePrefix
.
...
...
@@ 121,7 +120,7 @@ Section ArrivalSequencePrefix.
intros
j
t
IN
.
Fail
suff
:
arrived_between
j
0
t
by
rewrite
/
arrived_between
/=.
have
:
arrived_between
j
0
t
by
apply
in_arrivals_implies_arrived_between
.
by
rewrite
/
arrived_between
/=.
by
rewrite
/
arrived_between
/=.
Qed
.
(* Similarly, we prove that if a job from the arrival sequence arrives
...
...
behavior/facts/completion.v
View file @
edaa526b
...
...
@@ 3,7 +3,6 @@ From rt.behavior.facts Require Export service.
(** In this file, we establish basic facts about job completions. *)
Section
CompletionFacts
.
(* Consider any job type,...*)
Context
{
Job
:
JobType
}.
...
...
@@ 28,7 +27,7 @@ Section CompletionFacts.
Proof
.
move
=>
t
t'
LE
.
rewrite
/
completed_by
/
service
=>
COMP
.
apply
leq_trans
with
(
n
:
=
service_during
sched
j
0
t
)
;
auto
.
by
apply
service_monotonic
.
by
apply
service_monotonic
.
Qed
.
(* We observe that being incomplete is the same as not having received
...
...
@@ 66,7 +65,7 @@ Section CompletionFacts.
move
=>
t
SERVICE
.
rewrite
subn_gt0
/
service
/
service_during
.
apply
leq_trans
with
(
\
sum_
(
0
<=
t0
<
t
.+
1
)
service_at
sched
j
t0
)
;
last
by
rewrite
H_completed_jobs
.
last
by
rewrite
H_completed_jobs
.
by
rewrite
big_nat_recr
//=

addn1
leq_add2l
.
Qed
.
...
...
@@ 176,8 +175,8 @@ Section ServiceAndCompletionFacts.
move
/
eqP
in
EQ
.
rewrite
/
completed_by
EQ
//.
*
apply
leq_trans
with
(
n
:
=
service
sched
j
n
+
1
).

rewrite
leq_add2l
/
service_at
//.

rewrite
(
ltnS
(
service
sched
j
n
+
1
)
_
)
(
addn1
(
job_cost
j
))
ltn_add2r
//.

rewrite
leq_add2l
/
service_at
//.

rewrite
(
ltnS
(
service
sched
j
n
+
1
)
_
)
(
addn1
(
job_cost
j
))
ltn_add2r
//.
Qed
.
(* We show that the service received by job j in any interval is no larger
...
...
@@ 208,7 +207,7 @@ Section ServiceAndCompletionFacts.
move
=>
t
SCHED
.
rewrite
/
pending
.
apply
/
andP
;
split
;
first
by
apply
:
H_jobs_must_arrive
=>
//.
first
by
apply
:
H_jobs_must_arrive
=>
//.
apply
:
scheduled_implies_not_completed
=>
//.
Qed
.
...
...
@@ 225,13 +224,13 @@ Section ServiceAndCompletionFacts.
move
=>
t
.
rewrite
incomplete_is_positive_remaining_cost
=>
REMCOST
.
rewrite

less_service_than_cost_is_incomplete
(
service_cat
sched
j
t
)
;
last
by
rewrite

addnBA
//
;
apply
:
leq_addr
.
last
by
rewrite

addnBA
//
;
apply
:
leq_addr
.
apply
leq_ltn_trans
with
(
n
:
=
service
sched
j
t
+
remaining_cost
sched
j
t

1
).

by
rewrite
!
addnBA
//
;
rewrite
leq_add2l
;
apply
cumulative_service_le_delta
;
exact
.

rewrite
service_cost_invariant
//

subn_gt0
subKn
//.
move
:
REMCOST
.
rewrite
/
remaining_cost
subn_gt0
=>
SERVICE
.
by
apply
leq_ltn_trans
with
(
n
:
=
service
sched
j
t
).
Qed
.
by
apply
leq_ltn_trans
with
(
n
:
=
service
sched
j
t
).
Qed
.
End
ServiceAndCompletionFacts
.
...
...
@@ 275,8 +274,8 @@ Section PositiveCost.
move
=>
t
COMPLETE
.
have
POSITIVE_SERVICE
:
0
<
service
sched
j
t
by
apply
leq_trans
with
(
n
:
=
job_cost
j
)
;
auto
.
by
apply
:
positive_service_implies_scheduled_since_arrival
;
assumption
.
Qed
.
by
apply
:
positive_service_implies_scheduled_since_arrival
;
assumption
.
Qed
.
(* We also prove that the job is pending at the moment of its arrival. *)
Lemma
job_pending_at_arrival
:
...
...
@@ 284,7 +283,7 @@ Section PositiveCost.
Proof
.
rewrite
/
pending
.
apply
/
andP
;
split
;
first
by
rewrite
/
has_arrived
//.
first
by
rewrite
/
has_arrived
//.
rewrite
/
completed_by
no_service_before_arrival
//

ltnNge
//.
Qed
.
...
...
behavior/facts/ideal_schedule.v
View file @
edaa526b
...
...
@@ 8,15 +8,21 @@ Section OnlyOneJobScheduled.
model. *)
Context
{
Job
:
JobType
}.
(* Consider an ideal schedule... *)
Variable
sched
:
schedule
(
processor_state
Job
).
(* Consider an ideal schedule... *)
Variable
sched
:
schedule
(
processor_state
Job
).
(* ...and two given jobs that are to be scheduled. *)
Variable
j1
j2
:
Job
.
(* ...and two given jobs that are to be scheduled. *)
Variable
j1
j2
:
Job
.
(* At any time t, if both j1 and j2 are scheduled, then they must be the same
job. *)
Lemma
only_one_job_scheduled
:
forall
t
,
scheduled_at
sched
j1
t
>
scheduled_at
sched
j2
t
>
j1
=
j2
.
Proof
.
rewrite
/
scheduled_at
/
scheduled_in
/
pstate_instance
=>
t
/
eqP
>
/
eqP
EQ
.
by
inversion
EQ
.
Qed
.
job. *)
Lemma
only_one_job_scheduled
:
forall
t
,
scheduled_at
sched
j1
t
>
scheduled_at
sched
j2
t
>
j1
=
j2
.
Proof
.
by
rewrite
/
scheduled_at
=>
t
/
eqP
>/
eqP
[>].
Qed
.
End
OnlyOneJobScheduled
.
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