Library prosa.implementation.readiness.suspension
Readiness Model for Self-Suspending Jobs
Consider any kind of jobs...
... and any kind of processor state.
Suppose jobs have an arrival time, a cost, and that they exhibit
self-suspensions.
In the self-suspension model, a job is ready iff its current suspension
has passed and it is not yet complete.
#[local,program] Instance self_suspension_ready_instance : JobReady Job PState :=
{
job_ready sched j t := suspension_has_passed sched j t
&& ~~ completed_by sched j t
}.
{
job_ready sched j t := suspension_has_passed sched j t
&& ~~ completed_by sched j t
}.
The concrete self-suspension readiness instance satisfies the axiomatic
specification of self-suspension readiness.
Fact self_suspension_readiness_spec :
self_suspension_readiness self_suspension_ready_instance.
End ReadinessOfSelfSuspendingJobs.
self_suspension_readiness self_suspension_ready_instance.
End ReadinessOfSelfSuspendingJobs.
We add the concrete model's specification to the basic facts database so
implementation modules can use it automatically.
Global Hint Resolve self_suspension_readiness_spec : basic_rt_facts.