Library prosa.analysis.definitions.readiness

Properties of Readiness Models

In this file, we define commonsense properties of readiness models.
For any type of jobs with costs and arrival times ...
  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.

... and any kind of processor model, ...
  Context {PState: ProcessorState Job}.

... consider a notion of job readiness.
  Variable ReadinessModel : JobReady Job PState.

First, we define a notion of non-clairvoyance for readiness models. Intuitively, whether a job is ready or not should depend only on the past (i.e., prior allocation decisions and job behavior), not on future events. Formally, we say that the ReadinessModel is non-clairvoyant if a job's readiness at a given time does not vary across schedules with identical prefixes. That is, given two schedules sched and sched', the predicates job_ready sched j t and job_ready sched' j t may not differ if sched and sched' are identical prior to time t.
  Definition nonclairvoyant_readiness :=
     sched sched' j h,
      identical_prefix sched sched' h
       t,
        t h
        job_ready sched j t = job_ready sched' j t.

Next, we relate the readiness model to the preemption model.
  Context `{JobPreemptable Job}.

In a preemption-policy-compliant schedule, nonpreemptive jobs must remain scheduled. Further, in a valid schedule, scheduled jobs must be ready. Consequently, in a valid preemption-policy-compliant schedule, a nonpreemptive job must remain ready until at least the end of its nonpreemptive section.
  Definition valid_nonpreemptive_readiness sched :=
      j t,
        ~~ job_preemptable j (service sched j t) job_ready sched j t.

For the next definition, consider the tasks from which the jobs stem.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.

We say a readiness model is sequential iff only a task's earliest incomplete job is ready, meaning that later jobs can be executed only after all earlier jobs have been completed.