Commit 9e5687dd authored by Vedant Chavda's avatar Vedant Chavda

resolve threads

parent 3919cdd9
Pipeline #29007 passed with stages
in 16 minutes and 14 seconds
This diff is collapsed.
......@@ -23,11 +23,6 @@ Section JobIndexLemmas.
Hypothesis H_j2_from_arrival_sequence : arrives_in arr_seq j2.
Hypothesis H_same_task : job_task j1 = job_task j2.
(*(** For any job [j] with a positive [job_index] we define the notion
of a previous job. *)
Definition prev_job (j : Job) := nth j (task_arrivals_up_to_job_arrival arr_seq j)
(index j (task_arrivals_up_to_job_arrival arr_seq j) - 1).*)
(** In the next section, we prove some basic properties about jobs with equal indices. *)
Section EqualJobIndex.
......
......@@ -224,44 +224,44 @@ Section PeriodicModel.
(** The sequence [task_arrivals_up_to_job_arrival arr_seq j] can be written as a concatenation
of [task_arrivals_up_to_job_arrival arr_seq (prev_job j)] and [::j]. *)
Lemma prev_job_cat :
job_index arr_seq j1 > 0 ->
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [::j1] = task_arrivals_up_to_job_arrival arr_seq j1.
job_index arr_seq j1 > 0 ->
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [::j1] = task_arrivals_up_to_job_arrival arr_seq j1.
Proof.
intros JIND.
have A1 : index (prev_job arr_seq j1) (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) =
(job_index arr_seq j1 - 1); first by apply prev_job_index => //.
set (n := job_index arr_seq j1 - 1).
unfold task_arrivals_up_to_job_arrival.
pose proof prev_job_task as TSK. specialize (TSK arr_seq H_consistent_arrivals H_uniq_arr_seq j1). feed_n 2 TSK => //.
have A2 : job_arrival (prev_job arr_seq j1) < job_arrival j1; first by apply prev_job_arr_lt => //.
have A3 : forall tsk t_m t,
t_m <= t ->
task_arrivals_up_to arr_seq tsk t =
task_arrivals_up_to arr_seq tsk t_m ++ task_arrivals_between arr_seq tsk t_m.+1 t.+1.
{ intros tsk0 t_m t LT.
rewrite /task_arrivals_up_to /task_arrivals_between /arrivals_between.
now rewrite -filter_cat -arrivals_between_cat.
}
rewrite [in X in _ = X](A3 _ (job_arrival (prev_job arr_seq j1))); last by apply ltnW.
apply /eqP. rewrite eqseq_cat; last by rewrite TSK.
apply/andP. split; first by rewrite TSK.
have -> : task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1 (job_arrival j1).+1
= task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1 (job_arrival j1)
++ task_arrivals_at_job_arrival arr_seq j1.
{ assert (task_arrivals_at arr_seq (job_task j1) (job_arrival j1) =
task_arrivals_between arr_seq (job_task j1) (job_arrival j1) ((job_arrival j1).+1)) as ARR_AT.
{ rewrite /task_arrivals_at /task_arrivals_between /arrivals_between big_nat1.
now auto.
}
rewrite /task_arrivals_at_job_arrival.
now rewrite ARR_AT /task_arrivals_between -filter_cat -arrivals_between_cat.
}
rewrite only_j_in_task_arrivals_at_j //.
have -> : task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1
(job_arrival j1) = [::]; first by apply no_jobs_between_consecutive_jobs => //.
now easy.
(job_index arr_seq j1 - 1); first by apply prev_job_index => //.
set (n := job_index arr_seq j1 - 1).
unfold task_arrivals_up_to_job_arrival.
pose proof prev_job_task as TSK. specialize (TSK arr_seq H_consistent_arrivals H_uniq_arr_seq j1). feed_n 2 TSK => //.
have A2 : job_arrival (prev_job arr_seq j1) < job_arrival j1; first by apply prev_job_arr_lt => //.
have A3 : forall tsk t_m t,
t_m <= t ->
task_arrivals_up_to arr_seq tsk t =
task_arrivals_up_to arr_seq tsk t_m ++ task_arrivals_between arr_seq tsk t_m.+1 t.+1.
{ intros tsk0 t_m t LT.
rewrite /task_arrivals_up_to /task_arrivals_between /arrivals_between.
now rewrite -filter_cat -arrivals_between_cat.
}
rewrite [in X in _ = X](A3 _ (job_arrival (prev_job arr_seq j1))); last by apply ltnW.
apply /eqP. rewrite eqseq_cat; last by rewrite TSK.
apply/andP. split; first by rewrite TSK.
have -> : task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1 (job_arrival j1).+1
= task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1 (job_arrival j1)
++ task_arrivals_at_job_arrival arr_seq j1.
{ assert (task_arrivals_at arr_seq (job_task j1) (job_arrival j1) =
task_arrivals_between arr_seq (job_task j1) (job_arrival j1) ((job_arrival j1).+1)) as ARR_AT.
{ rewrite /task_arrivals_at /task_arrivals_between /arrivals_between big_nat1.
now auto.
}
rewrite /task_arrivals_at_job_arrival.
now rewrite ARR_AT /task_arrivals_between -filter_cat -arrivals_between_cat.
}
rewrite only_j_in_task_arrivals_at_j //.
have -> : task_arrivals_between arr_seq (job_task j1) (job_arrival (prev_job arr_seq j1)).+1
(job_arrival j1) = [::]; first by apply no_jobs_between_consecutive_jobs => //.
now easy.
Qed.
(** We show that for any job [j] the job index of [prev_job j] is one less
than the job index of [j]. *)
Lemma prev_job_index_j :
......@@ -311,11 +311,8 @@ Section PeriodicModel.
case: (boolP (j' == j)) => [/eqP EQ|NEQ]; first by rewrite -EQ TSK => //.
rewrite -ARRIVAL.
assert (job_index arr_seq j' = 0 \/ job_index arr_seq j' > 0) as Z_OR_NZ.
{ assert (forall n, n = 0 \/ n > 0) as z_or_s.
{ destruct n; first by auto.
by auto.
}
now apply z_or_s.
{ destruct (job_index arr_seq j'); first by auto.
now right; auto.
}
destruct Z_OR_NZ as [Z | NZ].
+ move : NEQ => /eqP. intro NEQ.
......
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.model.task.arrival.task_max_inter_arrival.
Require Export prosa.model.task.arrivals.
Require Export prosa.util.all.
Require Export prosa.model.task.offset.
Require Export prosa.util.all.
Require Export prosa.analysis.facts.job_index.
(** * The Periodic Task Model *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment