response_time_analysis/edf/
fully_preemptive.rs

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

response_time_analysis/edf/
fully_preemptive.rs
