Project Page Index Table of Contents

# Library prosa.model.task.jitter

Require Export prosa.model.task.concept.
Require Export prosa.model.readiness.jitter.

# Task Release Jitter Bound

We define a task-level parameter that expresses that the release jitter experienced by any of the task's jobs is bounded by a known constant.
Class TaskJitter (Task : TaskType) := { task_jitter : Task → duration }.
In the following, we connect the task-level bound to the job-level release jitter in the obvious way.
Section ValidTaskJitter.
Consider any type of tasks with associated jitter bounds...
Context {Task : TaskType} `{TaskJitter Task}.
...and the corresponding jobs.
Context {Job : JobType} `{JobTask Job Task} `{JobJitter Job}.
A jitter bound is valid iff it bounds the release jitter experienced by any of job of the task.
Definition valid_jitter (tsk : Task) :=
∀ j,
job_task j = tsk →
job_jitter j ≤ task_jitter tsk.
In the context of a set of tasks ts, ...
Variable ts : TaskSet Task.
... all tasks in the set must have valid jitter bounds.
Definition valid_jitter_bounds := ∀ tsk, tsk \in ts → valid_jitter tsk.
End ValidTaskJitter.