response_time_analysis/fixed_priority/
limited_preemptive.rs

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

response_time_analysis/fixed_priority/
limited_preemptive.rs
