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.
Structure concrete_task :=
  { task_id: nat (* for uniqueness *)
  ; task_cost: nat
  ; task_arrival: task_arrivals_bound
  ; task_deadline: instant
  ; task_priority : nat
  }.

To make it compatible with ssreflect, we define a decidable equality for concrete tasks.
Next, we prove that task_eqdef is indeed an equality, ...
..., 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
  ; job_arrival: instant
  ; job_cost: nat
  ; job_deadline: instant
  ; 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 task_arrival tsk with
  | Periodic pinter_arrival_to_prefix p
  | Sporadic minter_arrival_to_prefix m
  | ArrivalPrefix stepssteps
  end.

... and define the "arrival bound" concept for concrete tasks.
To make it compatible with ssreflect, we define a decidable equality for concrete jobs.
Next, we prove that job_eqdef is indeed an equality, ...
... 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 TaskCost : TaskCost Task := task_cost.
  #[global,program] Instance TaskPriority : TaskPriority Task := task_priority.
  #[global,program] Instance TaskDeadline : TaskDeadline Task := task_deadline.
  #[global,program] Instance ConcreteMaxArrivals : MaxArrivals Task := concrete_max_arrivals.

Second, we do the same for the above definition of job.
  Let Job := concrete_job : eqType.
  #[global,program] Instance JobTask : JobTask Job Task := job_task.
  #[global,program] Instance JobArrival : JobArrival Job := job_arrival.
  #[global,program] Instance JobCost : JobCost Job := job_cost.

End Parameters.