Commit a5f12a43 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Restructure directory + Add jitter-aware RTA

- Added definitions and implementation of jitter-aware RTA for
  uniprocessor scheduling.
- The Prosa directory was restructured to better accomodate the different
  types of arrival sequences and schedules.
parent 4c3e55e7
This diff is collapsed.
Require Import rt.util.all rt.util.divround.
Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.workload rt.model.global.response_time
rt.model.global.schedulability.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.apa.platform rt.model.apa.interference
rt.model.apa.affinity rt.model.apa.constrained_deadlines.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.platform rt.model.schedule.apa.interference
rt.model.schedule.apa.affinity rt.model.schedule.apa.constrained_deadlines.
Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound_edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.response_time rt.model.global.schedulability
rt.model.global.workload.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.apa.platform rt.model.apa.constrained_deadlines
rt.model.apa.interference rt.model.apa.affinity.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.schedulability
rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.platform rt.model.schedule.apa.constrained_deadlines
rt.model.schedule.apa.interference rt.model.schedule.apa.affinity.
Require Import rt.analysis.apa.workload_bound
rt.analysis.apa.interference_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.analysis.apa.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all rt.util.divround.
Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.workload rt.model.global.response_time
rt.model.global.schedulability.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.apa.platform rt.model.apa.interference
rt.model.apa.interference_edf rt.model.apa.affinity.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.platform rt.model.schedule.apa.interference
rt.model.schedule.apa.interference_edf rt.model.schedule.apa.affinity.
Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.priority.
Require Import rt.model.global.workload.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.apa.interference rt.model.apa.affinity.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.interference rt.model.schedule.apa.affinity.
Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all rt.util.divround.
Require Import rt.model.task rt.model.job rt.model.task_arrival.
Require Import rt.model.global.response_time rt.model.global.schedulability
rt.model.global.workload.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.schedulability
rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
Require Import rt.model.global.workload rt.model.global.schedulability
rt.model.global.response_time.
Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
rt.model.global.basic.interference rt.model.global.basic.platform
rt.model.global.basic.constrained_deadlines.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
rt.model.schedule.global.response_time.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
rt.model.schedule.global.basic.interference rt.model.schedule.global.basic.platform
rt.model.schedule.global.basic.constrained_deadlines.
Require Import rt.analysis.global.basic.workload_bound rt.analysis.global.basic.interference_bound_edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.workload rt.model.global.schedulability
rt.model.global.response_time.
Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
rt.model.global.basic.constrained_deadlines rt.model.global.basic.interference.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
rt.model.schedule.global.response_time.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
rt.model.schedule.global.basic.constrained_deadlines rt.model.schedule.global.basic.interference.
Require Import rt.analysis.global.basic.workload_bound
rt.analysis.global.basic.interference_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.analysis.global.basic.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
Require Import rt.model.global.response_time rt.model.global.workload
rt.model.global.schedulability.
Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
rt.model.global.basic.interference rt.model.global.basic.interference_edf.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
rt.model.schedule.global.basic.interference rt.model.schedule.global.basic.interference_edf.
Require Import rt.analysis.global.basic.workload_bound
rt.analysis.global.basic.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.priority.
Require Import rt.model.global.workload.
Require Import rt.model.global.basic.schedule rt.model.global.basic.interference.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference.
Require Import rt.analysis.global.basic.workload_bound
rt.analysis.global.basic.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.task_arrival.
Require Import rt.model.global.workload rt.model.global.response_time
rt.model.global.schedulability.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.workload rt.model.global.schedulability
rt.model.global.response_time.
Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
rt.model.global.jitter.platform rt.model.global.jitter.interference
rt.model.global.jitter.constrained_deadlines.
Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
rt.model.schedule.global.response_time.
Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
rt.model.schedule.global.jitter.platform rt.model.schedule.global.jitter.interference
rt.model.schedule.global.jitter.constrained_deadlines.
Require Import rt.analysis.global.jitter.workload_bound
rt.analysis.global.jitter.interference_bound_edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.workload rt.model.global.response_time
rt.model.global.schedulability.
Require Import rt.model.global.jitter.job rt.model.global.jitter.interference
rt.model.global.jitter.schedule rt.model.global.jitter.platform
rt.model.global.jitter.constrained_deadlines.
Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.interference
rt.model.schedule.global.jitter.schedule rt.model.schedule.global.jitter.platform
rt.model.schedule.global.jitter.constrained_deadlines.
Require Import rt.analysis.global.jitter.workload_bound
rt.analysis.global.jitter.interference_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.arrival_sequence rt.model.priority.
Require Import rt.model.global.jitter.schedule rt.model.global.jitter.interference.
Require Import rt.model.arrival.basic.arrival_sequence rt.model.priority.
Require Import rt.model.schedule.global.jitter.schedule rt.model.schedule.global.jitter.interference.
Require Import rt.analysis.global.jitter.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.response_time rt.model.global.workload
rt.model.global.schedulability.
Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
rt.model.global.jitter.platform rt.model.global.jitter.interference
rt.model.global.jitter.interference_edf.
Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
rt.model.schedule.global.jitter.platform rt.model.schedule.global.jitter.interference
rt.model.schedule.global.jitter.interference_edf.
Require Import rt.analysis.global.jitter.workload_bound rt.analysis.global.jitter.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.priority.
Require Import rt.model.global.workload.
Require Import rt.model.global.jitter.schedule rt.model.global.jitter.interference.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.jitter.schedule rt.model.schedule.global.jitter.interference.
Require Import rt.analysis.global.jitter.workload_bound rt.analysis.global.jitter.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.task_arrival.
Require Import rt.model.global.workload rt.model.global.response_time
rt.model.global.schedulability.
Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBoundJitter.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
Require Import rt.model.global.workload rt.model.global.schedulability
rt.model.global.response_time.
Require Import rt.model.global.basic.schedule rt.model.global.basic.interference
rt.model.global.basic.platform.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
rt.model.schedule.global.response_time.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference
rt.model.schedule.global.basic.platform.
Require Import rt.analysis.global.parallel.workload_bound
rt.analysis.global.parallel.interference_bound_edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.task_arrival
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival
rt.model.priority.
Require Import rt.model.global.workload rt.model.global.schedulability
rt.model.global.response_time.
Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
rt.model.global.basic.constrained_deadlines rt.model.global.basic.interference.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
rt.model.schedule.global.response_time.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
rt.model.schedule.global.basic.constrained_deadlines rt.model.schedule.global.basic.interference.
Require Import rt.analysis.global.parallel.workload_bound rt.analysis.global.parallel.interference_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.analysis.global.parallel.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
Require Import rt.model.global.response_time rt.model.global.workload
rt.model.global.schedulability.
Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
rt.model.global.basic.interference rt.model.global.basic.interference_edf.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
rt.model.schedule.global.basic.interference rt.model.schedule.global.basic.interference_edf.
Require Import rt.analysis.global.parallel.workload_bound
rt.analysis.global.parallel.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Require Import rt.util.all.
Require Import rt.model.priority.
Require Import rt.model.global.workload.
Require Import rt.model.global.basic.schedule rt.model.global.basic.interference.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference.
Require Import rt.analysis.global.parallel.workload_bound rt.analysis.global.parallel.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.task_arrival.
Require Import rt.model.global.response_time rt.model.global.workload
rt.model.global.schedulability.
Require Import rt.model.global.basic.schedule.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.arrival_sequence rt.model.priority
rt.model.task_arrival.
Require Import rt.model.uni.schedule rt.model.uni.schedulability rt.model.uni.response_time.
Require Import rt.model.uni.basic.platform.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority
rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability rt.model.schedule.uni.response_time.
Require Import rt.model.schedule.uni.basic.platform.
Require Import rt.analysis.uni.basic.workload_bound_fp rt.analysis.uni.basic.fp_rta_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path ssrfun.
......
Require Import rt.util.all.
Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival
rt.model.arrival_bounds.
Require Import rt.model.uni.schedule_of_task rt.model.uni.workload
rt.model.uni.schedulability rt.model.uni.response_time
rt.model.uni.service.
Require Import rt.model.uni.basic.busy_interval rt.model.uni.basic.platform.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival
rt.model.arrival.basic.arrival_bounds.
Require Import rt.model.schedule.uni.schedule_of_task rt.model.schedule.uni.workload
rt.model.schedule.uni.schedulability rt.model.schedule.uni.response_time
rt.model.schedule.uni.service.
Require Import rt.model.schedule.uni.basic.busy_interval rt.model.schedule.uni.basic.platform.
Require Import rt.analysis.uni.basic.workload_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.priority
rt.model.task_arrival rt.model.arrival_bounds.
Require Import rt.model.uni.schedule rt.model.uni.workload.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority
rt.model.arrival.basic.task_arrival rt.model.arrival.basic.arrival_bounds.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.workload.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module WorkloadBoundFP.
......
This diff is collapsed.
Require Import rt.util.all.
Require Import rt.model.priority.
Require Import rt.model.arrival.basic.task.
Require Import rt.model.arrival.jitter.job rt.model.arrival.jitter.task_arrival
rt.model.arrival.jitter.arrival_sequence rt.model.arrival.jitter.arrival_bounds.
Require Import rt.model.schedule.uni.schedule_of_task rt.model.schedule.uni.service
rt.model.schedule.uni.schedulability rt.model.schedule.uni.response_time.
Require Import rt.model.schedule.uni.jitter.schedule
rt.model.schedule.uni.jitter.workload
rt.model.schedule.uni.jitter.busy_interval
rt.model.schedule.uni.jitter.platform.
Require Import rt.analysis.uni.jitter.workload_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module ResponseTimeAnalysisFP.
Import ArrivalSequenceWithJitter JobWithJitter TaskArrivalWithJitter ArrivalBounds
UniprocessorScheduleWithJitter ScheduleOfTask SporadicTaskset Priority
ResponseTime WorkloadBoundFP Platform Schedulability BusyInterval Workload Service.
(* In this section, we prove that any fixed point in the RTA for jitter-aware
uniprocessor FP scheduling is a response-time bound. *)
Section ResponseTimeBound.
Context {SporadicTask: eqType}.
Variable task_cost: SporadicTask -> time.
Variable task_period: SporadicTask -> time.
Variable task_deadline: SporadicTask -> time.
Variable task_jitter: SporadicTask -> time.
Context {Job: eqType}.
Variable job_cost: Job -> time.
Variable job_deadline: Job -> time.
Variable job_jitter: Job -> time.
Variable job_task: Job -> SporadicTask.
(* Assume any job arrival sequence without duplicates... *)
Context {arr_seq: arrival_sequence Job}.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_sporadic_job_with_jitter task_cost task_deadline task_jitter
job_cost job_deadline job_jitter job_task j.
(* Consider a task set ts where all tasks have valid parameters... *)
Variable ts: seq SporadicTask.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ... and assume that all jobs in the arrival sequence come from the task set. *)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
(* Next, consider any uniprocessor schedule such that...*)
Variable sched: schedule arr_seq.
(* ...jobs do not execute before the jitter has passed nor after completion. *)
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter job_jitter sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* Consider any FP policy that indicates a higher-or-equal priority relation,
where the relation is reflexive and transitive. *)
Variable higher_eq_priority: FP_policy SporadicTask.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
(* Next, assume that the schedule is a jitter-aware, work-conserving FP schedule. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
Hypothesis H_respects_fp_policy:
respects_FP_policy job_cost job_jitter job_task sched higher_eq_priority.
(* Now we proceed with the analysis.
Let tsk be any task in ts that is to be analyzed. *)
Variable tsk: SporadicTask.
Hypothesis H_tsk_in_ts: tsk \in ts.
(* Recall the definition of response-time bound and the total workload bound W
for higher-or-equal-priority tasks (with respect to tsk). *)
Let response_time_bounded_by :=
is_response_time_bound_of_task job_cost job_task sched.
Let W := total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
(* Let R be any positive fixed point of the response-time recurrence. *)
Variable R: time.
Hypothesis H_R_positive: R > 0.
Hypothesis H_response_time_is_fixed_point: R = W R.
(* Since R = W R bounds the workload of higher-or-equal priority and actual arrival
time in any interval of length R, it follows from the busy-interval lemmas that
R bounds the response-time of job j.
(For more details, see model/uni/jitter/busy_interval.v and
analysis/uni/jitter/workload_bound_fp.v.) *)
Theorem uniprocessor_response_time_bound_fp:
response_time_bounded_by tsk (task_jitter tsk + R).
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job,
valid_sporadic_taskset, is_valid_sporadic_task in *.
rename H_response_time_is_fixed_point into FIX,
H_valid_task_parameters into PARAMS,