Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]


Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]


(** * Limited-Preemptive Task Model *)

(** In this module, we instantiate the task model in which jobs can be
    preempted only at certain preemption points. *)

(** ** Model Validity *)

(** To begin with, we introduce requirements that the function
    [task_max_nonpr_segment] must satisfy to be coherent with the
    limited-preemptive task model. *)
Section ValidModelWithFixedPreemptionPoints.

  (** Consider any type of tasks with WCET bounds and given preemption points ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskPreemptionPoints Task}.

  (**  ... and any type of jobs associated with these tasks, ... *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  (** ... where each job has an arrival time, an execution cost, and some
      preemption points. *)
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobPreemptionPoints Job}.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.

  (** Consider an arbitrary task set [ts]. *)
  Variable ts : TaskSet Task.

  (** First, we describe structural properties that a sequence of preemption
      points of a task should satisfy. *)

  (** (1) We require the sequence of preemption points to contain the beginning ... *)
  Definition task_beginning_of_execution_in_preemption_points :=
    forall tsk, tsk \in ts -> first0 (task_preemption_points tsk) = 0.

  (** ... and (2) the end of execution. *)
  Definition task_end_of_execution_in_preemption_points :=
    forall tsk, tsk \in ts -> last0 (task_preemption_points tsk) = task_cost tsk.

  (** (3) Furthermore, we require the sequence of preemption points to be a
          non-decreasing sequence. *)
  Definition nondecreasing_task_preemption_points :=
    forall tsk, tsk \in ts -> nondecreasing_sequence (task_preemption_points tsk).

  (** (4) We also require the number of nonpreemptive segments of a job to be
          equal to the number of nonpreemptive segments of its task. Note that
          some of nonpreemptive segments of a job can have zero length;
          nonetheless the number of segments should match. *)
  Definition consistent_job_segment_count :=
    forall j,
      arrives_in arr_seq j ->
      size (job_preemptive_points j) = size (task_preemption_points (job_task j)).

  (** (5) We require the lengths of the nonpreemptive segments of a job to be
          bounded by the lengths of the corresponding segments of its task.  *)
  Definition job_respects_segment_lengths :=
    forall j n,
      arrives_in arr_seq j ->
      nth 0 (distances (job_preemptive_points j)) n
      <= nth 0 (distances (task_preemption_points (job_task j))) n.

  (** (6) Lastly, we ban empty nonpreemptive segments at the task level. *)
  Definition task_segments_are_nonempty :=
    forall tsk n,
      (tsk \in ts) ->
      n < size (distances (task_preemption_points tsk)) ->
      ε <= nth 0 (distances (task_preemption_points tsk)) n.

  (** We define a valid task-level model with fixed preemption points as the
      conjunction of the hypotheses above. *)
  Definition valid_fixed_preemption_points_task_model :=
    task_beginning_of_execution_in_preemption_points /\
    task_end_of_execution_in_preemption_points /\
    nondecreasing_task_preemption_points /\
    consistent_job_segment_count /\
    job_respects_segment_lengths /\
    task_segments_are_nonempty.

  (** Finally, a model with fixed preemption points is valid if it is both valid
      a the job and task levels. *)
  Definition valid_fixed_preemption_points_model :=
    valid_limited_preemptions_job_model arr_seq /\
    valid_fixed_preemption_points_task_model.

End ValidModelWithFixedPreemptionPoints.

(** ** Run-to-Completion Threshold *)

(** In this section, we instantiate the task-level run-to-completion threshold
    for the task model with fixed preemption points. *)
Section TaskRTCThresholdLimitedPreemptions.

  (** Consider any type of tasks with WCET bounds and fixed preemption points. *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskPreemptionPoints Task}.

  (** Given fixed preemption points, no job can be preempted after a job
      reaches its last non-preemptive segment. Thus, we can set the task-level
      run-to-completion threshold to [task_cost tsk - (task_last_nonpr_seg tsk - ε)],
      which safely bounds [job_cost j - (job_last_nonpr_seg j - ε)]. *)
  Definition limited_preemptions_rtc_threshold : TaskRunToCompletionThreshold Task :=
    fun tsk : Task => task_cost tsk - (task_last_nonpr_segment tsk - ε).

End TaskRTCThresholdLimitedPreemptions.