Forked from
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
808 commits behind the upstream repository.
-
Felipe Cerqueira authored
1) Definition of a generic model for job suspensions based on received service (e.g., job j_1 should suspend for 4ms as soon as service reaches 5ms). 2) Definition of the dynamic suspension model (i.e., cumulative suspension of job j_1 <= X). 3) Analysis of suspension-aware scheduling by inflation of job costs (via schedule reduction). In the literature, this is called suspension-oblivious analysis. 4) Analysis of suspension-aware scheduling by adjusting job jitter (via schedule reduction). 5) Proof of (weak) sustainability of job costs under suspension-aware scheduling. We show that if we increase the costs of all jobs while reducing their suspension times in a certain way, the response times of all jobs do not decrease. This has an important implication regarding worst-case schedules: if some schedulability analysis already accounts for the fact that job suspension times can vary from 0 to the task suspension bound, then it's perfectly safe to assume that jobs execute for their WCET. 6) Proof of sustainability of the cost of a single job under suspension-aware scheduling. That is, we show that increasing the cost of a single job does not reduce its own response time. (Note that this is a very basic result that applies to many work-conserving, JLFP schedulers. We don't claim anything about the response time of other jobs.)
Felipe Cerqueira authored1) Definition of a generic model for job suspensions based on received service (e.g., job j_1 should suspend for 4ms as soon as service reaches 5ms). 2) Definition of the dynamic suspension model (i.e., cumulative suspension of job j_1 <= X). 3) Analysis of suspension-aware scheduling by inflation of job costs (via schedule reduction). In the literature, this is called suspension-oblivious analysis. 4) Analysis of suspension-aware scheduling by adjusting job jitter (via schedule reduction). 5) Proof of (weak) sustainability of job costs under suspension-aware scheduling. We show that if we increase the costs of all jobs while reducing their suspension times in a certain way, the response times of all jobs do not decrease. This has an important implication regarding worst-case schedules: if some schedulability analysis already accounts for the fact that job suspension times can vary from 0 to the task suspension bound, then it's perfectly safe to assume that jobs execute for their WCET. 6) Proof of sustainability of the cost of a single job under suspension-aware scheduling. That is, we show that increasing the cost of a single job does not reduce its own response time. (Note that this is a very basic result that applies to many work-conserving, JLFP schedulers. We don't claim anything about the response time of other jobs.)
reduction.v 4.18 KiB
Require Import rt.util.all.
Require Import rt.model.priority rt.model.suspension.
Require Import rt.model.schedule.uni.susp.schedule.
Require Import rt.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
(* In this file, we propose a reduction that converts a suspension-aware
schedule to another suspension-aware schedule where the cost of a certain
job is inflated and its response time does not decrease. *)
Module SustainabilitySingleCost.
Import ScheduleWithSuspensions Suspension Priority ScheduleConstruction.
Section Reduction.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
(** Basic Setup & Setting*)
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and assume any (schedule-independent) JLDP policy. *)
Variable higher_eq_priority: JLDP_policy Job.
(* Next, consider any suspension-aware schedule of the arrival sequence... *)
Variable sched_susp: schedule Job.
(* ...and the associated job suspension times. *)
Variable job_suspension_duration: job_suspension Job.
(** Definition of the Reduction *)
(* Now we proceed with the reduction. Let j be the job to be analyzed. *)
Variable j: Job.
(* Next, consider any job cost inflation that does not decrease the cost of job j
and that preserves the cost of the remaining jobs. *)
Variable inflated_job_cost: Job -> time.
(** Schedule Construction *)
(* We are going to construct a new schedule that copies the original suspension-aware
schedule and tries to preserve the service received by job j, until the time when
it completes in the original schedule. *)
Section ScheduleConstruction.
(* First, we define the schedule construction function. *)
Section ConstructionStep.
(* For any time t, suppose that we have generated the schedule prefix in the
interval [0, t). Then, we must define what should be scheduled at time t. *)
Variable sched_prefix: schedule Job.
Variable t: time.
(* For simplicity, let's define some local names. *)
Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
Let job_is_suspended :=
suspended_at job_arrival inflated_job_cost job_suspension_duration sched_prefix.
Let actual_job_arrivals_up_to := jobs_arrived_up_to arr_seq.
(* Recall that a job is ready in the new schedule iff it is pending and not suspended. *)
Let job_is_ready j t := job_is_pending j t && ~~ job_is_suspended j t.
(* Then, consider the list of ready jobs at time t in the new schedule. *)
Definition ready_jobs :=
[seq j_other <- actual_job_arrivals_up_to t | job_is_ready j_other t].
(* From the list of ready jobs, we take one of the (possibly many)
highest-priority jobs, or None, in case there are no ready jobs. *)
Definition highest_priority_job := seq_min (higher_eq_priority t) ready_jobs.
(* Then, we construct the new schedule at time t as follows.
a) If the currently scheduled job in sched_susp is ready to execute in the new schedule
and has highest priority, pick that job.
b) Else, pick one of the highest priority ready jobs in the new schedule. *)
Definition build_schedule : option Job :=
if highest_priority_job is Some j_hp then
if sched_susp t is Some j_in_susp then
if job_is_ready j_in_susp t && higher_eq_priority t j_in_susp j_hp then
Some j_in_susp
else
Some j_hp
else Some j_hp
else None.
End ConstructionStep.
(* To conclude, starting from the empty schedule, ...*)
Let empty_schedule : schedule Job := fun t => None.
(* ...we use the recursive definition above to construct the new schedule. *)
Definition sched_susp_highercost :=
build_schedule_from_prefixes build_schedule empty_schedule.
End ScheduleConstruction.
End Reduction.
End SustainabilitySingleCost.