Library prosa.analysis.facts.readiness.sequential

Throughout this file, we assume the sequential task readiness model, which means that a job is ready to execute only if all prior jobs of the same task have completed.
In this section, we show some useful properties of the sequential task readiness model.
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 : ProcessorState Job}.

Consider any arrival sequence with consistent arrivals.
Recall that we assume sequential tasks.
Consider any valid schedule of arr_seq.
  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

Consider an FP policy that indicates a reflexive higher-or-equal priority relation.
  Context `{FP_policy Task}.
  Hypothesis H_priority_is_reflexive : reflexive_priorities.

First, we show that the sequential readiness model is non-clairvoyant.
Next, we show that the sequential readiness model ensures that tasks are sequential. That is, that jobs of the same task execute in order of their arrival.
Finally, we show that the sequential readiness model is a work-bearing readiness model. That is, if a job j is pending but not ready at a time instant t, then there exists another (earlier) job of the same task that is pending and ready at time t.