Version 1.4 of ai05s/ai05-0055-1.txt

Unformatted version of ai05s/ai05-0055-1.txt version 1.4
Other versions for file ai05s/ai05-0055-1.txt

!standard D.2.6(26/2)          07-10-08 AI05-0055-1/03
!class binding interpretation 07-05-15
!status WG9 Approved 07-11-08
!status ARG Approved 10-0-2 07-06-01
!status work item 07-05-15
!status received 07-05-15
!priority Medium
!difficulty Easy
!qualifier Error
!subject Glitch in EDF protocol
!summary
It was the intention that EDF dispatching in Ada should support Baker's protocol for preemption level control over access to protected objects.
Unfortunately the model fails to implement the protocol in some situations. The wording is corrected to overcome the difficulty.
!question
In some circumstances it is possible that a task can be executing even though another task is otherwise eligible and has an earlier deadline. This violates the intention of EDF; was this intended? (No.)
!recommendation
(See Summary.)
!wording
Replace D.2.6(26/2) by
* the highest priority P, if any, less than the base priority of T such
that one or more tasks are executing within a protected object with ceiling priority P and task T has an earlier deadline than all such tasks; and furthermore T has an earlier deadline than all other tasks on ready queues with priorities in the given EDF_Across_Priorities range that are strictly less than P.
!discussion
The current rule (26/2) is one of three concerning active priority. The idea is that the active priority is the maximum of the three items given in 24, 25 and 26). The third in 26 says
the highest priority P, if any, less than the base priority of T such that one or more tasks are executing within a protected object with ceiling priority P and task T has an earlier deadline than all such tasks.
Unfortunately it seems that this is not adequate to support Baker's protocol in some circumstances. It turns out that it is not just the level P which matters but all lower levels as well. So the rule has to be extended by adding ... and all other tasks on ready queues with priorities strictly less than P.
The problem and proposed solution is described in detail in the attached paper (Correcting the EDF protocol in Ada 2005 by Zerzelidis, Burns and Wellings) which was discussed at the 13th International Real-Time Workshop (which took place in Vermont in April 2007). The proceedings of the workshop will be published in a forthcoming issue of the Ada User Journal.
The workshop discussed this problem at length and concluded that the proposed new wording was indeed correct. Here is the draft text of that part of the session report concerning this issue.
--begin
2. Correcting the EDF definition in Ada 2005
The first part of this session addressed a problem in the current description of the Earliest Deadline First (EDF) dispatching protocol in the Ada 2005 standard. The difficult part in the definition of the EDF policy is the description of Ted Baker's protocol for resource sharing.
The problematic wording is in the definition of the rules of EDF dispatching (ARM, Section D.2.6). In that clause the active priority of a task T when first activated or while it is blocked is defined as the maximum of the following:
24/2 the lowest priority in the range specified as EDF_Across_Priorities that includes the base priority of T,
25/2 the priorities, if any, currently inherited by T,
26/2 the highest priority P, if any, less than the base priority of T such that one or more tasks are executing within a protected object with ceiling priority P and task T has an earlier deadline than all such tasks.
Clause 26/2 contains the key semantics, and it is intended to ensure the behaviour required by Bakerís algorithm. Its current wording implies that a task could be placed on a ready queue above one on which a task with a shorter deadline is placed. Alan Burns described one scenario (the full details are in their position paper) showing that the current wording is not in full accordance with Baker's protocol.
Alan Burns then illustrated a simple rewording to 26/2 which makes the rule stricter and achieves correct EDF dispatching in full adherence with Baker's SRP algorithm. The proposed rewording is as follows:
26/2* the highest priority P, if any, less than the base priority of T such that one or more tasks are executing within a protected object with ceiling priority P and task T has an earlier deadline than all such tasks and all other tasks on ready queues with priorities strictly less than P.
The workshop agreed that the current wording in 26/2 is not correct, approved the proposed reworking of it and tasked Alan Burns (as a member of the ARG) to produce an Ada Issue (AI) to illustrate the problem and propose the fix to it.
Michael Gonzalez Harbour proposed to use a model checker to ensure that the definition complies with the intended semantics.
--end of workshop report extract
This present document is the AI referred to above. Note that the ARG later improved the proposed wording, so the wording actually adopted is not the same as that proposed by the workshop.
Baker's protocol is described in Stack-based scheduling of realtime processes by T P Baker in Real-Time Systems 3(1), March 1991.
Note that a formal proof of the correctness of the revised wording is not available. But then a formal proof of most aspects of the standard is not available. Suffice it to say that no counter example has been found and so the new wording has to be an improvement.
!example
See paper at http://www.ada-auth.org/ai-files/grab_bag/EDFpaper.pdf
!corrigendum D.2.6(26/2)
Replace the paragraph:
by:
!ACATS Test
!appendix

****************************************************************

Questions? Ask the ACAA Technical Agent