Library prosa.implementation.facts.generic_schedule


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.implementation.definitions.generic_scheduler.
Require Export prosa.analysis.facts.transform.replace_at.

Properties of the Generic Reference Scheduler

This file establishes some facts about the generic reference scheduler that constructs a schedule via pointwise scheduling decisions based on a given policy and the preceding prefix.
For any type of jobs and type of schedule, ...
  Context {Job : JobType} {PState : Type}.
  Context `{ProcessorState Job PState}.

... any scheduling policy, and ...
  Variable policy : PointwisePolicy PState.

... any notion of idleness.
  Variable idle_state : PState.

For notational convenience, we define [prefix t] to denote the finite prefix considered when scheduling a job at time [t].
To begin with, we establish two simple rewriting lemmas for unrolling [schedule_up_to]. First, we observe that the allocation is indeed determined by the policy based on the preceding prefix.
  Lemma schedule_up_to_def:
     t,
      schedule_up_to policy idle_state t t = policy (prefix t) t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 25)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  ============================
  forall t : instant,
  schedule_up_to policy idle_state t t = policy (prefix t) t

----------------------------------------------------------------------------- *)


  Proof. by elim⇒ [|n IH]; rewrite [LHS]/schedule_up_to -/(schedule_up_to _) /replace_at; apply ifT.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


Qed.

Second, we note how to replace [schedule_up_to] in the general case with its definition.
  Lemma schedule_up_to_unfold:
     h t,
      schedule_up_to policy idle_state h t = replace_at (prefix h) h (policy (prefix h) h) t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 31)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  ============================
  forall h t : instant,
  schedule_up_to policy idle_state h t =
  replace_at (prefix h) h (policy (prefix h) h) t

----------------------------------------------------------------------------- *)


  Proof. by moveh t; rewrite [LHS]/schedule_up_to /prefix; elim: h.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


Qed.

Next, we observe that we can increase a prefix's horizon by one time unit without changing any allocations in the prefix.
  Lemma schedule_up_to_widen:
     h t,
      t h
      schedule_up_to policy idle_state h t = schedule_up_to policy idle_state h.+1 t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 37)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  ============================
  forall h t : nat,
  t <= h ->
  schedule_up_to policy idle_state h t =
  schedule_up_to policy idle_state h.+1 t

----------------------------------------------------------------------------- *)


  Proof.
    moveh t RANGE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h, t : nat
  RANGE : t <= h
  ============================
  schedule_up_to policy idle_state h t =
  schedule_up_to policy idle_state h.+1 t

----------------------------------------------------------------------------- *)


    rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // ⇒ EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h, t : nat
  RANGE : t <= h
  EQ : t = h.+1
  ============================
  False

----------------------------------------------------------------------------- *)


    now move: RANGE; rewrite EQ ltnn.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

After the horizon of a prefix, the schedule is still "empty", meaning that all instants are idle.
  Lemma schedule_up_to_empty:
     h t,
      h < t
      schedule_up_to policy idle_state h t = idle_state.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  ============================
  forall h t : nat,
  h < t -> schedule_up_to policy idle_state h t = idle_state

----------------------------------------------------------------------------- *)


  Proof.
    moveh t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h, t : nat
  ============================
  h < t -> schedule_up_to policy idle_state h t = idle_state

----------------------------------------------------------------------------- *)


    elim: h ⇒ [LT|h IH LT].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 54)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t : nat
  LT : 0 < t
  ============================
  schedule_up_to policy idle_state 0 t = idle_state

subgoal 2 (ID 57) is:
 schedule_up_to policy idle_state h.+1 t = idle_state

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t : nat
  LT : 0 < t
  ============================
  schedule_up_to policy idle_state 0 t = idle_state

----------------------------------------------------------------------------- *)


rewrite /schedule_up_to rest_of_schedule_invariant // ⇒ ZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 98)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t : nat
  LT : 0 < t
  ZERO : t = 0
  ============================
  False

----------------------------------------------------------------------------- *)


      now subst.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 57) is:
 schedule_up_to policy idle_state h.+1 t = idle_state

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t, h : nat
  IH : h < t -> schedule_up_to policy idle_state h t = idle_state
  LT : h.+1 < t
  ============================
  schedule_up_to policy idle_state h.+1 t = idle_state

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t, h : nat
  IH : h < t -> schedule_up_to policy idle_state h t = idle_state
  LT : h.+1 < t
  ============================
  schedule_up_to policy idle_state h.+1 t = idle_state

----------------------------------------------------------------------------- *)


rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ h t);
        first by apply IH ⇒ //; apply ltn_trans with (n := h.+1).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 140)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t, h : nat
  IH : h < t -> schedule_up_to policy idle_state h t = idle_state
  LT : h.+1 < t
  ============================
  t <> h.+1

----------------------------------------------------------------------------- *)


      moveEQ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 166)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t, h : nat
  IH : h < t -> schedule_up_to policy idle_state h t = idle_state
  LT : h.+1 < t
  EQ : t = h.+1
  ============================
  False

----------------------------------------------------------------------------- *)


move: LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  t, h : nat
  IH : h < t -> schedule_up_to policy idle_state h t = idle_state
  EQ : t = h.+1
  ============================
  h.+1 < t -> False

----------------------------------------------------------------------------- *)


      now rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

A crucial fact is that a prefix up to horizon [h1] is identical to a prefix up to a later horizon [h2] at times up to [h1].
  Lemma schedule_up_to_prefix_inclusion:
     h1 h2,
      h1 h2
       t,
        t h1
        schedule_up_to policy idle_state h1 t = schedule_up_to policy idle_state h2 t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 49)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  ============================
  forall h1 h2 : nat,
  h1 <= h2 ->
  forall t : nat,
  t <= h1 ->
  schedule_up_to policy idle_state h1 t =
  schedule_up_to policy idle_state h2 t

----------------------------------------------------------------------------- *)


  Proof.
    moveh1 h2 LEQ t BEFORE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h1, h2 : nat
  LEQ : h1 <= h2
  t : nat
  BEFORE : t <= h1
  ============================
  schedule_up_to policy idle_state h1 t =
  schedule_up_to policy idle_state h2 t

----------------------------------------------------------------------------- *)


    elim: h2 LEQ BEFORE; first by rewrite leqn0 ⇒ /eqP →.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 67)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h1, t : nat
  ============================
  forall n : nat,
  (h1 <= n ->
   t <= h1 ->
   schedule_up_to policy idle_state h1 t =
   schedule_up_to policy idle_state n t) ->
  h1 <= n.+1 ->
  t <= h1 ->
  schedule_up_to policy idle_state h1 t =
  schedule_up_to policy idle_state n.+1 t

----------------------------------------------------------------------------- *)


    movet' IH.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 109)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h1, t, t' : nat
  IH : h1 <= t' ->
       t <= h1 ->
       schedule_up_to policy idle_state h1 t =
       schedule_up_to policy idle_state t' t
  ============================
  h1 <= t'.+1 ->
  t <= h1 ->
  schedule_up_to policy idle_state h1 t =
  schedule_up_to policy idle_state t'.+1 t

----------------------------------------------------------------------------- *)


    rewrite leq_eqVlt ltnS ⇒ /orP [/eqP <-|LEQ] // t_H1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 219)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h1, t, t' : nat
  IH : h1 <= t' ->
       t <= h1 ->
       schedule_up_to policy idle_state h1 t =
       schedule_up_to policy idle_state t' t
  LEQ : h1 <= t'
  t_H1 : t <= h1
  ============================
  schedule_up_to policy idle_state h1 t =
  schedule_up_to policy idle_state t'.+1 t

----------------------------------------------------------------------------- *)


    rewrite IH // schedule_up_to_widen //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 252)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h1, t, t' : nat
  IH : h1 <= t' ->
       t <= h1 ->
       schedule_up_to policy idle_state h1 t =
       schedule_up_to policy idle_state t' t
  LEQ : h1 <= t'
  t_H1 : t <= h1
  ============================
  t <= t'

----------------------------------------------------------------------------- *)


    now apply (leq_trans t_H1).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

It follows that [generic_schedule] and [schedule_up_to] for a given horizon [h] share an identical prefix.
  Corollary schedule_up_to_identical_prefix:
     h t,
      t h.+1
      identical_prefix (schedule_up_to policy idle_state h) (generic_schedule policy idle_state) t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  ============================
  forall h t : nat,
  t <= h.+1 ->
  identical_prefix (schedule_up_to policy idle_state h)
    (generic_schedule policy idle_state) t

----------------------------------------------------------------------------- *)


  Proof.
    moveh t LE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 58)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h, t : nat
  LE : t <= h.+1
  ============================
  identical_prefix (schedule_up_to policy idle_state h)
    (generic_schedule policy idle_state) t

----------------------------------------------------------------------------- *)


    rewrite /identical_prefix /generic_schedulet' LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 66)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h, t : nat
  LE : t <= h.+1
  t' : nat
  LT : t' < t
  ============================
  schedule_up_to policy idle_state h t' =
  schedule_up_to policy idle_state t' t'

----------------------------------------------------------------------------- *)


    rewrite (schedule_up_to_prefix_inclusion t' h) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  policy : PointwisePolicy PState
  idle_state : PState
  prefix := fun t : nat =>
            match t with
            | 0 => empty_schedule idle_state
            | t'.+1 => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h, t : nat
  LE : t <= h.+1
  t' : nat
  LT : t' < t
  ============================
  t' <= h

----------------------------------------------------------------------------- *)


    by move: (leq_trans LT LE); rewrite ltnS.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End GenericScheduleProperties.