Library prosa.analysis.definitions.work_bearing_readiness
Work-Bearing Readiness
In this module, we introduce a property of readiness models that
is called work-bearing readiness. Work-bearing readiness extracts
the useful property of the classic readiness model stating that,
if there is a job pending at a time instant
t, then there also
exists a job that is ready at time
t. In other words, we say
that a readiness model is a work-bearing readiness model if, for
any job
j and any time instant
t, if job
j is pending but
not ready at
t, then there is a job with higher or equal
priority
j_hp that is both pending and ready at time
t.
Consider any type of job associated with any type of tasks ...
... and any kind of processor state.
Further, allow for any notion of job readiness.
Consider any job arrival sequence, ...
... any schedule of these jobs, ...
... and a JLFP policy that indicates a higher-or-equal priority relation.
If a job
j is pending at a time instant
t, then (even if it
is not ready at time
t) there is a job
j_hp with
higher-or-equal priority that is ready at time instant
t.