Library prosa.analysis.definitions.task_schedule

Schedule and Service of task

In this section we define properties of the schedule and service of a task.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any arrival sequence of such jobs.
  Variable arr_seq : arrival_sequence Job.

Let sched be any kind of schedule
  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.

Let tsk be any task.
  Variable tsk : Task.

We define a set of jobs of task tsk that are scheduled at time t.
Next we define whether task tsk is scheduled at time t.
  Definition task_scheduled_at (t : instant) :=
    scheduled_jobs_of_task_at t != [::].

We define the instantaneous service of tsk as the total instantaneous service of all jobs of this task scheduled at time t.
Based on the notion of instantaneous service, we define the cumulative service received by tsk during any interval [t1, t2)>> ...
  Definition task_service_during (t1 t2 : instant) :=
    \sum_(t1 t < t2) task_service_at t.

...and the cumulative service received by tsk up to time t2, i.e., in the interval [0, t2).
  Definition task_service (t2 : instant) := task_service_during 0 t2.

Similarly, we define a set of jobs of task tsk receiving service at time t.
Next, we define whether tsk is served at time t.