response_time_analysis/fixed_priority/
fully_nonpreemptive.rs

1//! RTA for FP scheduling with fully non-preemptive jobs (**NP-FP**)
2use crate::arrival::ArrivalBound;
3use crate::demand::{self, RequestBound};
4use crate::time::{Duration, Offset, Service};
5use crate::{fixed_point, supply, wcet};
6
7/// The information about the task under analysis required to perform
8/// the analysis.
9/// Create one struct of this type to represent the task under analysis.
10pub struct TaskUnderAnalysis<'a, AB: ArrivalBound + ?Sized> {
11    /// The task's WCET.
12    pub wcet: wcet::Scalar,
13
14    /// The task's arrival bound.
15    pub arrivals: &'a AB,
16
17    /// The `blocking_bound` must be a bound on the maximum priority
18    /// inversion caused by tasks of lower priority, which corresponds
19    /// to the maximum WCET of any lower-priority task.
20    pub blocking_bound: Service,
21}
22
23/// Try to find a response-time bound for a task under
24/// fully-nonpreemptive fixed-priority scheduling on a dedicated
25/// uniprocessor.
26///
27/// The analysis assumes that all tasks are independent and that each
28/// is characterized by an arbitrary arrival curve and a WCET bound.
29/// The set of higher-or-equal-priority tasks is represented by
30/// `interfering_tasks`; the task under analysis is given by
31/// `tua`.
32///
33/// If no fixed point is found below the divergence limit given by
34/// `limit`, the function returns a
35/// [SearchFailure][fixed_point::SearchFailure] instead.
36///
37/// This analysis is an implementation of the corresponding  verified
38/// instantiation of [the abstract RTA of Bozhko and Brandenburg
39/// (ECRTS 2020)](https://drops.dagstuhl.de/opus/volltexte/2020/12385/pdf/LIPIcs-ECRTS-2020-22.pdf).
40/// See also [the Coq-verified instantiation](http://prosa.mpi-sws.org/branches/master/pretty/prosa.results.fixed_priority.rta.fully_nonpreemptive.html).
41#[allow(non_snake_case)]
42pub fn dedicated_uniproc_rta<InterferingRBF, AB>(
43    tua: &TaskUnderAnalysis<AB>,
44    interfering_tasks: &[InterferingRBF],
45    limit: Duration,
46) -> fixed_point::SearchResult
47where
48    InterferingRBF: RequestBound,
49    AB: ArrivalBound + ?Sized,
50{
51    // This analysis is specific to dedicated uniprocessors.
52    let proc = supply::Dedicated::new();
53
54    // For convenience, define the RBF for the task under analysis.
55    let tua_rbf = demand::RBF::new(tua.arrivals, tua.wcet);
56
57    // First, bound the maximum possible busy-window length.
58    let L = fixed_point::search(&proc, limit, |L| {
59        let interference_bound: Service = interfering_tasks
60            .iter()
61            .map(|rbf| rbf.service_needed(L))
62            .sum();
63
64        tua.blocking_bound + interference_bound + tua_rbf.service_needed(L)
65    })?;
66
67    // Second, define the RTA for a given offset A. To this end, we
68    // define some trivial components of the fixed-point equation to
69    // implement the RTA given in the aRTA paper as literally as
70    // possible.
71
72    // The run-to-completion threshold of the task under analysis,
73    //
74    // See also: http://prosa.mpi-sws.org/branches/master/pretty/prosa.model.task.preemption.fully_nonpreemptive.html#fully_nonpreemptive
75    // In the fully non-preemptive model, no job can be preempted
76    // prior to its completion. In other words, once a job starts
77    // running, it is guaranteed to finish. Thus, we can set the
78    // task-level run-to-completion threshold to epsilon.
79    let rtct = Service::epsilon();
80    // The remaining cost after the run-to-completion threshold has been reached.
81    let rem_cost = tua.wcet.wcet - rtct;
82
83    // Now define the offset-specific RTA.
84    let rta = |A: Offset| {
85        // Define the RHS of the equation in theorem 31 of the aRTA paper,
86        // where AF = A + F.
87        let rhs = |AF: Duration| {
88            // demand of the task under analysis
89            let self_interference = tua_rbf.service_needed(A.closed_since_time_zero());
90            let tua_demand = self_interference - rem_cost;
91
92            // demand of all interfering tasks
93            let interfering_demand = interfering_tasks
94                .iter()
95                .map(|rbf| rbf.service_needed(AF))
96                .sum();
97
98            // considering `blocking_bound` to account for priority inversion
99            tua.blocking_bound + tua_demand + interfering_demand
100        };
101
102        // Find the solution A+F that is the least fixed point.
103        let AF = fixed_point::search(&proc, limit, rhs)?;
104        // Extract the corresponding bound.
105        let F = AF - A.since_time_zero();
106        Ok(F + Duration::from(rem_cost))
107    };
108
109    // Third, define the search space. The search space is given by
110    // A=0 and each step below L of the task under analysis's RBF.
111    // The case of A=0 is not handled explicitly since `step_offsets()`
112    // necessarily yields it.
113    let max_offset = Offset::from_time_zero(L);
114    let search_space = demand::step_offsets(&tua_rbf).take_while(|A| *A < max_offset);
115
116    // Apply the offset-specific RTA to each offset in the search space and
117    // return the maximum response-time bound.
118    fixed_point::max_response_time(search_space.map(rta))
119}
response_time_analysis/fixed_priority/fully_nonpreemptive.rs

response_time_analysis/fixed_priority/
fully_nonpreemptive.rs
