Library prosa.analysis.definitions.readiness


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.behavior.ready.
Require Export prosa.analysis.definitions.schedule_prefix.
Require Export prosa.model.preemption.parameter.

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: Type} `{ProcessorState Job PState}.

... 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.

End ReadinessModelProperties.