- (1)
- The form of a pragma Task_Dispatching_Policy is as follows:
(2)
pragma Task_Dispatching_Policy(policy_identifier );
Legality Rules
- (3)
- The policy_identifier shall either be FIFO_Within_Priorities or an
implementation-defined identifier.
Post-Compilation Rules
- (4)
- A Task_Dispatching_Policy pragma is a configuration pragma.
- (5)
- If the FIFO_Within_Priorities policy is specified for a partition, then
the Ceiling_Locking policy (see D.3) shall also be
specified for the partition.
Dynamic Semantics
- (6)
- A task dispatching policy specifies the details of task dispatching that
are not covered by the basic task dispatching model. These rules govern when
tasks are inserted into and deleted from the ready queues, and whether a task
is inserted at the head or the tail of the queue for its active priority.
The task dispatching policy is specified by a Task_Dispatching_Policy
configuration pragma. If no such pragma appears in any of the program units
comprising a partition, the task dispatching policy for that partition is
unspecified.
- (7)
- The language defines only one task dispatching policy, FIFO_Within_Priorities; when this policy is in effect, modifications to the ready queues
occur only as follows:
- (8)
- When a blocked task becomes ready, it is added at the tail of the
ready queue for its active priority.
- (9)
- When the active priority of a ready task that is not running
changes, or the setting of its base priority takes effect, the
task is removed from the ready queue for its old active priority
and is added at the tail of the ready queue for its new active
priority, except in the case where the active priority is lowered
due to the loss of inherited priority, in which case the task is
added at the head of the ready queue for its new active priority.
- (10)
- When the setting of the base priority of a running task takes
effect, the task is added to the tail of the ready queue for its
active priority.
- (11)
- When a task executes a delay_statement that does not result in
blocking, it is added to the tail of the ready queue for its
active priority.
- (12)
- Each of the events specified above is a task dispatching point (see
D.2.1).
- (13)
- In addition, when a task is preempted, it is added at the head of the
ready queue for its active priority.
Documentation Requirements
- (14)
- Priority inversion is the duration for which a task remains at the head
of the highest priority ready queue while the processor executes a lower
priority task. The implementation shall document:
- (15)
- The maximum priority inversion a user task can experience due to
activity of the implementation (on behalf of lower priority
tasks), and
- (16)
- whether execution of a task can be preempted by the
implementation processing of delay expirations for lower priority
tasks, and if so, for how long.
Implementation Permissions
- (17)
- Implementations are allowed to define other task dispatching policies,
but need not support more than one such policy per partition.
- (18)
- For optimization purposes, an implementation may alter the points at
which task dispatching occurs, in an implementation defined manner. However,
a delay_statement always corresponds to at least one task dispatching point.
-
- (19)
(13) If the active priority of a running task is lowered due to loss of
inherited priority (as it is on completion of a protected operation) and
there is a ready task of the same active priority that is not running,
the running task continues to run (provided that there is no higher
priority task).
- (20)
(14) The setting of a task's base priority as a result of a call to Set_Priority does not always take effect immediately when Set_Priority is
called. The effect of setting the task's base priority is deferred
while the affected task performs a protected action.
- (21)
(15) Setting the base priority of a ready task causes the task to move
to the end of the queue for its active priority, regardless of whether
the active priority of the task actually changes.
-- Email comments, additions, corrections, gripes, kudos, etc. to:
Magnus Kempe -- Magnus.Kempe@di.epfl.ch
Copyright statement
Page last generated: 95-03-12