schedule.v 4.16 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.behavior Require Export arrival.arrival_sequence.

(* We define the notion of a generic processor state. The processor state type
 * 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 : eqType) (State : Type) :=
  {
    (* For a given processor state, the [scheduled_in] predicate checks whether a given
     * job is running in that state. *)
    scheduled_in: Job -> State -> bool;
    (* For a given processor state, the [service_in] function determines how much
     * service a given job receives in that state. *)
    service_in: Job -> State -> nat;
    (* For a given processor state, a job does not receive service if it is not scheduled
     * in that state *)
    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.

(* Definition of a generic type of parameter relating jobs to a discrete cost *)

Class JobCost (J : JobType) := job_cost : J -> nat.

Maxime Lesourd's avatar
Maxime Lesourd committed
29
Section Schedule.
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
  Context {Job : eqType} {PState : Type}.
  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}.
  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.

  (* 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.

  (* 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. *)
  Definition remaining_cost j t :=
    job_cost j - service j t.

Maxime Lesourd's avatar
Maxime Lesourd committed
74 75
  (* In this section, we define valid schedules. *)
  Section ValidSchedule.
76 77 78 79 80 81 82 83 84 85 86 87 88

    (* 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.

    (* ..., 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.

    (* ... and whether a job cannot be scheduled after it completes. *)
    Definition completed_jobs_dont_execute :=
      forall j t, service j t <= job_cost j.

Maxime Lesourd's avatar
Maxime Lesourd committed
89 90 91 92 93 94 95 96 97 98
    (* 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 schedule_is_valid (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.