Commit 2fb2053c authored by Maxime Lesourd's avatar Maxime Lesourd Committed by Björn Brandenburg

port notions of job/task deadlines and schedulability to restructuring

parent 03863f8f
From rt.restructuring.behavior Require Export schedule facts.completion.
From rt.restructuring.model Require Export task.
From rt.util Require Export seqset.
Section Task.
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and any schedule of these jobs. *)
Variable sched: schedule PState.
(* Let tsk be any task that is to be analyzed. *)
Variable tsk: Task.
(* Then, we say that R is a response-time bound of tsk in this schedule ... *)
Variable R: duration.
(* ... iff any job j of tsk in this arrival sequence has
completed by (job_arrival j + R). *)
Definition task_response_time_bound :=
forall j,
arrives_in arr_seq j ->
job_task j = tsk ->
job_response_time_bound sched j R.
(* We say that a task is schedulable if all its jobs meet their deadline *)
Definition schedulable_task :=
forall j,
arrives_in arr_seq j ->
job_task j = tsk ->
job_meets_deadline sched j.
End Task.
Section TaskSet.
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Variable ts : {set Task}.
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and any schedule of these jobs. *)
Variable sched: schedule PState.
(* We say that a task set is schedulable if all its tasks are schedulable *)
Definition schedulable_taskset :=
forall tsk, tsk \in ts -> schedulable_task arr_seq sched tsk.
End TaskSet.
Section Schedulability.
(* We can infer schedulability from a response-time bound of a task. *)
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{TaskDeadline Task}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and any schedule of these jobs. *)
Variable sched: schedule PState.
(* Assume that jobs don't execute after completion. *)
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* Let tsk be any task that is to be analyzed. *)
Variable tsk: Task.
(* Given a response-time bound of tsk in this schedule no larger than its deadline, ... *)
Variable R: duration.
Hypothesis H_R_le_deadline: R <= task_deadline tsk.
Hypothesis H_response_time_bounded: task_response_time_bound arr_seq sched tsk R.
(* ...then tsk is schedulable. *)
Lemma schedulability_from_response_time_bound:
schedulable_task arr_seq sched tsk.
Proof.
intros j ARRj JOBtsk.
rewrite /job_meets_deadline.
apply completion_monotonic with (t := job_arrival j + R);
[ | by apply H_response_time_bounded].
rewrite /job_deadline leq_add2l JOBtsk.
by rewrite (leq_trans H_R_le_deadline).
Qed.
End Schedulability.
......@@ -7,8 +7,11 @@ Definition JobType := eqType.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
Class JobCost (J : JobType) := job_cost : J -> nat.
Class JobCost (J : JobType) := job_cost : J -> duration.
(* Definition of a generic type of parameter for job_arrival *)
Class JobArrival (J : JobType) := job_arrival : J -> instant.
(* Definition of a generic type of parameter relating jobs to an absolute deadline *)
Class JobDeadline (J : JobType) := job_deadline : J -> instant.
\ No newline at end of file
......@@ -45,12 +45,22 @@ Section Schedule.
Definition service (j : Job) (t : instant) := service_during j 0 t.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobArrival Job}.
(* Next, we say that job j has completed by time t if it received enough
service in the interval [0, t). *)
Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
(* We say that R is a response time bound of a job j if j has completed
by R units after its arrival *)
Definition job_response_time_bound (j : Job) (R : duration) :=
completed_by j (job_arrival j + R).
(* We say that a job meets its deadline if it completes by its absolute deadline *)
Definition job_meets_deadline (j : Job) :=
completed_by j (job_deadline j).
(* Job j is pending at time t iff it has arrived but has not yet completed. *)
Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
......
From mathcomp Require Export ssrbool.
From rt.restructuring.behavior Require Export job.
(* Throughout the library we assume that jobs have decidable equality *)
(* Throughout the library we assume that tasks have decidable equality *)
Definition TaskType := eqType.
......@@ -9,7 +9,6 @@ Definition TaskType := eqType.
Class JobTask (J : JobType) (T : TaskType) := job_task : J -> T.
Section SameTask.
(* For any type of job associated with any type of tasks... *)
Context {Job: JobType}.
......@@ -21,3 +20,13 @@ Section SameTask.
Definition same_task j1 j2 := job_task j1 == job_task j2.
End SameTask.
(* Definition of a generic type of parameter for task deadlines *)
Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
(* Given task deadlines and a mapping from jobs to tasks we provide a generic definition of job_deadline *)
Instance job_deadline_from_task_deadline
(Job : JobType) (Task : TaskType)
`{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} :
JobDeadline Job := fun j => job_arrival j + task_deadline (job_task j).
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