response_time_analysis/fixed_priority/
floating_nonpreemptive.rs

1//! RTA for FP scheduling with floating non-preemptive sections (**FP-NPS**)
2
3use crate::demand::{self, RequestBound};
4use crate::time::{Duration, Offset, Service};
5use crate::{fixed_point, supply};
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, RBF: RequestBound + ?Sized> {
11    /// The RBF upper-bounding the task's demand.
12    pub rbf: &'a RBF,
13
14    /// The `blocking_bound` must be a bound on the maximum priority
15    /// inversion caused by tasks of lower priority, which corresponds
16    /// to the maximum non-preemptive segment of any lower-priority
17    /// task.
18    pub blocking_bound: Service,
19}
20
21/// Try to find a response-time bound for a task under fixed-priority
22/// scheduling with floating non-preemptive regions on a dedicated
23/// uniprocessor.
24///
25/// The analysis assumes that all tasks are independent and that each
26/// is characterized by an arbitrary arrival curve and a WCET bound.
27/// The set of higher-or-equal-priority tasks is represented by
28/// `interfering_tasks`; the task under analysis is given by
29/// `tua`.
30///
31/// If no fixed point is found below the divergence limit given by
32/// `limit`, the function returns a
33/// [SearchFailure][fixed_point::SearchFailure] instead.
34///
35/// This analysis is an implementation of the corresponding  verified
36/// instantiation of [the abstract RTA of Bozhko and Brandenburg
37/// (ECRTS 2020)](https://drops.dagstuhl.de/opus/volltexte/2020/12385/pdf/LIPIcs-ECRTS-2020-22.pdf).
38/// See also [the Coq-verified instantiation](http://prosa.mpi-sws.org/branches/master/pretty/prosa.results.fixed_priority.rta.floating_nonpreemptive.html).
39#[allow(non_snake_case)]
40pub fn dedicated_uniproc_rta<RBF, InterferingRBF>(
41    tua: &TaskUnderAnalysis<RBF>,
42    interfering_tasks: &[InterferingRBF],
43    limit: Duration,
44) -> fixed_point::SearchResult
45where
46    InterferingRBF: RequestBound,
47    RBF: RequestBound + ?Sized,
48{
49    // This analysis is specific to dedicated uniprocessors.
50    let proc = supply::Dedicated::new();
51
52    // First, bound the maximum possible busy-window length.
53    let L = fixed_point::search(&proc, limit, |L| {
54        let interference_bound: Service = interfering_tasks
55            .iter()
56            .map(|rbf| rbf.service_needed(L))
57            .sum();
58
59        tua.blocking_bound + interference_bound + tua.rbf.service_needed(L)
60    })?;
61
62    // In the model with floating non-preemptive regions, there is no
63    // static information about the placement of preemption points in
64    // all jobs, i.e., it is impossible to predict when exactly a job
65    // will be preemptable. Thus, the only safe run-to-completion
66    // threshold is the task's WCET. The remaining cost after the
67    // run-to-completion threshold has been reached is then zero, so
68    // omitted here. See also:
69    // http://prosa.mpi-sws.org/branches/master/pretty/prosa.model.task.
70    // preemption.floating_nonpreemptive.html
71
72    // Second, define the RTA for a given offset A.
73    let rta = |A: Offset| {
74        // Define the RHS of the equation in theorem 31 of the aRTA paper,
75        // where AF = A + F.
76        let rhs = |AF: Duration| {
77            // demand of the task under analysis
78            let tua_demand = tua.rbf.service_needed(A.closed_since_time_zero());
79
80            // demand of all interfering tasks
81            let interfering_demand = interfering_tasks
82                .iter()
83                .map(|rbf| rbf.service_needed(AF))
84                .sum();
85
86            // considering `blocking_bound` to account for priority inversion
87            tua.blocking_bound + tua_demand + interfering_demand
88        };
89
90        // Find the solution A+F that is the least fixed point.
91        let AF = fixed_point::search(&proc, limit, rhs)?;
92        // Extract the corresponding bound.
93        let F = AF - A.since_time_zero();
94        Ok(F)
95    };
96
97    // Third, define the search space. The search space is given by
98    // A=0 and each step below L of the task under analysis's RBF.
99    // The case of A=0 is not handled explicitly since `step_offsets()`
100    // necessarily yields it.
101    let max_offset = Offset::from_time_zero(L);
102    let search_space = demand::step_offsets(tua.rbf).take_while(|A| *A < max_offset);
103
104    // Apply the offset-specific RTA to each offset in the search space and
105    // return the maximum response-time bound.
106    fixed_point::max_response_time(search_space.map(rta))
107}
response_time_analysis/fixed_priority/floating_nonpreemptive.rs

response_time_analysis/fixed_priority/
floating_nonpreemptive.rs
