Commit 9f1add6d authored by Maxime Lesourd's avatar Maxime Lesourd

separate partitioned facts

parent 95b74067
Pipeline #32357 failed with stages
in 8 minutes and 40 seconds
From prosa Require Export model.schedule.partitioned.
Section Theory.
(** Consider any type of jobs... *)
Context {Job: JobType}.
(** ... and any kind of processor model. *)
Context {PState: Type}.
Context `{H : ProcessorState Job PState}.
(** Given an assignement of jobs to cores. *)
Context `{@JobCore Job PState H}. (* TODO : Should we have to refer explicitly to H here? *)
(** We define the projection of an arrival sequence on a core. *)
Variable arr_seq: arrival_sequence Job.
Lemma arrives_at_on : forall j t,
arrives_at arr_seq j t = arrives_at (arrival_sequence_on arr_seq (job_core j)) j t.
Proof.
move=> j t.
by rewrite /arrives_at/arrivals_at mem_filter eqxx.
Qed.
Lemma arrives_at_on_uniq : forall j r t,
arrives_at (arrival_sequence_on arr_seq r) j t ->
r = job_core j.
Proof.
move=> j r t.
by rewrite /arrives_at/arrivals_at mem_filter=>/andP[/eqP->].
Qed.
Lemma arrives_in_on : forall j,
arrives_in arr_seq j <-> arrives_in (arrival_sequence_on arr_seq (job_core j)) j.
Proof.
move=> j.
rewrite /arrives_in/arrivals_at/arrival_sequence_on.
split=>[[t]|[t Ht]]; exists t.
- by rewrite mem_filter eqxx.
- by rewrite mem_filter eqxx in Ht.
Qed.
Lemma arrives_in_on_uniq : forall j r,
arrives_in (arrival_sequence_on arr_seq r) j ->
r = job_core j.
Proof.
move=> j r.
rewrite /arrives_in/arrivals_at/arrival_sequence_on=>[[t]].
by rewrite mem_filter=>/andP[/eqP->].
Qed.
End Theory.
......@@ -72,55 +72,3 @@ Section Model.
Definition partitioned_model :=
forall r : Core, core_model r (arrival_sequence_on arr_seq r) (schedule_on sched r).
End Model.
(* TODO : move this out *)
Section Theory.
(** Consider any type of jobs... *)
Context {Job: JobType}.
(** ... and any kind of processor model. *)
Context {PState: Type}.
Context `{H : ProcessorState Job PState}.
(** Given an assignement of jobs to cores. *)
Context `{@JobCore Job PState H}. (* TODO : Should we have to refer explicitly to H here? *)
(** We define the projection of an arrival sequence on a core. *)
Variable arr_seq: arrival_sequence Job.
Lemma arrives_at_on : forall j t,
arrives_at arr_seq j t = arrives_at (arrival_sequence_on arr_seq (job_core j)) j t.
Proof.
move=> j t.
by rewrite /arrives_at/arrivals_at mem_filter eqxx.
Qed.
Lemma arrives_at_on_uniq : forall j r t,
arrives_at (arrival_sequence_on arr_seq r) j t ->
r = job_core j.
Proof.
move=> j r t.
by rewrite /arrives_at/arrivals_at mem_filter=>/andP[/eqP->].
Qed.
Lemma arrives_in_on : forall j,
arrives_in arr_seq j <-> arrives_in (arrival_sequence_on arr_seq (job_core j)) j.
Proof.
move=> j.
rewrite /arrives_in/arrivals_at/arrival_sequence_on.
split=>[[t]|[t Ht]]; exists t.
- by rewrite mem_filter eqxx.
- by rewrite mem_filter eqxx in Ht.
Qed.
Lemma arrives_in_on_uniq : forall j r,
arrives_in (arrival_sequence_on arr_seq r) j ->
r = job_core j.
Proof.
move=> j r.
rewrite /arrives_in/arrivals_at/arrival_sequence_on=>[[t]].
by rewrite mem_filter=>/andP[/eqP->].
Qed.
End Theory.
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