Commit 634bf9a3 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Latest changes

parent 195c9c41
MODULES := task job priority schedule platform identmp apa helper \
response_time task_arrival liulayland
VS := $(MODULES:%=%.v)
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
#############################################################################
.PHONY: coq clean
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
coq: Makefile.coq
$(MAKE) -f Makefile.coq
#
# This Makefile was generated by the command line :
# coq_makefile ExtraRelations.v Vbase.v apa.v extralib.v helper.v identmp.v job.v liulayland.v platform.v priority.v response_time.v schedule.v task.v task_arrival.v
#
Makefile.coq: Makefile $(VS)
coq_makefile -R . Sched $(VS) -o Makefile.coq
.DEFAULT_GOAL := all
#
# This Makefile may take arguments passed as environment variables:
# COQBIN to specify the directory where Coq binaries resides;
# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
# DSTROOT to specify a prefix to install path.
# Here is a hack to make $(eval $(shell works:
define donewline
endef
includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
$(call includecmdwithout@,$(COQBIN)coqtop -config)
##########################
# #
# Libraries definitions. #
# #
##########################
COQLIBS?=-I .
COQDOCLIBS?=
##########################
# #
# Variables definitions. #
# #
##########################
OPT?=
COQDEP?=$(COQBIN)coqdep -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
COQC?=$(COQBIN)coqc
GALLINA?=$(COQBIN)gallina
COQDOC?=$(COQBIN)coqdoc
COQCHK?=$(COQBIN)coqchk
##################
# #
# Install Paths. #
# #
##################
ifdef USERINSTALL
XDG_DATA_HOME?=$(HOME)/.local/share
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
COQLIBINSTALL=${COQLIB}user-contrib
COQDOCINSTALL=${DOCDIR}user-contrib
endif
######################
# #
# Files dispatching. #
# #
######################
VFILES:=ExtraRelations.v\
Vbase.v\
apa.v\
extralib.v\
helper.v\
identmp.v\
job.v\
liulayland.v\
platform.v\
priority.v\
response_time.v\
schedule.v\
task.v\
task_arrival.v
-include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES))
VOFILES:=$(VFILES:.v=.vo)
VOFILESINC=$(filter $(wildcard ./*),$(VOFILES))
GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)
ifeq '$(HASNATDYNLINK)' 'true'
HASNATDYNLINK_OR_EMPTY := yes
else
HASNATDYNLINK_OR_EMPTY :=
endif
#######################################
# #
# Definition of the toplevel targets. #
# #
#######################################
all: $(VOFILES)
spec: $(VIFILES)
gallina: $(GFILES)
html: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
gallinahtml: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
all.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
validate: $(VOFILES)
$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
beautify: $(VFILES:=.beautified)
for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
@echo 'Do not do "make clean" until you are sure that everything went well!'
@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
.PHONY: all opt byte archclean clean install userinstall depend html validate
####################
# #
# Special targets. #
# #
####################
byte:
$(MAKE) all "OPT:=-byte"
opt:
$(MAKE) all "OPT:=-opt"
userinstall:
+$(MAKE) USERINSTALL=true install
install:
install -d $(DSTROOT)$(COQLIBINSTALL)/$(INSTALLDEFAULTROOT); \
for i in $(VOFILESINC); do \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/$(INSTALLDEFAULTROOT)/`basename $$i`; \
done
install-doc:
install -d $(DSTROOT)$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/html
for i in html/*; do \
install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/$$i;\
done
clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- rm -rf html mlihtml
archclean:
rm -f *.cmx *.o
printenv:
@$(COQBIN)coqtop -config
@echo CAMLC = $(CAMLC)
@echo CAMLOPTC = $(CAMLOPTC)
@echo PP = $(PP)
@echo COQFLAGS = $(COQFLAGS)
@echo COQLIBINSTALL = $(COQLIBINSTALL)
@echo COQDOCINSTALL = $(COQDOCINSTALL)
###################
# #
# Implicit rules. #
# #
###################
%.vo %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
%.vi: %.v
$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
%.g: %.v
$(GALLINA) $<
%.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
%.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
%.g.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
%.g.html: %.v %.glob
$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@
%.v.d: %.v
$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
%.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
clean:: Makefile.coq
$(MAKE) -f Makefile.coq clean
rm -f Makefile.coq
Require Import Coq.Lists.List.
Require Export ListSet.
Require Export Arith.
Require Import Coq.Arith.Peano_dec.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import task.
Require Import job.
Require Import schedule.
Require Import platform.
Require Import priority.
Require Import helper.
Require Import identmp.
Require Import List Classical ListSet Arith Vbase task job schedule platform priority helper identmp.
(* Set of all possible affinities (mappings from jobs to processors) *)
Definition affinity := job -> set nat.
Definition affinity_non_empty := forall (alpha: affinity) (j: job), ~alpha j = empty_set nat.
Definition affinity_non_empty := forall (alpha: affinity) j, ~alpha j = empty_set nat.
(* Whether a schedule is produced by an APA identical multiprocessor *)
Record apa_ident_mp (num_cpus: nat) (hp: higher_priority)
(cpumap: processor_list) (alpha: affinity) (sched: schedule) : Prop :=
{
(* An identical multiprocessor has a fixed number of cpus *)
apa_ident_mp_cpus_nonzero: num_cpus > 0;
apa_ident_mp_num_cpus: forall (t: time), length (cpumap sched t) = num_cpus;
(* Job is scheduled iff it is mapped to a processor*)
apa_ident_mp_mapping: forall (j: job) (t: time),
List.In (Some j) (cpumap sched t)
<-> scheduled sched j t;
(* A job receives at most 1 unit of service *)
apa_ident_mp_sched_unit: forall (j: job) (t: time), service_at sched j t <= 1;
(* If a job is scheduled, then its affinity should allow it. *)
apa_ident_mp_restricted_affinities:
forall (t: time) (j: job) (cpu: nat),
(nth cpu (cpumap sched t) (None) = Some j) -> List.In cpu (alpha j);
(* (Weak) APA scheduling invariant *)
apa_ident_mp_invariant:
forall (jlow: job) (t: time),
backlogged sched jlow t <->
(forall (cpu: nat),
cpu < num_cpus ->
List.In cpu (alpha jlow) ->
(exists (jhigh: job),
hp sched t jhigh jlow
/\ (nth cpu (cpumap sched t) (None) = Some jhigh)))
}.
Definition apa_ident_mp (num_cpus: nat) (hp: higher_priority) (cpumap: processor_list)
(alpha: affinity) (sched: schedule) :=
(* An identical multiprocessor has a fixed number of cpus *)
<< apa_cpus_nonzero: num_cpus > 0 >> /\
<< apa_num_cpus: forall t, length (cpumap sched t) = num_cpus >> /\
(* Job is scheduled iff it is mapped to a processor*)
<< apa_mapping: forall j t, List.In (Some j) (cpumap sched t) <-> scheduled sched j t >> /\
(* 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,
(nth cpu (cpumap sched t) (None) = Some j) -> List.In cpu (alpha j) >> /\
(* (Weak) APA scheduling invariant *)
<< apa_invariant:
forall jlow t,
backlogged sched jlow t <->
(forall cpu, cpu < num_cpus ->
List.In cpu (alpha jlow) ->
(exists (jhigh: job), hp sched t jhigh jlow
/\ (nth cpu (cpumap sched t) (None) = Some jhigh))) >>.
(* 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: nat) (sched: schedule) (hp: higher_priority) (cpumap: processor_list),
ident_mp num_cpus hp cpumap sched ->
schedule_independent hp ->
exists (alpha: affinity),
forall (sched': schedule) (cpumap': processor_list),
apa_ident_mp num_cpus hp cpumap' alpha sched' ->
arrives_at sched = arrives_at sched' ->
(forall (j: job) (t: time), service sched j t = service sched' j t).
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.
intros num_cpus sched hp cpumap sched_is_identmp sched_ind.
inversion_clear sched_is_identmp as [num_cpus_positive _ _ _ invariant_sched].
exists (fun (j : job) => (seq 0 num_cpus)).
intros sched' cpumap' sched'_is_apa same_arr j t.
inversion_clear sched'_is_apa as [num_cpus_sched' _ _ _ _ invariant_sched'].
specialize (invariant_sched j t).
specialize (invariant_sched' j t).
induction t.
intros.
simpl.
destruct (excluded_middle (backlogged sched j 0)) as [j_backlogged_sched | j_not_backlogged_sched].
destruct (excluded_middle (backlogged sched' j 0)) as [j_backlogged_sched' | j_not_backlogged_sched'].
- rewrite 2 backlogged_no_service; trivial.
- rewrite 2 backlogged_no_service; trivial.
apply invariant_sched'. intros cpu cpu_less in_cpu.
inversion_clear invariant_sched as [invariant_sched_suf _].
specialize (invariant_sched_suf j_backlogged_sched).
ins. exists (fun j => (seq 0 num_cpus)).
unfold apa_ident_mp; ins; des.
induction t.
Admitted.
assert (bla : forall cpu0 : nat,
cpu0 < num_cpus ->
exists jhigh : job,
hp sched' 0 jhigh j /\
exists cpu', cpu' < num_cpus /\ nth cpu' (cpumap sched' 0) None = Some jhigh).
Admitted.
(* Definitions for APA affinity restoration *)
......@@ -98,27 +58,21 @@ Definition task_affinity (alpha: affinity) :=
Definition inter : set nat -> set nat -> set nat := set_inter eq_nat_dec.
Definition restrict (tsk_i: sporadic_task) (ts: taskset)
(alpha: affinity) (alpha': affinity) : Prop :=
task_affinity alpha
/\ task_affinity alpha'
/\ (forall (tsk: sporadic_task) (j: job) (j_i: job),
In tsk ts /\ In tsk_i ts
/\ job_of j = Some tsk /\ job_of j_i = Some tsk_i
-> alpha' j = inter (alpha j) (alpha j_i)).
Definition restrict (tsk_i: sporadic_task) (ts: taskset) (alpha: affinity) (alpha': affinity) :=
<< ALPHA: task_affinity alpha >> /\
<< ALPHA': task_affinity alpha' >> /\
forall tsk j j_i (INtsk: In tsk ts) (INtsk_i: In tsk_i ts) (JOBj: job_of j = Some tsk)
(JOBj_i: job_of j_i = Some tsk_i), alpha' j = inter (alpha j) (alpha j_i).
(* Service invariant from APA paper *)
Lemma APA_service_invariant :
forall (num_cpus: nat) (sched: schedule) (hp: higher_priority) (cpumap: processor_list)
(ts: taskset) (alpha: affinity) (alpha': affinity) (tsk_i: sporadic_task)
(j: job) (t: time),
apa_ident_mp num_cpus hp cpumap alpha sched
/\ In tsk_i ts
/\ task_affinity alpha /\ task_affinity alpha'
/\ restrict tsk_i ts alpha alpha'
-> exists (sched': schedule) (cpumap': processor_list),
(apa_ident_mp num_cpus hp cpumap' alpha' sched'
/\ service sched j t >= service sched' j t).
forall num_cpus sched hp cpumap ts alpha alpha' tsk_i 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: restrict tsk_i ts alpha alpha'),
exists sched' cpumap',
<< APA': apa_ident_mp num_cpus hp cpumap' alpha' sched' >> /\
<< SERV: service sched j t >= service sched' j t >>.
Proof.
intros.
Admitted.
\ No newline at end of file
Require Import Coq.Lists.List.
Require Import Coq.Arith.Lt.
Require Import Omega.
Require Import List Arith Vbase.
Lemma nat_seq_nth_In : forall len n, n < len -> In n (seq 0 len).
Proof. intros.
assert (H1 := seq_nth).
assert (H2 := H1 len 0 n len).
assert (H3 := H).
apply H2 in H. simpl in H.
assert (nth_In := nth_In).
assert (H4 := nth_In nat n (seq 0 len) len).
assert (H5 := seq_length len 0).
rewrite -> H5 in H4.
apply H4 in H3.
rewrite H in H3.
trivial.
Lemma nat_seq_nth_In : forall n len (LT: n < len), In n (seq 0 len).
Proof.
ins.
assert (NTH := seq_nth).
generalize LT; apply NTH with (start := 0) (d := len) in LT; simpl in LT; ins.
assert (NTHIn := nth_In).
specialize (NTHIn nat n (seq 0 len) len).
rewrite (seq_length len 0), LT in NTHIn.
eauto.
Qed.
Lemma In_singleton_list :
forall (A: Type) (x: A) l n, In (Some x) l -> n < 1 -> length l = 1 -> nth n l None = Some x.
forall (A: Type) (x: A) l n, In (Some x) l -> n < 1 -> length l = 1 -> nth n l None = Some x.
Proof.
intros.
destruct n; [|inversion H0; inversion H3].
destruct l; [inversion H1|].
destruct l; [|inversion H1].
destruct H; [|contradiction].
auto.
intros.
destruct n; [|inversion H0; inversion H3].
destruct l; [inversion H1|].
destruct l; [|inversion H1].
destruct H; [|contradiction].
auto.
Qed.
Lemma element_in_list : forall (A: Type) (x: A) (l: list (option A)) (n: nat),
......@@ -41,7 +35,7 @@ Lemma element_in_list_no_overflow :
forall (A: Type) (x: A) (l: list (option A)) (n: nat),
nth n l None = Some x -> n < length l.
Proof.
Admitted.
Admitted.
Definition least_nat (n: nat) (P: nat -> Prop) : Prop :=
P n /\ forall (n': nat), P n' -> n <= n'.
......@@ -49,9 +43,5 @@ Definition least_nat (n: nat) (P: nat -> Prop) : Prop :=
Definition greatest_nat (n: nat) (P: nat -> Prop) : Prop :=
P n /\ forall (n': nat), P n' -> n' <= n.
Axiom excluded_middle : forall P: Prop, P \/ ~P.
Theorem contrapositive : forall P Q : Prop, (P -> Q) -> (~Q -> ~P).
Proof. tauto. Qed.
Lemma not_gt_le : forall n m : nat, ~ n > m -> n <= m. intros; omega. Qed.
\ No newline at end of file
Lemma not_gt_le : forall n m : nat, ~ n > m -> n <= m.
Proof. by ins; omega. Qed.
\ No newline at end of file
Require Import Coq.Lists.List.
Require Import job.
Require Import schedule.
Require Import priority.
Require Import platform.
Require Import Vbase List job schedule priority platform.
(* Mapping from processors to tasks at time t *)
Definition processor_list := schedule -> time -> list (option job).
(* Whether a schedule is produced by an identical multiprocessor *)
Record ident_mp (num_cpus: nat) (hp: higher_priority)
(cpumap: processor_list) (sched: schedule) : Prop :=
{ (* An identical multiprocessor has a fixed number of cpus *)
ident_mp_cpus_nonzero: num_cpus > 0;
ident_mp_num_cpus: forall (t: time), length (cpumap sched t) = num_cpus;
Definition ident_mp (num_cpus: nat) (hp: higher_priority) (cpumap: processor_list) (sched: schedule) :=
(* Job is scheduled iff it is mapped to a processor*)
ident_mp_mapping: forall (j: job) (t: time),
List.In (Some j) (cpumap sched t)
<-> scheduled sched j t;
(* An identical multiprocessor has a fixed number of cpus *)
<< mp_cpus_nonzero: num_cpus > 0 >> /\
<< mp_num_cpus: forall t, length (cpumap sched t) = num_cpus >> /\
(* A job receives at most 1 unit of service *)
ident_mp_sched_unit: forall (j: job) (t: time), service_at sched j t <= 1;
(* Job is scheduled iff it is mapped to a processor*)
<< mp_mapping: forall j t, List.In (Some j) (cpumap sched t) <-> scheduled sched j t >> /\
(* Global scheduling invariant *)
ident_mp_invariant:
forall (jlow: job) (t: time),
backlogged sched jlow t <->
(forall (cpu: nat),
cpu < num_cpus ->
(exists (jhigh: job),
hp sched t jhigh jlow
/\ (nth cpu (cpumap sched t) None = Some jhigh)))
}.
(* A job receives at most 1 unit of service *)
<< mp_max_service: forall j t, service_at sched j t <= 1 >> /\
Lemma highest_prio_no_interference :
forall (tsk_i: sporadic_task),
(forall (sched' : schedule) (task_hp: sporadic_task->sporadic_task->Prop),
ident_mp num_cpus sched' ->
ts_arrival_sequence (tsk_i :: ts) sched' ->
fixed_priority hp task_hp ->
Forall (task_hp tsk_i) ts ) ->
task_response_time_max uniprocessor tsk_i (tsk_i :: ts) (task_cost tsk_i).
Proof.
intros tsk_i H.
unfold task_response_time_max. split.
- unfold task_response_time_ub. split. simpl. apply or_introl. trivial.
intros j t_a r plat arr_seq_of_j job_of_j arr_j resp_time_j.
unfold job_response_time in resp_time_j.
specialize (resp_time_j t_a arr_j).
unfold least_nat in resp_time_j.
inversion resp_time_j as [completed_j first_time_completed_j].
apply first_time_completed_j.
unfold completed.
split.
+ assert (tsk_i_cost_positive := task_cost_positive tsk_i).
destruct (task_cost tsk_i). inversion tsk_i_cost_positive.
rewrite <- plus_n_Sm. apply gt_Sn_O.
+ (* Prove that tsk_i has service = e_i, by induction on t *)
assert (always_scheduled : forall t, service sched j (t_a + t) = t + 1).
induction t.
* rewrite <- plus_n_O. simpl.
destruct t_a as [a | t_0]. simpl.
admit.
simpl.
rewrite (not_arrived_no_service sched j (S t_0) arr_j t_0).
simpl.
inversion S_t_0_less.
assert (H2 := le_Sn_n t_0).
assert (H3 := le_refl t_0).
omega. inversion H0.
unfold service.
destruct (t < t_a).
induction (t_a + task_cost tsk_i - 1).
Admitted.(*
Lemma highest_prio_no_interference :
forall (ts: taskset)(tsk_i: sporadic_task),
(forall (sched : schedule) (task_hp: sporadic_task->sporadic_task->Prop),
platform sched ->
ts_arrival_sequence (tsk_i :: ts) sched ->
fixed_priority hp task_hp ->
Forall (task_hp tsk_i) ts ) ->
task_response_time_max tsk_i (tsk_i :: ts) (task_cost tsk_i).
Proof.
*)
\ No newline at end of file
(* Global scheduling invariant *)
<< mp_invariant:
forall jlow t,
backlogged sched jlow t <->
(forall cpu, cpu < num_cpus ->
(exists (jhigh: job), hp sched t jhigh jlow
/\ (nth cpu (cpumap sched t) None = Some jhigh))) >>.
\ No newline at end of file
Require Import task.
Require Import Vbase task.
Section Job.
Record job_data : Type :=
{
job_id: nat; (* job_id allows multiple jobs with same parameters *)
job_cost: nat;
job_deadline: nat; (* relative deadline *)
job_of: option sporadic_task (* Whether a job is spawned by a particular task *)
}.
(* A job represents a single execution unit. *)
Record job : Type :=
{ jd:> job_data;
{
job_id: nat; (* job_id allows multiple jobs with same parameters *)
job_cost: nat;
job_deadline: nat; (* relative deadline *)
job_of: option sporadic_task; (* Whether a job is spawned by a particular task *)
(* Properties of a job *)
job_cost_positive: job_cost jd > 0;
job_cost_le_deadline: job_cost jd <= job_deadline jd;
job_deadline_positive: job_deadline jd > 0;
job_task_parameters : forall (tsk: sporadic_task),
job_of jd = Some tsk ->
(job_cost jd <= task_cost tsk
/\ job_deadline jd = task_deadline tsk)
}.
job_properties:
<< job_cost_positive: job_cost > 0 >> /\
<< job_cost_le_deadline: job_cost <= job_deadline >> /\
<< job_dl_positive: job_deadline > 0 >> /\
<< job_params: forall tsk (jTsk: job_of = Some tsk),
(job_cost <= task_cost tsk /\
job_deadline = task_deadline tsk)>>
}.
End Job.
Require Import Coq.Lists.List.
Require Import Coq.Arith.Lt.
Require Import job.
Require Import task.
Require Import schedule.
Require Import identmp.
Require Import priority.
Require Import helper.
Require Import response_time.