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.

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.

  (* To begin with, we establish that the cumulative service never exceeds a
     job's total cost if service increases only by one at each step since
     completed jobs don't execute. *)
  Lemma service_at_most_cost:
    ∀ t,
      service sched j t ≤ job_cost j.

  (* This lets us conclude 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.

  (* 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.

  (* 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).

  Section GuaranteedService.

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

    (* Assume that jobs are not released early. *)
    Context `{JobArrival Job}.
    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 GuaranteedService.

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.

Section CompletedJobs.
  (* Consider any kinds of jobs and any kind of processor state. *)
  Context {Job : JobType} {PState : Type}.
  Context `{ProcessorState Job PState}.

  (* Consider any schedule... *)
  Variable sched : schedule PState.

  (* ...and suppose that jobs have a cost, an arrival time, and a notion of
     readiness. *)
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
  Context `{JobReady Job PState}.

  (* We observe that a given job is ready only if it is also incomplete... *)
  Lemma ready_implies_incomplete:
    ∀ j t, job_ready sched j t → ~~ completed_by sched j t.

  (* ...and lift this observation also to the level of whole schedules. *)
  Lemma completed_jobs_are_not_ready:
    jobs_must_be_ready_to_execute sched →
    completed_jobs_dont_execute sched.

  (* We further observe that completed jobs don't execute if scheduled jobs
     always receive non-zero service and cumulative service never exceeds job
     costs. *)
  Lemma ideal_progress_completed_jobs:
    ideal_progress_proc_model →
    (∀ j t, service sched j t ≤ job_cost j) →
    completed_jobs_dont_execute sched.

End CompletedJobs.