Library rt.implementation.uni.basic.schedule_tdma

Require Import rt.util.all rt.util.find_seq
               Arith.
Require Import rt.model.arrival.basic.job
               rt.model.arrival.basic.arrival_sequence
               rt.model.schedule.uni.basic.platform_tdma
               rt.model.arrival.basic.task rt.model.policy_tdma.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
Require Import rt.model.priority
               rt.analysis.uni.basic.tdma_rta_theory
               rt.model.schedule.uni.transformation.construction.
Require Import rt.implementation.job rt.implementation.task
               rt.implementation.arrival_sequence
               rt.implementation.uni.basic.schedule.


Module ConcreteSchedulerTDMA.

  Import Job ArrivalSequence UniprocessorSchedule SporadicTaskset Schedulability Priority
         ResponseTimeAnalysisTDMA PolicyTDMA ScheduleConstruction Platform_TDMA.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler BigOp.

  Section ImplementationTDMA.

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

    Variable arr_seq: arrival_sequence Job.

    Variable ts: {set Task}.

    Variable time_slot: TDMA_slot Task.

    Variable slot_order: TDMA_slot_order Task.

    Hypothesis H_arrival_times_are_consistent:
        arrival_times_are_consistent job_arrival arr_seq.

    Section JobSchedule.

        Variable sched: schedule Job.
        Variable t:time.

        Let is_pending := pending job_arrival job_cost sched.

        Definition pending_jobs:=
             [seq j <- jobs_arrived_up_to arr_seq t | is_pending j t].

        Let job_in_time_slot:=
          fun job ⇒ Task_in_time_slot ts slot_order (job_task job) time_slot t.

        Definition job_to_schedule :=
          findP job_in_time_slot pending_jobs.

      Section Lemmas.

        Hypothesis arr_seq_is_a_set:
          arrival_sequence_is_a_set arr_seq.

        Lemma pending_jobs_uniq:
          uniq pending_jobs.

        Lemma respects_FIFO:
          ∀ j j', j \in pending_jobs → j' \in pending_jobs →
          find (fun job ⇒ job==j') pending_jobs
           < find (fun job ⇒ job==j) pending_jobs →
          job_arrival j' ≤ job_arrival j.

        Lemma pending_job_in_penging_list:
          ∀ j, arrives_in arr_seq j →
          pending job_arrival job_cost sched j t →
          j \in pending_jobs.

        Lemma pendinglist_jobs_in_arr_seq:
          ∀ j, j \in pending_jobs →
           arrives_in arr_seq j.
      End Lemmas.

    End JobSchedule.

    Section SchedulerTDMA.

        Let empty_schedule : schedule Job := fun t ⇒ None.
        Definition scheduler_tdma:=
           build_schedule_from_prefixes job_to_schedule empty_schedule.

        Lemma scheduler_depends_only_on_prefix:
          ∀ sched1 sched2 t,
          (∀ t0, t0 < t → sched1 t0 = sched2 t0) →
          job_to_schedule sched1 t = job_to_schedule sched2 t.

      Lemma scheduler_uses_construction_function:
      ∀ t, scheduler_tdma t = job_to_schedule scheduler_tdma t.

    End SchedulerTDMA.


    Let sched:=
      scheduler_tdma.

    Theorem scheduler_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.

    Theorem scheduler_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

  End ImplementationTDMA.

End ConcreteSchedulerTDMA.