Project Page Index Table of Contents

# Library prosa.implementation.readiness.sequential

Require Export prosa.model.readiness.sequential.

# Basic Sequential Readiness Model

In this module, we define the concrete readiness instance for the basic sequential task readiness model, in which 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} {Task : TaskType} `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
... and any kind of processor state.
Context {PState : ProcessorState Job}.
Consider a given job arrival sequence.
Variable arr_seq : arrival_sequence Job.
A job j is ready at a time instant t iff it is pending and all jobs from task job_task j that arrived earlier than job j are already completed by time t.
#[local,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. by move⇒ sched j t /andP[]. Qed.
The concrete sequential readiness instance satisfies the axiomatic specification of basic sequential readiness.
Fact sequential_readiness_spec :
basic_sequential_readiness sequential_ready_instance arr_seq.
Proof. by []. Qed.
End SequentialTasksReadiness.
We add the concrete model's specification to the basic facts database so implementation modules can use it automatically.
Global Hint Resolve sequential_readiness_spec : basic_rt_facts.