!standard D.7(1.3/5) 20-03-06 AI12-0369-1/01 !standard D.7(10.12/5) !class Amendment 20-03-06 !status work item 20-03-06 !status received 20-02-24 !priority Low !difficulty Easy !subject Relaxing barrier restrictions !summary Use "statically names" rather than "statically denotes" in the definition of the restrictions Pure_Barriers and Simple_Barriers. !problem A predicate of a protected type cannot access its components. An idiom (which is commonly used in SPARK) to add a predicate to the components of a protected type is to wrap the components in a record and then add the predicate to the record type. Thus, the illegal: protected type T with Dynamic_Predicate => (Count /= 0) or not Flag is entry E; private Flag : Boolean := False; Count : Natural :; end T; protected body T is entry E when Flag is begin ...; end E; end T; can be replaced by: type Rec is record Flag : Boolean; ... ... end record; protected type T is entry E; private Data : Rec; end T; protected body T is entry E when Data.Flag is begin ... end E; end T; Unfortunately, the barrier in the above is not allowed by restrictions Simple_Barriers or Pure_Barriers. This means this idiom cannot be used with the Ravenscar or Yorvik profiles - which are also commonly used by SPARK users. !proposal (See Summary.) !wording Replace D.7(1.3/5): - a name that statically denotes a scalar component of the immediately enclosing protected unit; with: - a name that statically names (see 4.9) a scalar subcomponent of the immediately enclosing protected unit; Replace D.7(10.12/5): - The Boolean expression in each entry barrier is either a static expression or a name that statically denotes a component of the enclosing protected object. with: - The Boolean expression in each entry barrier is either a static expression or a name that statically names (see 4.9) a subcomponent of the enclosing protected object. !discussion We already have the term "statically names" (originally defined for the Old attribute, now used for a number of other rules - see AI12-0368-1), which allows any prefix that does not require any dynamic evaluation or checking. This is exactly what we want (it also allows other cases, such as statically indexed array components). So we just revise the existing wording to use this term. !ASIS [Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.] !ACATS test ACATS B- and C-Tests are needed to check that the new capabilities are supported. !appendix From: Steve Baird Sent: Friday, February 21, 2020 3:15 PM [Not sending to Ada-Comment because this issue is a low-level detail.] A use-case has come up in internal discussions at AdaCore that (IMO) suggests that a small change to the definition of "pure-barrier-eligible" given in AI12-0290 would be appropriate. The issue has to do with allowing a name denoting a scalar subcomponent (not just a component) of the immediately enclosing protected object, provided that - the name does not denote a component that depends on a discriminant; and - no prefix of the name denotes an array. [The idea is that there are no checks of any kind associated with the evaluation of the name, even checks whose success is statically "obvious".] In the following example, the barrier expression is (currently) not pure-barrier-eligible: type Rec is record Flag : Boolean; ... ... end record; protected type T is entry E; private Data : Rec; end T; protected body T is entry E when Data.Flag is begin ... end E; end T; This proposal is about modifying the definition of pure-barrier-eligible (slightly) to change this. What is the motivation? Why does anyone care about being able to use this sort of construct when the Pure_Barriers restriction is in effect? Lots of folks (notably SPARK) want to be able to use the Pure_Barriers restriction (which is part of the Jorvik profile), so this reduces to the question of why anyone cares about being able to use this sort of construct in any context. In the above example, why couldn't the user declare Flag as a component of type T? This has to do with the use of predicates. A predicate for a protected type cannot name a component. The following example is illegal (which is a good thing that nobody is considering changing): protected type T with Dynamic_Predicate => (Count /= 0) or not Flag is entry E; private Flag : Boolean := False; Count : Natural :; end T; protected body T is entry E when Flag is begin ...; end E; end T; An idiom used to get this effect (which is important in SPARK) is to declare the protected type with only a single component; that component's type is a record which includes the multiple components we "really" want and is subject to the desired predicate. So the above example would be written instead as type Rec is record Flag : Boolean := False; Count : Natural := 0; end record with Dynamic_Predicate => (Count /= 0) or not Flag; protected type T is entry E; private Data : Rec; end T; protected body T is entry E when Data.Flag is begin null; end E; end T; which is fine until you try to compile it with a Jorvik profile in effect, at which point the Data.Flag barrier is rejected. A brief digression: As it happens, SPARK statically enforces subtype predicates in some cases where Ada defines no dynamic checks, notably an assignment to a subcomponent of an object of a predicate-bearing subtype. If anyone is interested in the details, see docs.adacore.com/live/wave/spark2014/html/spark2014_rm/declarations-and-types.html#subtype-predicates In the context of non-SPARK Ada, assertions of the form "Data in Rec" might need to be added to protected operations of type T to get any desired dynamic checking. [end of digression] For the sake of specificity, I propose the following wording change: Replace the bulleted-list item D.7 (1.3/5) - a name that statically denotes a scalar component of the immediately enclosing protected unit; with - a name that denotes a scalar subcomponent of the immediately enclosing protected unit which does not depend on a discriminant, and which is not part of an array. Obviously this may be subject to further wordsmithing. Opinions? **************************************************************** From: Randy Brukardt Sent: Friday, February 21, 2020 3:26 PM > A use-case has come up in internal discussions at AdaCore that (IMO) > suggests that a small change to the definition of > "pure-barrier-eligible" given in AI12-0290 would be appropriate. > > The issue has to do with allowing a name denoting a scalar > subcomponent (not just a component) of the immediately enclosing > protected object, provided that > - the name does not denote a component that depends on a > discriminant; and > - no prefix of the name denotes an array. > > [The idea is that there are no checks of any kind associated with the > evaluation of the name, even checks whose success is statically > "obvious".] This is (approximately) the purpose of the term "statically name" as defined in 6.1.1 (paragraphs 24.2-24.5). Would it be possible to use that terminology?? ... > For the sake of specificity, I propose the following wording change: > > Replace the bulleted-list item D.7 (1.3/5) > - a name that statically denotes a scalar component of the > immediately enclosing protected unit; > with > - a name that denotes a scalar subcomponent of the > immediately enclosing protected unit which does not > depend on a discriminant, and which is not part of an > array. > > Obviously this may be subject to further wordsmithing. How about: Replace the bulleted-list item D.7 (1.3/5) - a name that statically denotes a scalar component of the immediately enclosing protected unit; with - a name that statically names (see 6.1.1) a scalar component of the immediately enclosing protected unit; Let's not define the same thing twice!! **************************************************************** From: Tucker Taft Sent: Friday, February 21, 2020 3:29 PM > ... > For the sake of specificity, I propose the following wording change: > > Replace the bulleted-list item D.7 (1.3/5) > - a name that statically denotes a scalar component of the > immediately enclosing protected unit; > with > - a name that denotes a scalar subcomponent of the > immediately enclosing protected unit which does not > depend on a discriminant, and which is not part of an > array. > > Obviously this may be subject to further wordsmithing. > > Opinions? Go for it. **************************************************************** From: Randy Brukardt Sent: Friday, February 21, 2020 3:30 PM ... > How about: > > Replace the bulleted-list item D.7 (1.3/5) > - a name that statically denotes a scalar component of the > immediately enclosing protected unit; > with > - a name that statically names (see 6.1.1) a scalar component > of the immediately enclosing protected unit; Probably should talk about a "subcomponent" here rather than a "component". Still, the change is so obviously better (why would anyone want more restrictions than necessary?) that there doesn't really need to be any discussion about it (stick it into the presentation AI or an editorial review AI). **************************************************************** From: Tucker Taft Sent: Friday, February 21, 2020 3:32 PM >> [The idea is that there are no checks of any kind associated with the >> evaluation of the name, even checks whose success is statically >> "obvious".] > > This is (approximately) the purpose of the term "statically name" as > defined in 6.1.1 (paragraphs 24.2-24.5). Would it be possible to use > that terminology?? Good suggestion. This will allow statically-indexed array components, which is a reasonable further relaxation. > ... > How about: > > Replace the bulleted-list item D.7 (1.3/5) > - a name that statically denotes a scalar component of the > immediately enclosing protected unit; > with > - a name that statically names (see 6.1.1) a scalar component > of the immediately enclosing protected unit; I think you need to say "a scalar *sub*component". **************************************************************** From: Pat Rogers Sent: Friday, February 21, 2020 4:45 PM > [Not sending to Ada-Comment because this issue is a low-level detail.] > > A use-case has come up in internal discussions at AdaCore that (IMO) > suggests that a small change to the definition of > "pure-barrier-eligible" given in AI12-0290 would be appropriate. > > The issue has to do with allowing a name denoting a scalar > subcomponent (not just a component) of the immediately enclosing > protected object, provided that >    - the name does not denote a component that depends on a >      discriminant; and >    - no prefix of the name denotes an array. > ... > > Obviously this may be subject to further wordsmithing. > > Opinions? Looks good to me! **************************************************************** From: Steve Baird Sent: Friday, February 21, 2020 5:20 PM > How about: > > Replace the bulleted-list item D.7 (1.3/5) > - a name that statically denotes a scalar component of the > immediately enclosing protected unit; > with > - a name that statically names (see 6.1.1) a scalar component > of the immediately enclosing protected unit; and then later > Probably should talk about a "subcomponent" here rather than a "component". I agree, this is better than my proposed wording. I like it. > Still, the change is so obviously better (why would anyone want more > restrictions than necessary?) that there doesn't really need to be any > discussion about it (stick it into the presentation AI or an editorial > review AI) That reasoning sounds suspiciously slippery, but I agree with your conclusion. The resolution you suggest is fine with me if nobody objects. If someone sees a problem with this then please speak up and we'll do things differently. **************************************************************** From: Tullio Vardanega Sent: Saturday, February 22, 2020 8:05 AM I am fine with the outcome of this brief burst. **************************************************************** From: Tucker Taft Sent: Saturday, February 22, 2020 10:28 AM > ... > > So the above example would be written instead as > > type Rec is record > Flag : Boolean := False; > Count : Natural := 0; > end record with > Dynamic_Predicate => (Count /= 0) or not Flag; I think this example should probably be: Dynamic_Predicate => (Count /= 0) = Flag; based on other examples we have discussed. Otherwise Flag is undetermined (with the first predicate, if Count /= 0, Flag can have any value). **************************************************************** From: Tucker Taft Sent: Saturday, February 22, 2020 10:29 AM An interesting question is whether an analogous relaxation would be appropriate for Ravenscar. That is, should we change D.7(10.12/5) as follows: Simple_Barriers The Boolean expression in each entry barrier is either a static expression or a name that statically [denotes a component]{names a subcomponent} of the enclosing protected object. With this change, the Dynamic_Predicate-on-a-record-component trick could work with Ravenscar as well. One side comment on the Dynamic_Predicate trick. If you make all of the components of the record into discriminants (with defaults) then the only alterations permitted would be whole-record assignments, which would mean there is never an intermediate moment when the predicate wouldn't hold. That is, change: type Rec is record Flag : Boolean := False; Count : Natural := 0; end record with Dynamic_Predicate => (Count /= 0) or not Flag; to: type Rec (Flag : Boolean := False; Count : Natural := 0) is null record with Dynamic_Predicate => (Count /= 0) = Flag; -- incorporates minor fix-up to condition ;-) and you can ensure that you can never change one without changing the other. **************************************************************** From: Tullio Vardanega Sent: Monday, February 24, 2020 7:57 AM >I think this example should probably be: > > Dynamic_Predicate => (Count /= 0) = Flag; > >based on other examples we have discussed. Otherwise Flag is undetermined >(with the first predicate, if Count /= 0, Flag can have any value). Nice catch. **************************************************************** From: Tullio Vardanega Sent: Monday, February 24, 2020 7:59 AM >An interesting question is whether an analogous relaxation would be >appropriate for Ravenscar. That is, should we change D.7(10.12/5) as follows: ... Yes, that relaxation should also apply to the Ravenscar profile. **************************************************************** From: Steve Baird Sent: Monday, February 24, 2020 12:54 PM > I think this example should probably be: > > Dynamic_Predicate => (Count /= 0) = Flag; > > based on other examples we have discussed. Otherwise Flag is undetermined > (with the first predicate, if Count /= 0, Flag can have any value). It doesn't really matter because this is just an example, but FWIW I intended it as I originally wrote it - I did not want Flag to be redundant. **************************************************************** From: Tucker Taft Sent: Monday, February 24, 2020 12:58 PM Got it. ****************************************************************