response-time-analysis 0.3.2

//! RTA for EDF scheduling with floating non-preemptive sections (**EDF-NPS**)

use itertools::Itertools;

use crate::demand::{self, RequestBound};
use crate::time::{Duration, Offset, Service};
use crate::{fixed_point, supply};

/// The information about the task under analysis required to perform
/// the analysis.
/// Create one struct of this type to represent the task under analysis.
pub struct TaskUnderAnalysis<'a, RBF: RequestBound + ?Sized> {
    /// The RBF upper-bounding the task's demand.
    pub rbf: &'a RBF,
    /// The task's relative deadline.
    pub deadline: Duration,
}

/// The per-task information required to account for interfering tasks.
/// Create a struct of this type for each interfering task.
pub struct InterferingTask<'a, RBF: RequestBound + ?Sized> {
    /// The RBF upper-bounding the task's demand.
    pub rbf: &'a RBF,
    /// The task's relative deadline.    
    pub deadline: Duration,
    /// An upper bound on the task's maximum nonpreemptive section length.
    pub max_np_segment: Service,
}

/// Bound the maximum response time of a task under *earliest-deadline
/// first scheduling* with *floating nonpreemptive sections*
/// (**EDF-NPS**) on a dedicated, ideal uniprocessor.
///
/// That is, the analysis assumes that:
///
/// 1. The processor is available to the tasks 100% of the time.
/// 2. Scheduling overheads are negligible (i.e., already integrated
///    into the task parameters).
/// 3. Jobs are prioritized in order of increasing absolute deadlines
///    (with ties broken arbitrarily).
/// 4. Jobs can be preempted at any point outside of critical sections.
/// 5. Jobs are nonpreemptive within critical sections.
/// 6. Critical sections may appear at any point during a job's execution.
/// 7. The maximum critical-section length is known *a priori*.
///
/// The analysis further assumes that all tasks are independent and that each
/// task is characterized by an arbitrary arrival curve and a WCET
/// bound.
///
/// This analysis is an implementation of the corresponding  verified
/// instantiation of [the abstract RTA of Bozhko and Brandenburg
/// (ECRTS 2020)](https://drops.dagstuhl.de/opus/volltexte/2020/12385/pdf/LIPIcs-ECRTS-2020-22.pdf).
/// Refer to the [the Coq-verified instantiation](http://prosa.mpi-sws.org/branches/master/pretty/prosa.results.edf.rta.floating_nonpreemptive.html)
/// for the latest version.
///
/// The task for which a response-time bound is to be found is
/// represented by `tua`, the set of interfering tasks that share the
/// same processor is given by `other_tasks`.
///
/// If no fixed point is found below the divergence limit given by
/// `limit`, the function returns a
/// [SearchFailure][fixed_point::SearchFailure] instead.
#[allow(non_snake_case)]
pub fn dedicated_uniproc_rta<RBF1, RBF2>(
    tua: &TaskUnderAnalysis<RBF1>,
    other_tasks: &[InterferingTask<RBF2>],
    limit: Duration,
) -> fixed_point::SearchResult
where
    RBF1: RequestBound + ?Sized,
    RBF2: RequestBound + ?Sized,
{
    // This analysis is specific to dedicated uniprocessors.
    let proc = supply::Dedicated::new();

    // First, bound the maximum-possible busy-window length.
    let L = fixed_point::search(&proc, limit, |L| {
        let interference_bound: Service =
            other_tasks.iter().map(|ot| ot.rbf.service_needed(L)).sum();
        interference_bound + tua.rbf.service_needed(L)
    })?;

    // Second, define the RTA for a given offset A.
    let rta = |A: Offset| {
        // Bound on the priority inversion caused by jobs with lower priority.
        let blocking_bound = other_tasks
            .iter()
            .filter(|ot| {
                ot.deadline > tua.deadline + A.since_time_zero()
                    && ot.rbf.service_needed(Duration::epsilon()) > Service::none()
            })
            .map(|ot| ot.max_np_segment.saturating_sub(Service::epsilon()))
            .max()
            .unwrap_or_else(Service::none);

        // Define the RHS of the equation in theorem 31 of the aRTA paper,
        // where AF = A + F.
        let rhs = |AF: Duration| {
            // demand of the task under analysis
            let tua_demand = tua.rbf.service_needed(A.closed_since_time_zero());

            // demand of all interfering tasks
            let bound_on_total_hep_workload: Service = other_tasks
                .iter()
                .map(|ot| {
                    ot.rbf.service_needed(std::cmp::min(
                        AF,
                        (Offset::since_time_zero(A) + Duration::epsilon() + tua.deadline)
                            .saturating_sub(ot.deadline),
                    ))
                })
                .sum();

            blocking_bound + tua_demand + bound_on_total_hep_workload
        };

        // Find the solution A+F that is the least fixed point.
        let AF = fixed_point::search(&proc, limit, rhs)?;

        // Extract the corresponding bound.
        let F = AF.saturating_sub(A.since_time_zero());
        Ok(F)
    };

    // Third, define the search space. The search space is given by
    // A=0 and each step below L of the task under analysis's RBF.
    // The case of A=0 is not handled explicitly since `steps_iter()`
    // necessarily yields delta=1, which results in A=0 being
    // included in the search space.
    let max_offset = Offset::from_time_zero(L);
    let search_space_tua = demand::step_offsets(tua.rbf).take_while(|A| *A < max_offset);
    let search_space = other_tasks
        .iter()
        .map(|ot| {
            demand::step_offsets(ot.rbf)
                .map(move |delta| {
                    Offset::from_time_zero(
                        (delta + ot.deadline)
                            .since_time_zero()
                            .saturating_sub(tua.deadline),
                    )
                })
                .take_while(|A| *A < max_offset)
        })
        .kmerge()
        .merge(search_space_tua)
        .dedup();

    // Finally, apply the offset-specific RTA to each offset in the
    // search space and return the maximum response-time bound.
    fixed_point::max_response_time(search_space.map(rta))
}