response_time_analysis/fixed_priority/
fully_preemptive.rs

1//! RTA for FP scheduling with fully preemptive jobs (**FP**)
2
3use crate::demand::{self, RequestBound};
4use crate::time::{Duration, Offset, Service};
5use crate::{fixed_point, supply};
6
7/// Try to find a response-time bound for a task under
8/// fully-preemptive fixed-priority scheduling on a dedicated
9/// uniprocessor.
10///
11/// The analysis assumes that all tasks are independent and that each
12/// is characterized by an arbitrary arrival curve and a WCET bound.
13/// The total higher-or-equal-priority interference is represented by
14/// `interfering_tasks`, the task under analysis is given by `tua`.
15///
16/// If no fixed point is found below the divergence limit given by
17/// `limit`, the function returns a
18/// [SearchFailure][fixed_point::SearchFailure] instead.
19///
20/// This analysis is an implementation of the corresponding  verified
21/// instantiation of [the abstract RTA of Bozhko and Brandenburg
22/// (ECRTS 2020)](https://drops.dagstuhl.de/opus/volltexte/2020/12385/pdf/LIPIcs-ECRTS-2020-22.pdf).
23/// See also [the Coq-verified instantiation](http://prosa.mpi-sws.org/branches/master/pretty/prosa.results.fixed_priority.rta.fully_preemptive.html).
24#[allow(non_snake_case)]
25pub fn dedicated_uniproc_rta<TaskUnderAnalysisRBF, InterferingRBF>(
26    tua: &TaskUnderAnalysisRBF,
27    interfering_tasks: &[InterferingRBF],
28    limit: Duration,
29) -> fixed_point::SearchResult
30where
31    TaskUnderAnalysisRBF: RequestBound + ?Sized,
32    InterferingRBF: RequestBound,
33{
34    // This analysis is specific to dedicated uniprocessors.
35    let proc = supply::Dedicated::new();
36
37    // First, bound the maximum possible busy-window length.
38    let L = fixed_point::search(&proc, limit, |L| {
39        let interference_bound: Service = interfering_tasks
40            .iter()
41            .map(|rbf| rbf.service_needed(L))
42            .sum();
43        interference_bound + tua.service_needed(L)
44    })?;
45
46    // Second, define the RTA for a given offset A.
47    let rta = |A: Offset| {
48        // Define the RHS of the equation in theorem 31 of the aRTA paper,
49        // where AF = A + F.
50        let rhs = |AF: Duration| {
51            // demand of the task under analysis
52            let tua_demand = tua.service_needed(A.closed_since_time_zero());
53
54            // demand of all interfering tasks
55            let interfering_demand = interfering_tasks
56                .iter()
57                .map(|rbf| rbf.service_needed(AF))
58                .sum();
59
60            tua_demand + interfering_demand
61        };
62
63        // Find the solution A+F that is the least fixed point.
64        let AF = fixed_point::search(&proc, limit, rhs)?;
65        // Extract the corresponding bound.
66        let F = AF - A.since_time_zero();
67        Ok(F)
68    };
69
70    // Third, define the search space. The search space is given by
71    // A=0 and each step below L of the task under analysis's RBF.
72    // The case of A=0 is not handled explicitly since `step_offsets()`
73    // necessarily yields it.
74    let max_offset = Offset::from_time_zero(L);
75    let search_space = demand::step_offsets(tua).take_while(|A| *A < max_offset);
76
77    // Apply the offset-specific RTA to each offset in the search space and
78    // return the maximum response-time bound.
79    fixed_point::max_response_time(search_space.map(rta))
80}
response_time_analysis/fixed_priority/fully_preemptive.rs

response_time_analysis/fixed_priority/
fully_preemptive.rs
