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

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

--- ai12s/ai12-0079-1.txt	2017/10/03 01:58:22	1.11
+++ ai12s/ai12-0079-1.txt	2017/10/06 04:22:27	1.12
@@ -1431,7 +1431,8 @@
 Sent: Monday, September 25, 2017  4:33 PM
 
 Here is the first piece of my ARG homework.  Mostly I tried to fix up the
-syntax according to our discussions in Vienna.
+syntax according to our discussions in Vienna. [This is version /05
+ - Editor.]
 
 ****************************************************************
 
@@ -1505,5 +1506,559 @@
 (implementation-defined modifiers are allowed), and that seems preferable to
 defining in the language something contract-related that destroys the contract
 model!
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Monday, October 2, 2017  11:42 PM
+
+...
+>(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
+access-to-subprogram currently.
+
+...
+>(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 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?
+
+...
+>(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.
+
+>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 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.  
+
+****************************************************************
+
+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 
+>>access-to-subprogram types.
+
+>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
+deal with if Global is to work with the containers. And if it doesn't work
+with the containers, a significant number of programs couldn't use Global
+(including most of the intended uses of Global in parallel blocks and loops).
+
+Pre/Post are dynamic constructs in Ada (as opposed to SPARK), so it doesn't
+matter much how they work with access-to-subprogram. Indeed, there is an open
+AI to improve that (it's unlikely to stay precisely as it is).
+
+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).
+
+>>(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 
+>>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?
+
+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 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 considered
+state, as they ought to be.)
+
+[Poster's note: I should have mentioned that you don't want to have to name
+these unrelated packages in the Global of the package specification; the
+user should need to know nothing about them. Especially important for
+language-defied packages.]
+
+Forcing implementers to either remove the state or restructure their 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 in that package's
+specification.
+
+>> (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 
+>> don't want to see Ada going down that road.
+
+> This is completely wrong. :-)
+> 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.  
+
+I don't want any "except for" in Ada. Period. Good to hear that SPARK has
+moved away from complete source code, though.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 3, 2017  1:40 AM
+
+>The generic cases (which is mainly what I'm concerned about) are necessary
+>to deal with if Global is to work with the containers. And if it doesn't
+>work with the containers, a significant number of programs couldn't use
+>Global (including most of the intended uses of Global in parallel blocks and
+>loops).
+
+Why would you want to use Global on generic 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 Tuck's proposal you would
+have to mention the corresponding access type. But there is no strong
+guarantee here, as the formal parameters of the instance could write or read
+a global variable.
+
+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.
+
+>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 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.
+
+>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 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 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 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 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 that unit.
+
+>I don't want any "except for" in Ada. Period. Good to hear that SPARK has
+>moved away from complete source code, though.
+
+It was never the case, even for the first version of SPARK 83. :-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 3, 2017  2:28 AM
+
+...
+>Why would you want to use Global on generic containers?
+
+Because it's wildly incompatible if you don't. Since Global isn't currently
+specified on existing subprograms, all existing instances would fail until
+lobal is added. (Formals would have to have to have no global, that is
+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 
+> indeed have "Global => null"
+> 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
+(free chains and a serial number exist in the proposed Janus/Ada
+implementations). Perhaps we could ban that from the bounded containers (since
+node sharing isn't an option for those), but it is a dead-body issue for me on
+the other containers.
+
+> But there is no strong guarantee here, as the formal parameters of the
+> instance could write or read a global variable.
+
+There has to be. For the intended use in Ada 2020, preventing race conditions
+and other tasking screwups, detecting only some easy cases and letting the
+hard ones get through is not an option. This is also a dead-body issue for me;
+I'm not remotely interested in parallel statements unless they are safe by
+construction (it is easy to write unsafe Ada tasking code, using something
+like Brad's Parafin libraries; the language needs no enhancements to do that).
+And without parallel statements, we don't need Global at all (there's no other
+proposed use for it at this point), and in fact we probably don't need Ada
+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 
+> 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
+started on it ASAP. If we're not willing to do that, I would like to know
+right away so that we can either abandon or redirect our other work into
+productive areas (which Global would not be).
+
+Note that it isn't impossible; I worked out all of the details for Nonblocking
+(admittedly easier in some ways as a Boolean aspect) and following that pattern
+should work fine here (just more complex for the checking). (If we replaced
+Global by a boolean aspect -- say "Task_Safe" -- it would be trivial to do;
+just do the same as Nonblocking -- but of course that is rather limiting as
+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 
+>> 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 
+> 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.
+
+As noted above, for the intended use in preventing race conditions and other
+tasking errors, this is completely unacceptable. If there is a possible race
+condition, it *must* be detected either at compile-time or run-time. There's
+no grey area there. So putting off part of it to other tools is simply
+unacceptable. Some other tool might be able to prove that something Ada doesn't
+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 
+>>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 
+>>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 
+>>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 
+>>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 
+>>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 
+>that unit.
+
+Sure, but no one is going to put System.Basic_IO into the specification of
+Ada.Text_IO. It is only referenced from the body. Moreover, the specification
+of Ada.Text_IO in the RM has to somehow reference the possibility of state in
+these packages (different for every vendor) in the Global aspects that apply
+to the Ada.Text_IO package. We're surely not putting Global => System.Basic_IO
+into the RM!!
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Tuesday, October 3, 2017  2:53 AM
+
+>Because it's wildly incompatible if you don't. Since Global isn't currently
+>specified on existing subprograms, all existing instances would fail until
+>Global is added. (Formals would have to have to have no global, that is
+>global => in out null, and that would have to be checked during
+>instantiation.)
+
+It seems to me that this extremist approach is bound to fail. I see no point
+in forcing Global on everything.
+
+>There has to be. For the intended use in Ada 2020, preventing race
+>conditions and other tasking screwups, detecting only some easy cases and
+>letting the hard ones get through is not an option. This is also a dead-body
+>issue for me; I'm not remotely interested in parallel statements unless they
+>are safe by construction (it is easy to write unsafe Ada tasking code, using
+>something like Brad's Parafin libraries; the language needs no enhancements
+>to do that). And without parallel statements, we don't need Global at all
+>(there's no other proposed use for it at this point), and in fact we
+>probably don't need Ada 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).
+
+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. 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 contracts themselves to
+other tools.
+
+>>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
+>started on it ASAP. If we're not willing to do that, I would like to know
+>right away so that we can either abandon or redirect our other work into
+>productive areas (which Global would not be).
+
+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.
+
+>>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.
+>
+>As noted above, for the intended use in preventing race conditions and other
+>tasking errors, this is completely unacceptable. If there is a possible race
+>condition, it *must* be detected either at compile-time or run-time. There's
+>no grey area there. So putting off part of it to other tools is simply
+>unacceptable. Some other tool might be able to prove that something Ada
+>doesn't allow actually is OK, and that could be useful if the "Soft Error"
+>scheme is adopted, but that's about it.
+
+OK if you can pull it, but I doubt it's possible with "just" compilation
+techniques, while managing an acceptable complexity in annotations.
+
+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.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 3, 2017  2:59 PM
+
+>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. 
+>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 
+>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 
+>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" 
+>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
+like Global to work as well). But we have to have an assume-the-worst model
+in the generic body, and some form of reflection. Without that, you have to
+have body dependences, which (A) violate the Ada generic contract model,
+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 
+>> 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. ...
+
+We have already proposed using the 'Global attribute for generics in the AI.
+The few examples we have looked at seem to make sense.
+
+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 silently unsafe.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 3, 2017  6:46 PM
+
+...
+> 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,
+not 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.)
+
+> 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 
+> silently unsafe.
+
+I think I like this better than what the AI proposes.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, October 3, 2017  9:38 PM
+
+>> 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, not 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
+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.
+
+...
+> I think I like this better than what the AI proposes.
+
+OK, let's assume we go that direction then.
+
+****************************************************************
+
+From: Jeff Cousins
+Sent: Wednesday, October 4, 2017  3:52 AM
+
+Iím afraid that I havenít seen Tuckerís original message, please could you
+re-send it? [Editor's note: Tucker did so; not shown here.]
+
+****************************************************************
+
+From: Randy Brukardt
+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 
+> to be spelled out.
+
+You also need assume-the-best/assume-the-worst rules for the meaning of the
+attributes in a generic unit.
+
+Probably these can be quite simple, too: "Subp'Global" acts like "in out all"
+in a generic specification, with a recheck on instantiation; "Subp'Global"
+acts like "in out null" in a generic body, and specifically a call to Subp is
+allowed (while it does not allow other calls) in the scope of a contract
+including "Subp'Global".
+
+...
+
+BTW, I forgot to ask if implicit composite "=" is being handled somehow.
+Since the default for Global is "all", the default for "=" would have to be
+"all" as well. Which is silly, since most "=" are pure (don't use any
+globals). That was the biggest mess for Nonblocking, as we ended up defining
+Nonblocking for types in order to change the default. (Which required generic
+unit changes as well.)
+
+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.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent