Library prosa.implementation.facts.generic_schedule


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

Welcome to Coq 8.11.2 (June 2020)

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

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.

Section GenericScheduleProperties.
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].
  Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.

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 572)
  
  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
            | succn t' => 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 579)
  
  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
            | succn t' => 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 move⇒ h 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 586)
  
  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
            | succn t' => 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 (succn h) t

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

  Proof.
    move⇒ h t RANGE.

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

1 subgoal (ID 589)
  
  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
            | succn t' => 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 (succn h) t

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

    rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // ⇒ EQ.

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

1 subgoal (ID 640)
  
  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
            | succn t' => schedule_up_to policy idle_state t'
            end : nat -> schedule PState
  h, t : nat
  RANGE : t <= h
  EQ : t = succn h
  ============================
  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 592)
  
  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
            | succn t' => 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.
    move⇒ h t.

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

1 subgoal (ID 594)
  
  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
            | succn t' => 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 604)
  
  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
            | succn t' => 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 607) is:
 schedule_up_to policy idle_state (succn h) t = idle_state

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

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

1 subgoal (ID 604)
  
  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
            | succn t' => 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 649)
  
  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
            | succn t' => 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 (ID 607)

subgoal 1 (ID 607) is:
 schedule_up_to policy idle_state (succn h) t = idle_state

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

}

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

1 subgoal (ID 607)
  
  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
            | succn t' => 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 : succn h < t
  ============================
  schedule_up_to policy idle_state (succn h) t = idle_state

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

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

1 subgoal (ID 607)
  
  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
            | succn t' => 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 : succn h < t
  ============================
  schedule_up_to policy idle_state (succn h) 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 691)
  
  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
            | succn t' => 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 : succn h < t
  ============================
  t <> succn h

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

      move⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 718)
  
  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
            | succn t' => 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 : succn h < t
  EQ : t = succn h
  ============================
  False

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

move: LT.

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

1 subgoal (ID 720)
  
  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
            | succn t' => 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 = succn h
  ============================
  succn h < 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 600)
  
  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
            | succn t' => 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.
    move⇒ h1 h2 LEQ t BEFORE.

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

1 subgoal (ID 605)
  
  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
            | succn t' => 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 618)
  
  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
            | succn t' => 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 <= succn n ->
  t <= h1 ->
  schedule_up_to policy idle_state h1 t =
  schedule_up_to policy idle_state (succn n) t

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

    move⇒ t' IH.

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

1 subgoal (ID 661)
  
  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
            | succn t' => 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 <= succn t' ->
  t <= h1 ->
  schedule_up_to policy idle_state h1 t =
  schedule_up_to policy idle_state (succn t') t

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

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

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

1 subgoal (ID 773)
  
  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
            | succn t' => 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 (succn t') t

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

    rewrite IH // schedule_up_to_widen //.

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

1 subgoal (ID 807)
  
  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
            | succn t' => 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.

End GenericScheduleProperties.