CVS difference for ai12s/ai12-0079-1.txt

Differences between 1.13 and version 1.14
Log of other versions for file ai12s/ai12-0079-1.txt

--- ai12s/ai12-0079-1.txt	2017/11/30 04:18:01	1.13
+++ ai12s/ai12-0079-1.txt	2018/01/27 04:54:50	1.14
@@ -1439,7 +1439,7 @@
 From: Randy Brukardt
 Sent: Monday, October 2, 2017  8:53 PM
 
-> Here is the first piece of my ARG homework.  Mostly I tried to fix up 
+> Here is the first piece of my ARG homework.  Mostly I tried to fix up
 > the syntax according to our discussions in Vienna.
 
 Thanks for getting this done early. Can I expect the rest of your homework
@@ -1515,7 +1515,7 @@
 ...
 >(1) I think you need to soon (if not immediately) address how these are
 >going to work within generic units and presumably for access-to-subprogram
->types. 
+>types.
 
 Not sure why you're saying that. Pre/Post also don't work with
 access-to-subprogram currently.
@@ -1544,18 +1544,18 @@
 SPARK is fully modular, except for two things: checking of concurrency, which
 is rather a minor point, and generation of Global contracts but *only* when
 they are not provided by the user. And even in that second case, you only need
-to look at the sub-call graph from a subprogram to generate its Global.  
+to look at the sub-call graph from a subprogram to generate its Global.
 
 ****************************************************************
 
 From: Randy Brukardt
 Sent: Tuesday, October 3, 2017  12:25 AM
 
->>(1) I think you need to soon (if not immediately) address how these 
->>are going to work within generic units and presumably for 
+>>(1) I think you need to soon (if not immediately) address how these
+>>are going to work within generic units and presumably for
 >>access-to-subprogram types.
 
->Not sure why you're saying that. Pre/Post also don't work with 
+>Not sure why you're saying that. Pre/Post also don't work with
 >access-to-subprogram currently.
 
 The generic cases (which is mainly what I'm concerned about) are necessary to
@@ -1571,11 +1571,11 @@
 "right" for access-to-subprogram, generics, and any other such cases.
 There's no leeeway (something I learned in detail defining Nonblocking).
 
->>(3) I didn't see a solution for global data defined in hidden 
+>>(3) I didn't see a solution for global data defined in hidden
 >>packages, such as the System implementation helpers that both Janus/Ada
->>and GNAT have. We can't start requiring implementors to restructure their 
+>>and GNAT have. We can't start requiring implementors to restructure their
 >>entire runtime in order to meet Global settings.
-		
+
 >I think that's the part where package P is meant to represent all data
 >hidden in P and its private children. Or you have something else in mind?
 
@@ -1600,24 +1600,24 @@
 that might be used to implement a package but aren't visible in that package's
 specification.
 
->> (5) I think I object to the idea of "synthesized" global aspects. 
+>> (5) I think I object to the idea of "synthesized" global aspects.
 >> (I'm sorry I didn't think of this during the meeting.)
-		
+
 > I also do not like it. To me, it looks useless: absence of the aspect already
 > indicates we know nothing of its reads/writes of global variables.
 
 Glad to hear I'm not completely crazy.
 
->> My long time objection to systems like SPARK is their need to have 
->> the complete program available before they can prove anything. I 
+>> My long time objection to systems like SPARK is their need to have
+>> the complete program available before they can prove anything. I
 >> don't want to see Ada going down that road.
 
 > This is completely wrong. :-)
-> SPARK is fully modular, except for two things: checking of 
+> SPARK is fully modular, except for two things: checking of
 > concurrency, which is rather a minor point, and generation of Global
 > contracts but *only* when they are not provided by the user. And even in
 > that second case, you only need to look at the sub-call graph from a
-> subprogram to generate its Global.  
+> subprogram to generate its Global.
 
 I don't want any "except for" in Ada. Period. Good to hear that SPARK has
 moved away from complete source code, though.
@@ -1694,11 +1694,11 @@
 global => in out null, and that would have to be checked during
 instantiation.)
 
-> Morally, container's API reads/writes no globals (except for those 
-> like Query_Element and Update_Element that take a callback in 
-> argument, which may have such an effect). The bounded containers 
+> Morally, container's API reads/writes no globals (except for those
+> like Query_Element and Update_Element that take a callback in
+> argument, which may have such an effect). The bounded containers
 > indeed have "Global => null"
-> contracts, while the regular ones actually allocate memory, so with 
+> contracts, while the regular ones actually allocate memory, so with
 > Tuck's proposal you would have to mention the corresponding access type.
 
 Yes, that's part of it. Also, the container package itself may have some state
@@ -1721,8 +1721,8 @@
 2020 at all (there's just not enough else of value, and restarting from
 nothing is not going to get us anywhere useful by mid-2019).
 
-> A more complex scheme would have a way to describe the formal 
-> parameters or callbacks globals, something like Subp'Global, but that 
+> A more complex scheme would have a way to describe the formal
+> parameters or callbacks globals, something like Subp'Global, but that
 > would quickly turn into a nightmare I'm afraid.
 
 That's the only option that is compatible and safe, and thus I want to get
@@ -1738,12 +1738,12 @@
 parallel statements wouldn't allow any unprotected globals, even if they don't
 conflict.)
 
->> Global, however, is statically enforced in Ada, so it has to be 
+>> Global, however, is statically enforced in Ada, so it has to be
 >> handled "right" for access-to-subprogram, generics, and any other such cases.
 >> There's no leeeway (something I learned in detail defining Nonblocking).
-		
-> I don't see why we could not have a situation where the compiler 
-> enforces part of the property, leaving holes to be filled by other 
+
+> I don't see why we could not have a situation where the compiler
+> enforces part of the property, leaving holes to be filled by other
 > tools? That's similar to the distinction between static checking and
 > dynamic checking. Except here of course you cannot describe the static
 > analysis performed in these other tools that complete the compiler.
@@ -1756,24 +1756,24 @@
 allow actually is OK, and that could be useful if the "Soft Error"
 scheme is adopted, but that's about it.
 
->>I'm thinking of unrelated packages that are used to implement some 
->>library package. For instance, Janus/Ada bases all of its I/O packages 
+>>I'm thinking of unrelated packages that are used to implement some
+>>library package. For instance, Janus/Ada bases all of its I/O packages
 >>on a package called System.Basic_IO. That has some global state. I believe
->>GNAT does something similar with it's I/O packages; they seem to depend on 
+>>GNAT does something similar with it's I/O packages; they seem to depend on
 >>children of System and GNAT. It would be amazing if no such package ever
->>needed global state. (Certainly that will rarely happen if storage pools are 
+>>needed global state. (Certainly that will rarely happen if storage pools are
 >>considered state, as they ought to be.)
->>		
+>>
 >>Forcing implementers to either remove the state or restructure their
->>runtime to put everything in private packages (which might be very difficult 
+>>runtime to put everything in private packages (which might be very difficult
 >>given visibility issues and the like) seems like the wrong way to go.
->>		
->>It seems like there needs to be some way to refer to state of any/all 
->>packages that might be used to implement a package but aren't visible 
+>>
+>>It seems like there needs to be some way to refer to state of any/all
+>>packages that might be used to implement a package but aren't visible
 >>in that package's specification.
-		
+
 >I believe that's what Tuck proposes when he refers to the name of the
->package. So in your case, System.Basic_IO would refer to all hidden state in 
+>package. So in your case, System.Basic_IO would refer to all hidden state in
 >that unit.
 
 Sure, but no one is going to put System.Basic_IO into the specification of
@@ -1859,67 +1859,67 @@
 
 >It seems to me that this extremist approach is bound to fail. I see no
 >point in forcing Global on everything.
- 
+
 If we don't, then we cannot solve any of the problems that we are trying to
 solve. If you are right, then we should abandon work on Global immediately and
 switch to something simpler that will work (perhaps a pair of aspects
 "Task_Safe" and "Extra_Pure").
 
->I don't see why the compiler would have to check all the boxes here. 
+>I don't see why the compiler would have to check all the boxes here.
 >This will require analysis techniques beyond what the compiler can do.
- 
+
 No. There is no requirement that all things that might be parallelizable be
 legal Ada (you can always use an unsafe technique to get that). We just want
 to allow what is obviously safe.
- 
+
 >But I think that the compiler could do something very valuable, which is to
->check indeed that loops can be parallelized based on the Global contracts on 
->the subprograms it calls. That would leave the verification of Global 
+>check indeed that loops can be parallelized based on the Global contracts on
+>the subprograms it calls. That would leave the verification of Global
 >contracts themselves to other tools.
- 
+
 The vast majority of Ada users have no other tools. The language is wildly
 incomplete if it cannot be used without depending on "other tools".
 Moreover, if some "other tool" can exist that verifies some important
 property, then that tool can be part of the Ada compiler. Dependence on
 "other tools" for critical functionality is evil.
- 
+
 In any case, Global has to be defined in terms of what it allows. If it is
 not, then it has no semantic meaning within the Ada Standard, and that would
 make it nonsense to define. (Plus, that is NOT what Tucker is currently
 proposing.)
 
 ...
->Based on our experience with users using Global contracts, I'd say it's 
->unlikely you manage to make something that complex as Subp'Global 
+>Based on our experience with users using Global contracts, I'd say it's
+>unlikely you manage to make something that complex as Subp'Global
 >inside other contracts be useful to anyone.
- 
+
 It certainly works for Nonblocking (at least in the context of the containers,
 which is the critical case); I fail to see (today!) why it would be different
 for Global.
- 
+
 For the intended tasking purpose, the only truly interesting Global contracts
 are "in out null" and "synchronized" (everything else would conflict by
 definition in a parallel loop). They could be defined by aspects that work
 like Nonblocking, and that clearly will work in the context of the containers.
 If Global can't be made to work here, then we ought to abandon Global in favor
 of something that will work.
- 
+
 ...
->OK if you can pull it, but I doubt it's possible with "just" 
+>OK if you can pull it, but I doubt it's possible with "just"
 >compilation techniques, while managing an acceptable complexity in
 >annotations.
- 
+
 We don't need perfection, we only need a guarantee that the contract reflects
 reality. I fail to see why you think that requires advanced analysis (the
 Global contract of a subprogram is the union of all of the contracts of the
 subprograms that it calls, plus all of globals that it directly reads or
 writes -- hard to see where complex analysis would be needed).
- 
+
 >Or just settle for something very simple, such as Global=>null that indicates
 >that no global is read/written, which could be inferred by the compiler for
 >a subprogram based on the contracts of subprograms it calls (no need for a
 >global analysis), so would be inferred in particular for generic instances.
- 
+
 That's the model of Global in Ada (as opposed to SPARK). All of the contracts
 Tucker has are designed to be simply checked by a compiler. And inferring the
 contracts for generic instantiations is how Nonblocking works (and I would
@@ -1929,23 +1929,23 @@
 something we've never done to date; and (B) are a dead body issue for me (as
 previously noted) - Janus/Ada has no body dependence mechanism and is never
 going to have one.
- 
+
 If there is a problem with the Subp'Global model, it is likely to be with the
 needed assume-the-worst rule. In that case, my preference is to abandon Global
 (leaving it to SPARK) and instead define two Boolean contracts (which I know
 can be defined properly).
- 
+
 ****************************************************************
 
 From: Tucker Taft
 Sent: Tuesday, October 3, 2017  3:36 PM
 
->> Based on our experience with users using Global contracts, I'd say 
->> it's unlikely you manage to make something that complex as 
+>> Based on our experience with users using Global contracts, I'd say
+>> it's unlikely you manage to make something that complex as
 >> Subp'Global inside other contracts be useful to anyone.
-> 
-> It certainly works for Nonblocking (at least in the context of the 
-> containers, which is the critical case); I fail to see (today!) why it 
+>
+> It certainly works for Nonblocking (at least in the context of the
+> containers, which is the critical case); I fail to see (today!) why it
 > would be different for Global. ...
 
 We have already proposed using the 'Global attribute for generics in the AI.
@@ -1970,7 +1970,7 @@
 Sent: Tuesday, October 3, 2017  6:46 PM
 
 ...
-> We have already proposed using the 'Global attribute for generics in 
+> We have already proposed using the 'Global attribute for generics in
 > the AI.  The few examples we have looked at seem to make sense.
 
 Sorry, missed that. However, I didn't see the needed generic matching rules,
@@ -1979,20 +1979,20 @@
 to the ones for Nonblocking probably ought to be constructed to show the
 issues that need to be addressed.)
 
-> In our most recent discussion in the SPARK language-design group, we 
-> suggested we drop the explicit "Synthesized" value for the global 
-> aspect, and just give permission for an implementation to synthesize a 
+> In our most recent discussion in the SPARK language-design group, we
+> suggested we drop the explicit "Synthesized" value for the global
+> aspect, and just give permission for an implementation to synthesize a
 > more precise Global aspect
-> when it would otherwise default to "in out all."   Clearly if 
-> the compiler cannot synthesize a sufficiently precise Global aspect, 
-> there will be safe programs that are identified as unsafe, so such a 
-> program will not be as portable.  To make such a program portable, the 
-> tool that synthesizes the more precise Global aspect would have to 
-> generate the explicit annotations and add them to the source code, 
-> which seems doable.  But for a user who is happy to have non-portable 
-> code, they can leave off the explicit annotations and still have a 
-> modicum of safety.  If the code is given to a compiler that doesn't 
-> have the full machinery, it will be rejected rather than being 
+> when it would otherwise default to "in out all."   Clearly if
+> the compiler cannot synthesize a sufficiently precise Global aspect,
+> there will be safe programs that are identified as unsafe, so such a
+> program will not be as portable.  To make such a program portable, the
+> tool that synthesizes the more precise Global aspect would have to
+> generate the explicit annotations and add them to the source code,
+> which seems doable.  But for a user who is happy to have non-portable
+> code, they can leave off the explicit annotations and still have a
+> modicum of safety.  If the code is given to a compiler that doesn't
+> have the full machinery, it will be rejected rather than being
 > silently unsafe.
 
 I think I like this better than what the AI proposes.
@@ -2002,13 +2002,13 @@
 From: Tucker Taft
 Sent: Tuesday, October 3, 2017  9:38 PM
 
->> We have already proposed using the 'Global attribute for generics in 
+>> We have already proposed using the 'Global attribute for generics in
 >> the AI.  The few examples we have looked at seem to make sense.
-> 
-> Sorry, missed that. However, I didn't see the needed generic matching 
-> rules, nor the assume-the-best/assume-the-worst rules needed when 
-> using this inside a generic. So I'm not sure how it works in those 
-> cases. (Some examples similar to the ones for Nonblocking probably 
+>
+> Sorry, missed that. However, I didn't see the needed generic matching
+> rules, nor the assume-the-best/assume-the-worst rules needed when
+> using this inside a generic. So I'm not sure how it works in those
+> cases. (Some examples similar to the ones for Nonblocking probably
 > ought to be constructed to show the issues that need to be addressed.)
 
 Good point.  We need to specify requirements on actuals when a formal has
@@ -2035,9 +2035,9 @@
 Sent: Thursday, October 5, 2017  12:25 AM
 
 ...
-> Good point.  We need to specify requirements on actuals when a formal 
-> has a Global specified.  The requirements are pretty simple, as they 
-> will be based on some kind of set inclusion, but of course they need 
+> Good point.  We need to specify requirements on actuals when a formal
+> has a Global specified.  The requirements are pretty simple, as they
+> will be based on some kind of set inclusion, but of course they need
 > to be spelled out.
 
 You also need assume-the-best/assume-the-worst rules for the meaning of the
@@ -2060,5 +2060,199 @@
 
 Essentially, everything that was hard for Nonblocking is likely to have a
 similar problem for Global. Best that we check that we don't miss anything.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, January 25, 2018  4:04 AM
+
+...
+> I rather disagree; phone meetings are best for wordsmithing since it
+> isn't necessary to diagram on a whiteboard like it is for syntax
+> arguments. For Ada 2012, we used phone meetings to finalize almost all
+> of the wording, so it's amazing to me to think that it suddenly has
+> gotten difficult to do what we've done many times before.
+
+OK, I had a different goal for these phone calls.  We have asked the community
+to get all of their proposals in by Jan 15, so I presumed one of the points of
+these phone calls was to deal with the final influx of proposals.
+
+> In any case, AI12-0079-1 is nowhere near complete enough for me to be
+> able to annotate the containers with them, a job I need to start ASAP.
+> For instance, we have no solution in the AI yet to the problem of
+> implementation-defined helper packages. We haven't discussed how to
+> handle atomic writes in "synchronized" mode (these are easily race
+> conditions which shouldn't be allowed in general, lest our goal of
+> preventing unsynchronized access be completely undermined). There's
+> probably other issues that aren't mentioned in the AI.
+
+I am willing to spend more time on 0079.  I did not realize that the above was
+your concern.  Perhaps we can handle this offline.  If you can let me know what
+you feel you need to annotate the containers, I'll try to finalize that part of
+the wording.  For me it just seemed like there was a general fine tuning needed,
+but apparently you feel there are still some big issues, at least when it comes
+to annotating the libraries.  So if you can give me a clearer idea of what you
+need, I'll focus on that.
+
+> Moreover, you haven't really done much of an update for the last
+> couple of meetings. It seems like it isn't progressing, and it is the
+> most core thing we are working on.
+>
+> I was expecting that we would spend a bit of time on the 4 BIs (none
+> of which should require much discussion, but maybe some wordsmithing),
+> a bit of time on some of the new proposals (to determine whether or
+> not we want to pursue them, and find a victim, er, ARG author for the
+> AI), and the bulk of the time on AI12-0079-1 and AI12-0119-1 in the
+> hopes of getting some of our core work done. [Remember that
+> AI12-0119-1 depends on AI12-0079-1.] (We can't finish all of the AIs
+> for Ada 2020 in the last week, as I simply couldn't get the all into
+> Standard in the two weeks or so of editorial time the schedule
+> allows.) And then we would look at anything else as time permits.
+
+Unfortunately, it looks like perhaps we each had our own priorities for the
+phone calls.  I appreciate what you are saying, but alas, it wasn't what I
+prioritized for this first call.  Perhaps you and I can handle the 0079 issue
+ourselves without taking up time for the whole ARG.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, Janaury 25, 2018  6:00 PM
+
+...
+> > I rather disagree; phone meetings are best for wordsmithing since it
+> > isn't necessary to diagram on a whiteboard like it is for syntax
+> > arguments. For Ada 2012, we used phone meetings to finalize almost
+> > all of the wording, so it's amazing to me to think that it suddenly
+> > has gotten difficult to do what we've done many times before.
+>
+> OK, I had a different goal for these phone calls.  We have asked the
+> community to get all of their proposals in by Jan 15, so I presumed
+> one of the points of these phone calls was to deal with the final
+> influx of proposals.
+
+True, but at this stage, that mainly is discussing broad outlines of what to do,
+whether to do anything at all, and then finding a victim, er author to produce a
+real proposal.
+
+After that, I expect we'll work in priority order, which always puts 79 and
+119 first. And I've learned over the years that if you don't try to get the
+critical work done before doing things that are more fun, the critical work
+never does get done.
+
+> > In any case, AI12-0079-1 is nowhere near complete enough for me to
+> > be able to annotate the containers with them, a job I need to start ASAP.
+> > For instance, we have no solution in the AI yet to the problem of
+> > implementation-defined helper packages. We haven't discussed how to
+> > handle atomic writes in "synchronized" mode (these are easily race
+> > conditions which shouldn't be allowed in general, lest our goal of
+> > preventing unsynchronized access be completely undermined). There's
+> > probably other issues that aren't mentioned in the AI.
+>
+> I am willing to spend more time on 0079.  I did not realize that the
+> above was your concern.  Perhaps we can handle this offline.  If you
+> can let me know what you feel you need to annotate the containers,
+> I'll try to finalize that part of the wording.
+
+I'm not completely sure at this stage, as I've never felt the proposal was solid enough to proceed. Obviously, the containers are generic, so all of the rules involving combinations and reflecting the Globals of the actuals in generic specs need to be fig
ured out in detail.
+
+This is rather complex for Nonblocking (which is worked out), and Global is 10 times harder, so the lack of work in that area is concerning.
+
+> For me it just seemed like there was a general fine tuning needed, but
+> apparently you feel there are still some big issues, at least when it
+> comes to annotating the libraries.  So if you can give me a clearer
+> idea of what you need, I'll focus on that.
+
+The other issue for the libraries is clearly what to do about
+implementation-defined "helper" packages. We surely have to allow
+implementations to have such packages, and they might in some circumstances have
+globals in them. It would seem nasty to ban that (other than in Pure packages,
+of course). And we surely can't name any such packages in the Standard!
+
+There's also an issue that is not specific to Global, but matters a lot.
+Since attribute prefixes have to be unambiguous without context, most of the
+names of generic formals can't be directly used in an attribute. That means that
+they have to be renamed to a unique name so that they can be used. For instance,
+for Vectors:
+
+generic
+   type Index_Type is range <>;
+   type Element_Type is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Vectors
+   with Preelaborate, Remote_Types,
+        Nonblocking => Equal_Element'Nonblocking,
+        Global => Equal_Element'Global and <impl-def stuff??> and <the body of this package> is
+
+   function Equal_Element (Left, Right : Element_Type) return Boolean renames "=";
+
+   ...
+
+The aspects Nonblocking and Global give the default declaration of the aspects
+for the contents, and we surely don't want to repeat them on all (approx) 70
+subprograms.
+
+However, we've never defined what the freezing point of a package declaration
+is, so the place where these aspects are evaluated is not well-defined. So I
+don't even know if this formulation is legal. And if it isn't legal, is there
+any alternative that IS legal that doesn't require repeating Nonblocking and
+Global aspects 70 times.
+
+The third issue is about the actual definition of "synchronized". The purpose of
+this setting is to mark task-safe code that still uses global variables. It's
+pretty clear that 100% elimination of data races is impossible if any globals
+are involved (as soon as there is more than one global, data locks are
+impossible to avoid with static rules).
+
+But there definitely is low-hanging fruit that certainly should be detected.
+For instance, if A is a global atomic object, then
+   A := A + 1;
+is a guarenteed data race (assuming any parallel execution). One should be using
+one of the routines in the atomic update generic that Bob doesn't think is
+important. ;-)
+
+I can think of a number of relatively simple additional rules that would at
+least eliminate the worst of these data race conditions (essentially by making
+them illegal in "synchronized" code). But I don't know how far we should go.
+
+My fear in this case is that a user will slap "parallel" on an existing loop to
+see what happens. And they then get an error about not having Global and
+Nonblocking contracts. So they add those, and then get an error about having a
+unsynchronized global object (probably with a suggestion to make them protected
+or atomic). So they slap "atomic" on the object, the code compiles, and the loop
+malfunctions badly because the object is updated without using an atomic update
+operation.
+
+I know at least one substantial Ada user who would function this way (I see him
+in the mirror every morning ;-), and not detecting bad atomic updates would
+greatly reduce the value of all of the other things we've done. (There's a
+similar issue for protected objects if someone just provides separate read and
+write operations rather than the update operations.)
+
+So I'd like to explore this issue a bit to see what we can do to mitigate it.
+
+[I can write a much longer discussion of this issue, but I have to get AIs
+created and mail filed for the meeting, lest we not have a lot of topics that
+we're supposed to be able to talk about in place.]
+
+...
+> Unfortunately, it looks like perhaps we each had our own priorities
+> for the phone calls.  I appreciate what you are saying, but alas, it
+> wasn't what I prioritized for this first call.  Perhaps you and I can
+> handle the 0079 issue ourselves without taking up time for the whole
+> ARG.
+
+I'm just following the plan laid out by Jeff that he's followed at every
+previous meeting. I'm pretty sure that hasn't changed for this one. :-)
+
+We do have plans for more calls this winter, so this is hardly the only such
+opportunity. If we don't discuss it Monday, I'm sure we'll have a chance in late
+February. Experience shows that by the third call, Tucker is hardly touching his
+homework :-), so I'm trying to get you to do as much of it now as possible. (And
+you've certainly done some of it -- but we put priority indications on AIs for a
+reason ... High > Low :-)
+
+Anyway, I've laid out the issues I can think of off-hand above. I also noted
+above that I need to do other work today, so looking in detail at the proposals
+and AI12-0112-1 had better wait lest the Jan 15th rush not get processed.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent