Library prosa.implementation.definitions.task

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, ...
Lemma eqn_task : Equality.axiom task_eqdef.
Proof.
  unfold Equality.axiom; intros x y.
  destruct (task_eqdef x y) eqn:EQ.
  { apply ReflectT.
    unfold task_eqdef in ×.
    move: EQ ⇒ /andP [/andP [/andP [/andP [/eqP ID /eqP COST] /eqP PER] /eqP DL] /eqP PRIO].
    by destruct x, y; simpl in *; subst. }
  { apply ReflectF.
    unfold task_eqdef, not in × ⇒ BUG.
    apply negbT in EQ.
    repeat rewrite negb_and in EQ.
    destruct x, y.
    move: BUG ⇒ [ID COST PER DL PRIO].
    rewrite ID COST PER DL PRIO //= in EQ.
    by subst; rewrite !eq_refl in EQ.
  }
Qed.

..., which allows instantiating the canonical structure for [eqType of concrete_task].

Implementation of a Concrete Job

A job comprises of an id, an arrival time, a cost, a deadline and the task it belongs to.
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, ...
Lemma eqn_job : Equality.axiom job_eqdef.
Proof.
  unfold Equality.axiom; intros x y.
  destruct (job_eqdef x y) eqn:EQ.
  { apply ReflectT; unfold job_eqdef in ×.
    move: EQ ⇒ /andP [/andP [/andP [/andP [/eqP ID /eqP ARR] /eqP COST] /eqP DL] /eqP TASK].
    by destruct x, y; simpl in *; subst. }
  { apply ReflectF.
    unfold job_eqdef, not in *; intro BUG.
    apply negbT in EQ; rewrite negb_and in EQ.
    destruct x, y.
    rewrite negb_and in EQ.
    move: EQ ⇒ /orP [EQ | /eqP TASK].
    move: EQ ⇒ /orP [EQ | /eqP DL].
    rewrite negb_and in EQ.
    move: EQ ⇒ /orP [EQ | /eqP COST].
    rewrite negb_and in EQ.
    move: EQ ⇒ /orP [/eqP ID | /eqP ARR].
    - by apply ID; inversion BUG.
    - by apply ARR; inversion BUG.
    - by apply COST; inversion BUG.
    - by apply DL; inversion BUG.
    - by apply TASK; inversion BUG. }
Qed.

... which allows instantiating the canonical structure for [eqType of concrete_job].

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 := [eqType of concrete_task].
  #[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 := [eqType of concrete_job].
  #[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.