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

[Show code snippet]

  A2) Proof of correctness of the interference bound for work-conserving schedulers.

[Show code snippet]

  A3) Definition of the interference bound for EDF scheduling (with slack updates).

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

  A6) Definition of the APA reduction of Bertogna and Cirinei’s RTA for FP scheduling.

[Show code snippet]

  A7) Proof of correctness of the APA reduction of Bertogna and Cirinei’s RTA for FP scheduling.

[Show code snippet]

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

[Show code snippet]

  A9) Definition of the APA reduction of Bertogna and Cirinei’s RTA for EDF scheduling.

[Show code snippet]

  A10) Proof of correctness of the APA reduction of Bertogna and Cirinei’s RTA for EDF scheduling.

[Show code snippet]

  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.

[Show code snippet]

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

[Show code snippet]

  A13) Implementation of a work-conserving weak APA scheduler.

[Show code snippet]

  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.

[Show code snippet]

  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.

[Show code snippet]

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.

Hypothesis H_jobs_must_arrive_to_execute:
  jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
  completed_jobs_dont_execute job_cost sched.
Hypothesis H_valid_task_parameters:
  valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_valid_job_parameters:
   (j: JobIn arr_seq),
    valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_all_jobs_from_taskset:
   (j: JobIn arr_seq), job_task j ts.
Hypothesis H_constrained_deadlines:
   tsk, tsk ts task_deadline tsk task_period tsk.
Hypothesis H_sporadic_tasks:
  sporadic_task_model task_period arr_seq job_task.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_non_empty_affinity:
   tsk, tsk ts #|alpha' tsk| > 0.
Hypothesis H_subaffinity:
   tsk, tsk ts is_subaffinity (alpha' tsk) (alpha tsk).
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
Hypothesis H_edf_policy:
  enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
Hypothesis H_test_succeeds: edf_schedulable ts.