Commit 62b892e7 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Fix makefile

parent 5314c6ad
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile apa.v BertognaResponseTimeDefsEDF.v BertognaResponseTimeDefsJitter.v BertognaResponseTimeDefs.v BertognaResponseTimeFPJitter.v BertognaResponseTimeFP.v divround.v eqtask_dec.v eqtaskjitter_dec.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefsJitter.v WorkloadDefs.v
# coq_makefile BertognaResponseTimeDefsEDF.v BertognaResponseTimeDefsJitter.v BertognaResponseTimeDefs.v BertognaResponseTimeEDFComp.v BertognaResponseTimeFPJitter.v BertognaResponseTimeFP.v divround.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefsJitter.v WorkloadDefs.v
#
.DEFAULT_GOAL := all
......@@ -83,6 +83,7 @@ endif
VFILES:=BertognaResponseTimeDefsEDF.v\
BertognaResponseTimeDefsJitter.v\
BertognaResponseTimeDefs.v\
BertognaResponseTimeEDFComp.v\
BertognaResponseTimeFPJitter.v\
BertognaResponseTimeFP.v\
divround.v\
......
(*Require Import Classical Vbase task job schedule platform priority helper identmp.
(* All possible affinity relations *)
Definition affinity := job -> processor_id -> Prop.
Definition affinity_non_empty (alpha: affinity) (num_cpus: nat) (sched: schedule) :=
forall j arr (ARR: arrives_at sched j arr),
exists cpu, << MAX: cpu < num_cpus >> /\ << ALPHA: alpha j cpu >>.
(* APA multiprocessor platform *)
Definition apa_ident_mp (num_cpus: nat) (hp: sched_job_hp_relation) (mapped: job_mapping) (alpha: affinity) (sched: schedule) :=
(* The mapping has a finite number of cpus: [1, num_cpus) *)
<< apa_cpus_nonzero: num_cpus > 0 >> /\
<< apa_num_cpus: forall j cpu t, mapped j cpu t -> cpu < num_cpus >> /\
(* Job is scheduled iff it is mapped to a processor*)
<< apa_mapping: forall j t, scheduled sched j t <-> exists cpu, mapped j cpu t >> /\
(* Non-parallelism restrictions (mapping must be an injective function) *)
<< mp_mapping_fun: forall j cpu cpu' t, mapped j cpu t /\ mapped j cpu' t -> cpu = cpu' >> /\
<< mp_mapping_inj: forall j j' cpu t, mapped j cpu t /\ mapped j' cpu t -> j = j'>> /\
(* A job receives at most 1 unit of service *)
<< apa_max_service: forall j t, service_at sched j t <= 1 >> /\
(* If a job is scheduled, then its affinity should allow it. *)
<< apa_alpha: forall t j cpu, mapped j cpu t -> alpha j cpu >> /\
(* (Weak) APA scheduling invariant *)
<< apa_invariant: forall jlow t (ARRIVED: arrived sched jlow t),
backlogged sched jlow t <->
(exists (j0: job), earlier_job sched j0 jlow /\ pending sched j0 t) \/
(forall cpu (MAXcpu: cpu < num_cpus) (ALPHA: alpha jlow cpu),
exists jhigh, hp sched t jhigh jlow /\ mapped jhigh cpu t) >>.
(*
(* Proof that an APA multiprocessor with global affinities is the same as
an identical multiprocessor with equal number of cpus *)
Lemma exists_apa_platform_that_is_global :
forall num_cpus sched hp cpumap
(sMult: ident_mp num_cpus hp cpumap sched)
(hpInd: schedule_independent hp),
exists alpha: affinity,
forall sched' cpumap' j t
(s'APA: apa_ident_mp num_cpus hp cpumap' alpha sched')
(arrSame: arrives_at sched = arrives_at sched'),
service sched j t = service sched' j t.
Proof.
ins; exists (fun j cpu => True).
ins; des.
induction t.
(* Base case *)
(* Inductive Step *)
(* Definitions for APA affinity restoration -- IGNORE *)
(* Per-task affinities *)
Definition task_affinity (alpha: affinity) :=
forall (tsk: sporadic_task) (j1 j2: job),
job_task j1 = tsk /\ job_task j2 = tsk -> alpha j1 = alpha j2.
Definition restrict (tsk_i: sporadic_task) (ts: taskset) (alpha1 alpha2 alpha': affinity) := True.
(* Service invariant from APA paper *)
Lemma APA_service_invariant :
forall num_cpus sched hp cpumap ts alpha alpha' (tsk_i: sporadic_task) j t
(APA: apa_ident_mp num_cpus hp cpumap alpha sched) (INtsk_i: In tsk_i ts)
(ALPHAtsk: task_affinity alpha) (ALPHA'tsk: task_affinity alpha')
(*(RESTR: ...)*),
exists sched' cpumap',
<< APA': apa_ident_mp num_cpus hp cpumap' alpha' sched' >> /\
<< SERV: service sched j t >= service sched' j t >>.
Proof.
intros.
*)*)
\ No newline at end of file
(* Assume decidable equality for jobs, so that it can be
used in computations. *)
Require Import eqtype.
Parameter job_eq_dec: job -> job -> bool.
Axiom eqn_job : Equality.axiom job_eq_dec.
Canonical job_eqMixin := EqMixin eqn_job.
Canonical job_eqType := Eval hnf in EqType job job_eqMixin.
(*(* Define decidable equality for jobs, so that it can be
used in computations. *)
Definition job_eq_dec (x y: job) : {x = y} + {x <> y}.
destruct x, y;
destruct (eq_op job_id0 job_id1) eqn: Eid;
destruct (eq_op job_arrival0 job_arrival1) eqn:Earrival;
destruct (eq_op job_cost0 job_cost1) eqn:Ecost;
destruct (eq_op job_deadline0 job_deadline1) eqn:Edeadline;
move: Eid Earrival Ecost Edeadline => /eqP Eid /eqP Earrival /eqP Ecost /eqP Edeadline;
des; subst;
try (by left; ins);
try (by right; unfold not; intro EQ; inversion EQ; intuition).
Qed.
(* ssreflect decidable equality *)
Lemma eqn_job : Equality.axiom job_eq_dec.
Proof.
unfold Equality.axiom; ins; destruct (job_eq_dec x y);
[by apply ReflectT | by apply ReflectF].
Qed.
Canonical job_eqMixin := EqMixin eqn_job.
Canonical job_eqType := Eval hnf in EqType job job_eqMixin.
(* ---------------------------- *)*)
\ No newline at end of file
(* Assume decidable equality for tasks, so that it can be
used in computations. *)
Require Import eqtype.
Parameter task_eq_dec: sporadic_task -> sporadic_task -> bool.
Axiom eqn_task : Equality.axiom task_eq_dec.
Canonical task_eqMixin := EqMixin eqn_task.
Canonical task_eqType := Eval hnf in EqType sporadic_task task_eqMixin.
(*Definition task_eq_dec (x y: sporadic_task) : {x = y} + {x <> y}.
destruct x, y.
destruct (eq_op task_id0 task_id1) eqn:Eid;
destruct (eq_op task_cost0 task_cost1) eqn:Ecost;
destruct (eq_op task_period0 task_period1) eqn:Eperiod;
destruct (eq_op task_deadline0 task_deadline1) eqn:Edl;
move: Eid Ecost Eperiod Edl => /eqP Eid /eqP Ecost /eqP Eperiod /eqP Edl; subst;
try (by left; ins);
try (by right; unfold not; intro EQ; inversion EQ; intuition).
Qed.*)
\ No newline at end of file
(* Assume decidable equality for tasks, so that it can be
used in computations. *)
Require Import eqtype.
Parameter task_eq_dec: sporadic_task_with_jitter -> sporadic_task_with_jitter -> bool.
Axiom eqn_task : Equality.axiom task_eq_dec.
Canonical task_eqMixin := EqMixin eqn_task.
Canonical task_eqType := Eval hnf in EqType sporadic_task_with_jitter task_eqMixin.
(*Definition task_eq_dec (x y: sporadic_task) : {x = y} + {x <> y}.
destruct x, y.
destruct (eq_op task_id0 task_id1) eqn:Eid;
destruct (eq_op task_cost0 task_cost1) eqn:Ecost;
destruct (eq_op task_period0 task_period1) eqn:Eperiod;
destruct (eq_op task_deadline0 task_deadline1) eqn:Edl;
move: Eid Ecost Eperiod Edl => /eqP Eid /eqP Ecost /eqP Eperiod /eqP Edl; subst;
try (by left; ins);
try (by right; unfold not; intro EQ; inversion EQ; intuition).
Qed.*)
\ No newline at end of file
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