Finish Time of a Job

In this file, we define a job's precise finish time. Note that in general a job's finish time may not be defined: if a job never finishes in a given schedule, it does not have a finish time. To get around this, we define a job's finish time under the assumption that some (not necessarily tight) response-time bound R is known for the job. Under this assumption, we can simply re-use ssreflect's existing ex_minn search mechanism (for finding the minimum natural number satisfying a given predicate given a witness that some natural number satisfies the predicate) and benefit from the existing corresponding lemmas. This file briefly illustrates how this can be done.

Consider any type of jobs with arrival times and costs ...

... and any schedule of such jobs.

Consider an arbitrary job j.

In the following, we proceed under the assumption that j finishes eventually (i.e., no later than R time units after its arrival, for any finite R).

For technical reasons, we restate the response-time assumption explicitly as an existentially quantified variable.

We are now ready for the main definition: job j's finish time is the earliest time t such that completed_by sched j t holds. This time can be computed with ssreflect's ex_minn utility function, which is convenient because then we can reuse the corresponding lemmas.

In the following, we demonstrate the reuse of ex_minn properties by establishing three natural properties of a job's finish time. First, a job is indeed complete at its finish time.

Second, a job's finish time is the earliest time that it is complete.

Third, Prosa's notion of completes_at is satisfied at the finish time.

Finally, we can define a job's precise response time as usual as the time from its arrival until its finish time.