Library rt.restructuring.model.readiness.basic

From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import completion.

We define the readiness indicator function for the classic Liu & Layland model without jitter and no self-suspensions, where jobs are always ready.

Section LiuAndLaylandReadiness.

Consider any kind of jobs...

Context {Job : JobType}.

... and any kind of processor state.

Context {PState : Type}.
Context `{ProcessorState Job PState}.

Supose jobs have an arrival time and a cost.

Context `{JobArrival Job} `{JobCost Job}.

In the basic Liu & Layland model, a job is ready iff it is pending.

Under this definition, a schedule satisfies that only ready jobs execute as long as jobs must arrive to execute and completed jobs don't execute, which we note with the following theorem.

  Theorem basic_readiness_compliance:
    ∀ sched,
      jobs_must_arrive_to_execute sched →
      completed_jobs_dont_execute sched →
      jobs_must_be_ready_to_execute sched.

End LiuAndLaylandReadiness.