# Library prosa.model.processor.ideal

# The Ideal Uniprocessor Model

Consider any type of jobs.

We connect the notion of an ideal processor state with
the generic interface for the processor-state abstraction in Prosa by
declaring a so-called instance of the ProcessorState typeclass.

We define the ideal "processor state" as an option Job,
which means that it is either Some j (where j is a
Job) or None (which we use to indicate an idle
instant).

As this is a uniprocessor model, cores are implicitly defined
as the unit type containing a single element as a placeholder. We say that a given job j is scheduled in a
given state s iff s is Some j.

Any state of an ideal processor provides exactly one unit of
supply.

service_on j s (_ : unit) := if s == Some j then 1 else 0;

|}.

Next Obligation.

by move⇒ j s ?; rewrite /nat_of_bool; case: ifP ⇒ // ? /negP[].

Qed.

Next Obligation.

by move⇒ j s ?; rewrite /nat_of_bool; case: ifP ⇒ // ? /negP[].

Qed.

End State.

|}.

Next Obligation.

by move⇒ j s ?; rewrite /nat_of_bool; case: ifP ⇒ // ? /negP[].

Qed.

Next Obligation.

by move⇒ j s ?; rewrite /nat_of_bool; case: ifP ⇒ // ? /negP[].

Qed.

End State.

Consider any type of jobs...

... and any ideal uniprocessor schedule of such jobs.

We say that the processor is idle at time t iff there is no job being scheduled.