schedule.v 6.3 KB
Newer Older
1
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
2
From rt.restructuring.behavior Require Export arrival_sequence.
3 4

(* We define the notion of a generic processor state. The processor state type
5 6 7 8
   determines aspects of the execution environment are modeled (e.g., overheads, spinning).
   In the most simple case (i.e., Ideal.processor_state), at any time,
   either a particular job is either scheduled or it is idle. *)
Class ProcessorState (Job : JobType) (State : Type) :=
9 10
  {
    (* For a given processor state, the [scheduled_in] predicate checks whether a given
11
       job is running in that state. *)
12 13
    scheduled_in: Job -> State -> bool;
    (* For a given processor state, the [service_in] function determines how much
14
       service a given job receives in that state. *)
15 16
    service_in: Job -> State -> nat;
    (* For a given processor state, a job does not receive service if it is not scheduled
17
       in that state *)
18 19 20 21 22 23 24
    service_implies_scheduled :
      forall j s, scheduled_in j s = false -> service_in j s = 0
  }.

(* A schedule maps an instant to a processor state *)
Definition schedule (PState : Type) := instant -> PState.

Maxime Lesourd's avatar
Maxime Lesourd committed
25
Section Schedule.
26
  Context {Job : JobType} {PState : Type}.
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
  Context `{ProcessorState Job PState}.

  Variable sched : schedule PState.

  (* First, we define whether a job j is scheduled at time t, ... *)
  Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).

  (* ... and the instantaneous service received by
           job j at time t. *)
  Definition service_at (j : Job) (t : instant) := service_in j (sched t).

  (* Based on the notion of instantaneous service, we define the
           cumulative service received by job j during any interval [t1, t2). *)
  Definition service_during (j : Job) (t1 t2 : instant) :=
    \sum_(t1 <= t < t2) service_at j t.

  (* Using the previous definition, we define the cumulative service
           received by job j up to time t, i.e., during interval [0, t). *)
  Definition service (j : Job) (t : instant) := service_during j 0 t.

  Context `{JobCost Job}.
48
  Context `{JobDeadline Job}.
49 50 51 52 53 54
  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.

55 56 57 58
  (* We say that job j completes at time t if it has completed by time t but
     not by time t - 1 *)
  Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.

59 60 61 62 63 64 65 66 67
  (* 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).

68 69 70 71 72 73 74 75 76
  (* 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.

  (* Job j is pending earlier and at time t iff it has arrived before time t
           and has not been completed yet. *)
  Definition pending_earlier_and_at (j : Job) (t : instant) :=
    arrived_before j t && ~~ completed_by j t.

  (* Let's define the remaining cost of job j as the amount of service
77
     that has to be received for its completion. *)
78 79 80
  Definition remaining_cost j t :=
    job_cost j - service j t.

81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
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}.
101

102 103
  (* Allow for any notion of readiness. *)
  Context `{JobReady Job PState}.
104

105 106 107
  (* 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.
108

109
End Backlogged.
110

Maxime Lesourd's avatar
Maxime Lesourd committed
111

112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
(* 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.