Library rt.restructuring.behavior.facts.completion

Section CompletionFacts.
  (* Consider any job type,...*)
  Context {Job: JobType}.
  Context `{JobCost Job}.

  (* ...any kind of processor model,... *)
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

  (* ...and a given schedule. *)
  Variable sched: schedule PState.

  (* Let j be any job that is to be scheduled. *)
  Variable j: Job.

  (* We prove that after job j completes, it remains completed. *)
  Lemma completion_monotonic:
    ∀ t t',
      t ≤ t' →
      completed_by sched j t →
      completed_by sched j t'.

  (* We observe that being incomplete is the same as not having received
     sufficient service yet... *)
  Lemma less_service_than_cost_is_incomplete:
    ∀ t,
      service sched j t < job_cost j
      ↔
      ~~ completed_by sched j t.

  (* ...which is also the same as having positive remaining cost. *)
  Lemma incomplete_is_positive_remaining_cost:
    ∀ t,
      ~~ completed_by sched j t
      ↔
      remaining_cost sched j t > 0.

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

  (* Further, we note that if a job receives service at some time t, then its
     remaining cost at this time is positive. *)
  Lemma serviced_implies_positive_remaining_cost:
    ∀ t,
      service_at sched j t > 0 →
      remaining_cost sched j t > 0.

  (* Consequently, if we have a have processor model where scheduled jobs
   * necessarily receive service, we can conclude that scheduled jobs have
   * remaining positive cost. *)

  (* Assume a scheduled job always receives some positive service. *)
  Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.

  (* Then a scheduled job has positive remaining cost. *)
  Corollary scheduled_implies_positive_remaining_cost:
    ∀ t,
      scheduled_at sched j t →
      remaining_cost sched j t > 0.

  (* We also prove that a completed job cannot be scheduled... *)
  Lemma completed_implies_not_scheduled:
    ∀ t,
      completed_by sched j t →
      ~~ scheduled_at sched j t.

  (* ... and that a scheduled job cannot be completed. *)
  Lemma scheduled_implies_not_completed:
    ∀ t,
      scheduled_at sched j t →
      ~~ completed_by sched j t.

  (* We further observe that [service] and [remaining_cost] are complements of
     one another. *)
  Lemma service_cost_invariant:
    ∀ t,
      (service sched j t) + (remaining_cost sched j t) = job_cost j.

End CompletionFacts.

Section ServiceAndCompletionFacts.

  (* Consider any job type,...*)
  Context {Job: JobType}.
  Context `{JobCost Job}.

  (* ...any kind of processor model,... *)
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

  (* ...and a given schedule. *)
  Variable sched: schedule PState.

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

  (* Let j be any job that is to be scheduled. *)
  Variable j: Job.

  (* Assume that a scheduled job receives exactly one time unit of service. *)
  Hypothesis H_unit_service: unit_service_proc_model.

  Section GuaranteedService.

    (* Assume a scheduled job always receives some positive service. *)
    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.

    (* Then we can easily show that the service never exceeds the total cost of
       the job. *)
    Lemma service_le_cost:
      ∀ t,
        service sched j t ≤ job_cost j.

    (* We show that the service received by job j in any interval is no larger
       than its cost. *)
    Lemma cumulative_service_le_job_cost:
      ∀ t t',
        service_during sched j t t' ≤ job_cost j.

    Section ProperReleases.
      Context `{JobArrival Job}.

      (* Assume that jobs are not released early. *)
      Hypothesis H_jobs_must_arrive:
        jobs_must_arrive_to_execute sched.

      (* We show that if job j is scheduled, then it must be pending. *)
      Lemma scheduled_implies_pending:
        ∀ t,
          scheduled_at sched j t →
          pending sched j t.

    End ProperReleases.
  End GuaranteedService.

  (* If a job isn't complete at time t, it can't be completed at time (t +
     remaining_cost j t - 1). *)
  Lemma job_doesnt_complete_before_remaining_cost:
    ∀ t,
      ~~ completed_by sched j t →
      ~~ completed_by sched j (t + remaining_cost sched j t - 1).

End ServiceAndCompletionFacts.

Section PositiveCost.

  (* Consider any type of jobs with cost and arrival-time attributes,...*)
  Context {Job: JobType}.
  Context `{JobCost Job}.
  Context `{JobArrival Job}.

  (* ...any kind of processor model,... *)
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

  (* ...and a given schedule. *)
  Variable sched: schedule PState.

  (* Let j be any job that is to be scheduled. *)
  Variable j: Job.

  (* We assume that job j has positive cost, from which we can
     infer that there always is a time in which j is pending, ... *)
  Hypothesis H_positive_cost: job_cost j > 0.

  (* ...and that jobs must arrive to execute. *)
  Hypothesis H_jobs_must_arrive:
    jobs_must_arrive_to_execute sched.

  (* Then, we prove that the job with a positive cost
     must be scheduled to be completed. *)
  Lemma completed_implies_scheduled_before:
    ∀ t,
      completed_by sched j t →
      ∃ t',
        job_arrival j ≤ t' < t
        ∧ scheduled_at sched j t'.

  (* We also prove that the job is pending at the moment of its arrival. *)
  Lemma job_pending_at_arrival:
    pending sched j (job_arrival j).

End PositiveCost.