Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Xiaojie Guo
rtproofs
Commits
7a823328
Commit
7a823328
authored
Jan 19, 2016
by
Felipe Cerqueira
Browse files
Simplify lemma about task invariant in platform.v
parent
d64e731f
Changes
2
Hide whitespace changes
Inline
Sidebyside
platform.v
View file @
7a823328
...
...
@@ 121,11 +121,7 @@ Module Platform.
(* Assume the task set has no duplicates, ... *)
Hypothesis
H_ts_is_a_set
:
uniq
ts
.
(* ... all jobs have valid parameters ...*)
Hypothesis
H_valid_job_parameters
:
forall
(
j
:
JobIn
arr_seq
),
valid_sporadic_job
task_cost
task_deadline
job_cost
job_deadline
job_task
j
.
(* ... and come from the taskset. *)
(* ... and all jobs come from the taskset. *)
Hypothesis
H_all_jobs_from_taskset
:
forall
(
j
:
JobIn
arr_seq
),
job_task
j
\
in
ts
.
...
...
@@ 184,8 +180,7 @@ Module Platform.
H_sporadic_tasks
into
SPO
,
H_valid_task
into
PARAMS
,
H_all_previous_jobs_completed
into
PREV
,
H_completed_jobs_dont_execute
into
COMP
,
H_valid_job_parameters
into
JOBPARAMS
.
H_completed_jobs_dont_execute
into
COMP
.
unfold
JLFP_JLDP_scheduling_invariant_holds
,
valid_sporadic_job
,
valid_realtime_job
,
task_precedence_constraints
,
completed_jobs_dont_execute
,
...
...
@@ 206,18 +201,6 @@ Module Platform.
move
:
SCHED1
SCHED2
=>
/
eqP
SCHED1
/
eqP
SCHED2
.
by
rewrite

SCHED1

SCHED2
.
}
{
intros
x
cpu1
cpu2
SCHED1
SCHED2
.
unfold
schedules_job_of_tsk
in
*.
destruct
(
sched
cpu1
t
)
eqn
:
SCHED1'
;
last
by
done
.
destruct
(
sched
cpu2
t
)
eqn
:
SCHED2'
;
last
by
done
.
move
:
SCHED1
SCHED2
=>
/
eqP
SCHED1
/
eqP
SCHED2
;
subst
x
.
exploit
(
NOINTRA
j1
j0
t
SCHED2
)
;
[
by
apply
/
exists_inP
;
exists
cpu2
;
last
by
apply
/
eqP

by
apply
/
exists_inP
;
exists
cpu1
;
last
by
apply
/
eqP

intro
SAMEjob
;
subst
].
by
apply
SEQUENTIAL
with
(
j
:
=
j0
)
(
t
:
=
t
).
}
}
{
apply
leq_trans
with
(
n
:
=
count
((
higher_eq_priority
t
)^~
j
)
(
jobs_scheduled_at
sched
t
)).
...
...
@@ 234,7 +217,14 @@ Module Platform.
apply
sub_count
;
red
;
move
=>
j_hp
/
andP
[
HP
IN
].
rewrite
mem_scheduled_jobs_eq_scheduled
in
IN
.
rename
IN
into
SCHED
.
apply
/
andP
;
split
.
apply
/
andP
;
split
;
last
first
.
{
move
:
SCHED
=>
/
exists_inP
SCHED
.
destruct
SCHED
as
[
cpu
INcpu
SCHED
].
move
:
SCHED
=>
/
eqP
SCHED
.
apply
/
exists_inP
;
exists
cpu
;
first
by
done
.
by
unfold
schedules_job_of_tsk
;
rewrite
SCHED
.
}
{
unfold
is_interfering_task_jlfp
.
destruct
(
j
==
j_hp
)
eqn
:
EQjob
.
...
...
@@ 271,13 +261,6 @@ Module Platform.
move
:
COMPLETED
=>
/
eqP
COMPLETED
.
by
rewrite

COMPLETED
leqnn
.
}
{
move
:
SCHED
=>
/
exists_inP
SCHED
.
destruct
SCHED
as
[
cpu
INcpu
SCHED
].
move
:
SCHED
=>
/
eqP
SCHED
.
apply
/
exists_inP
;
exists
cpu
;
first
by
done
.
by
unfold
schedules_job_of_tsk
;
rewrite
SCHED
.
}
}
have
MAP
:
=
count_map
(
fun
(
x
:
JobIn
arr_seq
)
=>
job_task
x
)
(
fun
x
=>
is_interfering_task_jlfp
tsk
x
&&
task_is_scheduled
job_task
sched
x
t
).
rewrite

MAP
;
clear
MAP
.
...
...
platform_edf.v
View file @
7a823328
...
...
@@ 142,6 +142,210 @@ Module PlatformEDF.
End
IntraTaskParallelismAndTaskPrecedenceUnderEDF
.
(*Section JobInvariantAsTaskInvariant.
(* Consider task set ts. *)
Variable ts: taskset_of sporadic_task.
(* Assume the task set has no duplicates, ... *)
Hypothesis H_ts_is_a_set: uniq ts.
(* ... and all jobs come from the taskset. *)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
(* Suppose that a single job does not execute in parallel, ...*)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* ... jobs from the same task do not execute in parallel, ... *)
(*Hypothesis H_no_intra_task_parallelism:
jobs_of_same_task_dont_execute_in_parallel job_task sched.*)
(* ... and jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
(* Assume that the schedule satisfies the sporadic task model ...*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* and task precedence constraints. *)
(*Hypothesis H_task_precedence:
task_precedence_constraints job_cost job_task sched.*)
(* Consider a valid task tsk, ...*)
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
(*... whose job j ... *)
Variable j: JobIn arr_seq.
Variable H_job_of_tsk: job_task j = tsk.
(*... is backlogged at time t. *)
Variable t: time.
Hypothesis H_j_backlogged: backlogged job_cost sched j t.
(* Assume that any previous jobs of tsk have completed by time t. *)
Hypothesis H_all_previous_jobs_completed :
forall (j_other: JobIn arr_seq),
job_arrival j_other < job_arrival j >
completed job_cost sched j_other (job_arrival j_other + task_period (job_task j_other)).
(* If a job isn't scheduled, the processor are busy with interfering tasks. *)
Lemma cpus_busy_with_interfering_tasks :
count
(fun j : sporadic_task =>
is_interfering_task_jlfp tsk j &&
task_is_scheduled job_task sched j t)
ts = num_cpus.
Proof.
rename H_all_jobs_from_taskset into FROMTS,
H_no_parallelism into SEQUENTIAL,
(*H_no_intra_task_parallelism into NOINTRA,*)
H_global_scheduling_invariant into INV,
H_j_backlogged into BACK,
H_job_of_tsk into JOBtsk,
(*H_task_precedence into PREC,*)
H_valid_job_parameters into JOBPARAMS,
H_sporadic_tasks into SPO,
H_valid_task into TASKPARAMS,
H_all_previous_jobs_completed into PREV,
H_completed_jobs_dont_execute into COMP,
H_jobs_must_arrive_to_execute into ARRIVE.
unfold JLFP_JLDP_scheduling_invariant_holds,
valid_sporadic_job, valid_realtime_job,
task_precedence_constraints, completed_jobs_dont_execute,
sporadic_task_model, is_valid_sporadic_task,
jobs_of_same_task_dont_execute_in_parallel,
jobs_dont_execute_in_parallel in *.
apply/eqP; rewrite eqn_leq; apply/andP; split.
{
apply leq_trans with (n := count (fun x => task_is_scheduled job_task sched x t) ts);
first by apply sub_count; first by red; move => x /andP [_ SCHED].
unfold task_is_scheduled.
apply count_exists; first by done.
{
intros cpu x1 x2 SCHED1 SCHED2.
unfold schedules_job_of_tsk in *.
destruct (sched cpu t); last by done.
move: SCHED1 SCHED2 => /eqP SCHED1 /eqP SCHED2.
by rewrite SCHED1 SCHED2.
}
}
{
apply leq_trans with (n := count ((higher_eq_priority t)^~ j) (jobs_scheduled_at sched t));
first by rewrite > INV with (j := j) (t := t);
[by apply leqnn  by done].
apply leq_trans with (n := count (fun j: JobIn arr_seq => is_interfering_task_jlfp tsk (job_task j) && task_is_scheduled job_task sched (job_task j) t) (jobs_scheduled_at sched t)).
{
assert (SUBST: count ((higher_eq_priority t)^~ j) (jobs_scheduled_at sched t) = count (fun x => (higher_eq_priority t x j) && (x \in jobs_scheduled_at sched t)) (jobs_scheduled_at sched t)).
{
by apply eq_in_count; red; intros x IN; rewrite IN andbT.
} rewrite SUBST; clear SUBST.
apply sub_count; red; move => j_hp /andP [HP IN].
rewrite mem_scheduled_jobs_eq_scheduled in IN.
rename IN into SCHED.
apply/andP; split; last first.
{
move: SCHED => /exists_inP SCHED.
destruct SCHED as [cpu INcpu SCHED].
move: SCHED => /eqP SCHED.
apply/exists_inP; exists cpu; first by done.
by unfold schedules_job_of_tsk; rewrite SCHED.
}
{
unfold is_interfering_task_jlfp.
destruct (j == j_hp) eqn:EQjob.
{
move: EQjob => /eqP EQjob; subst.
unfold backlogged in *.
by rewrite SCHED andbF in BACK.
}
apply negbT in EQjob; move: EQjob => /eqP DIFF.
apply/negP; unfold not; move => /eqP SAMEtsk.
assert (INTERF: job_interference job_cost sched j j_hp t t.+1 != 0).
{
move: BACK => /andP [PENDING NOTSCHED].
unfold job_interference; rewrite lt0n.
rewrite big_nat_recr // /=.
by unfold backlogged; rewrite PENDING NOTSCHED SCHED 2!andbT addn1.
}
apply interference_under_edf_implies_shorter_deadlines
with (job_deadline0 := job_deadline) in INTERF; last by done.
have PARAMS := (JOBPARAMS j); have PARAMS' := (JOBPARAMS j_hp); des.
rewrite PARAMS1 PARAMS'1 JOBtsk SAMEtsk leq_add2r in INTERF.
exploit (SPO j_hp j);
[ by red; ins; subst  by rewrite JOBtsk SAMEtsk  by done ].
intros LEarr.
assert (LTarr: job_arrival j_hp < job_arrival j).
{
eapply leq_trans with (n := job_arrival j_hp + task_period (job_task j_hp));
last by done.
by rewrite addn1 leq_add2l SAMEtsk.
}
specialize (PREV j_hp LTarr).
apply completion_monotonic with (t' := t) in PREV;
try (by done); last first.
{
move: BACK => /andP [/andP [ARRIVED NOTCOMP] NOTSCHED].
by apply leq_trans with (n := job_arrival j);
[by apply LEarr  by apply ARRIVED].
}
apply completed_implies_not_scheduled in PREV; try (by done).
by rewrite SCHED in PREV.
}
}
have MAP := count_map (fun (x: JobIn arr_seq) => job_task x) (fun x => is_interfering_task_jlfp tsk x && task_is_scheduled job_task sched x t).
rewrite MAP; clear MAP.
apply count_sub_uniqr.
{
rewrite map_inj_in_uniq; first by apply scheduled_jobs_uniq.
red; intros j1 j2 SCHED1 SCHED2 SAMEtsk.
rewrite mem_scheduled_jobs_eq_scheduled in SCHED1.
rewrite mem_scheduled_jobs_eq_scheduled in SCHED2.
move: (SCHED1) (SCHED2) => PENDING1 PENDING2.
apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING1.
apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING2.
move: BACK => /andP [PENDING NOTSCHED].
assert (INTERF1: job_interference job_cost sched j j1 t t.+1 != 0).
{
unfold job_interference; rewrite lt0n.
rewrite big_nat_recr // /=.
by unfold backlogged; rewrite PENDING NOTSCHED SCHED1 2!andbT addn1.
}
assert (INTERF2: job_interference job_cost sched j j2 t t.+1 != 0).
{
unfold job_interference; rewrite lt0n.
rewrite big_nat_recr // /=.
by unfold backlogged; rewrite PENDING NOTSCHED SCHED2 2!andbT addn1.
}
apply interference_under_edf_implies_shorter_deadlines with (job_deadline0 := job_deadline) in INTERF1.
apply interference_under_edf_implies_shorter_deadlines with (job_deadline0 := job_deadline) in INTERF2.
destruct (job_arrival j1 < job_arrival j2) eqn:LEarr.
{
assert (DIFF: j1 <> j2). admit.
specialize (SPO j1 j2 DIFF SAMEtsk).
specialize (PREV j2).
Print task_precedence_constraints.
(*by red; ins; apply NOINTRA with (t := t);
rewrite // mem_scheduled_jobs_eq_scheduled.*)
}
{
red; intros x IN.
move: IN => /mapP IN; destruct IN as [j' _ EQx].
by rewrite EQx; apply FROMTS.
}
}
Qed.
End JobInvariantAsTaskInvariant.*)
End
Lemmas
.
End
PlatformEDF
.
\ No newline at end of file
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