Commit 3fbb1eda authored by Björn Brandenburg's avatar Björn Brandenburg

define [backlogged] in terms of job readiness

Add a [job_ready] parameter to the job model, akin to [pending], that
defines whether a job can be scheduled at a given time in a given schedule.

Then use this new general notion of readiness to define [backlogged].

A pending job may not be ready, whereas (under any reasonable
definition) a ready job ought to be pending, so this definition is
more precise and captures effects such as jitter and self-suspensions.
parent 91869441
......@@ -14,4 +14,8 @@ Class JobCost (J : JobType) := job_cost : J -> duration.
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
Class JobDeadline (J : JobType) := job_deadline : J -> instant.
(* Definition of a generic type of release jitter parameter. *)
Class JobJitter (J : JobType) := job_jitter : J -> duration.
......@@ -73,36 +73,81 @@ Section Schedule.
Definition pending_earlier_and_at (j : Job) (t : instant) :=
arrived_before j t && ~~ completed_by j t.
(* Job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (j : Job) (t : instant) := pending j t && ~~ scheduled_at j t.
(* Let's define the remaining cost of job j as the amount of service
that has to be received for its completion. *)
that has to be received for its completion. *)
Definition remaining_cost j t :=
job_cost j - service j t.
(* In this section, we define valid schedules. *)
Section ValidSchedule.
End Schedule.
(* We next define a general notion of readiness of a job: a job can be
scheduled only when it is ready. This notion of readiness is a general
concept that is used to model jitter, self-suspensions, etc. Crucially, we
require that any sensible notion of readiness is a refinement of the notion
of a pending job, i.e., any ready job must also be ready. *)
Class JobReady (Job : JobType) (PState : Type)
`{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
{
job_ready : schedule PState -> Job -> instant -> bool;
any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
}.
(* Based on the general notion of readiness, we define what it means to be
backlogged, i.e., ready to run but not executing. *)
Section Backlogged.
(* Conside any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
(* We define whether jobs come from some arrival sequence... *)
Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
forall j t, scheduled_at j t -> arrives_in arr_seq j.
(* Allow for any notion of readiness. *)
Context `{JobReady Job PState}.
(* ..., whether a job can only be scheduled if it has arrived ... *)
Definition jobs_must_arrive_to_execute :=
forall j t, scheduled_at j t -> has_arrived j t.
(* Job j is backlogged at time t iff it is ready and not scheduled. *)
Definition backlogged (sched : schedule PState) (j : Job) (t : instant) :=
job_ready sched j t && ~~ scheduled_at sched j t.
(* ... and whether a job cannot be scheduled after it completes. *)
Definition completed_jobs_dont_execute :=
forall j t, service j t <= job_cost j.
End Backlogged.
(* We say that the schedule is valid iff
- jobs come from some arrival sequence
- a job can only be scheduled if it has arrived and is not completed yet *)
Definition valid_schedule (arr_seq : arrival_sequence Job) :=
jobs_come_from_arrival_sequence arr_seq /\
jobs_must_arrive_to_execute /\
completed_jobs_dont_execute.
End ValidSchedule.
End Schedule.
(* In this section, we define valid schedules. *)
Section ValidSchedule.
(* Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
(* Consider any schedule. *)
Variable sched : schedule PState.
Context `{JobArrival Job}.
(* We define whether jobs come from some arrival sequence... *)
Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
forall j t, scheduled_at sched j t -> arrives_in arr_seq j.
(* ..., whether a job can only be scheduled if it has arrived ... *)
Definition jobs_must_arrive_to_execute :=
forall j t, scheduled_at sched j t -> has_arrived j t.
Context `{JobCost Job}.
Context `{JobReady Job PState}.
(* ..., whether a job can only be scheduled if it is ready ... *)
Definition jobs_must_be_ready_to_execute :=
forall j t, scheduled_at sched j t -> job_ready sched j t.
(* ... and whether a job cannot be scheduled after it completes. *)
Definition completed_jobs_dont_execute :=
forall j t, service sched j t <= job_cost j.
(* We say that the schedule is valid iff
- jobs come from some arrival sequence
- a job is scheduled if it is ready *)
Definition valid_schedule (arr_seq : arrival_sequence Job) :=
jobs_come_from_arrival_sequence arr_seq /\
jobs_must_be_ready_to_execute.
(* Note that we do not explicitly require that a valid schedule satisfies
jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
properties are implied by jobs_must_be_ready_to_execute. *)
End ValidSchedule.
From rt.restructuring.behavior Require Export schedule.
(* We define the readiness indicator function for the classic Liu & Layland
model without jitter and no self-suspensions, where jobs are always
ready. *)
Section LiuAndLaylandReadiness.
(* Consider any kind of jobs... *)
Context {Job : JobType}.
(* ... and any kind of processor state. *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(* Supose jobs have an arrival time and a cost. *)
Context `{JobArrival Job} `{JobCost Job}.
(* In the basic Liu & Layland model, a job is ready iff it is pending. *)
Global Instance basic_ready_instance : JobReady Job PState :=
{
job_ready sched j t := pending sched j t
}.
Proof. trivial. Defined.
End LiuAndLaylandReadiness.
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.restructuring.behavior Require Export schedule.
From rt.util Require Import nat.
(* We define the readiness indicator function for models with release jitter
(and no self-suspensions). *)
Section ReadinessOfJitteryJobs.
(* Consider any kind of jobs... *)
Context {Job : JobType}.
(* ... and any kind of processor state. *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(* Supose jobs have an arrival time, a cost, and a release jitter bound. *)
Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.
(* We say that a job is released at a time after its arrival if the job's
release jitter has passed. *)
Definition is_released (j : Job) (t : instant) := job_arrival j + job_jitter j <= t.
(* A job that experiences jitter is ready only when the jitter-induced delay
has passed after its arrival and if it is not yet complete. *)
Global Instance jitter_ready_instance : JobReady Job PState :=
{
job_ready sched j t := is_released j t && ~~ completed_by sched j t
}.
Proof.
move=> sched j t /andP [REL UNFINISHED].
rewrite /pending. apply /andP. split => //.
move: REL. rewrite /is_released /has_arrived.
by apply leq_addk.
Defined.
End ReadinessOfJitteryJobs.
......@@ -14,6 +14,9 @@ Section Priority.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Context `{JobReady Job PState}.
Variable sched : schedule PState.
Definition respects_preemptive_priorities :=
......
......@@ -92,7 +92,7 @@ Section TDMASchedule.
Context {Task : TaskType} {Job : JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobArrival Job} `{JobCost Job} `{JobReady Job (option Job)} `{JobTask Job Task}.
(* Consider any job arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
......@@ -130,4 +130,4 @@ Section TDMASchedule.
arrives_in arr_seq j ->
sched_implies_in_slot j t /\
backlogged_implies_not_in_slot_or_other_job_sched j t.
End TDMASchedule.
\ No newline at end of file
End TDMASchedule.
......@@ -19,6 +19,9 @@ Section WorkConserving.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(* Further, allow for any notion of job readiness. *)
Context `{JobReady Job PState}.
(* Given an arrival sequence and a schedule ... *)
Variable arr_seq : arrival_sequence Job.
Variable sched: schedule PState.
......
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