Library prosa.implementation.definitions.task

From HB Require Import structures.
Require Export prosa.implementation.definitions.arrival_bound.
Require Export prosa.model.task.arrival.curves.
Require Export prosa.model.priority.numeric_fixed_priority.

Implementation of Tasks and Jobs

This file provides reference implementations of the notions of "tasks" and "jobs" that can be used to meet the hypotheses on which many of the analyses in Prosa are based.
Note that their use is entirely optional: clients of Prosa may choose to use these types or implement their own notions of "tasks" and "jobs".

Implementation of a Concrete Task

A task comprises of an ID, a cost, an arrival bound, a deadline and a priority. The ID is required to ensure uniqueness.
Structure concrete_task :=
  { task_id: nat
  ; concrete_task_cost: nat
  ; concrete_task_arrival: task_arrivals_bound
  ; concrete_task_deadline: instant
  ; concrete_task_priority : nat
  }.

To make it compatible with ssreflect, we define a decidable equality for concrete tasks.
Definition task_eqdef (t1 t2 : concrete_task) :=
  (task_id t1 == task_id t2)
  && (concrete_task_cost t1 == concrete_task_cost t2)
  && (concrete_task_arrival t1 == concrete_task_arrival t2)
  && (concrete_task_deadline t1 == concrete_task_deadline t2)
  && (concrete_task_priority t1 == concrete_task_priority t2).

Next, we prove that task_eqdef is indeed an equality, ...
Lemma eqn_task : Equality.axiom task_eqdef.

..., which allows instantiating the canonical structure for concrete_task : eqType.

Implementation of a Concrete Job

A job comprises of an id, an arrival time, a cost, a deadline and the task it belongs to.
Record concrete_job :=
  { job_id: nat
  ; concrete_job_arrival: instant
  ; concrete_job_cost: nat
  ; concrete_job_deadline: instant
  ; concrete_job_task: concrete_task : eqType
  }.

For convenience, we define a function that converts each possible arrival bound (periodic, sporadic, and arrival-curve prefix) into an arrival-curve prefix...
Definition get_arrival_curve_prefix tsk :=
  match concrete_task_arrival tsk with
  | Periodic p ⇒ inter_arrival_to_prefix p
  | Sporadic m ⇒ inter_arrival_to_prefix m
  | ArrivalPrefix steps ⇒ steps
  end.

... and define the "arrival bound" concept for concrete tasks.
Definition concrete_max_arrivals tsk Δ :=
  extrapolated_arrival_curve (get_arrival_curve_prefix tsk) Δ.

To make it compatible with ssreflect, we define a decidable equality for concrete jobs.
Definition job_eqdef (j1 j2 : concrete_job) :=
  (job_id j1 == job_id j2)
  && (concrete_job_arrival j1 == concrete_job_arrival j2)
  && (concrete_job_cost j1 == concrete_job_cost j2)
  && (concrete_job_deadline j1 == concrete_job_deadline j2)
  && (concrete_job_task j1 == concrete_job_task j2).

Next, we prove that job_eqdef is indeed an equality, ...
Lemma eqn_job : Equality.axiom job_eqdef.
... which allows instantiating the canonical structure for concrete_job : eqType.

Instances for Concrete Jobs and Tasks.

In the following, we connect the concrete task and job types defined above to the generic Prosa interfaces for task and job parameters.
Section Parameters.

First, we connect the above definition of tasks with the generic Prosa task-parameter interfaces.
  Let Task := concrete_task : eqType.
  #[global,program] Instance concrete_task_cost_instance : TaskCost Task :=
  {
    task_cost := concrete_task_cost
  }.
  #[global,program] Instance concrete_task_priority_instance : TaskPriority Task :=
  {
    task_priority := concrete_task_priority
  }.
  #[global,program] Instance concrete_task_deadline_instance : TaskDeadline Task :=
  {
    task_deadline := concrete_task_deadline
  }.
  #[global,program] Instance concrete_max_arrivals_instance : MaxArrivals Task :=
  {
    max_arrivals := concrete_max_arrivals
  }.

Second, we do the same for the above definition of job.
  Let Job := concrete_job : eqType.
  #[global,program] Instance concrete_job_task_instance : JobTask Job Task :=
  {
    job_task := concrete_job_task
  }.
  #[global,program] Instance concrete_job_arrival_instance : JobArrival Job :=
  {
    job_arrival := concrete_job_arrival
  }.
  #[global,program] Instance concrete_job_cost_instance : JobCost Job :=
  {
    job_cost := concrete_job_cost
  }.

End Parameters.