response_time_analysis/edf/
fully_nonpreemptive.rs

1//! RTA for EDF scheduling with fully non-preemptive jobs (**NP-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 per-task information required to perform the analysis.
11pub struct Task<'a, AB: ArrivalBound + ?Sized> {
12    /// The task's worst-case execution time.
13    pub wcet: wcet::Scalar,
14    /// The task's arrival curve.
15    pub arrivals: &'a AB,
16    /// The task's relative deadline.
17    pub deadline: Duration,
18}
19
20impl<'a, AB: ArrivalBound + ?Sized> Task<'a, AB> {
21    fn rbf(&self) -> impl RequestBound + '_ {
22        demand::RBF::new(self.arrivals, self.wcet)
23    }
24}
25
26/// The information about the task under analysis required to perform
27/// the analysis.
28/// Create one struct of this type to represent the task under analysis.
29pub type TaskUnderAnalysis<'a, T> = Task<'a, T>;
30
31/// The per-task information required to account for interfering tasks.
32/// Create a struct of this type for each interfering task.
33pub type InterferingTask<'a, T> = Task<'a, T>;
34
35/// Bound the maximum response time of a task under *fully nonpreemptive
36/// earliest-deadline first* (**NP-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. Jobs have run-to-completion semantics: once started, a job will
47///    not relinquish the processor until it is complete.
48///
49/// The analysis further assumes that all tasks are independent and that each
50/// task is characterized by an arbitrary arrival curve and a WCET
51/// bound.
52///
53/// This analysis is an implementation of the corresponding  verified
54/// instantiation of [the abstract RTA of Bozhko and Brandenburg
55/// (ECRTS 2020)](https://drops.dagstuhl.de/opus/volltexte/2020/12385/pdf/LIPIcs-ECRTS-2020-22.pdf).
56/// Refer to the [the Coq-verified instantiation](http://prosa.mpi-sws.org/branches/master/pretty/prosa.results.edf.rta.fully_nonpreemptive.html)
57/// for the latest version.
58///
59/// The task for which a response-time bound is to be found is
60/// represented by `tua`, the set of interfering tasks that share the
61/// same processor is given by `other_tasks`.
62///
63/// If no fixed point is found below the divergence limit given by
64/// `limit`, the function returns a
65/// [SearchFailure][fixed_point::SearchFailure] instead.
66#[allow(non_snake_case)]
67pub fn dedicated_uniproc_rta<AB1, AB2>(
68    tua: &TaskUnderAnalysis<AB1>,
69    other_tasks: &[InterferingTask<AB2>],
70    limit: Duration,
71) -> fixed_point::SearchResult
72where
73    AB1: ArrivalBound + ?Sized,
74    AB2: ArrivalBound + ?Sized,
75{
76    // This analysis is specific to dedicated uniprocessors.
77    let proc = supply::Dedicated::new();
78
79    // For convenience, define the RBFs for the task under analysis...
80    let task_under_analysis = tua.rbf();
81    // ...and for the interfering tasks.
82    let rbfs: Vec<_> = other_tasks.iter().map(Task::rbf).collect();
83
84    // First, bound the maximum possible busy-window length.
85    let L = fixed_point::search(&proc, limit, |L| {
86        let interference_bound: Service = rbfs.iter().map(|rbf| rbf.service_needed(L)).sum();
87        interference_bound + task_under_analysis.service_needed(L)
88    })?;
89
90    // Second, define the RTA for a given offset A. To this end, we
91    // first define some components of the fixed-point equation.
92
93    // The run-to-completion threshold of the task under analysis. In
94    // the fully non-preemptive model, no job can be preempted prior to
95    // its completion. In other words, once a job starts running, it is
96    // guaranteed to finish. Thus, we can set the task-level
97    // run-to-completion threshold to epsilon.
98    // See also: http://prosa.mpi-sws.org/branches/master/pretty/prosa.model.task.preemption.fully_nonpreemptive.html#fully_nonpreemptive
99    let rtct = Service::epsilon();
100
101    // The remaining cost after the run-to-completion threshold has been
102    // reached.
103    let rem_cost = tua.wcet.wcet - rtct;
104
105    // Now define the offset-specific RTA.
106    let rta = |A: Offset| {
107        // Bound on the priority inversion caused by jobs with lower priority.
108        let blocking_bound = other_tasks
109            .iter()
110            .filter(|ot| {
111                ot.deadline > tua.deadline + A.since_time_zero()
112                    && ot.rbf().service_needed(Duration::epsilon()) > Service::none()
113            })
114            .map(|ot| ot.wcet.wcet.saturating_sub(Service::epsilon()))
115            .max()
116            .unwrap_or_else(Service::none);
117
118        // Define the RHS of the equation in theorem 31 of the aRTA paper,
119        // where AF = A + F.
120        let rhs = |AF: Duration| {
121            // demand of the task under analysis
122            let self_interference = task_under_analysis.service_needed(A.closed_since_time_zero());
123            let tua_demand = self_interference - rem_cost;
124
125            // demand of all interfering tasks
126            let bound_on_total_hep_workload: Service = other_tasks
127                .iter()
128                .map(|ot| {
129                    ot.rbf().service_needed(std::cmp::min(
130                        AF,
131                        (A.closed_since_time_zero() + tua.deadline).saturating_sub(ot.deadline),
132                    ))
133                })
134                .sum();
135
136            blocking_bound + tua_demand + bound_on_total_hep_workload
137        };
138
139        // Find the solution A+F that is the least fixed point.
140        let AF = fixed_point::search(&proc, limit, rhs)?;
141        // Extract the corresponding bound.
142        let F = AF.saturating_sub(A.since_time_zero());
143        Ok(F + Duration::from(rem_cost))
144    };
145
146    // Third, define the search space. The search space is given by
147    // A=0 and each step below L of the task under analysis's RBF.
148    // The case of A=0 is not handled explicitly since `steps_iter()`
149    // necessarily yields delta=1, which results in A=0 being
150    // included in the search space.
151    let max_offset = Offset::from_time_zero(L);
152    let search_space_tua =
153        demand::step_offsets(&task_under_analysis).take_while(|A| *A < max_offset);
154    let search_space = other_tasks
155        .iter()
156        .zip(rbfs.iter())
157        .map(|(ot, rbf)| {
158            demand::step_offsets(rbf)
159                .map(move |delta| {
160                    Offset::from_time_zero(
161                        (delta + ot.deadline)
162                            .since_time_zero()
163                            .saturating_sub(tua.deadline),
164                    )
165                })
166                .take_while(|A| *A < max_offset)
167        })
168        .kmerge()
169        .merge(search_space_tua)
170        .dedup();
171
172    // Finally, apply the offset-specific RTA to each offset in the
173    // search space and return the maximum response-time bound.
174    fixed_point::max_response_time(search_space.map(rta))
175}
response_time_analysis/edf/fully_nonpreemptive.rs

response_time_analysis/edf/
fully_nonpreemptive.rs
