Library prosa.model.readiness.sequential


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

Require Export prosa.behavior.all.
Require Export prosa.model.task.sequentiality.

Sequential Readiness Model

In this module, we define the notion of sequential task readiness. This notion is similar to the classic Liu & Layland model without jitter or self-suspensions. However, an important difference is that in the sequential task readiness model only the earliest pending job of a task is ready.

Section SequentialTasksReadiness.

Consider any type of job associated with any type of tasks...
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

... and any kind of processor state.
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

Consider any job arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

  (* A job [j] is ready at a time instant [t] iff all jobs from task
     [job_task j] that arrived earlier than job [j] are already
     completed by time [t]. *)
  Global Program Instance sequential_ready_instance : JobReady Job PState :=
    {
    job_ready sched j t :=
      pending sched j t &&
      prior_jobs_complete arr_seq sched j t
    }.
  Next Obligation.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 64)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  t : instant
  H3 : pending sched j t && prior_jobs_complete arr_seq sched j t
  ============================
  pending sched j t

----------------------------------------------------------------------------- *)

    by move: H3 ⇒ /andP [T _].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Defined.

End SequentialTasksReadiness.