Prosa: Mechanized Proofs of Reduction-Based APA Schedulability Analysis

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.

Locating the Main Results about APA Scheduling

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.

Interference Bounds

  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.)

Response-time Bounds

  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.

Implementation of a Concrete APA Scheduler

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.

Assumptions for the APA reduction of Bertogna and Cirinei’s RTA for EDF scheduling

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.

• Assumption 1: Jobs are not allowed to execute before their arrival times.

• Assumption 2: Jobs are not allowed to execute after completion.

• Assumption 3: All tasks in the task set have valid parameters (e.g., WCET and relative deadline both greater than zero).

• Assumption 4: The jobs in the arrival sequence also have valid parameters (e.g., Job ACET ≤ Task WCET).

• Assumption 5: All jobs in the arrival sequence come from the task set (i.e., there are no other unexpected jobs to be scheduled).

• Assumption 6: All tasks have constrained deadlines.

• Assumption 7: Jobs have sporadic arrival times.

• Assumption 8: Jobs are sequential (i.e., a single job cannot use multiple processors).

• Assumption 9: Every affinity #\alpha’# used in the analysis is a non-empty subaffinity of the actual affinity #\alpha# of each task. (Note that we divide the total interference by #|\alpha’(\cdot)|#, which cannot be zero.)

• Assumption 10: The schedule respects processor affinities, i.e., a job can only be scheduled on a processor if that is allowed by the affinity of its task.

• Assumption 11: The schedule is APA work-conserving, i.e., for every backlogged job #j# at any time #t#, no processor in the affinity of #j\text{’s}# task remains idle.

• Assumption 12: The schedule enforces EDF priority under weak APA scheduling, i.e., for every backlogged job #j# at any time #t#, if there exists a job #j’# executing on the affinity of #j\text{‘s}# task, then #\textit{job_deadline}\ j’ \leq \textit{job_deadline}\ j#.

• Assumption 13: Since the RTA is a sufficient test, we only prove schedulability if the test succeeds.