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

[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]

**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]

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]

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

Hypothesis H_valid_job_parameters:

∀ (j: JobIn arr_seq),

valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

∀ (j: JobIn arr_seq),

valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

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

Hypothesis H_non_empty_affinity:

∀ tsk, tsk ∈ ts → #|alpha' tsk| > 0.

Hypothesis H_subaffinity:

∀ tsk, tsk ∈ ts → is_subaffinity (alpha' tsk) (alpha tsk).

∀ tsk, tsk ∈ ts → #|alpha' tsk| > 0.

Hypothesis H_subaffinity:

∀ tsk, tsk ∈ ts → is_subaffinity (alpha' tsk) (alpha tsk).

**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#.

Hypothesis H_edf_policy:

enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).

enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).

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