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
d5871c8f
Commit
d5871c8f
authored
Feb 14, 2022
by
Pierre Roux
Browse files
Fix some Admitted
parent
56194c99
Pipeline
#62031
failed with stages
in 1 minute and 44 seconds
Changes
13
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
analysis/abstract/ideal_jlfp_rta.v
View file @
d5871c8f
...
...
@@ 261,13 +261,12 @@ Section JLFPInstantiation.
have
Fact
:
forall
b
,
~~
b
+
b
=
true
;
first
by
intros
b
;
destruct
b
.
rewrite
Bool
.
andb_true_r
Fact
;
simpl
;
rewrite
lt0b
;
clear
Fact
.
apply
/
hasP
;
exists
j
.
Admitted
.
(* * rewrite mem_filter; apply/andP; split; first by done. *)
(* by eapply arrivals_between_sub with (t2 := 0) (t3 := upp); eauto 2. *)
(* * destruct (hep_job s j) eqn:HP; apply/orP; [rightleft]; last by done. *)
(* by rewrite /is_interference_from_another_hep_job EQ *)
(* /another_hep_job NEQ Bool.andb_true_r. *)
(* Qed. *)
*
rewrite
in_fsetE
inE
eqxx
andbT
.
exact
:
(
arrivals_between_sub
_
_
0
_
upp
).
*
destruct
(
hep_job
s
j
)
eqn
:
HP
;
apply
/
orP
;
[
right

left
]
;
last
by
done
.
by
rewrite
/
is_interference_from_another_hep_job
EQ
/
another_hep_job
NEQ
Bool
.
andb_true_r
.
Qed
.
(** In this section we prove that the (abstract) cumulative interfering workload is equivalent to
conventional workload, i.e., the one defined with concrete schedule parameters. *)
...
...
@@ 465,11 +464,11 @@ Section JLFPInstantiation.
intros
;
apply
QT
.

by
apply
in_arrivals_implies_arrived
in
H4
.

by
move
:
H5
=>
/
andP
[
H6
H7
].

by
apply
in_arrivals_implies_arrived_between
in
H4
.
Admitted
.
(*  by apply in_arrivals_implies_arrived_between in H4. *)
(* } *)
(* { rewrite negb_and Bool.negb_involutive; apply/orP. *)
(* case ARR: (arrived_before j t); [right  by left].
*)
(* case ARR: (arrived_before j t); [right  by left]. *)
(* apply QT; try eauto 2. *)
(* } *)
(* Qed. *)
...
...
analysis/facts/busy_interval/busy_interval.v
View file @
d5871c8f
...
...
@@ 9,6 +9,9 @@ Require Export prosa.analysis.definitions.work_bearing_readiness.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require
Import
prosa
.
model
.
processor
.
ideal
.
Local
Open
Scope
fset_scope
.
Local
Open
Scope
nat_scope
.
(** * Existence of Busy Interval for JLFPmodels *)
(** In this module we derive a sufficient condition for existence of
busy intervals for uniprocessor for JLFP schedulers. *)
...
...
@@ 188,37 +191,35 @@ Section ExistsBusyIntervalJLFP.
by
rewrite

REL
;
eapply
job_pending_at_arrival
;
eauto
2
.
+
by
apply
(
H_priority_is_reflexive
0
).

by
exfalso
;
move_neq_down
CONTR
;
eapply
leq_ltn_trans
;
eauto
2
.

have
EX
:
exists
hp__seq
:
se
q
Job
,

have
[
hp__seq
SE
]
:
exists
hp__seq
:
{
f
se
t
Job
}
,
forall
j__hp
,
j__hp
\
in
hp__seq
<>
arrives_in
arr_seq
j__hp
/\
job_pending_at
j__hp
t
/\
hep_job
j__hp
j
.
{
exists
(
filter
(
fun
jo
=>
(
job_pending_at
jo
t
)
&&
(
hep_job
jo
j
))
(
arrivals_between
0
t
.+
1
))
.
{
exists
[
fset
jo
in
arrivals_between
0
t
.+
1

job_pending_at
jo
t
&&
hep_job
jo
j
]
.
intros
;
split
;
intros
T
.

move
:
T
;
rewrite
mem_filter
;
move
=>
/
andP
[/
andP
[
PEN
HP
]
IN
].
repeat
split
;
eauto
using
in_arrivals_implies_arrived
.
Admitted
.
(*  move: T => [ARR [PEN HP]]. *)
(* rewrite mem_filter; apply/andP; split; first (apply/andP; split); try done. *)
(* eapply arrived_between_implies_in_arrivals; try done. *)
(* by apply/andP; split; last rewrite ltnS; move: PEN => /andP [T _]. *)
(* } move: EX => [hp__seq SE]; case FL: (hp__seq) => [  jhp jhps]. *)
(* + subst hp__seq; exfalso. *)
(* move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ GE]. *)
(* * subst t. *)
(* apply NQT with t1.+1; first by apply/andP; split. *)
(* intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP. *)
(* move: (SE jhp) => [_ SE2]. *)
(* rewrite in_nil in SE2; feed SE2; [clear SE2  by done]. *)
(* repeat split; try done; first apply/andP; split; try done. *)
(* apply/negP; intros COMLP. *)
(* move: NCOMP => /negP NCOMP; apply: NCOMP. *)
(* by apply completion_monotonic with t1. *)
(* * apply NQT with t; first by apply/andP; split. *)
(* intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP. *)
(* move: (SE jhp) => [_ SE2]. *)
(* rewrite in_nil in SE2; feed SE2; [clear SE2  by done]. *)
(* by repeat split; auto; apply/andP; split; first apply ltnW. *)
(* + move: (SE jhp)=> [SE1 _]; subst; clear SE. *)
(* by exists jhp; apply SE1; rewrite in_cons; apply/orP; left. *)
(* Qed. *)

move
:
T
;
rewrite
in_fsetE
inE
=>
/
andP
[
IN
/
andP
[
PEN
HP
]].
split
=>
[//]
;
exact
:
in_arrivals_implies_arrived
IN
.

move
:
T
=>
[
ARR
[
PEN
HP
]].
rewrite
in_fsetE
inE
;
apply
/
andP
;
split
;
last
by
apply
/
andP
;
split
.
apply
:
arrived_between_implies_in_arrivals
ARR
_
=>
//.
by
apply
/
andP
;
split
;
last
rewrite
ltnS
;
move
:
PEN
=>
/
andP
[
T
_
].
}
case
:
(
fset_0Vmem
hp__seq
)
=>
[
hp__seq0
[
jhp
jhpP
]].
+
subst
hp__seq
;
exfalso
.
move
:
GE
;
rewrite
leq_eqVlt
;
move
=>
/
orP
[/
eqP
EQ

GE
].
*
subst
t
.
apply
NQT
with
t1
.+
1
;
first
by
apply
/
andP
;
split
.
intros
jhp
ARR
HP
ARRB
;
apply
negbNE
;
apply
/
negP
;
intros
NCOMP
.
move
:
(
SE
jhp
)
=>
[
_
SE2
].
rewrite
in_nil
in
SE2
;
feed
SE2
;
[
clear
SE2

by
done
].
repeat
split
;
try
done
;
first
apply
/
andP
;
split
;
try
done
.
apply
/
negP
;
intros
COMLP
.
move
:
NCOMP
=>
/
negP
NCOMP
;
apply
:
NCOMP
.
by
apply
completion_monotonic
with
t1
.
*
apply
NQT
with
t
;
first
by
apply
/
andP
;
split
.
intros
jhp
ARR
HP
ARRB
;
apply
negbNE
;
apply
/
negP
;
intros
NCOMP
.
move
:
(
SE
jhp
)
=>
[
_
SE2
].
rewrite
in_nil
in
SE2
;
feed
SE2
;
[
clear
SE2

by
done
].
by
repeat
split
;
auto
;
apply
/
andP
;
split
;
first
apply
ltnW
.
+
exists
jhp
;
exact
:
(
SE
jhp
).
1
.
Qed
.
(** We prove that at any time instant [t] within <<[t1, t2)>> the processor is not idle. *)
Lemma
not_quiet_implies_not_idle
:
...
...
analysis/facts/busy_interval/priority_inversion.v
View file @
d5871c8f
...
...
@@ 126,9 +126,8 @@ Section PriorityInversionIsBounded.
~
is_idle
sched
t
.
Proof
.
intros
IDLE
.
Admitted
.
(* by exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2 with basic_facts. *)
(* Qed. *)
by
exfalso
;
eapply
not_quiet_implies_not_idle
with
(
t0
:
=
t
)
;
eauto
2
with
basic_facts
.
Qed
.
(** Next we consider two cases: (1) when [t] is less than [t2  1] and (2) [t] is equal to [t2  1]. *)
Lemma
t_lt_t2_or_t_eq_t2
:
...
...
@@ 308,42 +307,41 @@ Section PriorityInversionIsBounded.
move
=>
tp
t
PRPOINT
/
andP
[
GEtp
LTtp
]
/
andP
[
LEtp
LTt
].
ideal_proc_model_sched_case_analysis_eq
sched
t
jhp
.
{
apply
instant_t_is_not_idle
in
Idle
;
first
by
done
.
Admitted
.
(* by apply/andP; split; first apply leq_trans with tp. } *)
(* exists jhp. *)
(* have HP: hep_job jhp j. *)
(* { intros. *)
(* move:(H_valid_model_with_bounded_nonpreemptive_segments) => [PREE ?]. *)
(* specialize (scheduling_of_any_segment_starts_with_preemption_time arr_seq sched H_sched_valid PREE jhp t Sched_jhp) => SOAS. *)
(* move: SOAS => [prt [/andP [_ LE] [PR SCH]]]. *)
(* case E:(t1 <= prt). *)
(*  move: E => /eqP /eqP E; rewrite subn_eq0 in E. *)
(* edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jlp [_ [HEP SCHEDjhp]]]; eauto 2. *)
(* { by apply /andP; split; last by apply leq_ltn_trans with t. } *)
(* enough (EQ : jhp = jlp); first by subst. *)
(* eapply ideal_proc_model_is_a_uniprocessor_model with (t0 := prt); eauto; *)
(* by apply SCH; apply/andP; split. *)
(*  move: E => /eqP /neqP E; rewrite lt0n subn_gt0 in E. *)
(* apply negbNE; apply/negP; intros LP; rename jhp into jlp. *)
(* edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point *)
(* as [jhp [_ [HEP SCHEDjhp]]]; [  apply PRPOINT ]; first by apply/andP; split. *)
(* move: LP => /negP LP; apply: LP. *)
(* enough (EQ : jhp = jlp); first by subst. *)
(* eapply ideal_proc_model_is_a_uniprocessor_model with (j1 := jhp) (t0 := tp); eauto. *)
(* by apply SCH; apply/andP; split; first apply leq_trans with t1; auto. *)
(* } *)
(* repeat split; try done. *)
(* move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) => PENDING. *)
(* eapply scheduled_implies_pending in PENDING; eauto with basic_facts. *)
(* apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _]. *)
(* apply contraT; rewrite ltnNge; intro LT; exfalso. *)
(* feed (QUIET jhp); first by eapply H_jobs_come_from_arrival_sequence, Sched_jhp. *)
(* specialize (QUIET HP LT). *)
(* have COMP: job_completed_by jhp t. *)
(* { by apply completion_monotonic with (t0 := t1); [ apply leq_trans with tp  ]. } *)
(* apply completed_implies_not_scheduled in COMP; eauto with basic_facts. *)
(* by move : COMP => /negP COMP; apply : COMP. *)
(* Qed. *)
by
apply
/
andP
;
split
;
first
apply
leq_trans
with
tp
.
}
exists
jhp
.
have
HP
:
hep_job
jhp
j
.
{
intros
.
move
:
(
H_valid_model_with_bounded_nonpreemptive_segments
)
=>
[
PREE
?].
specialize
(
scheduling_of_any_segment_starts_with_preemption_time
arr_seq
sched
H_sched_valid
PREE
jhp
t
Sched_jhp
)
=>
SOAS
.
move
:
SOAS
=>
[
prt
[/
andP
[
_
LE
]
[
PR
SCH
]]].
case
E
:
(
t1
<=
prt
).

move
:
E
=>
/
eqP
/
eqP
E
;
rewrite
subn_eq0
in
E
.
edestruct
not_quiet_implies_exists_scheduled_hp_job_at_preemption_point
as
[
jlp
[
_
[
HEP
SCHEDjhp
]]]
;
eauto
2
.
{
by
apply
/
andP
;
split
;
last
by
apply
leq_ltn_trans
with
t
.
}
enough
(
EQ
:
jhp
=
jlp
)
;
first
by
subst
.
eapply
ideal_proc_model_is_a_uniprocessor_model
with
(
t0
:
=
prt
)
;
eauto
;
by
apply
SCH
;
apply
/
andP
;
split
.

move
:
E
=>
/
eqP
/
neqP
E
;
rewrite

lt0n
subn_gt0
in
E
.
apply
negbNE
;
apply
/
negP
;
intros
LP
;
rename
jhp
into
jlp
.
edestruct
not_quiet_implies_exists_scheduled_hp_job_at_preemption_point
as
[
jhp
[
_
[
HEP
SCHEDjhp
]]]
;
[

apply
PRPOINT

]
;
first
by
apply
/
andP
;
split
.
move
:
LP
=>
/
negP
LP
;
apply
:
LP
.
enough
(
EQ
:
jhp
=
jlp
)
;
first
by
subst
.
eapply
ideal_proc_model_is_a_uniprocessor_model
with
(
j1
:
=
jhp
)
(
t0
:
=
tp
)
;
eauto
.
by
apply
SCH
;
apply
/
andP
;
split
;
first
apply
leq_trans
with
t1
;
auto
.
}
repeat
split
;
try
done
.
move
:
(
H_busy_interval_prefix
)
=>
[
SL
[
QUIET
[
NOTQUIET
EXj
]]]
;
move
:
(
Sched_jhp
)
=>
PENDING
.
eapply
scheduled_implies_pending
in
PENDING
;
eauto
with
basic_facts
.
apply
/
andP
;
split
;
last
by
apply
leq_ltn_trans
with
(
n
:
=
t
)
;
first
by
move
:
PENDING
=>
/
andP
[
ARR
_
].
apply
contraT
;
rewrite

ltnNge
;
intro
LT
;
exfalso
.
feed
(
QUIET
jhp
)
;
first
by
eapply
H_jobs_come_from_arrival_sequence
,
Sched_jhp
.
specialize
(
QUIET
HP
LT
).
have
COMP
:
job_completed_by
jhp
t
.
{
by
apply
completion_monotonic
with
(
t0
:
=
t1
)
;
[
apply
leq_trans
with
tp

].
}
apply
completed_implies_not_scheduled
in
COMP
;
eauto
with
basic_facts
.
by
move
:
COMP
=>
/
negP
COMP
;
apply
:
COMP
.
Qed
.
(** Now, suppose there exists some constant K that bounds the distance to
a preemption time from the beginning of the busy interval. *)
...
...
analysis/facts/readiness/sequential.v
View file @
d5871c8f
...
...
@@ 65,11 +65,10 @@ Section SequentialTasksReadiness.
intros
j1
j2
t
ARR1
ARR2
SAME
LT
SCHED
.
destruct
(
boolP
(
job_ready
sched
j2
t
))
as
[
READY

NREADY
].

move
:
READY
=>
/
andP
[
PEND
/
allP
ALL
]
;
apply
:
ALL
.
Admitted
.
(* rewrite mem_filter; apply/andP; split; first by done. *)
(* by apply arrived_between_implies_in_arrivals => //. *)
(*  by apply H_valid_schedule in SCHED; rewrite SCHED in NREADY. *)
(* Qed. *)
rewrite
in_fsetE
inE
/(
same_task
j1
j2
)
SAME
andbT
.
exact
:
arrived_between_implies_in_arrivals
.

by
apply
H_valid_schedule
in
SCHED
;
rewrite
SCHED
in
NREADY
.
Qed
.
(* Finally, we show that the sequential readiness model is a
workbearing readiness model. That is, if a job [j] is pending
...
...
model/task/arrival/arrival_curve_to_rbf.v
View file @
d5871c8f
From
mathcomp
Require
Import
ssreflect
ssrnat
finmap
.
Require
Export
prosa
.
util
.
all
.
Require
Export
prosa
.
model
.
task
.
arrival
.
request_bound_functions
.
Require
Export
prosa
.
model
.
task
.
arrival
.
curves
.
...
...
@@ 88,13 +89,11 @@ Section ArrivalCurveToRBF.
move
=>
TASK_COST
RESPECT
t1
t2
LEQ
.
specialize
(
RESPECT
t1
t2
LEQ
).
apply
leq_trans
with
(
n
:
=
task_cost
tsk
*
number_of_task_arrivals
arr_seq
tsk
t1
t2
)
=>
//.

rewrite
/
max_arrivals
/
number_of_task_arrivals

sum1_size
big_distrr
//=
muln1
leq_sum_seq
//
=>
j
.
Admitted
.
(* rewrite mem_filter => /andP [/eqP TSK _] _. *)
(* rewrite TSK. *)
(* by apply TASK_COST. *)
(*  by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l. *)
(* Qed. *)

rewrite
/
number_of_task_arrivals
.
rewrite

sum1_size
big_distrr
/=
muln1
leq_sum_seq
//
=>
j
.
rewrite
in_fsetE
inE
=>
/
andP
[
_
/
eqP
<
_
]
;
exact
:
TASK_COST
.

by
destruct
(
task_cost
tsk
)
eqn
:
C
;
rewrite
/
task_max_rbf
C
//
leq_pmul2l
.
Qed
.
(** Finally, we prove that the task respects the requestbound function also in
the lowerbounding case. This time, we assume that the cost of tasks lowerbounds
...
...
@@ 108,12 +107,10 @@ Section ArrivalCurveToRBF.
specialize
(
RESPECT
t1
t2
LEQ
).
apply
leq_trans
with
(
n
:
=
task_min_cost
tsk
*
number_of_task_arrivals
arr_seq
tsk
t1
t2
)
=>
//.

by
destruct
(
task_min_cost
tsk
)
eqn
:
C
;
rewrite
/
task_min_rbf
C
//
leq_pmul2l
.

rewrite
/
min_arrivals
/
number_of_task_arrivals

sum1_size
big_distrr
//=
muln1
leq_sum_seq
//
=>
j
.
Admitted
.
(* rewrite mem_filter => /andP [/eqP TSK _] _. *)
(* rewrite TSK. *)
(* by apply TASK_COST. *)
(* Qed. *)

rewrite
/
number_of_task_arrivals
.
rewrite

sum1_size
big_distrr
/=
muln1
leq_sum_seq
//
=>
j
.
rewrite
in_fsetE
inE
=>
/
andP
[
_
/
eqP
<
_
]
;
exact
:
TASK_COST
.
Qed
.
End
SingleTask
.
...
...
model/task/arrivals.v
View file @
d5871c8f
...
...
@@ 42,7 +42,7 @@ Section TaskArrivals.
(** ... and finally count the number of job arrivals. *)
Definition
number_of_task_arrivals
(
t1
t2
:
instant
)
:
=
size
(
task_arrivals_between
t1
t2
)
.
#
`
task_arrivals_between
t1
t2

.
(** ... and also count the cost of job arrivals. *)
Definition
cost_of_task_arrivals
(
t1
t2
:
instant
)
:
=
...
...
results/edf/rta/bounded_nps.v
View file @
d5871c8f
...
...
@@ 167,32 +167,30 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
intros
j'
JINB
NOTHEP
.
apply
leq_bigmax_cond_seq
with
(
x
:
=
(
job_task
j'
))
(
F
:
=
fun
tsk
=>
task_max_nonpreemptive_segment
tsk

1
).
{
apply
H_all_jobs_from_taskset
.
Admitted
.
(* apply mem_bigcat_nat_exists in JINB. *)
(* by inversion JINB as [ta' [JIN' _]]; exists ta'. } *)
(* { have NINTSK: job_task j' != tsk. *)
(* { apply/eqP; intros TSKj'. *)
(* rewrite /EDF ltnNge in NOTHEP. *)
(* rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP. *)
(* rewrite TSKj' TSK ltn_add2r in NOTHEP. *)
(* move: NOTHEP; rewrite ltnNge; move => /negP T; apply: T. *)
(* apply leq_trans with t; last by done. *)
(* eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2. *)
(* move: JINB; move => /andP [_ T]. *)
(* by apply ltnW. *)
(* } *)
(* apply/andP; split; first by done. *)
(* rewrite /EDF ltnNge in NOTHEP. *)
(* rewrite TSK. *)
(* have ARRLE: job_arrival j' < job_arrival j. *)
(* { apply leq_trans with t; last by done. *)
(* eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2. *)
(* by move: JINB; move => /andP [_ T]. *)
(* } *)
(* rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP. *)
(* rewrite /D; ssrlia. *)
(* } *)
(* Qed. *)
by
move
:
JINB
=>
/
bigfcup_natP
[
ta'
_
JIN'
]
;
exists
ta'
.
}
{
have
NINTSK
:
job_task
j'
!=
tsk
.
{
apply
/
eqP
;
intros
TSKj'
.
rewrite
/
EDF

ltnNge
in
NOTHEP
.
rewrite
/
job_deadline
/
absolute_deadline
.
job_deadline_from_task_deadline
in
NOTHEP
.
rewrite
TSKj'
TSK
ltn_add2r
in
NOTHEP
.
move
:
NOTHEP
;
rewrite
ltnNge
;
move
=>
/
negP
T
;
apply
:
T
.
apply
leq_trans
with
t
;
last
by
done
.
eapply
in_arrivals_implies_arrived_between
in
JINB
;
last
by
eauto
2
.
move
:
JINB
;
move
=>
/
andP
[
_
T
].
by
apply
ltnW
.
}
apply
/
andP
;
split
;
first
by
done
.
rewrite
/
EDF

ltnNge
in
NOTHEP
.
rewrite

TSK
.
have
ARRLE
:
job_arrival
j'
<
job_arrival
j
.
{
apply
leq_trans
with
t
;
last
by
done
.
eapply
in_arrivals_implies_arrived_between
in
JINB
;
last
by
eauto
2
.
by
move
:
JINB
;
move
=>
/
andP
[
_
T
].
}
rewrite
/
job_deadline
/
absolute_deadline
.
job_deadline_from_task_deadline
in
NOTHEP
.
rewrite
/
D
;
ssrlia
.
}
Qed
.
(** Using the lemma above, we prove that the priority inversion of the task is bounded by
the maximum length of a nonpreemptive section of lowerpriority tasks. *)
...
...
results/edf/rta/bounded_pi.v
View file @
d5871c8f
...
...
@@ 228,27 +228,26 @@ Section AbstractRTAforEDFwithArrivalCurves.
{
exfalso
;
clear
HYP1
HYP2
.
eapply
instantiated_busy_interval_equivalent_busy_interval
in
BUSY
;
eauto
2
with
basic_facts
.
move
:
BUSY
=>
[
PREF
_
].
Admitted
.
(* by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. } *)
(* { clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo. *)
(* rewrite EqSched_jo in HYP1, HYP2. *)
(* move: HYP1 HYP2. *)
(* rewrite Bool.negb_involutive negb_and. *)
(* move => HYP1 /orP [/negP HYP2 /eqP HYP2]. *)
(*  by exfalso. *)
(*  rewrite Bool.negb_involutive in HYP2. *)
(* move: HYP2 => /eqP /eqP HYP2. *)
(* by subst jo; rewrite scheduled_at_def EqSched_jo. *)
(* } *)
(* } *)
(* { apply/negP; *)
(* rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion *)
(* /is_interference_from_another_hep_job *)
(* HYP negb_or; apply/andP; split. *)
(*  by rewrite Bool.negb_involutive; eapply (EDF_is_reflexive 0). *)
(*  by rewrite negb_and Bool.negb_involutive; apply/orP; right. *)
(* } *)
(* Qed. *)
by
eapply
not_quiet_implies_not_idle
;
eauto
2
with
basic_facts
.
}
{
clear
EqSched_jo
;
move
:
Sched_jo
;
rewrite
scheduled_at_def
;
move
=>
/
eqP
EqSched_jo
.
rewrite
EqSched_jo
in
HYP1
,
HYP2
.
move
:
HYP1
HYP2
.
rewrite
Bool
.
negb_involutive
negb_and
.
move
=>
HYP1
/
orP
[/
negP
HYP2

/
eqP
HYP2
].

by
exfalso
.

rewrite
Bool
.
negb_involutive
in
HYP2
.
move
:
HYP2
=>
/
eqP
/
eqP
HYP2
.
by
subst
jo
;
rewrite
scheduled_at_def
EqSched_jo
.
}
}
{
apply
/
negP
;
rewrite
/
interference
/
ideal_jlfp_rta
.
interference
/
is_priority_inversion
/
is_interference_from_another_hep_job
HYP
negb_or
;
apply
/
andP
;
split
.

by
rewrite
Bool
.
negb_involutive
;
eapply
(
EDF_is_reflexive
0
).

by
rewrite
negb_and
Bool
.
negb_involutive
;
apply
/
orP
;
right
.
}
Qed
.
(** Next, we prove that the interference and interfering workload
functions are consistent with sequential tasks. *)
...
...
results/fixed_priority/rta/bounded_nps.v
View file @
d5871c8f
...
...
@@ 146,18 +146,16 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
intros
j'
JINB
NOTHEP
.
rewrite
leq_sub2r
//.
apply
H_valid_model_with_bounded_nonpreemptive_segments
.
Admitted
.
(* by eapply in_arrivals_implies_arrived; eauto 2. *)
(* } *)
(* { apply /bigmax_leq_seqP. *)
(* intros j' JINB NOTHEP. *)
(* apply leq_bigmax_cond_seq with *)
(* (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk  1); last by done. *)
(* apply H_all_jobs_from_taskset. *)
(* apply mem_bigcat_nat_exists in JINB. *)
(* by inversion JINB as [ta' [JIN' _]]; exists ta'. *)
(* } *)
(* Qed. *)
exact
:
in_arrivals_implies_arrived
JINB
.
}
{
apply
/
bigmax_leq_seqP
.
intros
j'
JINB
NOTHEP
.
apply
leq_bigmax_cond_seq
with
(
x
:
=
(
job_task
j'
))
(
F
:
=
fun
tsk
=>
task_max_nonpreemptive_segment
tsk

1
)
;
last
by
done
.
apply
H_all_jobs_from_taskset
.
by
have
/
bigfcup_natP
[
i
_
{}
JINB
]
:
=
JINB
;
exists
i
.
}
Qed
.
(** Using the above lemma, we prove that the priority inversion of the task is bounded by blocking_bound. *)
Lemma
priority_inversion_is_bounded
:
...
...
@@ 175,37 +173,36 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
}
move
:
NEQ
=>
/
negP
/
negP
;
rewrite

ltnNge
;
move
=>
BOUND
.
edestruct
(@
preemption_time_exists
)
as
[
ppt
[
PPT
NEQ
]]
;
eauto
2
with
basic_facts
.
Admitted
.
(* move: NEQ => /andP [GE LE]. *)
(* apply leq_trans with (cumulative_priority_inversion sched j t1 ppt); *)
(* last apply leq_trans with (ppt  t1); first last. *)
(*  rewrite leq_subLR. *)
(* apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done. *)
(* by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2. *)
(*  rewrite /cumulative_priority_inversion /is_priority_inversion. *)
(* rewrite [X in _ <= X]addn0 [ppt  t1]mul1n iter_addn big_const_nat. *)
(* rewrite leq_sum //; intros t _; case: (sched t); last by done. *)
(* by intros s; case: (hep_job s j). *)
(*  rewrite /cumulative_priority_inversion /is_priority_inversion. *)
(* rewrite (@big_cat_nat _ _ _ ppt) //=; last first. *)
(* { rewrite ltn_subRL in BOUND. *)
(* apply leq_trans with (t1 + blocking_bound); last by apply ltnW. *)
(* apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done. *)
(* rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2. *)
(* } *)
(* rewrite [X in _ <= X]addn0 leq_add2l leqn0. *)
(* rewrite big_nat_cond big1 //; move => t /andP [/andP [GEt LTt] _ ]. *)
(* case SCHED: (sched t) => [s  ]; last by done. *)
(* edestruct (@not_quiet_implies_exists_scheduled_hp_job) *)
(* with (K := ppt  t1) (t1 := t1) (t2 := t2) (t := t) *)
(* as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts. *)
(* { by exists ppt; split; [done  rewrite subnKC //; apply/andP]. } *)
(* { by rewrite subnKC //; apply/andP; split. } *)
(* apply/eqP; rewrite eqb0 Bool.negb_involutive. *)
(* enough (EQef : s = j_hp); first by subst;auto. *)
(* eapply ideal_proc_model_is_a_uniprocessor_model; eauto 2. *)
(* by rewrite scheduled_at_def SCHED. *)
(* Qed. *)
move
:
NEQ
=>
/
andP
[
GE
LE
].
apply
leq_trans
with
(
cumulative_priority_inversion
sched
j
t1
ppt
)
;
last
apply
leq_trans
with
(
ppt

t1
)
;
first
last
.

rewrite
leq_subLR
.
apply
leq_trans
with
(
t1
+
max_length_of_priority_inversion
j
t1
)
;
first
by
done
.
by
rewrite
leq_add2l
;
eapply
priority_inversion_is_bounded_by_blocking
;
eauto
2
.

rewrite
/
cumulative_priority_inversion
/
is_priority_inversion
.
rewrite
[
X
in
_
<=
X
]
addn0
[
ppt

t1
]
mul1n

iter_addn

big_const_nat
.
rewrite
leq_sum
//
;
intros
t
_;
case
:
(
sched
t
)
;
last
by
done
.
by
intros
s
;
case
:
(
hep_job
s
j
).

rewrite
/
cumulative_priority_inversion
/
is_priority_inversion
.
rewrite
(@
big_cat_nat
_
_
_
ppt
)
//=
;
last
first
.
{
rewrite
ltn_subRL
in
BOUND
.
apply
leq_trans
with
(
t1
+
blocking_bound
)
;
last
by
apply
ltnW
.
apply
leq_trans
with
(
t1
+
max_length_of_priority_inversion
j
t1
)
;
first
by
done
.
rewrite
leq_add2l
;
eapply
priority_inversion_is_bounded_by_blocking
;
eauto
2
.
}
rewrite
[
X
in
_
<=
X
]
addn0
leq_add2l
leqn0
.
rewrite
big_nat_cond
big1
//
;
move
=>
t
/
andP
[/
andP
[
GEt
LTt
]
_
].
case
SCHED
:
(
sched
t
)
=>
[
s

]
;
last
by
done
.
edestruct
(@
not_quiet_implies_exists_scheduled_hp_job
)
with
(
K
:
=
ppt

t1
)
(
t1
:
=
t1
)
(
t2
:
=
t2
)
(
t
:
=
t
)
as
[
j_hp
[
ARRB
[
HP
SCHEDHP
]]]
;
eauto
2
with
basic_facts
.
{
by
exists
ppt
;
split
;
[
done

rewrite
subnKC
//
;
apply
/
andP
].
}
{
by
rewrite
subnKC
//
;
apply
/
andP
;
split
.
}
apply
/
eqP
;
rewrite
eqb0
Bool
.
negb_involutive
.
enough
(
EQef
:
s
=
j_hp
)
;
first
by
subst
;
auto
.
eapply
ideal_proc_model_is_a_uniprocessor_model
;
eauto
2
.
by
rewrite
scheduled_at_def
SCHED
.
Qed
.
End
PriorityInversionIsBounded
.
...
...
results/fixed_priority/rta/floating_nonpreemptive.v
View file @
d5871c8f
...
...
@@ 150,12 +150,11 @@ Section RTAforFloatingModelwithArrivalCurves.
eapply
uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
.
all
:
eauto
2
with
basic_facts
.

by
apply
sequential_readiness_implies_work_bearing_readiness
.
Admitted
.
(*  by apply sequential_readiness_implies_sequential_tasks. *)
(*  intros A SP. *)
(* rewrite subnn subn0. *)
(* destruct (H_R_is_maximum _ SP) as [F [EQ LE]]. *)
(* by exists F; rewrite addn0; split. *)
(* Qed. *)

by
apply
sequential_readiness_implies_sequential_tasks
.

intros
A
SP
.
rewrite
subnn
subn0
.
destruct
(
H_R_is_maximum
_
SP
)
as
[
F
[
EQ
LE
]].
by
exists
F
;
rewrite
addn0
;
split
.
Qed
.
End
RTAforFloatingModelwithArrivalCurves
.
results/fixed_priority/rta/fully_nonpreemptive.v
View file @
d5871c8f
...
...
@@ 152,8 +152,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(
L0
:
=
L
).
all
:
eauto
3
with
basic_facts
.

by
apply
sequential_readiness_implies_work_bearing_readiness
.
Admitted
.
(*  by apply sequential_readiness_implies_sequential_tasks. *)
(* Qed. *)

by
apply
sequential_readiness_implies_sequential_tasks
.
Qed
.
End
RTAforFullyNonPreemptiveFPModelwithArrivalCurves
.
results/fixed_priority/rta/fully_preemptive.v
View file @
d5871c8f
...
...
@@ 139,15 +139,14 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
all
:
eauto
2
with
basic_facts
.
rewrite
/
work_bearing_readiness
.

by
apply
sequential_readiness_implies_work_bearing_readiness
.
Admitted
.
(*  by apply sequential_readiness_implies_sequential_tasks => //. *)
(*  by rewrite BLOCK add0n. *)
(*  move => A /andP [LT NEQ]. *)
(* edestruct H_R_is_maximum as [F [FIX BOUND]]. *)
(* { by apply/andP; split; eauto 2. } *)
(* exists F; split. *)
(* + by rewrite BLOCK add0n subnn subn0. *)
(* + by rewrite subnn addn0. *)
(* Qed. *)

by
apply
sequential_readiness_implies_sequential_tasks
=>
//.

by
rewrite
BLOCK
add0n
.

move
=>
A
/
andP
[
LT
NEQ
].
edestruct
H_R_is_maximum
as
[
F
[
FIX
BOUND
]].
{
by
apply
/
andP
;
split
;
eauto
2
.
}
exists
F
;
split
.
+
by
rewrite
BLOCK
add0n
subnn
subn0
.
+
by
rewrite
subnn
addn0
.
Qed
.
End
RTAforFullyPreemptiveFPModelwithArrivalCurves
.
results/fixed_priority/rta/limited_preemptive.v
View file @
d5871c8f
...
...
@@ 158,24 +158,23 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
with
(
L0
:
=
L
).
all
:
eauto
2
with
basic_facts
.

by
apply
sequential_readiness_implies_work_bearing_readiness
.
Admitted
.
(*  by apply sequential_readiness_implies_sequential_tasks. *)
(*  intros A SP. *)
(* destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]]. *)
(* exists FF; rewrite subKn; first by done. *)
(* rewrite /task_last_nonpr_segment (leq_add2r 1) subn1 !addn1 prednK; last first. *)
(* + rewrite /last0 nth_last. *)
(* apply HYP3; try by done. *)
(* rewrite (ltn_add2r 1) !addn1 prednK //. *)
(* move: (number_of_preemption_points_in_task_at_least_two *)
(* _ _ H_valid_model_with_fixed_preemption_points _ H_tsk_in_ts POSt) => Fact2. *)
(* move: (Fact2) => Fact3. *)
(* by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2. *)
(* + apply leq_trans with (task_max_nonpreemptive_segment tsk). *)
(* * by apply last_of_seq_le_max_of_seq. *)
(* * rewrite END; last by done. *)
(* apply ltnW; rewrite ltnS; try done. *)
(* by apply max_distance_in_seq_le_last_element_of_seq; eauto 2. *)
(* Qed. *)

by
apply
sequential_readiness_implies_sequential_tasks
.

intros
A
SP
.
destruct
(
H_R_is_maximum
_
SP
)
as
[
FF
[
EQ1
EQ2
]].
exis