Lock-in service of a job

In this module, we provide a sufficient condition under which a job receives enough service to become nonpreemptive.
Module AbstractRTALockInService.

  Import Job UniprocessorSchedule Service AbstractRTADefinitions.

  (* Previously we defined the notion of lock-in service (see limited.schedule.v file). 
     Lock-in service is the amount of service after which a job cannot be preempted until 
     its completion. In this section we prove that if cumulative interference inside a 
     busy interval is bounded by a certain constant then a job executes long enough to 
     reach its lock-in service and become nonpreemptive. *)

  Section LockInService.

    Context {Task: eqType}.
    Variable task_cost: Task time.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_task: Job Task.

    (* Consider any arrival sequence with consistent arrivals... *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.

    (* Next, consider any uniprocessor schedule of this arrival sequence. *)
    Variable sched: schedule Job.

    (* Assume that the job costs are no larger than the task costs. *)
    Hypothesis H_job_cost_le_task_cost:
        task_cost job_cost job_task arr_seq.

    (* Let tsk be any task that is to be analyzed. *)
    Variable tsk: Task.

    (* Assume we are provided with abstract functions for interference and interfering workload. *)
    Variable interference: Job time bool.
    Variable interfering_workload: Job time time.

    (* For simplicity, let's define some local names. *)
    Let work_conserving := work_conserving job_arrival job_cost job_task arr_seq sched tsk.
    Let cumul_interference := cumul_interference interference.
    Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
    Let busy_interval := busy_interval job_arrival job_cost sched interference interfering_workload.

    (* We assume that the schedule is work-conserving. *)
    Hypothesis H_work_conserving: work_conserving interference interfering_workload.

    (* Let j be any job of task tsk with positive job cost. *)
    Variable j: Job.
    Hypothesis H_j_arrives: arrives_in arr_seq j.
    Hypothesis H_job_of_tsk: job_task j = tsk.
    Hypothesis H_job_cost_positive: job_cost_positive job_cost j.

    (* Next, consider any busy interval t1, t2) of job j. *)
    Variable t1 t2: time.
    Hypothesis H_busy_interval: busy_interval j t1 t2.

    (* First, we prove that job j completes by the end of the busy interval. 
       Note that the busy interval contains the execution of job j, in addition
       time instant t2 is a quiet time. Thus by the definition of a quiet time
       the job should be completed before time t2. *)

    Lemma job_completes_within_busy_interval:
      completed_by job_cost sched j t2.

    (* In this section we show that the cumulative interference is a complement to 
       the total time where job j is scheduled inside the busy interval. *)

    Section InterferenceIsComplement.

      (* Consider any subinterval t, t + delta) inside the busy interval [t1, t2). *)
      Variable t delta: time.
      Hypothesis H_greater_than_or_equal: t1 t.
      Hypothesis H_less_or_equal: t + delta t2.

      (* We prove that sum of cumulative service and cumulative interference 
         in the interval t, t + delta) is equal to delta. *)

      Lemma interference_is_complement_to_schedule:
        service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.

    End InterferenceIsComplement.

    (* In this section, we prove a sufficient condition under which job j receives enough service. *)
    Section InterferenceBoundedImpliesEnoughService.

      (* Let progress_of_job be the desired service of job j. *)
      Variable progress_of_job: time.
      Hypothesis H_progress_le_job_cost: progress_of_job job_cost j.

      (* Assume that for some delta, the sum of desired progress and cumulative 
         interference is bounded by delta (i.e., the supply). *)

      Variable delta: time.
      Hypothesis H_total_workload_is_bounded:
        progress_of_job + cumul_interference j t1 (t1 + delta) delta.

      (* Then, it must be the case that the job has received no less service than progress_of_job. *)
      Theorem j_receives_at_least_lock_in_service:
        service sched j (t1 + delta) progress_of_job.

    End InterferenceBoundedImpliesEnoughService.

    (* In this section we prove a simple lemma about completion of 
       a job after is reaches lock-in service. *)

    Section CompletionOfJobAfterLockInService.

      (* Assume that completed jobs do not execute. *)
      Hypothesis H_completed_jobs_dont_execute:
        completed_jobs_dont_execute job_cost sched.

      (* Consider a proper job lock-in service function, i.e... *)
      Variable job_lock_in_service: Job time.

      (* ...(1) for any job j the lock-in service of job j is positive... *)
      Hypothesis H_lock_in_service_positive:
        job_lock_in_service_positive job_cost arr_seq job_lock_in_service.

      (* ...(2) it also less-than-or-equal to the job_cost... *)
      Hypothesis H_lock_in_service_le_job_cost:
        job_lock_in_service_le_job_cost job_cost arr_seq job_lock_in_service.

      (* ..., and (3) we assume that the scheduler respects the notion of the lock-in service. *)
      Hypothesis H_job_nonpreemptive_after_lock_in_service:
        job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service.

      (* Then, job j must complete in job_cost j - job_lock_in_service j time 
         units after it reaches lock-in service. *)

      Lemma job_completes_after_reaching_lock_in_service:
          job_lock_in_service j service sched j t
          completed_by job_cost sched j (t + (job_cost j - job_lock_in_service j)).

    End CompletionOfJobAfterLockInService.

  End LockInService.

End AbstractRTALockInService.