Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]


(** * Service Received by Sets of Jobs *)

(** In this file, we define the notion of service received by a set of
    jobs. *)

Section ServiceOfJobs.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

  (** Consider any kind of processor model, ... *)
  Context {PState : ProcessorState Job}.

  (** ... any job arrival sequence, ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and any given schedule. *)
  Variable sched : schedule PState.

  (** First, we define the service received by a generic set of jobs. *)
  Section ServiceOfSetOfJobs.

    (** Let [P] be any computable predicate over jobs, ...*)
    Variable P : pred Job.

    (** ... and let [jobs] denote any (finite) set of jobs. *)
    Variable jobs : seq Job.

    (** We define the cumulative service received at time [t] by
        jobs in [jobs] that satisfy predicate [P] ... *)
    Definition service_of_jobs_at (t : instant) :=
      \sum_(j <- jobs | P j) service_at sched j t.

    (** ... and the cumulative service received during the interval
        <<[t1, t2)>> by jobs that satisfy predicate [P]. *)
    Definition service_of_jobs (t1 t2 : instant) :=
      \sum_(j <- jobs | P j) service_during sched j t1 t2.

  End ServiceOfSetOfJobs.

  (** Next, we define the service received by jobs with higher or
     equal priority under JLFP policies. *)
  Section PerJobPriority.

    (** Consider any JLDP policy. *)
    Context `{JLFP_policy Job}.

    (** Let jobs denote any (finite) set of jobs. *)
    Variable jobs : seq Job.

    (** Let j be the job to be analyzed. *)
    Variable j : Job.

    (** Based on the definition of jobs of higher or equal priority, ... *)
    Let of_higher_or_equal_priority j_hp := hep_job j_hp j.

    (** ...we define the service received during <<[t1, t2)>> by jobs of higher or equal priority. *)
    Definition service_of_higher_or_equal_priority_jobs (t1 t2 : instant) :=
      service_of_jobs of_higher_or_equal_priority jobs t1 t2.

    (** Furthermore, we define similar notions on jobs arriving in a
        given time interval, such as ... *)

    (** ... (1) service of all other jobs with higher-or-equal
        priority (w.r.t. job [j]) distinct from job [j], ... *)
    Definition service_of_other_hep_jobs (t1 t2 : instant) :=
      service_of_jobs
        (fun jhp => another_hep_job jhp j)
        (arrivals_between arr_seq t1 t2) t1 t2.

    (** ... (2) notion of service of higher-or-equal priority jobs
      from other tasks, ... *)
    Definition service_of_other_task_hep_jobs (t1 t2 : instant) :=
      service_of_jobs
        (fun jhp => another_task_hep_job jhp j)
        (arrivals_between arr_seq t1 t2) t1 t2.

    (** ... (3) and service of jobs with higher-or-equal priority
        arriving in an interval <<[t1, t2)>>. *)
    Definition service_of_hep_jobs (t1 t2 : instant) :=
      service_of_jobs
        (fun jhp => hep_job jhp j)
        (arrivals_between arr_seq t1 t2) t1 t2.

  End PerJobPriority.

  (** We define the notion of cumulative service received by
      the jobs of a given task. *)
  Section ServiceOfTask.

    (** Let [tsk] be the task to be analyzed ... *)
    Variable tsk : Task.

    (** ... and let [jobs] denote any (finite) set of jobs. *)
    Variable jobs : seq Job.

    (** We define the cumulative task service received by the jobs of
        task [tsk] within time interval <<[t1, t2)>>. *)
    Definition task_service_of_jobs_in t1 t2 :=
      service_of_jobs (job_of_task tsk) jobs t1 t2.

  End ServiceOfTask.

  (** Finally, we define the notion of total service received by a set of jobs. *)
  Section TotalService.

    (** Let [jobs] denote any (finite) set of jobs. *)
    Variable jobs : seq Job.

    (** We define the total service of [jobs] in an interval <<[t1,t2)>> simply
        as a sum of the service of individual jobs in interval <<[t1,t2)>>.

        (The predicate [predT] is the trivial predicate that always evaluates to
        [true], meaning that no jobs are filtered, and hence all jobs are
        accounted for.) *)
    Definition total_service_of_jobs_in (t1 t2 : instant) :=
      service_of_jobs predT jobs t1 t2.

  End TotalService.

End ServiceOfJobs.