response_time_analysis/edf/
limited_preemptive.rs

1//! RTA for EDF scheduling with limited-preemptive jobs (**LP-EDF**)
2
3use itertools::Itertools;
4
5use crate::arrival::ArrivalBound;
6use crate::demand::{self, RequestBound};
7use crate::time::{Duration, Offset, Service};
8use crate::{fixed_point, supply, wcet};
9
10/// The information about the task under analysis required to perform
11/// the analysis.
12/// Create one struct of this type to represent the task under analysis.
13pub struct TaskUnderAnalysis<'a, AB: ArrivalBound + ?Sized> {
14    /// The task's worst-case execution time.
15    pub wcet: wcet::Scalar,
16    /// The task's arrival curve.
17    pub arrivals: &'a AB,
18    /// The task's relative deadline.
19    pub deadline: Duration,
20    /// An upper bound on the length of the task's last segment.
21    pub last_np_segment: Service,
22}
23
24/// The per-task information required to account for interfering tasks.
25/// Create a struct of this type for each interfering task.
26pub struct InterferingTask<'a, RBF: RequestBound + ?Sized> {
27    /// The RBF upper-bounding the task's demand.
28    pub rbf: &'a RBF,
29    /// The task's relative deadline.
30    pub deadline: Duration,
31    /// An upper bound on the task's maximum segment length.
32    pub max_np_segment: Service,
33}
34
35/// Bound the maximum response time of a task under *limited-preemptive
36/// earliest-deadline first* (**LP-EDF**) scheduling on a dedicated,
37/// ideal uniprocessor.
38///
39/// That is, the analysis assumes that:
40///
41/// 1. The processor is available to the tasks 100% of the time.
42/// 2. Scheduling overheads are negligible (i.e., already integrated
43///    into the task parameters).
44/// 3. Jobs are prioritized in order of increasing absolute deadlines
45///    (with ties broken arbitrarily).
46/// 4. Each job executes a sequence of nonpreemptive segments.
47/// 5. Jobs cannot be preempted within segments.
48/// 6. Between any two segments there is a preemption point at which a
49///    job may be preempted.
50/// 7. The maximum segment length is known for all interfering tasks.
51/// 8. The length of the last segment is known for the task under analysis.
52///
53/// The analysis further assumes that all tasks are independent and that each
54/// task is characterized by an arbitrary arrival curve and a WCET
55/// bound.
56///
57/// This analysis is an implementation of the corresponding  verified
58/// instantiation of [the abstract RTA of Bozhko and Brandenburg
59/// (ECRTS 2020)](https://drops.dagstuhl.de/opus/volltexte/2020/12385/pdf/LIPIcs-ECRTS-2020-22.pdf).
60/// Refer to the [the Coq-verified instantiation](http://prosa.mpi-sws.org/branches/master/pretty/prosa.results.edf.rta.limited_preemptive.html)
61/// for the latest version.
62///
63/// The task for which a response-time bound is to be found is
64/// represented by `tua`, the set of interfering tasks that share the
65/// same processor is given by `other_tasks`.
66///
67/// If no fixed point is found below the divergence limit given by
68/// `limit`, the function returns a
69/// [SearchFailure][fixed_point::SearchFailure] instead.
70#[allow(non_snake_case)]
71pub fn dedicated_uniproc_rta<RBF, AB>(
72    tua: &TaskUnderAnalysis<AB>,
73    other_tasks: &[InterferingTask<RBF>],
74    limit: Duration,
75) -> fixed_point::SearchResult
76where
77    RBF: RequestBound + ?Sized,
78    AB: ArrivalBound + ?Sized,
79{
80    // This analysis is specific to dedicated uniprocessors.
81    let proc = supply::Dedicated::new();
82
83    // For convenience, define the RBF for the task under analysis.
84    let tua_rbf = demand::RBF::new(tua.arrivals, &tua.wcet);
85
86    // First, bound the maximum possible busy-window length.
87    let L = fixed_point::search(&proc, limit, |L| {
88        let interference_bound: Service =
89            other_tasks.iter().map(|ot| ot.rbf.service_needed(L)).sum();
90        interference_bound + tua_rbf.service_needed(L)
91    })?;
92
93    // Second, define the RTA for a given offset A. To this end, we
94    // first define some components of the fixed-point equation.
95
96    // The run-to-completion threshold of the task under analysis. Given
97    // limited preemptive case no job can be preempted after a job
98    // reaches its last non-preemptive segment.
99    // See also: https://prosa.mpi-sws.org/branches/master/pretty/prosa.model.task.preemption.limited_preemptive.html#limited_preemptive
100    let rtct = tua.wcet.wcet - (tua.last_np_segment - Service::epsilon());
101
102    // The remaining cost after the run-to-completion threshold has been
103    // reached.
104    let rem_cost = tua.wcet.wcet - rtct;
105
106    // Now define the offset-specific RTA.
107    let rta = |A: Offset| {
108        // Bound on the priority inversion caused by jobs with lower priority.
109        let blocking_bound = other_tasks
110            .iter()
111            .filter(|ot| {
112                ot.deadline > tua.deadline + A.since_time_zero()
113                    && ot.rbf.service_needed(Duration::epsilon()) > Service::none()
114            })
115            .map(|ot| ot.max_np_segment.saturating_sub(Service::epsilon()))
116            .max()
117            .unwrap_or_else(Service::none);
118
119        // Define the RHS of the equation in theorem 31 of the aRTA paper,
120        // where AF = A + F.
121        let rhs = |AF: Duration| {
122            // demand of the task under analysis
123            let self_interference = tua_rbf.service_needed(A.closed_since_time_zero());
124
125            let tua_demand = self_interference - rem_cost;
126
127            // demand of all interfering tasks
128            let bound_on_total_hep_workload: Service = other_tasks
129                .iter()
130                .map(|ot| {
131                    ot.rbf.service_needed(std::cmp::min(
132                        AF,
133                        (Offset::since_time_zero(A) + Duration::epsilon() + tua.deadline)
134                            .saturating_sub(ot.deadline),
135                    ))
136                })
137                .sum();
138
139            // considering `blocking_bound` to account for priority inversion.
140            blocking_bound + tua_demand + bound_on_total_hep_workload
141        };
142
143        // Find the solution A+F that is the least fixed point.
144        let AF = fixed_point::search(&proc, limit, rhs)?;
145        // Extract the corresponding bound.
146        let F = AF.saturating_sub(A.since_time_zero());
147
148        Ok(F + Duration::from(rem_cost))
149    };
150
151    // Third, define the search space. The search space is given by
152    // A=0 and each step below L of the task under analysis's RBF.
153    // The case of A=0 is not handled explicitly since `steps_iter()`
154    // necessarily yields delta=1, which results in A=0 being
155    // included in the search space.
156    let max_offset = Offset::from_time_zero(L);
157    let search_space_tua = demand::step_offsets(&tua_rbf).take_while(|A| *A < max_offset);
158    let search_space = other_tasks
159        .iter()
160        .map(|ot| {
161            demand::step_offsets(ot.rbf)
162                .map(move |delta| {
163                    Offset::from_time_zero(
164                        (delta + ot.deadline)
165                            .since_time_zero()
166                            .saturating_sub(tua.deadline),
167                    )
168                })
169                .take_while(|A| *A < max_offset)
170        })
171        .kmerge()
172        .merge(search_space_tua)
173        .dedup();
174
175    // Finally, apply the offset-specific RTA to each offset in the
176    // search space and return the maximum response-time bound.
177    fixed_point::max_response_time(search_space.map(rta))
178}
response_time_analysis/edf/limited_preemptive.rs

response_time_analysis/edf/
limited_preemptive.rs
