In the correspondence article A Correction of the Reduction-Based Schedulability Analysis for APA Scheduling, we restate and rectify an overgeneralized claim in Section 4 of the paper Multiprocessor Real-Time Scheduling with Arbitrary Processor Affinities: From Practice to Theory by Gujarati et al. (2015). To support the correction with the highest degree of confidence, we have mechanized the key results using the Prosa framework. In the following, we provide an overview to the formalization and highlight the main results and proofs, as well as the underlying assumptions.
For an introduction to Prosa, we suggest checking out the Artifact Evaluation. In case of problems or further questions, feel free to ask questions on the mailing list.
In this section, we present the main schedulability results and provide some guidance on how to locate the proofs. For convenience and as a navigation aid, the referenced statements are reproduced here.
To understand how the Prosa directory is organized, please refer to the table of contents.
A1) Definition of the interference bound for work-conserving schedulers (with slack updates).
A2) Proof of correctness of the interference bound for work-conserving schedulers.
A3) Definition of the interference bound for EDF scheduling (with slack updates).
A4) Proof of correctness of the interference bound for EDF scheduling. (Note that even though the lemma statement is the same as for the standard sporadic task model, the definition of interference under APA scheduling is different.)
A5) Proof that any fixed point of the APA reduction of Bertogna and Cirinei’s response-time recurrence for FP scheduling is a safe response-time bound. (This result corresponds to Lemma 9 in the revised version of the ECRTS 2013 paper.)
A6) Definition of the APA reduction of Bertogna and Cirinei’s RTA for FP scheduling.
A7) Proof of correctness of the APA reduction of Bertogna and Cirinei’s RTA for FP scheduling.
A8) Proof that any fixed point of the APA reduction of Bertogna and Cirinei’s response-time recurrence for EDF scheduling is a safe response-time bound. (This result corresponds to Lemma 10 in the revised version of the ECRTS 2013 paper.)
A9) Definition of the APA reduction of Bertogna and Cirinei’s RTA for EDF scheduling.
A10) Proof of correctness of the APA reduction of Bertogna and Cirinei’s RTA for EDF scheduling.
A11) Proof that the iteration of the APA reduction of Bertogna and Cirinei’s RTA for EDF computes the least fixed point of the response-time recurrence.
In addition to the schedulability proofs, we also implement the corresponding schedulers in order to instantiate and test the theorems. Since the implementation is used in an assumption-free context, the fact that we are able to apply the schedulability analysis to actual task sets implies that the theorems have no contradictory assumptions.
As part of the implementation, we constructed job and task structures, a periodic arrival sequence and an APA scheduler (i.e., the actual function that at every time t sorts the pending jobs by priority and assigns them to processors), as described next.
A12) Implementation of a periodic job arrival sequence. (Note that this implementation is just for testing the RTA procedures; all the schedulability analyses we verified apply to sporadic tasks.)
A13) Implementation of a work-conserving weak APA scheduler.
A14) Example of applying the APA reduction of FP RTA on a task set with three tasks. The absence of hypotheses in the proof of schedulability implies that there are no contradictory assumptions.
A15) Example of applying the APA reduction of EDF RTA on a task set with three tasks. The absence of hypotheses in the proof of schedulability implies that there are no contradictory assumptions.
Next, we present the hypotheses used in the schedulability analysis for APA scheduling. These can be found in the section MainProof in the EDF RTA proof file. For more details about the analysis, please refer to Lemma 10 in the revised version of the ECRTS 2013 paper.