Library rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties

Require Import rt.util.all.
Require Import rt.model.priority rt.model.suspension.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
               rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.arrival.jitter.job.
Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
               rt.model.schedule.uni.workload
               rt.model.schedule.uni.response_time.
Require Import rt.model.schedule.uni.jitter.schedule
               rt.model.schedule.uni.jitter.valid_schedule
               rt.model.schedule.uni.jitter.platform.
Require Import rt.model.schedule.uni.susp.suspension_intervals
               rt.model.schedule.uni.susp.schedule
               rt.model.schedule.uni.susp.valid_schedule
               rt.model.schedule.uni.susp.platform.
Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule.
Require Import rt.model.schedule.uni.transformation.construction.

(* In this file, we prove several properties about the constructed jitter-aware schedule. *)
Module JitterScheduleProperties.

  Import Job SporadicTaskset Suspension Priority SuspensionIntervals Workload Service
         UniprocessorScheduleWithJitter Schedulability ResponseTime
         ScheduleConstruction ValidSuspensionAwareSchedule ValidJitterAwareSchedule.

  Module basic := schedule.UniprocessorSchedule.
  Module susp := ScheduleWithSuspensions.
  Module jitter_aware := Platform.
  Module susp_aware := PlatformWithSuspensions.
  Module job_jitter := JobWithJitter.
  Module reduction := JitterScheduleConstruction.

  Section ProvingScheduleProperties.

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

    (* Let ts be any task set to be analyzed. *)
    Variable ts: seq Task.

    (* Next, consider any consistent job arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.

    (* ...whose jobs come from task set ts. *)
    Hypothesis H_jobs_from_taskset:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

    (* Consider any FP policy that is reflexive, transitive and total. *)
    Variable higher_eq_priority: FP_policy Task.
    Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
    Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
    Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.

    (* Consider the original job and task costs from the suspension-aware schedule. *)
    Variable job_cost: Job → time.
    Variable task_cost: Task → time.

    (* Assume that jobs have associated suspension times. *)
    Variable job_suspension_duration: job_suspension Job.

    (* Next, consider any valid suspension-aware schedule of this arrival sequence.
       (Note: see rt.model.schedule.uni.susp.valid_schedule.v for details) *)
    Variable sched_susp: schedule Job.
    Hypothesis H_valid_schedule:
      valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
                                      job_suspension_duration job_cost sched_susp.

    (* Finally, recall the definition of a job response-time bound in sched_susp. *)
    Let job_response_time_in_sched_susp_bounded_by :=
      is_response_time_bound_of_job job_arrival job_cost sched_susp.

    (* Now we proceed with the reduction. Let j be the job to be analyzed. *)
    Variable j: Job.
    Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.

    (* For simplicity, let's give some local names for the parameters of this job... *)
    Let arr_j := job_arrival j.
    Let task_of_j := job_task j.

    (* ...and recall the definition of other higher-or-equal-priority tasks. *)
    Let other_hep_task tsk_other :=
      higher_eq_priority tsk_other task_of_j && (tsk_other != task_of_j).

    (* Moreover, assume that each job is associated a response-time bound R. *)
    Variable R: Job → time.

    (* Next, recall the jitter-aware schedule from the reduction. *)
    Let sched_jitter := reduction.sched_jitter job_arrival job_task arr_seq higher_eq_priority
                                               job_cost job_suspension_duration j R.
    Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
    Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j R.

    (* In this section, we prove that the jitter-aware schedule uses its construction function. *)
    Section PropertiesOfScheduleConstruction.

      Let build_schedule := reduction.build_schedule job_arrival job_task arr_seq higher_eq_priority
                                                     job_cost job_suspension_duration j R.

      (* Then, by showing that the construction function depends only on the previous service, ... *)
      Lemma sched_jitter_depends_only_on_service:
        ∀ sched1 sched2 t,
          (∀ j, service sched1 j t = service sched2 j t) →
          build_schedule sched1 t = build_schedule sched2 t.

      (* ...we infer that the generated schedule is indeed based on the construction function. *)
      Corollary sched_jitter_uses_construction_function:
        ∀ t,
          sched_jitter t = build_schedule sched_jitter t.

    End PropertiesOfScheduleConstruction.

    (* In this section, we prove that sched_jitter is a valid jitter-aware schedule. *)
    Section ScheduleIsValid.

      (* For simplicity, let's recall some definitions from the schedule construction. *)
      Let pending_jobs_other_than_j :=
        reduction.pending_jobs_other_than_j job_arrival job_task arr_seq higher_eq_priority
                                            job_cost job_suspension_duration j R sched_jitter.
      Let hp_job_other_than_j :=
        reduction.highest_priority_job_other_than_j job_arrival job_task arr_seq higher_eq_priority
                                                    job_cost job_suspension_duration j R sched_jitter.

      (* Also recall the definition of a valid jitter-aware schedule. *)
      Let is_valid_jitter_aware_schedule :=
        valid_jitter_aware_schedule job_arrival arr_seq job_higher_eq_priority
                                    inflated_job_cost job_jitter.

      (* First, we show that scheduled jobs come from the arrival sequence. *)
      Lemma sched_jitter_jobs_come_from_arrival_sequence:
        jobs_come_from_arrival_sequence sched_jitter arr_seq.

      (* Next, we show that jobs do not execute before their arrival times... *)
      Lemma sched_jitter_jobs_execute_after_jitter:
        jobs_execute_after_jitter job_arrival job_jitter sched_jitter.

      (* ...nor longer than their execution costs. *)
      Lemma sched_jitter_completed_jobs_dont_execute:
        completed_jobs_dont_execute inflated_job_cost sched_jitter.

      (* In addition, we prove that the schedule is (jitter-aware) work-conserving... *)
      Lemma sched_jitter_work_conserving:
        jitter_aware.work_conserving job_arrival inflated_job_cost job_jitter arr_seq sched_jitter.

      (* ...and respects task priorities. *)
      Lemma sched_jitter_respects_policy:
        jitter_aware.respects_FP_policy job_arrival inflated_job_cost job_jitter
                                        job_task arr_seq sched_jitter higher_eq_priority.

      (* From the properties above, we conclude that the generated schedule is valid. *)
      Corollary sched_jitter_is_valid: is_valid_jitter_aware_schedule sched_jitter.

      (* Finally, we show that the generated schedule does not pick job j if
         there are other pending higher-or-equal-priority jobs. *)
      Lemma sched_jitter_does_not_pick_j:
        ∀ j_hp t,
          arrives_in arr_seq j_hp →
          j_hp != j →
          pending job_arrival inflated_job_cost job_jitter sched_jitter j_hp t →
          higher_eq_priority (job_task j_hp) (job_task j) →
          ~~ scheduled_at sched_jitter j t.

    End ScheduleIsValid.

  End ProvingScheduleProperties.

End JitterScheduleProperties.