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