Library prosa.analysis.definitions.task_schedule
Due to historical reasons this file defines the notion of a schedule of a
task for (arbitrary) uni-processor models. This is not a fundamental
limitation and the notion can be further generalized to multiprocessor
models.
Schedule of task
In this section we define properties of the schedule of a task.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any arrival sequence of such jobs.
Let sched be any kind of uniprocessor schedule
Let tsk be any task.
Next we define whether a task is scheduled at time t, ...
Definition task_scheduled_at (t : instant) :=
if (scheduled_job_at arr_seq sched t) is Some j then
job_task j == tsk
else false.
if (scheduled_job_at arr_seq sched t) is Some j then
job_task j == tsk
else false.
...which also corresponds to the instantaneous service it receives.
Based on the notion of instantaneous service, we define the cumulative
service received by tsk during any interval
[t1, t2)
...