Version 1.1 of ai12s/ai12-0276-1.txt

Unformatted version of ai12s/ai12-0276-1.txt version 1.1
Other versions for file ai12s/ai12-0276-1.txt

!standard D.4.1          18-05-11 AI12-0276-1/01
!standard 9.5.1(19)
!class Amendment 18-05-11
!status work item 18-05-11
!status received 18-04-28
!priority Low
!difficulty Medium
!subject Admission Policy Defined for Acquiring a Protected Object Resource
!summary
The FIFO_Spinning Admission policy is defined for protected actions on multiprocessor systems
!problem
The topic of scheduling real-time tasks on multiprocessors has received a great deal of attention. An important aspect in this context is communication and synchronization with shared objects, and the use of suitable access protocols for bounding the duration of blocking introduced by priority inversion.
On multiprocessor systems, a spinlock is typically used to gain access to a protected object in order to execute a protected action. For real time systems, it is very desirable to be able to bound the time needed to acquire this lock, however the language does not presume any ordering or queuing for tasks competing to start a protected action (See 9.5.1(19)).
Most multiprocessor locking algorithms specify that spin waiting is used to gain access to the resource, and also prescribe that if there is more than one request competing for the same resource, the requests are served in FIFO order.
For real time systems it should be possible to specify FIFO ordering for obtaining the spinlock that needs to be acquired before executing protected actions of a protected object when tasks are executing on multiprocessor systems.
This is important because it bounds the time it takes for a lower priority task to gain access to a protected object.
One example of using this facility is in a Ravenscar context. Here all tasks are statically allocated to processors. If each protected object used by tasks on different processors is given a high ceiling priority then the blocking time for each task can be computed.
!proposal
(See Summary.)
Modify 9.5.1 (19)
If two tasks both try to start a protected action on a protected object, and at most one is calling a protected {nonexclusive} function, then only one of the tasks can proceed. Although the other task cannot proceed, it is not considered blocked, and it might be consuming processing resources while it awaits its turn. {Unless the FIFO_Spinning admission policy (see D.4.1) is in effect, there}[There] is no language-defined ordering or queuing presumed for tasks competing to start a protected action — on a multiprocessor such tasks might use busy-waiting; for {further} monoprocessor {and multiprocessor} considerations, see D.3, “Priority Ceiling Locking”.
Add before D.1 (23)
- {While starting a protected action on a protected object when the FIFO_Spinning
admission policy is in effect, a task inherits the ceiling priority of the protected object (see 9.5[ and]{,} D.3{, and D.4.1}).
AARM Reason: Priority inheritance is needed for FIFO_Spinning to ensure that lower priority tasks that initiate spin waiting earlier than other higher priority tasks continue to spin to ensure that they can be granted the resource when it becomes available in order to support FIFO ordering.
D.4.1 Admission Policies
[This subclause specifies a mechanism for a user to choose an admission policy. It also defines one such policy. Other policies are implementation defined.]
Implementation defined: Implementation-defined admission policies. Syntax
The form of a pragma Admission_Policy is as follows:
pragma Admission_Policy(policy_identifier);
Legality Rules
The policy_identifier shall be either FIFO_Spinning or an implementation-defined identifier.
Post-Compilation Rules
An Admission_Policy pragma is a configuration pragma.
Dynamic Semantics
[An admission policy governs the order in which competing tasks are evaluated for acquiring the execution resource associated with a protected object] The admission policy is specified by an Admission_Policy pragma.
One admission policy, FIFO_Spinning, is language defined. If no Admission_Policy pragma applies to any of the program units in the partition, the admission policy for that partition is implementation defined. The rules for the FIFO_Spinning admission policy are defined as follows.
- If starting a protected action on a protected object involves busy-waiting, then calls are selected for acquiring the execution resource of the protected object in the order of having initiated the busy-wait; otherwise the admission policy has no effect.
AARM Implementation Note: A possible implementation for this policy would be to apply the abstraction of a ticketting system by assigning two sequence number values to each protected object. One sequence number represents the next available ticket number, and the other sequence number represents the ticket number currently being serviced by the protected object. The next available ticket number is incremented and assigned to a task when the task initiates a busy-wait for acquiring the execution resource associated with the protected object. The ticket number currently being serviced is incremented when a task acquires this execution resource. As part of acquiring the execution resource, a task busy-waits until its assigned ticket number equals the protected object's value for the ticket number currently being serviced. While a task busy-waits, it monitors the active priority of the protected object in order to inherit any modifications to the protected object's active priority.
Implementation Permissions
Implementations are allowed to define other admission policies, but need not support more than one admission policy per partition.
Discussion: This rule is really redundant, as 10.1.5 allows an implementation to limit the use of configuration pragmas to an empty environment. In that case, there would be no way to have multiple policies in a partition.
!discussion
On uniprocessor systems, the Priority Ceiling Protocol (PCP) and the Stack Resource Policy (SRP) are generally accepted as the most appropriate access protocols, as they exhibit some interesting properties: • Deadlock free execution. • Only tasks of higher priority can preempt running tasks and only if they do not share any locked resource. • Tasks of lower priority can only prevent the execution of higher priority tasks as a result of having locked a shared resource. • The duration of the blocking is bounded by the the maximum execution time of an operation on the resource invoked by a lower priority task.
Among the various access protocols that have been proposed for multiprocessor systems, two extensions of SRP have raised a high interest in the context of the Ada programming language:
- the Multiprocessor Stack Resource Policy (MSRP), and - the Multiprocessor resource sharing Protocol (MrsP).
Both protocols involve the the use of spin waiting to obtain the lock associated with a protected object in order to execute protected actions and entry calls. MSRP in particular specifies that the servicing of the tasks competing for the spinlock be serviced in FIFO order. Other candidate protocols also exist that involve spin waiting and would similarly benefit from being serviced in FIFO order.
It was considered that different queuing priorities might be desired based on whether the tasks accessing a protected object belonged to the same dispatching domain or not. A sensible approach might for instance be to use priority based selection when the tasks of the protected object belong to the same dispatching domain, and then use FIFO ordered selection when the tasks of the protected object belong to multiple dispatching domains. FIFO ordering however is a good general choice. For now, supporting just FIFO ordering would be a simpler proposal and would be much better than no order at all which is currently the situation.
!ASIS
No ASIS effect.
!ACATS test
An ACATS C-Test is needed to check that the new capabilities are supported.
!appendix

From: Brad Moore
Sent: Saturday, April 28, 2018  9:37 PM

We had a good session at IRTAW last week, with interesting discussions.

One of the outputs from the workshop is that there is a need to be able to 
specify an order when busy-waiting for a gaining access to a PO.

The language currently doesn't presume any order.

Multiprocessor locking algorithms such as MSRP and MrsP specify that competing
tasks are served in FIFO order.

I have written up the AI with wording and motivation, as well as notes on a 
possible implementation, which is attached.

We came up with notion of an Admission Policy as the Ada policy that allows a 
configuration pragma to specify ordering for busy waiting on a PO, as well as 
defined a single admission policy called FIFO_Spinning.

The IRTAW workshop unanimously felt that this was an important AI to consider 
for inclusion in Ada 202x.

Hopefully, it can be accommodated.

In addition, Tullio is working on an AI with a minor wording change for the 
Non-Preemtive dispatching policy, where I believe the issue is that
D.2.4 (10/3) describes the dispatching points using the word "blocking", when
it should have been "potentially blocking". This is just a heads up that the AI
is forthcoming.

We also discussed the Deadline Floor Protocol AI, and Alan is working on
providing an update to that AI. (AI12-0230-1/02 - Editor.)

Finally, we also discussed the Compare and Swap AI (AI12-0234-1/02 - Editor).
We unanimously agreed that  a set of atomic primitives should be provided
similar to the GCC API available to C programmers, as Tucker had suggested.
We also agreed that pragma CPU should be allowed to be specified for a 
protected object, so that only tasks belonging to that CPU are allowed to
call into the CPU. Adacore already has this implemented. That would provide
allow for a lock free implementation, as uniprocessor implementations already
do not require locking. 

I also presented Adacore's Lock_Free pragma, but IRTAW unanimously agreed that
the Lock_Free aspect for protected objects should not be standardized at this 
time.

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

From: Jeffrey Cousins
Sent: Monday, April 30, 2018  3:19 AM

The undefined order when spinning had always seemed like an omission to me, 
but I'd be told that it didn't matter as it wasn't blocking. So I'd like to 
have an option to be able to choose.

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

Questions? Ask the ACAA Technical Agent