www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - assert semantic change proposal

reply "David Bregman" <drb sfu.ca> writes:
I am creating this thread because I believe the other ones [1,6] 
have gotten too bogged down in minutiae and the big picture has 
gotten lost.

Walter has proposed a change to D's assert function as follows 
[1]:
"The compiler can make use of assert expressions to improve 
optimization, even in -release mode."

I would like to raise a series of questions, comments, and 
potential objections to this proposal which I hope will help 
clarify the big picture.

1. Who and Why? What is the impetus behind this proposal? What is 
the case for it? Walter made strong statements such as "there is 
inexorable pressure for this", and "this will happen", and I am 
wondering where this is coming from. Is it just Walter? If not, 
who or what is pushing this idea? (the 'yea' side, referred to 
below)

2. Semantic change.
The proposal changes the meaning of assert(), which will result 
in breaking existing code. Regardless of philosophizing about 
whether or not the code was "already broken" according to some 
definition of assert, the fact is that shipping programs that 
worked perfectly well before may no longer work after this change.
Q2a. In other areas, code breakage has recently been anathema. 
Why is this case different?
Q2b. Has any attempt been made to estimate the impact of this 
change on existing code? Has code breakage been considered in 
making this proposal?
2c. I note that the proposal also breaks with (at least) one of 
D's stated "Major Design Goals".[2] ("Where D code looks the same 
as C code, have it either behave the same or issue an error.")

3. Undefined behavior.
The purpose of the proposal is to improve code generation, and 
this is accomplished by allowing the compiler to generate code 
with arbitrary (undefined) behavior in the case that the 
assertion does not hold. Undefined behavior is well known to be a 
source of severe problems, such as security exploits[3,4], and 
so-called "heisenbugs"[5].
3a. An alternate statement of the proposal is literally "in 
release mode, assert expressions introduce undefined behavior 
into your code in if the expression is false".
3b. Since assert is such a widely used feature (with the original 
semantics, "more asserts never hurt"), the proposal will inject a 
massive amount of undefined behavior into existing code bases, 
greatly increasing the probability of experiencing problems 
related to undefined behavior.
Q3c. Have the implications of so much additional undefined 
behavior been sufficiently considered and weighed with the 
performance benefits of the proposal?
Q3d. How can the addition of large amounts of undefined behavior 
be reconciled with D's Major Design Goals #2,3,5,15,17? [2]?
3f. I note that it has been demonstrated in the other threads 
that the proposal as it stands can even break the memory safety 
guarantee of  safe code.

4. Performance.
Q4a. What level of performance increases are expected of this 
proposal, for a representative sample of D programs?
Q4b. Is there any threshold level of expected performance 
required to justify this proposal? For example, if a study 
determined that the average program could expect a speedup of 
0.01% or less, would that still be considered a good tradeoff 
against the negatives?
Q4c. Have any works or studies, empirical or otherwise, been done 
to estimate the expected performance benefit? Is there any 
evidence at all for a speedup sufficient to justify this proposal?
Q4d. When evaluating the potential negative effects of the 
proposal on their codebase, D users may decide it is now too 
risky to compile with -release. (Even if their own code has been 
constructed with the new assert semantics in mind, the libraries 
they use might not). Thus the effect of the proposal would 
actually be to decrease the performance of their program instead 
of increase it. Has this been considered in the evaluation of 
tradeoffs?

5. High level goals
The feedback so far demonstrates that the proposal is 
controversial at least. While I do not endorse democratic or 
design-by-committee approaches to language design, I do think it 
is relevant if a large subset of users have issues with a 
proposal. Note that this is not bikeshedding, I believe it has 
now been sufficiently demonstrated there are real concerns about 
real negative effects of the proposal.
5a. Is this proposal the best way to go or is there an 
alternative that would achieve the same goals while satisfying 
both sides?
5b. Has the 'yea' side been sufficiently involved in this 
discussion? Are they aware of the tradeoffs? Mostly what I've 
seen is Walter defending the yea side from the perspective that 
the decision has already been made. Maybe if the yea side was 
consulted, they might easily agree to an alternative way of 
achieving the improved optimization goal, such as creating a new 
function that has the proposed semantics.

References:
[1]: http://forum.dlang.org/thread/lrbpvj$mih$1 digitalmars.com
[2]: http://dlang.org/overview.html
[3]: 
http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
[4]: http://blog.regehr.org/archives/213
[5]: http://en.wikipedia.org/wiki/Heisenbug
[6]: 
http://forum.dlang.org/thread/jrxrmcmeksxwlyuitzqp forum.dlang.org
Aug 03 2014
next sibling parent reply "bachmeier" <no spam.net> writes:
Thanks for the summary. I apologize for the uninformed question, 
but is it possible to explain how the change wrt assert will 
break existing code? Those details are probably buried in the 
extensive threads you've referenced. I ask because my 
understanding of assert has always been that you should use it to 
test your programs but not rely on it at runtime.


On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:
 I am creating this thread because I believe the other ones 
 [1,6] have gotten too bogged down in minutiae and the big 
 picture has gotten lost.

 Walter has proposed a change to D's assert function as follows 
 [1]:
 "The compiler can make use of assert expressions to improve 
 optimization, even in -release mode."

 I would like to raise a series of questions, comments, and 
 potential objections to this proposal which I hope will help 
 clarify the big picture.

 1. Who and Why? What is the impetus behind this proposal? What 
 is the case for it? Walter made strong statements such as 
 "there is inexorable pressure for this", and "this will 
 happen", and I am wondering where this is coming from. Is it 
 just Walter? If not, who or what is pushing this idea? (the 
 'yea' side, referred to below)

 2. Semantic change.
 The proposal changes the meaning of assert(), which will result 
 in breaking existing code. Regardless of philosophizing about 
 whether or not the code was "already broken" according to some 
 definition of assert, the fact is that shipping programs that 
 worked perfectly well before may no longer work after this 
 change.
 Q2a. In other areas, code breakage has recently been anathema. 
 Why is this case different?
 Q2b. Has any attempt been made to estimate the impact of this 
 change on existing code? Has code breakage been considered in 
 making this proposal?
 2c. I note that the proposal also breaks with (at least) one of 
 D's stated "Major Design Goals".[2] ("Where D code looks the 
 same as C code, have it either behave the same or issue an 
 error.")

 3. Undefined behavior.
 The purpose of the proposal is to improve code generation, and 
 this is accomplished by allowing the compiler to generate code 
 with arbitrary (undefined) behavior in the case that the 
 assertion does not hold. Undefined behavior is well known to be 
 a source of severe problems, such as security exploits[3,4], 
 and so-called "heisenbugs"[5].
 3a. An alternate statement of the proposal is literally "in 
 release mode, assert expressions introduce undefined behavior 
 into your code in if the expression is false".
 3b. Since assert is such a widely used feature (with the 
 original semantics, "more asserts never hurt"), the proposal 
 will inject a massive amount of undefined behavior into 
 existing code bases, greatly increasing the probability of 
 experiencing problems related to undefined behavior.
 Q3c. Have the implications of so much additional undefined 
 behavior been sufficiently considered and weighed with the 
 performance benefits of the proposal?
 Q3d. How can the addition of large amounts of undefined 
 behavior be reconciled with D's Major Design Goals 
 #2,3,5,15,17? [2]?
 3f. I note that it has been demonstrated in the other threads 
 that the proposal as it stands can even break the memory safety 
 guarantee of  safe code.

 4. Performance.
 Q4a. What level of performance increases are expected of this 
 proposal, for a representative sample of D programs?
 Q4b. Is there any threshold level of expected performance 
 required to justify this proposal? For example, if a study 
 determined that the average program could expect a speedup of 
 0.01% or less, would that still be considered a good tradeoff 
 against the negatives?
 Q4c. Have any works or studies, empirical or otherwise, been 
 done to estimate the expected performance benefit? Is there any 
 evidence at all for a speedup sufficient to justify this 
 proposal?
 Q4d. When evaluating the potential negative effects of the 
 proposal on their codebase, D users may decide it is now too 
 risky to compile with -release. (Even if their own code has 
 been constructed with the new assert semantics in mind, the 
 libraries they use might not). Thus the effect of the proposal 
 would actually be to decrease the performance of their program 
 instead of increase it. Has this been considered in the 
 evaluation of tradeoffs?

 5. High level goals
 The feedback so far demonstrates that the proposal is 
 controversial at least. While I do not endorse democratic or 
 design-by-committee approaches to language design, I do think 
 it is relevant if a large subset of users have issues with a 
 proposal. Note that this is not bikeshedding, I believe it has 
 now been sufficiently demonstrated there are real concerns 
 about real negative effects of the proposal.
 5a. Is this proposal the best way to go or is there an 
 alternative that would achieve the same goals while satisfying 
 both sides?
 5b. Has the 'yea' side been sufficiently involved in this 
 discussion? Are they aware of the tradeoffs? Mostly what I've 
 seen is Walter defending the yea side from the perspective that 
 the decision has already been made. Maybe if the yea side was 
 consulted, they might easily agree to an alternative way of 
 achieving the improved optimization goal, such as creating a 
 new function that has the proposed semantics.

 References:
 [1]: http://forum.dlang.org/thread/lrbpvj$mih$1 digitalmars.com
 [2]: http://dlang.org/overview.html
 [3]: 
 http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
 [4]: http://blog.regehr.org/archives/213
 [5]: http://en.wikipedia.org/wiki/Heisenbug
 [6]: 
 http://forum.dlang.org/thread/jrxrmcmeksxwlyuitzqp forum.dlang.org
Aug 03 2014
next sibling parent "David Bregman" <drb sfu.ca> writes:
On Sunday, 3 August 2014 at 20:05:22 UTC, bachmeier wrote:
 Thanks for the summary. I apologize for the uninformed 
 question, but is it possible to explain how the change wrt 
 assert will break existing code? Those details are probably 
 buried in the extensive threads you've referenced. I ask 
 because my understanding of assert has always been that you 
 should use it to test your programs but not rely on it at 
 runtime.
Yes, it was discussed in the threads. The basic way it happens is something like this: assert(x); if(!x) { // some side effect on the program // the optimizer will remove this path under the proposal } It's much more insidious if the assert and the if are separated by some distance, such as being in different functions or even modules. for example: assert(x < 1000); // this assert is wrong, but has never been hit during testing. unfortunate but real life programs are not bug free. someFunction(x); now suppose someFunction is a library sort of function, coded in "defensive programming" style. It does something important so it validates its input first to make sure nothing bad happens. But now someFunction is inlined, and code is generated with the (wrong) assumption that x<1000. The input validation checks are removed by the optimizer. As a result, someFunction runs with invalid input, and [user's harddrive is formatted, hacker gains root access, etc]. There are other ways too. The code does not explicitly need to have an if statement checking for !x to be broken by this - any implicit checks, any kind of control flow structures can be broken just the same.
Aug 03 2014
prev sibling next sibling parent Daniel Gibson <metalcaedes gmail.com> writes:
Am 03.08.2014 22:05, schrieb bachmeier:
 Thanks for the summary. I apologize for the uninformed question, but is
 it possible to explain how the change wrt assert will break existing
 code? Those details are probably buried in the extensive threads you've
 referenced. I ask because my understanding of assert has always been
 that you should use it to test your programs but not rely on it at runtime.
Example: assert(x !is null); if(x !is null) { x.foo = 42; } in release mode, the assert() will (as to Walters plans) tell the compiler, that x cannot be null, so it will optimize the "if(x !is null)" away. Currently this would not happen and this code won't segfault, with that optimization it would, in case in release mode x is null after all in some circumstance that hasn't occured during testing. Walters stance on this is, that if x is null under some circumstance, the program is buggy anyway and in an undefined state. Furthermore he interprets "assert()" as "the programmer asserts (as in promises) that the given condition is true". Other people say that assert(), as it's implemented in many programming languages (including D up to now), just is a runtime check with a funny name that can be deactivated (e.g. for/in release builds). Some have proposed to have an assume() that does what Walter wants assert() to do. Cheers, Daniel
Aug 03 2014
prev sibling parent reply "John Carter" <john.carter taitradio.com> writes:
On Sunday, 3 August 2014 at 20:05:22 UTC, bachmeier wrote:

 3. Undefined behavior.
Actually I have had an extensive battle within my own workplace on this subject and I think I have a reasonable insight in to both points of view. It comes down to two opposing view of what we use asserts for. My view, which I think corresponds with Walter's and Betrand Meyer's, is that asserts define what correct behaviour is. If an assert fires, your program is fundamentally defective in a manner that can only be corrected by a new version of the program. And the sooner you know that, preferably at compile time, the better. Continuing past such an assert inevitably results in defective, possibly catastrophic, possibly flaky behaviour. In the opposing view, an assert statement is a debug aid. In the same category as a logging printf. If it fires, it's "Huh. That's interesting. I didn't think that would happen, but OK, it does. Cool." Alas, these two uses have been given the same name. assert. One resolution would be to create two assert interfaces, one that the compiler pays attention to, and one that is just a "Huh. That's interesting, I didn't expect that."
Aug 03 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Sunday, 3 August 2014 at 22:18:29 UTC, John Carter wrote:
 My view, which I think corresponds with Walter's and Betrand 
 Meyer's, is that asserts define what correct behaviour is.
No. The propositions describe what the correct behaviour ought to be. The asserts request them to be proved.
 And the sooner you know that, preferably at compile time, the 
 better.
And to do that you need a theorem prover capable of solving NP-Hard problems. So you need a veeeery intelligent programmer to write provably correct code without any special tools.
 Continuing past such an assert inevitably results in defective, 
 possibly catastrophic, possibly flaky behaviour.
And Walter thinks it would a great idea to make that catastrophic behaviour occur with a much greater probability and also every time you execute your program, undetected, not only in the select few cases where slight overlap in conditions were detected. So basically if your program contains an assert that states that the program should stop working in 30 years from now, it is a good idea to make it fail randomly right away. That's the view that Andrei, Don and Walter has expressed very explicitly. People who thinks this is a great idea defies reason. They only learn from failure. You have to realize that a deduction engine cannot tolerate a single contradiction in axioms. If there is a single contradiction it can basically deduce anything, possibly undetected. Turning asserts in program+libaries into globally available axioms is insane.
Aug 03 2014
next sibling parent "David Bregman" <drb sfu.ca> writes:
On Sunday, 3 August 2014 at 22:57:24 UTC, Ola Fosheim Grøstad 
wrote:
 On Sunday, 3 August 2014 at 22:18:29 UTC, John Carter wrote:
 My view, which I think corresponds with Walter's and Betrand 
 Meyer's, is that asserts define what correct behaviour is.
No. The propositions describe what the correct behaviour ought to be. The asserts request them to be proved.
 And the sooner you know that, preferably at compile time, the 
 better.
And to do that you need a theorem prover capable of solving NP-Hard problems. So you need a veeeery intelligent programmer to write provably correct code without any special tools.
 Continuing past such an assert inevitably results in 
 defective, possibly catastrophic, possibly flaky behaviour.
And Walter thinks it would a great idea to make that catastrophic behaviour occur with a much greater probability and also every time you execute your program, undetected, not only in the select few cases where slight overlap in conditions were detected. So basically if your program contains an assert that states that the program should stop working in 30 years from now, it is a good idea to make it fail randomly right away. That's the view that Andrei, Don and Walter has expressed very explicitly. People who thinks this is a great idea defies reason. They only learn from failure. You have to realize that a deduction engine cannot tolerate a single contradiction in axioms. If there is a single contradiction it can basically deduce anything, possibly undetected. Turning asserts in program+libaries into globally available axioms is insane.
John proposes a separate function, so I think you two are in agreement on what really matters. Let's try to avoid going too deep into tangents, unlike the other threads - it didn't work well last time.
Aug 03 2014
prev sibling parent reply "John Carter" <john.carter taitradio.com> writes:
On Sunday, 3 August 2014 at 22:57:24 UTC, Ola Fosheim Grøstad 
wrote:

 Turning asserts in program+libaries into globally available 
 axioms is insane.
I guess this is the heart of the difference in the way DbC programmers program. I know that program proving is impossibly hard, so my asserts are a kind of short cut on it. I use asserts to define my architecture. So that I can say, " In my architecture, I know, by design, certain eventualities will never occur. I don't expect any compiler to be able prove that for me (although it would be nice if it could), but I certainly will be relying on these facets of the architecture." When I assert, I'm stating "In my architecture, as I designed it, this will always be true, and everything in the code downstream of here can AND DOES rely on this. My code explicitly relies on these simplifying assumptions, and will go hideously wrong if those assumptions are false.... So why can't the compiler rely on them too? Of course it can, as every single line I write after the assert is absolutely relying on the assert being true." My asserts are never "I believe this is true". They are _always_ "In this design, the following must be true, as I'm about to code absolutely relying on this fact." And if the compiler chooses to rely on it too... I can absolutely gaurantee you that differing optimizations will be the least of my worries if the expression is false. However, that said, it is very clear to me that this is a very different usage of "assert" to what many of colleagues do. Hence my suggestion we make explicit by differing names what usage we mean. Oh, and I will just thow this happy observation into the mix... in case you think this sort of optimization is too revolutionary... http://www.airs.com/blog/archives/120
Aug 03 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Sunday, 3 August 2014 at 23:54:46 UTC, John Carter wrote:
 I know that program proving is impossibly hard, so my asserts 
 are a kind of short cut on it.
Yes, but the dual is that writing a correct program is impossibly hard. A correct program works as specified for all improbable input and configurations. No shipped programs are correct. However, if you turn asserts into assume, you let the compiler use any defect in the program or the specification to prove "true==false". And after that all bets are off. With asserts on, you can tell where the flaw is. With asserts off and logging on you can figure out where the flaw is not. With asserts turned to assumes, no amount of logging can help you. You just know there is a flaw. Worse, an improbably occurring bug can now become a probable one.
 When I assert, I'm stating "In my architecture, as I designed 
 it, this will always be true, and everything in the code 
 downstream of here can AND DOES rely on this.
But it does not matter if it holds. The deduction engine in the compiler is not required to limit itself to the location of the "assert turned into axiom". It can move it upstream and downstream. It is also not only a problem of mismatch between two axioms, but between any derivable theorems.
 My code explicitly relies on these simplifying assumptions, and 
 will go hideously wrong if those assumptions are false.... So 
 why can't the compiler rely on them too?
Because the compiler can move them around and will assume all improbable configurations and input sequences.
 Of course it can, as every single line I write after the assert 
 is absolutely relying on the assert being true."
Yes, but the axioms can move anywhere. And any contradiction derivable from any set of axioms can lead to boolean expressions turned to random values anywhere in your program. Not only near the flawed assert turned into an axiom.
 My asserts are never "I believe this is true".

 They are _always_ "In this design, the following must be true, 
 as I'm about to code absolutely relying on this fact."
Yes, but if you state it differently elsewhere, indirectly (through a series of axioms), you may have a contradiction from which you can deduce "true==false" Please note that any potentially reachable code will be included in the axiom database. Not only the ones that will execute, also branches that will never execute in a running program. Those can now propagate upwards since they are true. Almost no shipped programs are correct. They are all wrong, but we take them as "working" because we don't push them to extremes very often. Let me quote from the CompCert webpage: http://compcert.inria.fr/motivations.html <<More recently, Yang et al generalized their testing of C compilers and, again, found many instances of miscompilation: We created a tool that generates random C programs, and then spent two and a half years using it to find compiler bugs. So far, we have reported more than 325 previously unknown bugs to compiler developers. Moreover, every compiler that we tested has been found to crash and also to silently generate wrong code when presented with valid inputs. (PLDI 2011) For non-critical, "everyday" software, miscompilation is an annoyance but not a major issue: bugs introduced by the compiler are negligible compared to those already present in the source program. >>
Aug 04 2014
prev sibling next sibling parent reply "John Carter" <john.carter taitradio.com> writes:
On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:

 Walter has proposed a change to D's assert function as follows 
 [1]:
 "The compiler can make use of assert expressions to improve 
 optimization, even in -release mode."
Hmm. I really really do like that idea. I suspect it is one of those ideas of Walter's that has consequences that reach further than anyone foresees..... but that's OK, because it is fundamentally the correct course of action, it's implications foreseen and unforeseen will be correct. One "near term" implication is to permit deeper static checking of the code. Both in terms of "Well, actually there is a code path in which the assert expression could be false, flag it with a warning" and in terms of "There is a code path which is unused / incorrect / erroneous is the assert expression is true", flag as an error/warning. Furthermore, in the presence of the deeper compile time function evaluation, I suspect we will get deeper and even more suprising consequences from this decision. Suddenly we have, at compile time, an expression we know to be true, always, at run time. Thus where possible, the compiler can infer as much as it can from this. The implications of that will be very very interesting and far reaching. As I said, this choice will have very far reaching and unforeseen and unforeseeable consequences.... but that's OK, since it is fundamentally the correct choice, those consequences will be correct too.
Aug 03 2014
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 2:57 PM, John Carter wrote:
 On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:

 Walter has proposed a change to D's assert function as follows [1]:
 "The compiler can make use of assert expressions to improve
 optimization, even in -release mode."
Hmm. I really really do like that idea. I suspect it is one of those ideas of Walter's that has consequences that reach further than anyone foresees..... but that's OK, because it is fundamentally the correct course of action, it's implications foreseen and unforeseen will be correct.
Agreed. One related point that has been discussed only a little is the competitive aspect of it all. Generating fast code is of paramount importance for D's survival and thriving in the market. Competition in language design and implementation is acerbic and only getting more cutthroat. In the foreseeable future efficiency will become more important at scale seeing as data is growing and frequency scaling has stalled. Availing ourselves of a built-in "assert" that has a meaning and informativeness unachievable to e.g. a C/C++ macro is a very important and attractive competitive advantage compared to these and other languages. Walter has always meant assert the way he discusses it today. Has he (and subsequently he and I) been imprecise in documenting it? Of course, but that just means it's Tuesday. That said, should we proceed carefully about realizing this advantage? Of course; that's a given. But I think it's very important to fully understand the advantages of gaining an edge over the competition. Andrei
Aug 03 2014
next sibling parent reply "David Bregman" <drb sfu.ca> writes:
On Sunday, 3 August 2014 at 22:15:52 UTC, Andrei Alexandrescu 
wrote:
 On 8/3/14, 2:57 PM, John Carter wrote:
 On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:

 Walter has proposed a change to D's assert function as 
 follows [1]:
 "The compiler can make use of assert expressions to improve
 optimization, even in -release mode."
Hmm. I really really do like that idea. I suspect it is one of those ideas of Walter's that has consequences that reach further than anyone foresees..... but that's OK, because it is fundamentally the correct course of action, it's implications foreseen and unforeseen will be correct.
Agreed.
I hope that agree was referring to some bits from the other paragraphs, and that you don't seriously agree with that blatantly self contradictory statement about unforseeable unforseens :p
 One related point that has been discussed only a little is the 
 competitive aspect of it all. Generating fast code is of 
 paramount importance for D's survival and thriving in the 
 market. Competition in language design and implementation is 
 acerbic and only getting more cutthroat. In the foreseeable 
 future efficiency will become more important at scale seeing as 
 data is growing and frequency scaling has stalled.
Would you care to address the questions about performance raised in the OP?
 Availing ourselves of a built-in "assert" that has a meaning 
 and informativeness unachievable to e.g. a C/C++ macro is a 
 very important and attractive competitive advantage compared to 
 these and other languages.
Not really, you can redefine the C macro to behave exactly as proposed, using compiler specific commands to invoke undefined behavior. Didn't you say in the other thread that you tried exactly that?
 Walter has always meant assert the way he discusses it today. 
 Has he (and subsequently he and I) been imprecise in 
 documenting it? Of course, but that just means it's Tuesday.

 That said, should we proceed carefully about realizing this 
 advantage? Of course; that's a given. But I think it's very 
 important to fully understand the advantages of gaining an edge 
 over the competition.
Please comment on the concerns raised by the OP.
Aug 03 2014
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 3:26 PM, David Bregman wrote:
 On Sunday, 3 August 2014 at 22:15:52 UTC, Andrei Alexandrescu wrote:
 One related point that has been discussed only a little is the
 competitive aspect of it all. Generating fast code is of paramount
 importance for D's survival and thriving in the market. Competition in
 language design and implementation is acerbic and only getting more
 cutthroat. In the foreseeable future efficiency will become more
 important at scale seeing as data is growing and frequency scaling has
 stalled.
Would you care to address the questions about performance raised in the OP?
I thought I just did.
 Availing ourselves of a built-in "assert" that has a meaning and
 informativeness unachievable to e.g. a C/C++ macro is a very important
 and attractive competitive advantage compared to these and other
 languages.
Not really, you can redefine the C macro to behave exactly as proposed, using compiler specific commands to invoke undefined behavior. Didn't you say in the other thread that you tried exactly that?
That might be possible, but one thing I was discussing with Walter (reverse flow analysis) may be more difficult with the traditional definition of assert. Also I'm not sure whether the C and C++ standards require assert to do nothing in NDEBUG builds.
 Walter has always meant assert the way he discusses it today. Has he
 (and subsequently he and I) been imprecise in documenting it? Of
 course, but that just means it's Tuesday.

 That said, should we proceed carefully about realizing this advantage?
 Of course; that's a given. But I think it's very important to fully
 understand the advantages of gaining an edge over the competition.
Please comment on the concerns raised by the OP.
Probably not - there's little motivation to do so. The original post is little else than a self-important rehash of a matter in which everybody has stated their opinion, several times, in an exchange that has long ran its course. Having everyone paste their thoughts once again seems counterproductive. Andrei
Aug 03 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Monday, 4 August 2014 at 00:24:19 UTC, Andrei Alexandrescu 
wrote:
 On 8/3/14, 3:26 PM, David Bregman wrote:
 On Sunday, 3 August 2014 at 22:15:52 UTC, Andrei Alexandrescu 
 wrote:
 One related point that has been discussed only a little is the
 competitive aspect of it all. Generating fast code is of 
 paramount
 importance for D's survival and thriving in the market. 
 Competition in
 language design and implementation is acerbic and only 
 getting more
 cutthroat. In the foreseeable future efficiency will become 
 more
 important at scale seeing as data is growing and frequency 
 scaling has
 stalled.
Would you care to address the questions about performance raised in the OP?
I thought I just did.
You made some generic statements about performance being good. This is obvious and undisputed. You did not answer any concerns raised in the OP. I am left to wonder if you even read it.
 Availing ourselves of a built-in "assert" that has a meaning 
 and
 informativeness unachievable to e.g. a C/C++ macro is a very 
 important
 and attractive competitive advantage compared to these and 
 other
 languages.
Not really, you can redefine the C macro to behave exactly as proposed, using compiler specific commands to invoke undefined behavior. Didn't you say in the other thread that you tried exactly that?
That might be possible, but one thing I was discussing with Walter (reverse flow analysis) may be more difficult with the traditional definition of assert. Also I'm not sure whether the C and C++ standards require assert to do nothing in NDEBUG builds.
 Walter has always meant assert the way he discusses it today. 
 Has he
 (and subsequently he and I) been imprecise in documenting it? 
 Of
 course, but that just means it's Tuesday.

 That said, should we proceed carefully about realizing this 
 advantage?
 Of course; that's a given. But I think it's very important to 
 fully
 understand the advantages of gaining an edge over the 
 competition.
Please comment on the concerns raised by the OP.
Probably not - there's little motivation to do so. The original post is little else than a self-important rehash of a matter in which everybody has stated their opinion, several times, in an exchange that has long ran its course. Having everyone paste their thoughts once again seems counterproductive.
Wow. Don't pretend like the questions are all "asked and answered". The concerns are legitimate, but the responses so far have been mostly arrogant handwaving. The fact that you believe you answered the performance concerns by merely stating "performance is important to make D competitive" is case in point. There has been no evidence presented that there are any nontrivial performance gains to be had by reusing information from asserts. There has been no case made that the performance gains (if they exist) justify code breakage and other issues. There has been no effort to determine if there are alternate ways to achieve the goals which satisfy all groups. I could go on, and on, but I refer you back to the OP. I really believe this whole thing could be handled much better, it doesn't have to be a zero sum game between the two sides of this issue. That's why I bothered to write the post, to try to achieve that.
Aug 03 2014
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 5:57 PM, David Bregman wrote:
 On Monday, 4 August 2014 at 00:24:19 UTC, Andrei Alexandrescu wrote:
 On 8/3/14, 3:26 PM, David Bregman wrote:
 On Sunday, 3 August 2014 at 22:15:52 UTC, Andrei Alexandrescu wrote:
 One related point that has been discussed only a little is the
 competitive aspect of it all. Generating fast code is of paramount
 importance for D's survival and thriving in the market. Competition in
 language design and implementation is acerbic and only getting more
 cutthroat. In the foreseeable future efficiency will become more
 important at scale seeing as data is growing and frequency scaling has
 stalled.
Would you care to address the questions about performance raised in the OP?
I thought I just did.
You made some generic statements about performance being good. This is obvious and undisputed. You did not answer any concerns raised in the OP. I am left to wonder if you even read it.
I did read it. Forgive me, but I don't have much new to answer to it. It seems you consider the lack of a long answer accompanied by research and measurements offensive, and you also find my previous answers arrogant. This, to continue what I was mentioning in another post, is the kind of stuff I find difficult to answer meaningfully. Andrei
Aug 03 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Monday, 4 August 2014 at 01:17:36 UTC, Andrei Alexandrescu 
wrote:
 On 8/3/14, 5:57 PM, David Bregman wrote:
 On Monday, 4 August 2014 at 00:24:19 UTC, Andrei Alexandrescu 
 wrote:
 On 8/3/14, 3:26 PM, David Bregman wrote:
 On Sunday, 3 August 2014 at 22:15:52 UTC, Andrei 
 Alexandrescu wrote:
 One related point that has been discussed only a little is 
 the
 competitive aspect of it all. Generating fast code is of 
 paramount
 importance for D's survival and thriving in the market. 
 Competition in
 language design and implementation is acerbic and only 
 getting more
 cutthroat. In the foreseeable future efficiency will become 
 more
 important at scale seeing as data is growing and frequency 
 scaling has
 stalled.
Would you care to address the questions about performance raised in the OP?
I thought I just did.
You made some generic statements about performance being good. This is obvious and undisputed. You did not answer any concerns raised in the OP. I am left to wonder if you even read it.
I did read it. Forgive me, but I don't have much new to answer to it. It seems you consider the lack of a long answer accompanied by research and measurements offensive, and you also find my previous answers arrogant. This, to continue what I was mentioning in another post, is the kind of stuff I find difficult to answer meaningfully.
Well, I don't want this to devolve to ad hominem level. I never used the word offensive by the way, though I will admit to being temporarily offended by your description of my carefully constructed post as a self important rehash :) Basically, I didn't find your reply useful because, as I said, you were simply stating a generality about performance (which I agree with), and not addressing any concerns at all. If you don't have time to address this stuff right now, I completely understand, you are an important and busy person. But please don't give a generality or dodge the question, and then pretend the issue is addressed. This is what I call arrogant and it is worse than no reply at all. w.r.t the one question about performance justification: I'm not necessarily asking for research papers and measurements, but based on these threads I'm not aware that there is any justification at all. For all I know this is all based on a wild guess that it will help performance "a lot", like someone who optimizes without profiling first. That certainly isn't enough to justify code breakage and massive UB injection, is it? I hope we can agree on that much at least!
Aug 03 2014
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 6:59 PM, David Bregman wrote:
 w.r.t the one question about performance justification: I'm not
 necessarily asking for research papers and measurements, but based on
 these threads I'm not aware that there is any justification at all. For
 all I know this is all based on a wild guess that it will help
 performance "a lot", like someone who optimizes without profiling first.
 That certainly isn't enough to justify code breakage and massive UB
 injection, is it? I hope we can agree on that much at least!
I think at this point (without more data) a bit of trust in one's experience would be needed. I've worked on performance on and off for years, and so has Walter. We have plenty of war stories that inform our expertise in the matter, including weird stuff like "swap these two enum values and you'll get a massive performance regressions although code is correct either way". I draw from numerous concrete cases that the right/wrong optimization at the right/wrong place may as well be the difference between winning and losing. Consider the recent php engine that gets within 20% of hhvm; heck, I know where to go to make hhvm 20% slower with 50 lines of code (compare at 2M+). Conversely, gaining those 20% were months multiplied by Facebook's best engineers. Efficiency is hard to come by and easy to waste. I consider Walter's take on "assert" a modern, refreshing take on an old pattern that nicely preserves its spirit, and a good opportunity and differential advantage for D. If anything, these long threads have strengthened that belief. It has also clarified to me that: (a) We must make sure we don't transform safe code into unsafe code; in the first approximation that may simply mean assert() has no special meaning in release mode. Also bounds checking would need to probably be not elided by assert. I consider these challenging but in good, gainful ways. (b) Deployment of optimizations must be carefully staggered and documented. Andrei
Aug 03 2014
next sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 8:22 PM, Andrei Alexandrescu wrote:
 (a) We must make sure we don't transform  safe code into unsafe code; in
 the first approximation that may simply mean assert() has no special
 meaning in release mode.
... in safe code! -- Andrei
Aug 03 2014
prev sibling next sibling parent "David Bregman" <drb sfu.ca> writes:
On Monday, 4 August 2014 at 03:22:51 UTC, Andrei Alexandrescu 
wrote:
 On 8/3/14, 6:59 PM, David Bregman wrote:
 w.r.t the one question about performance justification: I'm not
 necessarily asking for research papers and measurements, but 
 based on
 these threads I'm not aware that there is any justification at 
 all. For
 all I know this is all based on a wild guess that it will help
 performance "a lot", like someone who optimizes without 
 profiling first.
 That certainly isn't enough to justify code breakage and 
 massive UB
 injection, is it? I hope we can agree on that much at least!
I think at this point (without more data) a bit of trust in one's experience would be needed. I've worked on performance on and off for years, and so has Walter. We have plenty of war stories that inform our expertise in the matter, including weird stuff like "swap these two enum values and you'll get a massive performance regressions although code is correct either way". I draw from numerous concrete cases that the right/wrong optimization at the right/wrong place may as well be the difference between winning and losing. Consider the recent php engine that gets within 20% of hhvm; heck, I know where to go to make hhvm 20% slower with 50 lines of code (compare at 2M+). Conversely, gaining those 20% were months multiplied by Facebook's best engineers. Efficiency is hard to come by and easy to waste. I consider Walter's take on "assert" a modern, refreshing take on an old pattern that nicely preserves its spirit, and a good opportunity and differential advantage for D. If anything, these long threads have strengthened that belief. It has also clarified to me that: (a) We must make sure we don't transform safe code into unsafe code; in the first approximation that may simply mean assert() has no special meaning in release mode. Also bounds checking would need to probably be not elided by assert. I consider these challenging but in good, gainful ways. (b) Deployment of optimizations must be carefully staggered and documented. Andrei
First of all, thank you for the reply. I agree with nearly everything you say. I also have significant experience with code optimization. I greatly enjoyed the talk you gave on C++ optimization, partly because it validated what I've spent so much of my own efforts doing. I think we reach different conclusions from our experience though, my feeling is that typical asserts are unlikely to contain much info that can give a speedup. This is not to say that the compiler can't be helped by extra information, on the contrary I wholeheartedly believe it can. However I would guess this will usually require the asserts to be specifically written for that purpose, using inside knowledge about the kinds of information the optimizer is capable of using. In the end there isn't a substitute for measurement, so if we rely on experience we're both just guessing. Is it really justified to say that we're going to break stuff on a hunch it'll help performance? Considering the downsides to reusing existing asserts, what if you're wrong about performance? If new, specialized asserts need to be written anyways, we might as well use a new keyword and avoid all the downsides, essentially giving the best of both worlds. Also, I'm still curious about how you are evaluating the performance tradeoff in the first place, or do you even see it as a tradeoff? Is your estimation of the downside so small that any performance increase at all is sufficient to justify semantic change, UB injection and code breakage? If so then I see why you treat it as a forgone conclusion, certainly in a large enough codebase there will be some asserts here and there that allow you to shave off some instructions.
Aug 03 2014
prev sibling parent "Kagamin" <spam here.lot> writes:
On Monday, 4 August 2014 at 03:22:51 UTC, Andrei Alexandrescu 
wrote:
 Efficiency is hard to come by and easy to waste.
It's perfectly understandable, why one would want unsafe optimizations, and D already has the way to provide unsafe features: safe is default, unsafe is possible when requested explicitly. I'd say -Ounsafe switch would be good, it would enable various unsafe optimizations; other examples are fast math and no signed overflow assumption. They just shouldn't be forced on everyone, then you will get the upside you want and others won't get the downside they didn't want. Efficiency is not very hard: currently `assert` is not the most prominent direction of optimizations, I'd recommend to improve inlining and deep inlining of ranges so that they will become as fast as hand-written cycles or even faster. That would be much more beneficial. Or ask bearophile, he can have more ideas for very beneficial optimizations, or ask everyone.
Aug 05 2014
prev sibling next sibling parent reply Daniel Gibson <metalcaedes gmail.com> writes:
Am 04.08.2014 00:15, schrieb Andrei Alexandrescu:
 That said, should we proceed carefully about realizing this advantage?
 Of course; that's a given. But I think it's very important to fully
 understand the advantages of gaining an edge over the competition.
Gaining an edge over the competition? "A new DMD release broke my code in a totally unexpected way and people tell me it's because I'm using assert() wrong. I've been using it like this in C/C++/Java/Python and D since forever and *now*, after >10years, they changed D's meaning of assert() to somehow imply assume() and optimize my safety-checks away.. they pretend it was always planned like this but they never got around to tell anyone until recently. It took me a week to find this freaking bug!" Doesn't really sound like the kind of advantage over the competition that many people would appreciate. If some rant like this (from Reddit or whatever) is the first impression someone gets of D, he's unlikely to ever take a closer look, regardless of the many merits the language actually has. (Yes, Johhannes Pfau actually brought a similar argument somewhere in the depth of one of the other threads) D could still get this kind of edge over the competition by doing these kind of optimizations when another keyword (like assume()) is used - without breaking any code. Cheers, Daniel
Aug 03 2014
next sibling parent reply Dmitry Olshansky <dmitry.olsh gmail.com> writes:
04-Aug-2014 02:35, Daniel Gibson пишет:
 Am 04.08.2014 00:15, schrieb Andrei Alexandrescu:
 That said, should we proceed carefully about realizing this advantage?
 Of course; that's a given. But I think it's very important to fully
 understand the advantages of gaining an edge over the competition.
Gaining an edge over the competition? "A new DMD release broke my code in a totally unexpected way and people tell me it's because I'm using assert() wrong. I've been using it like this in C/C++/Java/Python and D since forever and *now*, after >10years, they changed D's meaning of assert() to somehow imply assume() and optimize my safety-checks away.. they pretend it was always planned like this but they never got around to tell anyone until recently. It took me a week to find this freaking bug!"
Wait a sec - it's not any better even today, it already strips them away. So unless debugging "-release -O -inline" programs is considered a norm nothing changes. -- Dmitry Olshansky
Aug 03 2014
parent Daniel Gibson <metalcaedes gmail.com> writes:
Am 04.08.2014 00:45, schrieb Dmitry Olshansky:
 04-Aug-2014 02:35, Daniel Gibson пишет:
 Am 04.08.2014 00:15, schrieb Andrei Alexandrescu:
 That said, should we proceed carefully about realizing this advantage?
 Of course; that's a given. But I think it's very important to fully
 understand the advantages of gaining an edge over the competition.
Gaining an edge over the competition? "A new DMD release broke my code in a totally unexpected way and people tell me it's because I'm using assert() wrong. I've been using it like this in C/C++/Java/Python and D since forever and *now*, after >10years, they changed D's meaning of assert() to somehow imply assume() and optimize my safety-checks away.. they pretend it was always planned like this but they never got around to tell anyone until recently. It took me a week to find this freaking bug!"
Wait a sec - it's not any better even today, it already strips them away. So unless debugging "-release -O -inline" programs is considered a norm nothing changes.
It strips them away, but it doesn't eliminate other code based on the (removed) assertion. See my other post for an example.
Aug 03 2014
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 3:35 PM, Daniel Gibson wrote:
 Am 04.08.2014 00:15, schrieb Andrei Alexandrescu:
 That said, should we proceed carefully about realizing this advantage?
 Of course; that's a given. But I think it's very important to fully
 understand the advantages of gaining an edge over the competition.
Gaining an edge over the competition?
Yes, as I explained.
 "A new DMD release broke my code in a totally unexpected way and people
 tell me it's because I'm using assert() wrong.
This has been discussed several times, and I agree there's downside. All I want to do is raise awareness of the upside, which is solid but probably less obvious to some. There's no need to trot again in response the downside that has been mentioned many times already.
 I've been using it like this in C/C++/Java/Python and D since forever
 and *now*, after >10years, they changed D's meaning of assert() to
 somehow imply assume() and optimize my safety-checks away.. they pretend
 it was always planned like this but they never got around to tell anyone
 until recently.
 It took me a week to find this freaking bug!"

 Doesn't really sound like the kind of advantage over the competition
 that many people would appreciate.

 If some rant like this (from Reddit or whatever) is the first impression
 someone gets of D, he's unlikely to ever take a closer look, regardless
 of the many merits the language actually has.
From what I remember there has been good reception (both on reddit and at work) of increased aggressiveness of compiler optimizations.
 (Yes, Johhannes Pfau actually brought a similar  argument somewhere in
 the depth of one of the other threads)

 D could still get this kind of edge over the competition by doing these
 kind of optimizations when another keyword (like assume()) is used -
 without breaking any code.
I don't think D will add assume(). Andrei
Aug 03 2014
parent reply Daniel Gibson <metalcaedes gmail.com> writes:
Am 04.08.2014 02:28, schrieb Andrei Alexandrescu:
 On 8/3/14, 3:35 PM, Daniel Gibson wrote:
 Am 04.08.2014 00:15, schrieb Andrei Alexandrescu:
 That said, should we proceed carefully about realizing this advantage?
 Of course; that's a given. But I think it's very important to fully
 understand the advantages of gaining an edge over the competition.
Gaining an edge over the competition?
Yes, as I explained.
 "A new DMD release broke my code in a totally unexpected way and people
 tell me it's because I'm using assert() wrong.
This has been discussed several times, and I agree there's downside. All I want to do is raise awareness of the upside, which is solid but probably less obvious to some. There's no need to trot again in response the downside that has been mentioned many times already.
Ok, so you agree that there's a downside and code (that you consider incorrect, but that most probably exists and works ok so far) will *silently* break (as in: the compiler won't tell you about it). So when should this change be introduced? In 2.x or in D3? I don't really like the idea of introducing a silently breaking change in a minor version - and it destroys the trust into future decisions for D. Cheers, Daniel
Aug 03 2014
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 5:40 PM, Daniel Gibson wrote:
 Ok, so you agree that there's a downside and code (that you consider
 incorrect, but that most probably exists and works ok so far) will
 *silently* break (as in: the compiler won't tell you about it).
Yes, I agree there's a downside. I missed the part where you agreed there's an upside :o).
 So when should this change be introduced? In 2.x or in D3?
More aggressive optimizations should be introduced gradually in future releases of the D compilers. I think your perception of the downside is greater, and that of the upside is lesser, than mine.
 I don't really like the idea of introducing a silently breaking change
 in a minor version - and it destroys the trust into future decisions for D.
I understand. At some point there are judgment calls to be made that aren't going to please everybody. Andrei
Aug 03 2014
parent Daniel Gibson <metalcaedes gmail.com> writes:
Am 04.08.2014 03:02, schrieb Andrei Alexandrescu:
 On 8/3/14, 5:40 PM, Daniel Gibson wrote:
 Ok, so you agree that there's a downside and code (that you consider
 incorrect, but that most probably exists and works ok so far) will
 *silently* break (as in: the compiler won't tell you about it).
Yes, I agree there's a downside. I missed the part where you agreed there's an upside :o).
I see a small upside in the concept of "syntax that tells the compiler it can take something for granted for optimization and that causes an error in debug mode". For me this kind of optimization is similar to GCC's __builtin_expect() to aid branch-prediction: probably useful to get even more performance, but I guess I wouldn't use it in everyday code. However, I see no upside in redefining an existent keyword (that had a different meaning.. or at least behavior.. before and in most programming languages) to achieve this. /Maybe/ an attribute for assert() would also be ok, so we don't need a new keyword: optimize assert(x); or hint, promise, always, for_real, whatever. Cheers, Daniel
Aug 03 2014
prev sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08/04/2014 12:15 AM, Andrei Alexandrescu wrote:
 I suspect it is one of those ideas of Walter's that has consequences
 that reach further than anyone foresees..... but that's OK, because it
 is fundamentally the correct course of action, it's implications
 foreseen and unforeseen will be correct.
Agreed.
No, please hold on. Walter is not a supernatural being.
 Walter has always meant assert the way he discusses it today.
This argument has no merit. Please stop bringing it up.
 That said, should we proceed carefully about realizing this advantage? Of
course; that's a given.
That is reasonable.
But I think it's very important to fully understand
 the advantages of gaining an edge over the competition.
Note that this is achievable without claiming the Humpty Dumpty privilege once again. Furthermore the potential for the development of concepts is actually usually larger if concepts stay properly separated from the beginning. E.g. the current proposal already has the issue that an assumption of unreachability cannot be expressed in the straightforward way: switch(x){ // ... default: assert(0); // cannot be optimized away in -release }
Aug 03 2014
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 4:01 PM, Timon Gehr wrote:
 On 08/04/2014 12:15 AM, Andrei Alexandrescu wrote:
 I suspect it is one of those ideas of Walter's that has consequences
 that reach further than anyone foresees..... but that's OK, because it
 is fundamentally the correct course of action, it's implications
 foreseen and unforeseen will be correct.
Agreed.
No, please hold on. Walter is not a supernatural being.
There's something to be said about vision and perspective.
 Walter has always meant assert the way he discusses it today.
This argument has no merit. Please stop bringing it up.
Actually it does offer value: for a large fragment of the discussion, Walter has been confused that people have a very different understanding of assert than his. Andrei
Aug 03 2014
parent Daniel Gibson <metalcaedes gmail.com> writes:
Am 04.08.2014 02:30, schrieb Andrei Alexandrescu:
 On 8/3/14, 4:01 PM, Timon Gehr wrote:
 On 08/04/2014 12:15 AM, Andrei Alexandrescu wrote:
 I suspect it is one of those ideas of Walter's that has consequences
 that reach further than anyone foresees..... but that's OK, because it
 is fundamentally the correct course of action, it's implications
 foreseen and unforeseen will be correct.
Agreed.
No, please hold on. Walter is not a supernatural being.
There's something to be said about vision and perspective.
 Walter has always meant assert the way he discusses it today.
This argument has no merit. Please stop bringing it up.
Actually it does offer value: for a large fragment of the discussion, Walter has been confused that people have a very different understanding of assert than his.
Yes, this kinda helps understanding Walters point. But as his point has only been communicated to *you*, not D users in general, you (and Walter) could be more understanding towards them being surprised and confused by this change of asserts()'s semantics. Instead you insist that your interpretation of what assert() should *mean* is the ultimate truth, even though assert() doesn't *behave* like that way in current D or any popular programming language I know of. BTW, TCPL ("KnR") (Second Edition) defines assert as: "The assert macro is used to add diagnostics to programs: void assert(int expression) If expression is zero when assert(expression) is executed, the assert macro will print on stderr a message, (...) It then calls abort to terminate execution. (...) If NDEBUG is defined at the time <assert.h> is included, the assert macro is ignored." Of course KnR is not the ultimate truth, but it shows that there have been definitions (by clever people!) of assert() that contradict yours for a long time. Cheers, Daniel
Aug 03 2014
prev sibling parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/3/2014 4:01 PM, Timon Gehr wrote:
 Walter is not a supernatural being.
Yes, I am. I demand tribute.
Aug 05 2014
prev sibling next sibling parent "David Bregman" <drb sfu.ca> writes:
On Sunday, 3 August 2014 at 21:57:08 UTC, John Carter wrote:

 One "near term" implication is to permit deeper static checking 
 of the code.
 Both in terms of "Well, actually there is a code path in which 
 the assert expression could be false, flag it with a warning" 
 and in terms of "There is a code path which is unused / 
 incorrect / erroneous is the assert expression is true", flag 
 as an error/warning.

 Furthermore, in the presence of the deeper compile time 
 function evaluation, I suspect we will get deeper and even more 
 suprising consequences from this decision.

 Suddenly we have, at compile time, an expression we know to be 
 true, always, at run time. Thus where possible, the compiler 
 can infer as much as it can from this.

 The implications of that will be very very interesting and far 
 reaching.
I totally agree, static analysis tools should consider information contained in asserts. In the case of C/C++, I believe many of the analysis tools already do this. That doesn't mean it's a good idea for this information to be used for optimization though, for reasons explained in the OP.
 As I said, this choice will have very far reaching and 
 unforeseen and unforeseeable consequences.... but that's OK, 
 since it is fundamentally the correct choice, those 
 consequences will be correct too.
This is mystical sounding gibberish. If the consequences are unforseen and unforseeable, then by definition you cannot forsee that they are correct.
Aug 03 2014
prev sibling next sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Sunday, 3 August 2014 at 21:57:08 UTC, John Carter wrote:
 consequences that reach further than anyone foresees..... but 
 that's OK, because it is fundamentally the correct course of 
 action, it's implications foreseen and unforeseen will be 
 correct.
The implications are foreseen. Any assert that will depend on any kind of notion of progress over time risk blowing up random logic undetected with a decent optimizer (> dmd). But go ahead. This will lead to a fork.
Aug 03 2014
parent reply "John Carter" <john.carter taitradio.com> writes:
On Sunday, 3 August 2014 at 22:19:16 UTC, Ola Fosheim Grøstad 
wrote:

 But go ahead. This will lead to a fork.
What should fork is the two opposing intentions for assert. They should have two different names and different consequences. On Sunday, 3 August 2014 at 22:18:29 UTC, John Carter wrote:
 It comes down to two opposing view of what we use asserts for.
To give a more concrete example of this... in the team I work with we have the following issue. When the DbC type programmers turn "asserts are fatal" on, we get asserts firing all over the place in non-DbC programmers code. On closer inspection these come down to things like "stupid factory didn't connect cable A to device B, the installation instructions are clear, the cable always should be attached in the production model". And the solution is one of... * Find a Device B and plug cable A into it. * There is a bug somewhere in the firmware. * There is a bug in the firmware of device B * You have a debugger in the entrails of device B, so the heartbeat stopped. * Something somewhere increased the latency so the timeout fired, maybe increase timeout.. Whereas for DbC programmers a pre-condition assert firing meant _very_ directly that the function that _directly_ invoked me is clearly defective in this manner. The bug is undoubtably there, there may be a bug elsewhere as well, but it is undoubtably a bug in my calling routine if it let defective values propagate as far as me. Or if a postcondition assert fired, it means, _this_ function is defective in this manner. The simple harsh fact is DbC type programmers mean completely different things to non DbC type programmers by "assert", yet unfortunately it is mapped on to the same thing with the same name. The obvious simple correct resolution is to give them two different names.
Aug 03 2014
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08/04/2014 12:51 AM, John Carter wrote:
 On Sunday, 3 August 2014 at 22:19:16 UTC, Ola Fosheim Grøstad wrote:

 But go ahead. This will lead to a fork.
What should fork is the two opposing intentions for assert. They should have two different names and different consequences.
Yes. :)
Aug 03 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Sunday, 3 August 2014 at 23:05:23 UTC, Timon Gehr wrote:
 On 08/04/2014 12:51 AM, John Carter wrote:
 But go ahead. This will lead to a fork.
What should fork is the two opposing intentions for assert. They should have two different names and different consequences.
Yes. :)
If "assert" remains having assume semantics then it basically means that you will have to rewrite all libraries. Switching the names of "assert" and "assume" is comparable to asking me to drive a car where the accelerator and break pedals have switched positions. Adjusting the compiler is less work…
Aug 04 2014
prev sibling parent "David Bregman" <drb sfu.ca> writes:
On Sunday, 3 August 2014 at 22:51:58 UTC, John Carter wrote:
 The obvious simple correct resolution is to give them two 
 different names.
Agreed, but it remains to see if those in favor of the original proposal will agree also.
Aug 03 2014
prev sibling parent reply "deadalnix" <deadalnix gmail.com> writes:
On Sunday, 3 August 2014 at 21:57:08 UTC, John Carter wrote:
 On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:

 Walter has proposed a change to D's assert function as follows 
 [1]:
 "The compiler can make use of assert expressions to improve 
 optimization, even in -release mode."
Hmm. I really really do like that idea. I suspect it is one of those ideas of Walter's that has consequences that reach further than anyone foresees..... but that's OK, because it is fundamentally the correct course of action, it's implications foreseen and unforeseen will be correct. One "near term" implication is to permit deeper static checking of the code.
I allow myself to chime in. I don't have much time to follow the whole thing, but I have this in my mind for quite a while. First thing first, the proposed behavior is what I had in mind for SDC since pretty much day 1. It already uses hint for the optimizer to tell it the branch won't be taken, but I definitively want to go further. By definition, when an assert has been removed in release that would have failed in debug, you are in undefined behavior land already. So there is no reason not to optimize.
Aug 03 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Monday, 4 August 2014 at 02:40:49 UTC, deadalnix wrote:
 I allow myself to chime in. I don't have much time to follow 
 the whole thing, but I have this in my mind for quite a while.

 First thing first, the proposed behavior is what I had in mind 
 for SDC since pretty much day 1. It already uses hint for the 
 optimizer to tell it the branch won't be taken, but I 
 definitively want to go further.
Not everyone had that definition in mind when writing their asserts.
 By definition, when an assert has been removed in release that 
 would have failed in debug, you are in undefined behavior land 
 already. So there is no reason not to optimize.
By the new definition, yes. But is it reasonable to change the definition, and then retroactively declare previous code broken? Maybe the ends justify the means in this case but it certainly isn't obvious that they do. I don't understand why breaking code is sacrilege one time, and the next time can be done without any justifications.
Aug 03 2014
parent "deadalnix" <deadalnix gmail.com> writes:
On Monday, 4 August 2014 at 02:56:35 UTC, David Bregman wrote:
 On Monday, 4 August 2014 at 02:40:49 UTC, deadalnix wrote:
 I allow myself to chime in. I don't have much time to follow 
 the whole thing, but I have this in my mind for quite a while.

 First thing first, the proposed behavior is what I had in mind 
 for SDC since pretty much day 1. It already uses hint for the 
 optimizer to tell it the branch won't be taken, but I 
 definitively want to go further.
Not everyone had that definition in mind when writing their asserts.
 By definition, when an assert has been removed in release that 
 would have failed in debug, you are in undefined behavior land 
 already. So there is no reason not to optimize.
By the new definition, yes. But is it reasonable to change the definition, and then retroactively declare previous code broken? Maybe the ends justify the means in this case but it certainly isn't obvious that they do. I don't understand why breaking code is sacrilege one time, and the next time can be done without any justifications.
The fact that the compiler can optimize based on assert is not new in D world. Maybe it wasn't advertized properly, but it always was an option. If one want to make sure a check is done, one can use expect.
Aug 03 2014
prev sibling next sibling parent reply Martin Krejcirik <mk-junk i-line.cz> writes:
On 3.8.2014 21:47, David Bregman wrote:
 Walter has proposed a change to D's assert function as follows [1]:
 "The compiler can make use of assert expressions to improve
 optimization, even in -release mode."
Couldn't this new assert behaviour be introduced as a new optimization switch ? Say -Oassert ? It would be off by default and would work both in debug and release mode. -- mk
Aug 03 2014
next sibling parent "David Bregman" <drb sfu.ca> writes:
On Sunday, 3 August 2014 at 23:24:08 UTC, Martin Krejcirik wrote:
 On 3.8.2014 21:47, David Bregman wrote:
 Walter has proposed a change to D's assert function as follows 
 [1]:
 "The compiler can make use of assert expressions to improve
 optimization, even in -release mode."
Couldn't this new assert behaviour be introduced as a new optimization switch ? Say -Oassert ? It would be off by default and would work both in debug and release mode.
That would be an improvement over the current proposal in my opinion, but I see some issues. One is the general argument against more compiler switches: complexity, and people will always enable stuff that seems like it might give the fastest code. Another is how do you mix and match code which is meant to be compiled with or without the switch? I suppose it could also be used in complement to a new function that has the proposed behavior regardless of switches. Regardless, it goes to show there exists a design space of possible alternatives to the proposal.
Aug 03 2014
prev sibling next sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 4:24 PM, Martin Krejcirik wrote:
 On 3.8.2014 21:47, David Bregman wrote:
 Walter has proposed a change to D's assert function as follows [1]:
 "The compiler can make use of assert expressions to improve
 optimization, even in -release mode."
Couldn't this new assert behaviour be introduced as a new optimization switch ? Say -Oassert ? It would be off by default and would work both in debug and release mode.
That sounds like a good idea for careful introducing of assert-driven optimizations. -- Andrei
Aug 03 2014
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/3/2014 4:24 PM, Martin Krejcirik wrote:
 Couldn't this new assert behaviour be introduced as a new optimization
 switch ? Say -Oassert ? It would be off by default and would work both
 in debug and release mode.
It could, but every one of these: 1. doubles the time it takes to test dmd, it doesn't take many of these to render dmd untestable 2. adds confusion to most programmers as to what switch does what 3. adds complexity, i.e. bugs 4. interactions between optimization switches often exhibits emergent behavior - i.e. extremely hard to test for
Aug 05 2014
parent "Kagamin" <spam here.lot> writes:
On Wednesday, 6 August 2014 at 00:50:07 UTC, Walter Bright wrote:
 On 8/3/2014 4:24 PM, Martin Krejcirik wrote:
 Couldn't this new assert behaviour be introduced as a new 
 optimization
 switch ? Say -Oassert ? It would be off by default and would 
 work both
 in debug and release mode.
It could, but every one of these: 1. doubles the time it takes to test dmd, it doesn't take many of these to render dmd untestable 2. adds confusion to most programmers as to what switch does what 3. adds complexity, i.e. bugs
If performance is not worth associated complexity, then it doesn't pull its weight.
 4. interactions between optimization switches often exhibits 
 emergent behavior - i.e. extremely hard to test for
Why do you think the emergent behavior is caused by interactions between switches, you think optimizations themselves don't interact? You said, it's factorial, is it a number of permutations of switches or a number of permutations of optimizations? Switches should not be sensitive to permutations. On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:
 1. it's long with an unappealing hackish look
It's an established practice in D that unsafe features should look unappealing. Example: __gshared.
 3. users will be faced with two kinds of asserts, with a subtle 
 difference that is hard to explain, hard to remember which is 
 which, and will most likely use inappropriately
Andrei already proposed `debug assert` - a safe flavor of (dangerous by default) assert. So two kinds of assert are inevitable and should be documented, because user should be informed about dangerous optimizations. But frankly "compiler will break your code" is not a subtle difference and can be easily explained in just 5 words. And BTW why safe behavior must be invoked with an extra syntax? That goes against best D practices and hence surprising, confusing and counterintuitive.
 I'll sum up with the old saw that any programming problem can 
 be solved with another level of indirection. I submit a 
 corollary that any language issue can be solved by adding 
 another keyword or compiler flag. The (much) harder thing is to 
 solve a problem with an elegant solution that does not involve 
 new keywords/flags, and fits in naturally.
So what is this elegant solution? To break code silently in the worst possible way and selectively and exactly at the most critical points? Another downside of assert being dangerous - you can't add it to code freely. Every assert can order the compiler to break the code, adding an assert becomes a difficult task, because the asserted expression (being assumed) begins to require a thorough future-proof environment-independent proof, which is very hard to come by: it needs to be an actual proof than just a guess, because the tradeoff is to be literally punished by death. Unittests don't provide such proof.
Aug 06 2014
prev sibling next sibling parent reply "Mike Farnsworth" <mike.farnsworth gmail.com> writes:
This all seems to have a very simple solution, to use something 
like: expect()

GCC for example has an intrinsic, __builtin_expect() that is used 
to notify the compiler of a data constraint it can use in 
optimization for branches.  Why not make something like this a 
first-class citizen in D (and even expand the concept to more 
than just branch prediction)?

That way you don't have to hijack the meaning of assert(), but 
optimizations can be made based on the condition.  
__buitin_expect() in gcc usually just figures the expected 
condition is fulfilled the vast majority of the time, but it 
could be expanded to make a lack of fulfillment trigger an 
exception (in non-release mode).  And the compiler is always free 
to optimize with the assumption the expectation is met.

On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:
 I am creating this thread because I believe the other ones 
 [1,6] have gotten too bogged down in minutiae and the big 
 picture has gotten lost.

 ...

 References:
 [1]: http://forum.dlang.org/thread/lrbpvj$mih$1 digitalmars.com
 [2]: http://dlang.org/overview.html
 [3]: 
 http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
 [4]: http://blog.regehr.org/archives/213
 [5]: http://en.wikipedia.org/wiki/Heisenbug
 [6]: 
 http://forum.dlang.org/thread/jrxrmcmeksxwlyuitzqp forum.dlang.org
Aug 03 2014
next sibling parent "David Bregman" <drb sfu.ca> writes:
On Sunday, 3 August 2014 at 23:51:30 UTC, Mike Farnsworth wrote:
 This all seems to have a very simple solution, to use something 
 like: expect()

 GCC for example has an intrinsic, __builtin_expect() that is 
 used to notify the compiler of a data constraint it can use in 
 optimization for branches.  Why not make something like this a 
 first-class citizen in D (and even expand the concept to more 
 than just branch prediction)?

 That way you don't have to hijack the meaning of assert(), but 
 optimizations can be made based on the condition.  
 __buitin_expect() in gcc usually just figures the expected 
 condition is fulfilled the vast majority of the time, but it 
 could be expanded to make a lack of fulfillment trigger an 
 exception (in non-release mode).  And the compiler is always 
 free to optimize with the assumption the expectation is met.
Indeed, having a new function instead of hijacking assert would seem to be the obvious solution. That's really interesting about the possibility of conveying probabilistic information to the compiler. Of course, we'd need different functions for constant axioms and probabilistic ones: we could use (for example) assume() for constants and expect() for probabilities.
Aug 03 2014
prev sibling next sibling parent Daniel Gibson <metalcaedes gmail.com> writes:
Well, this is not just about branch prediction, but about "let the 
compiler assume the condition is always true and let it eliminate code 
that handles other cases".

I /think/ that in C with GCC assume() could be implemented (for release 
mode, otherwise it's just like assert()) like
   #define assume(cond) if(!(cond)) __builtin_unreachable()
I'm not sure what kind of optimizations GCC does based on "unreachable", 
though.

However, something like expect() /might/ be a useful addition to the 
language as well. Maybe as an annotation for if()/else?

Cheers,
Daniel

Am 04.08.2014 01:51, schrieb Mike Farnsworth:
 This all seems to have a very simple solution, to use something like:
 expect()

 GCC for example has an intrinsic, __builtin_expect() that is used to
 notify the compiler of a data constraint it can use in optimization for
 branches.  Why not make something like this a first-class citizen in D
 (and even expand the concept to more than just branch prediction)?

 That way you don't have to hijack the meaning of assert(), but
 optimizations can be made based on the condition. __buitin_expect() in
 gcc usually just figures the expected condition is fulfilled the vast
 majority of the time, but it could be expanded to make a lack of
 fulfillment trigger an exception (in non-release mode).  And the
 compiler is always free to optimize with the assumption the expectation
 is met.

 On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:
 I am creating this thread because I believe the other ones [1,6] have
 gotten too bogged down in minutiae and the big picture has gotten lost.

 ...

 References:
 [1]: http://forum.dlang.org/thread/lrbpvj$mih$1 digitalmars.com
 [2]: http://dlang.org/overview.html
 [3]:
 http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
 [4]: http://blog.regehr.org/archives/213
 [5]: http://en.wikipedia.org/wiki/Heisenbug
 [6]: http://forum.dlang.org/thread/jrxrmcmeksxwlyuitzqp forum.dlang.org
Aug 03 2014
prev sibling next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 4:51 PM, Mike Farnsworth wrote:
 This all seems to have a very simple solution, to use something like:
 expect()

 GCC for example has an intrinsic, __builtin_expect() that is used to
 notify the compiler of a data constraint it can use in optimization for
 branches.  Why not make something like this a first-class citizen in D
 (and even expand the concept to more than just branch prediction)?
__builtin_expect is actually not that. It still generates code when the expression is false. It simply uses the static assumption to minimize jumps and maximize straight execution for the true case. -- Andrei
Aug 03 2014
parent "Mike Farnsworth" <mike.farnsworth gmail.com> writes:
On Monday, 4 August 2014 at 00:34:30 UTC, Andrei Alexandrescu 
wrote:
 On 8/3/14, 4:51 PM, Mike Farnsworth wrote:
 This all seems to have a very simple solution, to use 
 something like:
 expect()

 GCC for example has an intrinsic, __builtin_expect() that is 
 used to
 notify the compiler of a data constraint it can use in 
 optimization for
 branches.  Why not make something like this a first-class 
 citizen in D
 (and even expand the concept to more than just branch 
 prediction)?
__builtin_expect is actually not that. It still generates code when the expression is false. It simply uses the static assumption to minimize jumps and maximize straight execution for the true case. -- Andrei
Yes, that's why I pointed out expanding it to actually throw an exception when the expectation isn't meant. I guess that's really more like assume() that has been mentioned? At EA we used two versions of an assertion: assert() which compiled out in non-debug builds, etc; and verify() that was kept in non-debug builds but just boiled back down to the condition. The latter was when we relied on the side-effects of the logic (used the condition in a real runtime branch), but really we wanted to know if it ever took the else so to speak as that was an error we never wanted to ship with. FFIW, at my current job, in C++ we use assert() that compiles out for final builds (very performance-driven code, so even the conditions tested have to scat), and we also have likely() and unlikely() macros that take advantage of __builtin_expect(). There are only a few places where we do both, where the assertion may be violated and we still want to recover nicely from it, but still don't want the performance suck of the else case code polluting the instruction cache.
Aug 03 2014
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/3/2014 4:51 PM, Mike Farnsworth wrote:
 This all seems to have a very simple solution, to use something like: expect()
I see code coming that looks like: expect(x > 2); // must be true assert(x > 2); // check that it is true All I can think of is, shoot me now :-)
Aug 05 2014
parent reply "Tofu Ninja" <emmons0 purdue.edu> writes:
On Wednesday, 6 August 2014 at 00:52:32 UTC, Walter Bright wrote:
 On 8/3/2014 4:51 PM, Mike Farnsworth wrote:
 This all seems to have a very simple solution, to use 
 something like: expect()
I see code coming that looks like: expect(x > 2); // must be true assert(x > 2); // check that it is true All I can think of is, shoot me now :-)
How about something like expected assert(x > 2); or assumed assert(x > 2); It wouldn't introduce a new keyword, but still introduces the expected/assumed semantics. You should keep in mind that you might have to make a compromise, regardless of your feelings on the subject. Also, I am going to try to say this in as respectful a way as I can... Please stop responding in such a dismissive way, I think it is already pretty obvious that some are getting frustrated by these threads. Responding in a dismissive way makes it seem like you don't take the arguments seriously.
Aug 05 2014
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/5/14, 11:28 PM, Tofu Ninja wrote:
 On Wednesday, 6 August 2014 at 00:52:32 UTC, Walter Bright wrote:
 On 8/3/2014 4:51 PM, Mike Farnsworth wrote:
 This all seems to have a very simple solution, to use something like:
 expect()
I see code coming that looks like: expect(x > 2); // must be true assert(x > 2); // check that it is true All I can think of is, shoot me now :-)
How about something like expected assert(x > 2); or assumed assert(x > 2); It wouldn't introduce a new keyword, but still introduces the expected/assumed semantics. You should keep in mind that you might have to make a compromise, regardless of your feelings on the subject.
I think "assert" is good to use for optimization, and "debug assert" would be a good choice for soft assertions. Care must be exercised with tying new optimizations to build flags.
 Also, I am going to try to say this in as respectful a way as I
 can...

 Please stop responding in such a dismissive way, I think it is
 already pretty obvious that some are getting frustrated by these
 threads. Responding in a dismissive way makes it seem like you
 don't take the arguments seriously.
I have difficulty figuring how such answers can be considered dismissive. The quoted code is considered an antipattern at least e.g. at my workplace. (Wouldn't pass review, and disproportionate insistence on such might curb one's career.) Even though some might not agree with Walter's opinion, it's entirely reasonable to express dislike of that code; I don't quite get why that would be consider dismissive. I think we're at the point where everybody understands one another, and there must be a way to express polite but definite disagreement. What would that be? Thanks, Andrei
Aug 06 2014
next sibling parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 07:19:21 UTC, Andrei Alexandrescu 
wrote:
 The quoted code is considered an antipattern at least e.g. at 
 my workplace.
What about: « if(x==0){ …free of x…} …free of x… assume(x!=0) » being equivalent to « assume(x!=0) if(x==0){ …free of x…} …free of x… »
 I think we're at the point where everybody understands one 
 another
Really? I am the point where I realize that a significant portion of programmers have gullible expectations of their own ability to produce provably correct code and a very sloppy understanding of what computing is. So now we don't have Design by Contract, but Design by Gullible Assumptions. Great…
Aug 06 2014
prev sibling parent "eles" <eles eles.com> writes:
On Wednesday, 6 August 2014 at 07:19:21 UTC, Andrei Alexandrescu 
wrote:
 On 8/5/14, 11:28 PM, Tofu Ninja wrote:
 On Wednesday, 6 August 2014 at 00:52:32 UTC, Walter Bright 
 wrote:
 On 8/3/2014 4:51 PM, Mike Farnsworth wrote:
 I think "assert" is good to use for optimization, and "debug 
 assert" would be a good choice for soft assertions. Care must
Conceptually, this means a "release assert" (both in debug and release builds) and a "debug assert" (only in debug builds). Thus, question: it is acceptable to optimize a (release) build based on code that is present only into another (debug) build?
Aug 06 2014
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/5/2014 11:28 PM, Tofu Ninja wrote:
 Please stop responding in such a dismissive way, I think it is
 already pretty obvious that some are getting frustrated by these
 threads. Responding in a dismissive way makes it seem like you
 don't take the arguments seriously.
I responded to the equivalent design proposal several times already, with detailed answers. This one is shorter, but the essential aspects are there. I know those negative aspects came across because they are addressed with your counter:
 How about something like
  expected assert(x > 2); or  assumed assert(x > 2);
 It wouldn't introduce a new keyword, but still introduces the
expected/assumed semantics. The riposte: 1. it's long with an unappealing hackish look 2. it follows in the C++ tradition of the best practice being the long ugly way, and the deprecated practice is the straightforward way (see arrays in C++) 3. users will be faced with two kinds of asserts, with a subtle difference that is hard to explain, hard to remember which is which, and will most likely use inappropriately 4. everyone who wants faster assert optimizations will have to rewrite their (possibly extensive) use of asserts that we'd told them was best practice. I know I'd be unhappy about having to do such to my D code.
 You should keep in mind that you might have to make a compromise, regardless 
 of your feelings on the subject.
This is not about my feelings, other than my desire to find the best design based on a number of tradeoffs. I'll sum up with the old saw that any programming problem can be solved with another level of indirection. I submit a corollary that any language issue can be solved by adding another keyword or compiler flag. The (much) harder thing is to solve a problem with an elegant solution that does not involve new keywords/flags, and fits in naturally.
Aug 06 2014
next sibling parent "Tofu Ninja" <emmons0 purdue.edu> writes:
On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:

Thank you for the well thought out response.

 I responded to the equivalent design proposal several times 
 already, with detailed answers. This one is shorter, but the 
 essential aspects are there. I know those negative aspects came 
 across because they are addressed with your counter:
I was not trying to attack you, but rather inform you. I think that is all I want to say on the subject so I am going to stop talking about it.
 1. it's long with an unappealing hackish look
I find this a positive, the proposed assert has quite dangerous implications, having a slightly "hackish" look will serve to discourage using it when it is not obviously needed.
 2. it follows in the C++ tradition of the best practice being 
 the long ugly way, and the deprecated practice is the 
 straightforward way (see arrays in C++)
That is implying that the best practice is your version of assert. As it can introduce undefined behavior, I find it hard to believe.
 3. users will be faced with two kinds of asserts, with a subtle 
 difference that is hard to explain, hard to remember which is 
 which, and will most likely use inappropriately
This is why I think it would be best added as an annotation on assert. People who don't care enough to look up what the extra annotation does will just use assert by itself and have no risk of undefined behavior and it will behave as expected(similar to how it behaves in other languages).
 4. everyone who wants faster assert optimizations will have to 
 rewrite their (possibly extensive) use of asserts that we'd 
 told them was best practice. I know I'd be unhappy about having 
 to do such to my D code.
This is a fare point but it would happen the same either way. If some one used assert expecting it to act like the C assert and found out it did not any more, they would be forced to go through though there code and change all the asserts. As this is a change, I am inclined to say we should favor the old version and not force users of the old version to update.
 This is not about my feelings, other than my desire to find the 
 best design based on a number of tradeoffs.
I was just trying to say that it is a possibility that should not be forgotten, I think I may have said it in a harsher way than I meant to, I apologize. The annotated assert was my attempt at a possible compromise.
Aug 06 2014
prev sibling next sibling parent "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:
 On 8/5/2014 11:28 PM, Tofu Ninja wrote:
 Please stop responding in such a dismissive way, I think it is
 already pretty obvious that some are getting frustrated by 
 these
 threads. Responding in a dismissive way makes it seem like you
 don't take the arguments seriously.
I responded to the equivalent design proposal several times already, with detailed answers. This one is shorter, but the essential aspects are there. I know those negative aspects came across because they are addressed with your counter:
I don't think I've seen your arguments against adding assume(), last time this was discussed you were still claiming that there was no difference between the two, so we couldn't even get to discussing it!
 How about something like
  expected assert(x > 2); or  assumed assert(x > 2);
 It wouldn't introduce a new keyword, but still introduces the
expected/assumed semantics. The riposte: 1. it's long with an unappealing hackish look 2. it follows in the C++ tradition of the best practice being the long ugly way, and the deprecated practice is the straightforward way (see arrays in C++) 3. users will be faced with two kinds of asserts, with a subtle difference that is hard to explain, hard to remember which is which, and will most likely use inappropriately 4. everyone who wants faster assert optimizations will have to rewrite their (possibly extensive) use of asserts that we'd told them was best practice. I know I'd be unhappy about having to do such to my D code.
Nice, this is progress. You're giving us some actual reasoning! :) Is this the full list of your reasons or just a subset? 1, 2: Those don't apply to assume() without the annotations right? I agree that's hacky looking with annotations. 3: If the separation is not made official, a lot of people will end up having to roll their own, potentially with all kinds of names. This is much more fragmenting than just having official assert and assume. myAssert, debugCheck, smurfAssert, etc. ugh. As for the difference being subtle, hard to remember, understand, or explain: This totally supports my argument. If people don't even understand the subtlety, there's no way they are ready to be inserting undefined behavior everywhere in their code. assume (or your assert) is a dangerous power tool, joe coder probably shouldn't be using it at all. Yet you want it used everywhere by default? 4: This is a valid argument. The flip side is that everyone else has to invent their own function and rewrite their code with it, unless they have 100% faith their code is not buggy, or don't care about undefined behavior (or don't know they care about it until they get bitten by it later). Or if they go for the quick fix by disabling -release, then you just pessimized their code instead of optimized it. Plus what about people who miss the change, or unmaintained code? Isn't the default way of doing things to err on the side of not breaking people's code? Why is this time different? I know you hate more switches (for good reason), but this seems like a good case for -Oassert or -Ounsafe, for the elite few people whose code is actually suitable for such dangerous transformation. I would like to note some additional benefits of separating the two concepts and hopefully get your thoughts on these. Some of these are repeating from previous posts. -assert(0) is defined as a special case, so it can't express unreachability. This makes it less powerful for optimizing than it should be. assume(0) does not have this problem. e.g. switch(){ /* ... */ default: assume(0); } -the proposed assert is not safe, which creates complications since the current assert is. assume() does not have this problem, as it can be defined as system from the start. -with the functions separate, it can be made clear that assume() is a dangerous tool that should be used sparingly. It will mean that code is more searchable and easier to audit - if there is a heisenbug, try a search for trusted and assume() constructs. -retain C compatibility, which is supposed to be a goal of D.
Aug 06 2014
prev sibling parent "Kagamin" <spam here.lot> writes:
On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:
 4. everyone who wants faster assert optimizations will have to 
 rewrite their (possibly extensive) use of asserts that we'd 
 told them was best practice. I know I'd be unhappy about having 
 to do such to my D code.
Also having the same syntax for both kinds of assert makes it easier to try unsafe optimizations: the code can be written safe, then unsafe optimizations can tried effortlessly and performance gains evaluated. In C one would only need to edit the macro to do this. Whether we want to allow such experiments is debatable, but I find it at least reasonable. One may also want the optimizations to propagate backwards for even more performance - this would be a different kind of optimization, which may or may not require yet another syntax.
Aug 06 2014
prev sibling next sibling parent reply "John Carter" <john.carter taitradio.com> writes:
On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:

 2. Semantic change.
 The proposal changes the meaning of assert(), which will result 
 in breaking existing code. Regardless of philosophizing about 
 whether or not the code was "already broken" according to some 
 definition of assert, the fact is that shipping programs that 
 worked perfectly well before may no longer work after this 
 change.
Subject to the caveat suggesting having two assert's with different names and different meanings, I am in the position to comment on this one from experience. So assuming we do have a "hard assert" that is used within the standard libraries and a "soft assert" in user code (unless they explicitly choose to use the "hard assert"....) What happens? Well, I'm the dogsbody who has the job of upgrading the toolchain and handling the fallout of doing so. So I have been walking multimegaline code bases through every gcc version in the last 15 years. This is relevant because on every new version they have added stricter warnings, and more importantly, deeper optimizations. It's especially the deeper optimizations that are interesting here. They are often better data flow analysis which result in more "insightful" warnings. So given I'm taking megalines of C/C++ code from a warnings free state on gcc version N to warnings free on version N+1, I'll make some empirical observations. * They have _always_ highlighted dodgy / non-portable / non-standard compliant code. * They have quite often highlighted existing defects in the code. * They have quite often highlighted error handling code as "unreachable", because it is... and the only sane thing to do is delete it. * They have often highlighted the error handling code of "defensive programmers" as opposed to DbC programmers. Why? Because around 30% of the code of a defensive programmer is error handling crud that has never been executed, not even in development and hence is untested and unmaintained. The clean up effort was often fairly largish, maybe a week or two, but always resulted in better code. Customer impacting defects introduced by the new optimizations have been.... a) Very very rare. b) Invariably from really bad code that was blatantly defective, non-standard compliant and non-portable. So what do I expect, from experience from Walter's proposed change? Another guy in this thread complained about the compiler suddenly relying on thousands of global axioms from the core and standard libraries. Yup. Exactly what is going to happen. As you get... * more and more optimization passes that rely on asserts, * in particular pre and post condition asserts within the standard libraries, * you are going to have flocks of user code that used to compile without warning * and ran without any known defect... ...suddenly spewing error messages and warnings. But that's OK. Because I bet 99.999% of those warnings will be pointing straight at bone fide defects. And yes, this will be a regular feature of life. New version of compiler, new optimization passes, new warnings... That's OK, clean 'em up, and a bunch of latent defects won't come back as customer complaints.
Aug 03 2014
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/3/14, 6:17 PM, John Carter wrote:
 Well, I'm the dogsbody who has the job of upgrading the toolchain and
 handling the fallout of doing so.

 So I have been walking multimegaline code bases through every gcc
 version in the last 15 years.
Truth. This man speaks it. Great post, thanks! Andrei
Aug 03 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Monday, 4 August 2014 at 01:19:28 UTC, Andrei Alexandrescu 
wrote:
 On 8/3/14, 6:17 PM, John Carter wrote:
 Well, I'm the dogsbody who has the job of upgrading the 
 toolchain and
 handling the fallout of doing so.

 So I have been walking multimegaline code bases through every 
 gcc
 version in the last 15 years.
Truth. This man speaks it. Great post, thanks! Andrei
His post basically says that his real life experience leads him to believe that a static analyzer based on using information from asserts will very likely generate a ton of warnings/errors, because real life code is imperfect. In other words, if you use that information to optimize instead, you are going to get a ton of bugs, because the asserts are inconsistent with the code. So his post completely supports the conclusion that you've disagreed with, unless this has convinced you and you're switching sides now (could it be?) :)
Aug 03 2014
parent reply "John Carter" <john.carter taitradio.com> writes:
On Monday, 4 August 2014 at 02:18:12 UTC, David Bregman wrote:
 His post basically says that his real life experience leads him 
 to believe that a static analyzer based on using information 
 from asserts will very likely generate a ton of 
 warnings/errors, because real life code is imperfect.

 In other words, if you use that information to optimize 
 instead, you are going to get a ton of bugs, because the 
 asserts are inconsistent with the code.
No. My experience says deeper optimization comes from deeper understanding of the dataflow, with deeper understanding of the dataflow comes stricter warnings about defective usage. ie. A Good compiler writer, as Walter and the gcc guys clearly are, don't just slap in an optimization pass out of nowhere. They are all too painfully aware that if their optimization pass breaks anything, they will be fending off thousands of complaints that "Optimization X broke....". Compiler users always blame the optimizer long before they blame their crappy code. Watching the gcc mailing list over the years, those guys bend over backwards to prevent that happening. But since an optimization has to be based on additional hard information, they have, with every new version of gcc, used that information both for warnings and optimization.
Aug 03 2014
next sibling parent "John Carter" <john.carter taitradio.com> writes:
On Monday, 4 August 2014 at 02:31:36 UTC, John Carter wrote:

 But since an optimization has to be based on additional hard 
 information, they have, with every new version of gcc, used 
 that information both for warnings and optimization.
Hmm. Not sure I made that clear. ie. Yes, it is possible that a defect may be injected by an optimization that assumes an assert is true when it isn't. However, experience suggests that many (maybe two full orders of magnitude) more defects will be flagged. ie. In terms of defect reduction it's a big win rather than a loss. The tragedy of C optimization and static analysis is that the language is so loosely defined in terms of how it is used, the compiler has very little to go on. This proposal looks to me to be a Big Win, because it gifts the compiler (and any analysis tools) with a huge amount of eminently usable information.
Aug 03 2014
prev sibling next sibling parent "David Bregman" <drb sfu.ca> writes:
On Monday, 4 August 2014 at 02:31:36 UTC, John Carter wrote:
 On Monday, 4 August 2014 at 02:18:12 UTC, David Bregman wrote:
 His post basically says that his real life experience leads 
 him to believe that a static analyzer based on using 
 information from asserts will very likely generate a ton of 
 warnings/errors, because real life code is imperfect.

 In other words, if you use that information to optimize 
 instead, you are going to get a ton of bugs, because the 
 asserts are inconsistent with the code.
No. My experience says deeper optimization comes from deeper understanding of the dataflow, with deeper understanding of the dataflow comes stricter warnings about defective usage.
Yes, that isn't what is being proposed though. This is about optimization, not warnings or errors.
 ie. A Good compiler writer, as Walter and the gcc guys clearly 
 are, don't just slap in an optimization pass out of nowhere.

 They are all too painfully aware that if their optimization 
 pass breaks anything, they will be fending off thousands of 
 complaints that "Optimization X broke....".
If you read the earlier threads, you will see Walter freely admits this will break code. Actually he says that such code is already broken. This doesn't involve new warnings, it will just break silently. It would be very difficult to do otherwise (see Daniel Gibson's reply to your post).
Aug 03 2014
prev sibling parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/3/2014 7:31 PM, John Carter wrote:
 Compiler users always blame the optimizer long before they blame their crappy
code.

 Watching the gcc mailing list over the years, those guys bend over backwards to
 prevent that happening.

 But since an optimization has to be based on additional hard information, they
 have, with every new version of gcc, used that information both for warnings
and
 optimization.
Recent optimization improvements in gcc and clang have also broken existing code that has worked fine for decades. In particular, overflow checks often now get optimized out, as the check relied on, pedantically, undefined behavior. This is why D has added the core.checkedint module, to have overflow checks that are guaranteed to work. Another optimization that has broken existing code is removal of dead assignments. This has broken crypto code that would overwrite passwords after using them. It's also why D now has volatileStore() and volatileLoad(), if only someone will pull them. I.e. silent breakage of existing, working code is hardly unknown in the C/C++ world.
Aug 05 2014
prev sibling next sibling parent reply Daniel Gibson <metalcaedes gmail.com> writes:
Am 04.08.2014 03:17, schrieb John Carter:
 As you get...

 * more and more optimization passes that rely on asserts,
 * in particular pre and post condition asserts within the standard
 libraries,
 * you are going to have flocks of user code that used to compile without
 warning
 * and ran without any known defect...

 ...suddenly spewing error messages and warnings.

 But that's OK.

 Because I bet 99.999% of those warnings will be pointing straight at
 bone fide defects.
Well, that would make the problem more acceptable.. However, it has been argued that it's very hard to warn about code that will be eliminated, because that code often only become dead or redundant due to inlining, template instantiation, mixin, ... and you can't warn in those cases. So I doubt that the compiler will warn every time it removes checks that are considered superfluous because of a preceding assert(). Cheers, Daniel
Aug 03 2014
parent reply "Tove" <tove fransson.se> writes:
On Monday, 4 August 2014 at 01:26:10 UTC, Daniel Gibson wrote:
 Am 04.08.2014 03:17, schrieb John Carter:
 But that's OK.

 Because I bet 99.999% of those warnings will be pointing 
 straight at
 bone fide defects.
Well, that would make the problem more acceptable.. However, it has been argued that it's very hard to warn about code that will be eliminated, because that code often only become dead or redundant due to inlining, template instantiation, mixin, ... and you can't warn in those cases. So I doubt that the compiler will warn every time it removes checks that are considered superfluous because of a preceding assert(). Cheers, Daniel
It is possible, just not as a default enabled warning. Some compilers offers optimization diagnostics which can be enabled by a switch, I'm quite fond of those as it's a much faster way to go through a list of compiler highlighted failed/successful optimizations rather than being forced to check the asm output after every new compiler version or minor code refactoring. In my experience, it actually works fine in huge projects, even if there are false positives you can analyse what changes from the previous version as well as ignoring modules which you know is not performance critical.
Aug 03 2014
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/3/2014 7:26 PM, Tove wrote:
 It is possible, just not as a default enabled warning.

 Some compilers offers optimization diagnostics which can be enabled by a
switch,
 I'm quite fond of those as it's a much faster way to go through a list of
 compiler highlighted failed/successful optimizations rather than being forced
to
 check the asm output after every new compiler version or minor code
refactoring.

 In my experience, it actually works fine in huge projects, even if there are
 false positives you can analyse what changes from the previous version as well
 as ignoring modules which you know is not performance critical.
If you build dmd in debug mode, and then run it with -O --c, it will give you a list of all the data flow transformations it does. But the list is a blizzard on non-trivial programs.
Aug 05 2014
next sibling parent "Tove" <tove fransson.se> writes:
On Wednesday, 6 August 2014 at 00:47:28 UTC, Walter Bright wrote:
 If you build dmd in debug mode, and then run it with -O --c, it 
 will give you a list of all the data flow transformations it 
 does.

 But the list is a blizzard on non-trivial programs.
Awesome, thanks! Will give it a whirl, as soon as my vacation is over.
Aug 05 2014
prev sibling parent "Sebastiaan Koppe" <mail skoppe.eu> writes:
On Wednesday, 6 August 2014 at 00:47:28 UTC, Walter Bright wrote:
 On 8/3/2014 7:26 PM, Tove wrote:
 It is possible, just not as a default enabled warning.

 Some compilers offers optimization diagnostics which can be 
 enabled by a switch,
 I'm quite fond of those as it's a much faster way to go 
 through a list of
 compiler highlighted failed/successful optimizations rather 
 than being forced to
 check the asm output after every new compiler version or minor 
 code refactoring.

 In my experience, it actually works fine in huge projects, 
 even if there are
 false positives you can analyse what changes from the previous 
 version as well
 as ignoring modules which you know is not performance critical.
If you build dmd in debug mode, and then run it with -O --c, it will give you a list of all the data flow transformations it does. But the list is a blizzard on non-trivial programs.
What about making a diff file? Or are the transformations so deep that it would be impossible to link them to lines in the source code?
Aug 08 2014
prev sibling parent reply "Atila Neves" <atila.neves gmail.com> writes:
This. 1000x this.

Atila

On Monday, 4 August 2014 at 01:17:23 UTC, John Carter wrote:
 On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:

 2. Semantic change.
 The proposal changes the meaning of assert(), which will 
 result in breaking existing code. Regardless of philosophizing 
 about whether or not the code was "already broken" according 
 to some definition of assert, the fact is that shipping 
 programs that worked perfectly well before may no longer work 
 after this change.
Subject to the caveat suggesting having two assert's with different names and different meanings, I am in the position to comment on this one from experience. So assuming we do have a "hard assert" that is used within the standard libraries and a "soft assert" in user code (unless they explicitly choose to use the "hard assert"....) What happens? Well, I'm the dogsbody who has the job of upgrading the toolchain and handling the fallout of doing so. So I have been walking multimegaline code bases through every gcc version in the last 15 years. This is relevant because on every new version they have added stricter warnings, and more importantly, deeper optimizations. It's especially the deeper optimizations that are interesting here. They are often better data flow analysis which result in more "insightful" warnings. So given I'm taking megalines of C/C++ code from a warnings free state on gcc version N to warnings free on version N+1, I'll make some empirical observations. * They have _always_ highlighted dodgy / non-portable / non-standard compliant code. * They have quite often highlighted existing defects in the code. * They have quite often highlighted error handling code as "unreachable", because it is... and the only sane thing to do is delete it. * They have often highlighted the error handling code of "defensive programmers" as opposed to DbC programmers. Why? Because around 30% of the code of a defensive programmer is error handling crud that has never been executed, not even in development and hence is untested and unmaintained. The clean up effort was often fairly largish, maybe a week or two, but always resulted in better code. Customer impacting defects introduced by the new optimizations have been.... a) Very very rare. b) Invariably from really bad code that was blatantly defective, non-standard compliant and non-portable. So what do I expect, from experience from Walter's proposed change? Another guy in this thread complained about the compiler suddenly relying on thousands of global axioms from the core and standard libraries. Yup. Exactly what is going to happen. As you get... * more and more optimization passes that rely on asserts, * in particular pre and post condition asserts within the standard libraries, * you are going to have flocks of user code that used to compile without warning * and ran without any known defect... ...suddenly spewing error messages and warnings. But that's OK. Because I bet 99.999% of those warnings will be pointing straight at bone fide defects. And yes, this will be a regular feature of life. New version of compiler, new optimization passes, new warnings... That's OK, clean 'em up, and a bunch of latent defects won't come back as customer complaints.
Aug 04 2014
parent "David Bregman" <drb sfu.ca> writes:
On Monday, 4 August 2014 at 09:38:26 UTC, Atila Neves wrote:
 This. 1000x this.

 Atila
Yeah, I don't think anyone disagrees with getting better warning and error messages. Static analysis rocks. Anyways I just want to point out that this isn't what's being proposed, so it's kind of off topic. It's not an argument either for or against the proposal, just in case that wasn't clear.
Aug 04 2014
prev sibling next sibling parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Sunday, 3 August 2014 at 19:47:27 UTC, David Bregman wrote:
 4. Performance.
 Q4a. What level of performance increases are expected of this 
 proposal, for a representative sample of D programs?
 Q4b. Is there any threshold level of expected performance 
 required to justify this proposal? For example, if a study 
 determined that the average program could expect a speedup of 
 0.01% or less, would that still be considered a good tradeoff 
 against the negatives?
 Q4c. Have any works or studies, empirical or otherwise, been 
 done to estimate the expected performance benefit? Is there any 
 evidence at all for a speedup sufficient to justify this 
 proposal?
 Q4d. When evaluating the potential negative effects of the 
 proposal on their codebase, D users may decide it is now too 
 risky to compile with -release. (Even if their own code has 
 been constructed with the new assert semantics in mind, the 
 libraries they use might not). Thus the effect of the proposal 
 would actually be to decrease the performance of their program 
 instead of increase it. Has this been considered in the 
 evaluation of tradeoffs?
I'd like to add: Q4e: Have other alternatives been taken into consideration that could achieve the same performance gains, but in a safer way? I'm particularly thinking about whole program optimization. I suspect that WPO can prove most of what can only be assumed with asserts.
Aug 04 2014
parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
Should this semantics extend to array bounds checking, i.e. after 
the statement

foo[5] := 0;

can the optimizer assume that foo.length >= 6 ?
Aug 04 2014
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 8/4/14, 7:27 AM, Matthias Bentrup wrote:
 Should this semantics extend to array bounds checking, i.e. after the
 statement

 foo[5] := 0;

 can the optimizer assume that foo.length >= 6 ?
Yes, definitely. -- Andrei
Aug 04 2014
parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/4/2014 8:01 AM, Andrei Alexandrescu wrote:
 On 8/4/14, 7:27 AM, Matthias Bentrup wrote:
 Should this semantics extend to array bounds checking, i.e. after the
 statement

 foo[5] := 0;

 can the optimizer assume that foo.length >= 6 ?
Yes, definitely. -- Andrei
Yes, after all, bounds checking is just another form of asserts.
Aug 05 2014
prev sibling next sibling parent reply Jeremy Powers via Digitalmars-d <digitalmars-d puremagic.com> writes:
This has already been stated by others, but I just wanted to pile on - I
agree with Walter's definition of assert.

2. Semantic change.
 The proposal changes the meaning of assert(), which will result in
 breaking existing code.  Regardless of philosophizing about whether or not
 the code was "already broken" according to some definition of assert, the
 fact is that shipping programs that worked perfectly well before may no
 longer work after this change.
Disagree. Assert (as I always understood it) means 'this must be true, or my program is broken.' In -release builds the explicit explosion on a triggered assert is skipped, but any code after a non-true assert is, by definition, broken. And by broken I mean the fundamental constraints of the program are violated, and so all bets are off on it working properly. A shipping program that 'worked perfectly well' but has unfulfilled asserts is broken - either the asserts are not actually true constraints, or the broken path just hasn't been hit yet. Looking at the 'breaking' example: assert(x!=1); if (x==1) { ... } If the if is optimized out, this will change from existing behaviour. But it is also obviously (to me at least) broken code already. The assert says that x cannot be 1 at this point in the program, if it ever is then there is an error in the program.... and then it continues as if the program were still valid. If x could be one, then the assert is invalid here. And this code will already behave differently between -release and non-release builds, which is another kind of broken. 3a. An alternate statement of the proposal is literally "in release mode,
 assert expressions introduce undefined behavior into your code in if the
 expression is false".
This statement seems fundamentally true to me of asserts already, regardless of whether they are used for optimizations. If your assert fails, and you have turned off 'blow up on assert' then your program is in an undefined state. It is not that the assert introduces the undefined behaviour, it is that the assert makes plain an expectation of the code and if that expectation is false the code will have undefined behaviour. 3b. Since assert is such a widely used feature (with the original
 semantics, "more asserts never hurt"), the proposal will inject a massive
 amount of undefined behavior into existing code bases, greatly increasing
 the probability of experiencing problems related to undefined behavior.
I actually disagree with the 'more asserts never hurt' statement. Exactly because asserts get compiled out in release builds, I do not find them very useful/desirable. If they worked as optimization hints I might actually use them more. And there will be no injection of undefined behaviour - the undefined behaviour is already there if the asserted constraints are not valid. Maybe if the yea side was consulted, they might easily agree to an
 alternative way of achieving the improved optimization goal, such as
 creating a new function that has the proposed semantics.
Prior to this (incredibly long) discussion, I was not aware people had a different interpretation of assert. To me, this 'new semantics' is precisely what I always thought assert was, and the proposal is just leveraging it for some additional optimizations. So from my standpoint, adding a new function would make sense to support this 'existing' behaviour that others seem to rely on - assert is fine as is, if the definition of 'is' is what I think it is.
Aug 05 2014
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08/05/2014 08:18 PM, Jeremy Powers via Digitalmars-d wrote:
 And there will be no injection of undefined behaviour - the undefined
 behaviour is already there if the asserted constraints are not valid.
Well, no. http://en.wikipedia.org/wiki/Undefined_behavior
Aug 05 2014
parent reply Jeremy Powers via Digitalmars-d <digitalmars-d puremagic.com> writes:
 And there will be no injection of undefined behaviour - the undefined
 behaviour is already there if the asserted constraints are not valid.
Well, no. http://en.wikipedia.org/wiki/Undefined_behavior
Well, yes: Undefined behaviour in the sense the writer of the program has not defined it. A program is written with certain assumptions about the state at certain points. An assert can be used to explicitly state those assumptions, and halt the program (in non-release) if the assumptions are invalid. If the state does not match what the assert assumes it to be, then any code relying on that state is invalid, and what it does has no definition given by the programmer. (And here I've circled back to assert==assume... all because I assume what assert means) If the state that is being checked could actually ever be valid, then it is not valid for an assert - use some other validation.
Aug 05 2014
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08/05/2014 08:59 PM, Jeremy Powers via Digitalmars-d wrote:
 ...

 Well, yes: Undefined behaviour in the sense
"And there will be no injection of undefined behaviour ^~~~~~~~~~~~~~~~~~~ conventional sense - the undefined behaviour is already there if the asserted constraints ^~~~~~~~~~~~~~~~~~~ altered sense are not valid."
Aug 05 2014
parent reply Jeremy Powers via Digitalmars-d <digitalmars-d puremagic.com> writes:
 Well, yes: Undefined behaviour in the sense
"And there will be no injection of undefined behaviour ^~~~~~~~~~~~~~~~~~~ conventional sense - the undefined behaviour is already there if the asserted constraints ^~~~~~~~~~~~~~~~~~~ altered sense are not valid."
I still don't quite see your point. Perhaps I should have said: In the case where an asserted constraint is not met, the program is invalid. Being invalid it has undefined behaviour if it continues.
From another:
 There is a difference between invalid and undefined: A program is invalid
 ("buggy"), if it doesn't do what it's programmer intended, while
 "undefined" is a matter of the language specification. The (wrong)
 behaviour of an invalid program need not be undefined, and often isn't in
 practice.
I disagree with this characterization. Something can be buggy, not doing what the programmer intended, while also a perfectly valid program. You can make wrong logic that is valid/reasonable in the context of the program. Invalid in this case means the programmer has explicitly stated certain constraints must hold, and such constraints do not hold. So if you continue with the program in the face of invalid constraints, you have no guarantee what will happen - this is what I mean by 'undefined'.
Aug 05 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Tuesday, 5 August 2014 at 20:50:06 UTC, Jeremy Powers via 
Digitalmars-d wrote:
 Well, yes: Undefined behaviour in the sense
"And there will be no injection of undefined behaviour ^~~~~~~~~~~~~~~~~~~ conventional sense - the undefined behaviour is already there if the asserted constraints ^~~~~~~~~~~~~~~~~~~ altered sense are not valid."
I still don't quite see your point. Perhaps I should have said: In the case where an asserted constraint is not met, the program is invalid. Being invalid it has undefined behaviour if it continues.
From another:
 There is a difference between invalid and undefined: A program 
 is invalid
 ("buggy"), if it doesn't do what it's programmer intended, 
 while
 "undefined" is a matter of the language specification. The 
 (wrong)
 behaviour of an invalid program need not be undefined, and 
 often isn't in
 practice.
I disagree with this characterization. Something can be buggy, not doing what the programmer intended, while also a perfectly valid program. You can make wrong logic that is valid/reasonable in the context of the program. Invalid in this case means the programmer has explicitly stated certain constraints must hold, and such constraints do not hold. So if you continue with the program in the face of invalid constraints, you have no guarantee what will happen - this is what I mean by 'undefined'.
You're using a nonstandard definition of undefined behavior. Undefined behavior has a precise meaning, that's why Timon linked the wiki article for you. The regular definition of assert does not involve any undefined behavior, only the newly proposed one.
Aug 05 2014
parent reply Jeremy Powers via Digitalmars-d <digitalmars-d puremagic.com> writes:
 You're using a nonstandard definition of undefined behavior. Undefined
 behavior has a precise meaning, that's why Timon linked the wiki article
 for you.

 The regular definition of assert does not involve any undefined behavior,
 only the newly proposed one.
But the 'newly proposed one' is the definition that I have been using all along. The 'regular' definition of assert that you claim is what I see as the redefinition - it is a definition based on the particular implementation of assert in other languages, not on the conceptual idea of assert as I understand it (and as it appears to be intended in D). This appears to be the root of the argument, and has been circled repeatedly... it's not my intent to restart another round of discussion on that well traveled ground, I just wanted to state my support for the definition as I understand it.
Aug 05 2014
next sibling parent "bachmeier" <no spam.net> writes:
 But the 'newly proposed one' is the definition that I have been 
 using all
 along.
+1. Until this came up, I didn't know another definition existed.
 The 'regular' definition of assert that you claim is what I see 
 as
 the redefinition - it is a definition based on the particular
 implementation of assert in other languages, not on the 
 conceptual idea of
 assert as I understand it (and as it appears to be intended in 
 D).
In my view, it's also a redefinition of -release. My view is influenced by Common Lisp. If you want speed, you test your program, and then when you feel comfortable, set the optimization levels to get as much speed as possible. If you want safety and debugging, set the optimization levels accordingly. I was always under the impression that -release was a statement to the compiler that "I've tested the program, make it run as fast as possible, and let me worry about any remaining bugs."
Aug 05 2014
prev sibling parent reply "David Bregman" <drb sfu.ca> writes:
On Tuesday, 5 August 2014 at 22:25:59 UTC, Jeremy Powers via 
Digitalmars-d wrote:
 You're using a nonstandard definition of undefined behavior. 
 Undefined
 behavior has a precise meaning, that's why Timon linked the 
 wiki article
 for you.

 The regular definition of assert does not involve any 
 undefined behavior,
 only the newly proposed one.
But the 'newly proposed one' is the definition that I have been using all along.
OK, but my point was you were using a different definition of undefined behavior. We can't communicate if we aren't using the same meanings of words.
 The 'regular' definition of assert that you claim is what I see 
 as
 the redefinition - it is a definition based on the particular
 implementation of assert in other languages, not on the 
 conceptual idea of
 assert as I understand it (and as it appears to be intended in 
 D).
The 'regular' definition of assert is used in C, C++ and for the last >10years (afaik), in D. If you want to change it you need a good justification. I'm not saying such justification necessarily exist doesn't either, maybe it does but I have not seen it.
 This appears to be the root of the argument, and has been 
 circled
 repeatedly... it's not my intent to restart another round of 
 discussion on
 that well traveled ground, I just wanted to state my support 
 for the
 definition as I understand it.
I disagree. I don't think the fact that some people already had the new definition in mind before is really all that relevant. That's in the past. This is all about the pros and cons of changing it now and for the future.
Aug 05 2014
next sibling parent reply Jeremy Powers via Digitalmars-d <digitalmars-d puremagic.com> writes:
 That's in the past. This is all about the pros and cons of changing it now
 and for the future.
The main argument seems to revolve around whether this is actually a change or not. In my (and others') view, the treatment of assert as 'assume' is not a change at all. It was in there all along, we just needed the wizard to tell us. The below can safely be ignored, as I just continue the pedantic discussions.... OK, but my point was you were using a different definition of undefined
 behavior. We can't communicate if we aren't using the same meanings of
 words.
Yes, very true. My definition of undefined in this case hinges on my definition of what assert means. If a failed assert means all code after it is invalid, then by definition (as I interpret the definition) that code is invalid and can be said to have undefined behaviour. That is, it makes sense to me that it is specified as undefined, by the spec that is incredibly unclear. I may be reading too much into it here, but this follows the strict definition of undefined - it is undefined because it is defined to be undefined. This is the 'because I said so' defense.
  The 'regular' definition of assert that you claim is what I see as
 the redefinition - it is a definition based on the particular
 implementation of assert in other languages, not on the conceptual idea of
 assert as I understand it (and as it appears to be intended in D).
The 'regular' definition of assert is used in C, C++ and for the last
10years (afaik), in D. If you want to change it you need a good
justification. I'm not saying such justification necessarily exist doesn't either, maybe it does but I have not seen it.
This 'regular' definition is a somewhat strict interpretation of the definition to only match how languages have implemented it. I have always interpreted the intent of assert to be 'here is something that must be true, if it is not then my program is in an invalid state' - the fact it is only a debug halting tool in practice means it falls short of its potential. And in fact I very rarely use it in practice for this reason, as I find the way it works almost useless and definitely dangerous.
 This appears to be the root of the argument, and has been circled
 repeatedly... it's not my intent to restart another round of discussion on
 that well traveled ground, I just wanted to state my support for the
 definition as I understand it.
I disagree. I don't think the fact that some people already had the new definition in mind before is really all that relevant.
It comes back to whether the new definition is actually new. If it is a new definition, then we can argue about whether it is good or not. If it is the old definition (which slightly differs from how assert works in practice in other languages) then we can argue about whether D should conform to other languages or leverage the existing definition... I contend that it is not new, and is simply an extension of the actual definition. Some people agree, some people don't... very lengthy and esoteric discussions have already spiraled through this repeatedly, so us arguing about it again probably won't get anywhere. My stance is that this new/old definition is a good thing, as it matches how I thought things were already, and any code that surfaces as broken because of it was already broken in my definition. Therefore this 'change' is good, does not introduce breaking changes, and arguments about such should be redirected towards mitigation and fixing of expectations. In an attempt to return this discussion to something useful, question: If assert means what I think it means (and assuming we agree on what the actual two interpretations are), how do we allay concerns about it? Is there anything fundamentally/irretrievably bad if we use this new/old definition? (Can we programmatically (sp?) identify and flag/resolve issues that occur from a mismatch of expectations?)
Aug 05 2014
next sibling parent reply "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 01:11:55 UTC, Jeremy Powers via 
Digitalmars-d wrote:
 That's in the past. This is all about the pros and cons of 
 changing it now
 and for the future.
The main argument seems to revolve around whether this is actually a change or not. In my (and others') view, the treatment of assert as 'assume' is not a change at all. It was in there all along, we just needed the wizard to tell us.
How can there be any question? This is a change in the compiler, a change in the docs, change in what your program does, change of the very bytes in the executable. If my program worked before and doesn't now, how is that not a change? This must be considered a change by any reasonable definition of the word change. I don't think I can take seriously this idea that someone's unstated, unmanifested intentions define change more so than things that are .. you know.. actual real changes. Much of the rest of your post seems to be predicated on this, so I don't think I can respond to it. Let me know if I missed something.
 In an attempt to return this discussion to something useful, 
 question:

 If assert means what I think it means (and assuming we agree on 
 what the
 actual two interpretations are), how do we allay concerns about 
 it?  Is
 there anything fundamentally/irretrievably bad if we use this 
 new/old
 definition?
Well I think I outlined the issues in the OP. As for solutions, there have been some suggestions in this thread, the simplest is to leave things as is and introduce the optimizer hint as a separate function, assume(). I don't think there was any argument presented against a separate function besides that Walter couldn't see any difference between the two behaviors, or the intention thing which doesn't really help us here. I guess the only real argument against it is that pre-existing asserts contain significant optimization information that we can't afford to not reuse. But this is a claim I'm pretty skeptical of. Andrei admitted it's just a hunch at this point. Try looking through your code base to see how many asserts would be useful for optimizing. For me, it's mostly default:assert(false); in switch statements, though ironically that is defined to produce a halt even in release, so the compiler won't optimize away the branch like it should. Heh, I just realized, that particular special case is another argument for a separate function, because assert(false) can't express unreachability. assume(false) could.
 (Can we programmatically (sp?) identify and flag/resolve
 issues that occur from a mismatch of expectations?)
I'm not an expert on this, but my guess is it's possible in theory but would never happen in practice. Such things are very complex to implement, if Walter won't agree to a simple and easy solution, I'm pretty sure there's no way in hell he would agree to a complex one that takes a massive amount of effort.
Aug 05 2014
next sibling parent reply "eles" <eles eles.com> writes:
On Wednesday, 6 August 2014 at 04:05:41 UTC, David Bregman wrote:
 On Wednesday, 6 August 2014 at 01:11:55 UTC, Jeremy Powers via 
 Digitalmars-d wrote:
 How can there be any question? This is a change in the 
 compiler, a change in the docs, change in what your program 
 does, change of the very bytes in the executable. If my program
I feel that, at this stage, is only about how a compiler glag, specifically "-release" works. For other configurations, there is no problem: event if the optimizer optimizes based on asserts, the asserts themselves are part of the code: code is there and the assertion will fail before execution enters the optimized path. This is just like any other optimization, nothing special about it. The problem with "-release" might be formulated in that it optimizes based on a code that is no longer present (the asserts are wiped out). It keeps the optimization, but it dismisses the garde-fous.
Aug 05 2014
next sibling parent Jeremy Powers via Digitalmars-d <digitalmars-d puremagic.com> writes:
 I feel that, at this stage, is only about how a compiler glag,
 specifically "-release" works. For other configurations, there is no
 problem: event if the optimizer optimizes based on asserts, the asserts
 themselves are part of the code: code is there and the assertion will fail
 before execution enters the optimized path. This is just like any other
 optimization, nothing special about it.

 The problem with "-release" might be formulated in that it optimizes based
 on a code that is no longer present (the asserts are wiped out). It keeps
 the optimization, but it dismisses the garde-fous.
Yes! [lengthy and imprecise rambling about assert definition omitted]
Aug 06 2014
prev sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 06:56:40 UTC, eles wrote:
 I feel that, at this stage, is only about how a compiler glag, 
 specifically "-release" works. For other configurations, there 
 is no problem: event if the optimizer optimizes based on 
 asserts, the asserts themselves are part of the code: code is 
 there and the assertion will fail before execution enters the 
 optimized path. This is just like any other optimization, 
 nothing special about it.
Not right: b = a+1 assume(b>C) implies assume(a+1>C) b = a+1
Aug 06 2014
parent reply "eles" <eles eles.com> writes:
On Wednesday, 6 August 2014 at 07:29:02 UTC, Ola Fosheim Grøstad 
wrote:
 On Wednesday, 6 August 2014 at 06:56:40 UTC, eles wrote:
 Not right:

 b = a+1
 assume(b>C)

 implies

 assume(a+1>C)
 b = a+1
b = a+1 if(C<=b) exit(1); implies if(C<=a+1) exit(1); b = a+1 Is not the same? Still, one would allow the optimizer to exit before executing b=a+1 line (in the first version) based on that condition (considering no volatile variables). I stick to my point: as long as the code is there, optimization based on it is acceptable (as long as the functionality of the program is not changed, of course). The sole floating point is what to do when the code that is used for optimization is discarded. Would you accept optimization of a C program based on code that is guarded by: #ifndef _NDEBUG //code that could be used for optimization #endif in the -D_NDEBUG version? (I am not convinced 100% that for D is the same, but should help with the concepts)
Aug 06 2014
parent reply Artur Skawina via Digitalmars-d <digitalmars-d puremagic.com> writes:
On 08/06/14 10:28, eles via Digitalmars-d wrote:
 On Wednesday, 6 August 2014 at 07:29:02 UTC, Ola Fosheim Grøstad wrote:
 On Wednesday, 6 August 2014 at 06:56:40 UTC, eles wrote:
 Not right:

 b = a+1
 assume(b>C)

 implies

 assume(a+1>C)
 b = a+1
b = a+1 if(C<=b) exit(1); implies if(C<=a+1) exit(1); b = a+1 Is not the same? Still, one would allow the optimizer to exit before executing b=a+1 line (in the first version) based on that condition (considering no volatile variables).
It is *very* different. In the `exit` case this kind of transformation is only valid if that assignment has no externally observable effects. `assume` makes the transformation *unconditionally* valid, even when executing 'b=a+1' would affect the output of the program. The compiler can /assume/ that the condition never fails. Hence, it does not need to generate any code to check that the assumption is valid. It does not need to emit any code for any path that would only be taken if the condition would be false. If that ever happens the CPU can start executing any random instructions. That's ok, since you explicitly told the compiler that this situation will never occur. Hence, it can also skip generating any code for any path that unconditionally leads to a failing `assume` directive. Because it is all dead code that will never be executed, as long as all `assume` conditions are true. artur
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 12:41:16 UTC, Artur Skawina via 
Digitalmars-d wrote:
 The compiler can /assume/ that the condition never fails. 
 Hence, it does
 not need to generate any code to check that the assumption is 
 valid.
Exactly, worse example using a coroutine: « label: … while(running) { // forevah! … yield … } … assume(anything local not assigned below label) // reachable, but never executed » is equivalent to: « assume(anything local not assigned below label) // optimize based on this label: … while(running) { … yield … } » Woops?
Aug 06 2014
parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
On Wednesday, 6 August 2014 at 13:31:54 UTC, Ola Fosheim Grøstad 
wrote:
 On Wednesday, 6 August 2014 at 12:41:16 UTC, Artur Skawina via 
 Digitalmars-d wrote:
 The compiler can /assume/ that the condition never fails. 
 Hence, it does
 not need to generate any code to check that the assumption is 
 valid.
Exactly, worse example using a coroutine: « label: … while(running) { // forevah! … yield … } … assume(anything local not assigned below label) // reachable, but never executed » is equivalent to: « assume(anything local not assigned below label) // optimize based on this label: … while(running) { … yield … } » Woops?
But even if there is no explicit assert()/assume() given by the developer, I guess the optimizer is free to insert assumes that are provably correct, e.g. while(running) { ...don't assign to running, don't break... } is equivalent to while(running) { ...don't assign to running, don't break... } assume(!running); is equivalent to assume(!running); while(running) { ...don't assign to running, don't break... } is equivalent to assume(!running); So I take the compiler is allowed to throw away code without any asserts already ?
Aug 06 2014
next sibling parent "Tofu Ninja" <emmons0 purdue.edu> writes:
On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup 
wrote:
 So I take the compiler is allowed to throw away code without 
 any asserts already ?
Yes it can, but only in the cases where it can prove it is the same. The main difference is that assume does not need to be proved, it is stated to always be true so no proof needed. Some have said that the compiler can still try to prove what it can and issue warnings if it is provable untrue, but it would actually be a little silly on the part of the compiler to waist it's time trying to disprove things it "knows" are true. If it "knows" it is true then why even bother checking?
Aug 06 2014
prev sibling next sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup 
wrote:
 is equivalent to

   while(running) {
     ...don't assign to running, don't break...
   }
   assume(!running);
You have to prove termination to get there? Plain Hoare logic cannot deal with non-terminating loops. Otherwise you risk proving any theorem below the loop to hold? But I was talking about explicit assumptions made by the programmer, who does not know the rules… It was obviously wrong to assume anything to hold if the loop never terminates. The rule for proving loop termination is quite involved where you basically prove that every time you move through the loop you get something "less" than you had before (ensured by t and D). This is no fun, and a good reason to hate reasoning about correctness: a < b: is a well-founded ordering on the set D if this holds: [P ∧ B ∧ t ∈ D ∧ t = z] S [P ∧ t ∈ D ∧ t < z ] then this holds: [P ∧ t ∈ D] while B do S done [¬B ∧ P ∧ t ∈ D] I think… or maybe not. Who can tell from just glancing at it?
Aug 06 2014
next sibling parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 15:29:13 UTC, Ola Fosheim Grøstad 
wrote:
 On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup 
 wrote:
 is equivalent to

  while(running) {
    ...don't assign to running, don't break...
  }
  assume(!running);
You have to prove termination to get there? Plain Hoare logic cannot deal with non-terminating loops. Otherwise you risk proving any theorem below the loop to hold?
This is an assume, not an assert. The user tells the compiler that `running` is false after the loop, it can thus conclude that the loop will never run. So there is no non-terminating loop in this case.
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 15:36:52 UTC, Marc Schütz wrote:
 This is an assume, not an assert.
Not sure what you mean. An assume is an assert proven (or defined) to hold. It can be a proven theorem which has been given the status of an axiom. It is known to keep the algebraic system sound. If you claim that something unsound is proven then all bets are off everywhere? I am quite confident that assume(false) anywhere in your program is basically stating that the program is unsound (true==false) and should not be compiled and run at all. If true==false anywhere in your program then it surely holds everywhere in your program? The only reason c-style assert(false) "works", is because you delay the verification until the last moment, at which point the system says "woopsie", gotta terminate this because this program should never have compiled in the first place. Sounds consistent to me?
Aug 06 2014
next sibling parent reply "Artur Skawina" <art.08.09 gmail.com> writes:
On 08/06/14 18:00, via Digitalmars-d wrote:
 I am quite confident that assume(false) anywhere in your 
 program is basically stating that the program is unsound 
 (true==false) and should not be compiled and run at all.
No, an assume(false) in a program only means that every _path_ _leading_to_that_statement is 'unsound'. For practical purposes it's better to treat 'unsound' as impossible and unreachable. IOW import std.stdio, std.array; int main(string[] argv) { if (argv.length<2) assume(0); if (argv.length==1) writeln("help text"); return argv.empty; } => 0000000000403890 <_Dmain>: 403890: 31 c0 xor %eax,%eax 403892: c3 retq The alternatives would be to make it either: a) always a compile error, or b) always a runtime error. The former would add little value (`static assert` already exists); the latter is already available as `assert(0)`. The above example after "s/assume(0)/assert(0)/" becomes: 0000000000403890 <_Dmain>: 403890: 48 83 ff 01 cmp $0x1,%rdi 403894: 76 03 jbe 403899 <_Dmain+0x9> 403896: 31 c0 xor %eax,%eax 403898: c3 retq 403899: 50 push %rax 40389a: e8 71 e7 ff ff callq 402010 <abort plt> IOW the compiler can still optimize based on the (un)reachability, but the behavior in no longer undefined. artur
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 16:59:18 UTC, Artur Skawina wrote:
 No, an assume(false) in a program only means that every _path_
 _leading_to_that_statement is 'unsound'. For practical purposes
 it's better to treat 'unsound' as impossible and unreachable.
I don't think so. Because a program is only correct if all axioms and proposed theorems are proven true. All axioms are by definition true, so if you assume(false==true) anywhere it has to hold everywhere. Neither "false" or "true" are variables. Just like assume(PI==3.14…) has to hold everywhere. false, true and PI are constant throughout every path in the program. Not really sure how it is possible to disagree with that?
Aug 06 2014
next sibling parent reply "Artur Skawina" <art.08.09 gmail.com> writes:
On Wednesday, 6 August 2014 at 17:03:45 UTC, Ola Fosheim Grøstad 
wrote:
 On Wednesday, 6 August 2014 at 16:59:18 UTC, Artur Skawina 
 wrote:
 No, an assume(false) in a program only means that every _path_
 _leading_to_that_statement is 'unsound'. For practical purposes
 it's better to treat 'unsound' as impossible and unreachable.
I don't think so. Because a program is only correct if all axioms and proposed theorems are proven true. All axioms are by definition true, so if you assume(false==true) anywhere it has to hold everywhere. Neither "false" or "true" are variables. Just like assume(PI==3.14…) has to hold everywhere. false, true and PI are constant throughout every path in the program. Not really sure how it is possible to disagree with that?
These threads have proven that it's apparently possible to disagree even about the definition of words like "disagreement" and "definition"... But, in a practical programming language definition context, consider: if (0) assume(0); Yes, `assume` could be defined in a way that would make this always a compile error. But then `assume(0)` would be useless. If it means 'unreachable' instead, then the behavior is still consistent - it becomes a way to to tell the compiler: "this can never happen, optimize accordingly". [gmail smtp servers seem to be broken right now; had to post this via the webform; probably won't be posting until the mailing list i/f starts working for me again] artur
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 17:36:00 UTC, Artur Skawina wrote:
    if (0)
       assume(0);

 Yes, `assume` could be defined in a way that would make this
 always a compile error. But then `assume(0)` would be useless.
I don't think so. It makes a lot of sense to halt compilation if you from templates or other constructs emit assume(true==false) or assert(true==false) or any other verification-annotation that contradicts predefined language axioms in a way that the compiler can detect at compile time. Otherwise you risk having "unreachable" unintended in generic code. It also basically gives you a very limited version of a theorem prover and thus the capability of doing real program verification. This should be extended later so that the language supports program verification within it's own syntax. I also dislike this kind of special casing in general. Semantics should be consistent. assert(false) and assume(false) are aberrations, I totally agree with what bearophile has previously stated. Making formal program verification impossible by odd special casing (C mal-practice) is counter productive in the long run.
Aug 06 2014
parent reply Artur Skawina via Digitalmars-d <digitalmars-d puremagic.com> writes:
On 08/06/14 22:57, via Digitalmars-d wrote:
 On Wednesday, 6 August 2014 at 17:36:00 UTC, Artur Skawina wrote:
    if (0)
       assume(0);

 Yes, `assume` could be defined in a way that would make this
 always a compile error. But then `assume(0)` would be useless.
I don't think so. It makes a lot of sense to halt compilation if you from templates or other constructs emit assume(true==false) or assert(true==false) or any other verification-annotation that contradicts predefined language axioms in a way that the compiler can detect at compile time. Otherwise you risk having "unreachable" unintended in generic code.
D already has `static assert`, which can be used for compile-time checks. Eliminating unreachable paths based on the extra information from (a combination of) `assume` statements is desirable, and exactly what this thread is about. I get what you're saying, but it's not really relevant in the context of `D`; such fundamental changes are not exactly likely to happen soon... OTOH the extremely dangerous assert->assume redefinition seems to be seriously considered, despite the grave consequences... artur
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 22:28:08 UTC, Artur Skawina via 
Digitalmars-d wrote:
 D already has `static assert`, which can be used for 
 compile-time checks.
The static modifier would just be a modifier to the regular c-style assert that basically tells the compiler to refuse to add run-time checks. * static assert: prove this or stop compilation * assert: prove this or emit runtime check * assume: define this to hold
 OTOH the extremely dangerous assert->assume redefinition seems 
 to be seriously considered, despite the grave consequences...
Well, I don't worry. It just means that some people, who believe in the concept, are going to spend a lot of effort on something that probably does not pay off. It would be a lot better if they rather spent some effort in adding sound annotations, like bearophile argues for, though. It could be put it to good use by annotating foreign functions Keep in mind that this is an issue that is easy to fix in a private fork. It is a small modification to turn "d-assert" into "assume" and add a "c-assert". It requires no changes to D code?
Aug 06 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
I'll also add that perhaps a source of confusion is that 
assert(X) is presumed to take a bool at compile time. That is not 
the case, there are 3 outcomes:

X==true : this has been proved to hold

X==false: this has been proved to not hold

X not computable: too weak theorem prover, check at runtime
Aug 06 2014
prev sibling parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 17:03:45 UTC, Ola Fosheim Grøstad 
wrote:
 On Wednesday, 6 August 2014 at 16:59:18 UTC, Artur Skawina 
 wrote:
 No, an assume(false) in a program only means that every _path_
 _leading_to_that_statement is 'unsound'. For practical purposes
 it's better to treat 'unsound' as impossible and unreachable.
I don't think so. Because a program is only correct if all axioms and proposed theorems are proven true. All axioms are by definition true, so if you assume(false==true) anywhere it has to hold everywhere. Neither "false" or "true" are variables. Just like assume(PI==3.14…) has to hold everywhere. false, true and PI are constant throughout every path in the program. Not really sure how it is possible to disagree with that?
The crux is the axiom that is being defined. When you write `assume(condition)`, the axiom is not: "`condition` is true." but: "When control flow reaches this point, then `condition` is true." It's not an unconditionally true condition :-P
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 17:59:06 UTC, Marc Schütz wrote:
 The crux is the axiom that is being defined. When you write 
 `assume(condition)`, the axiom is not:

     "`condition` is true."

 but:

     "When control flow reaches this point, then `condition` is 
 true."

 It's not an unconditionally true condition :-P
Assume(X) does not provide a condition. It defines a proposition/relation to be true. If you define a relation between two constants then it has to hold globally. Otherwise they are not constant… Assume(P) defines that the proposition holds. If it does not involve variables, then it will be free to move anywhere by the rules of Hoare-logic (and propositional logic)? If assume(PI==3.14…) can move everywhere, by the rules, then so can assume(true==false). You surely don't want to special case "true==false" in the hoare logic rules? Please note that it is perfectly fine to define "true==false", but you then have to live by it, that is, you no longer have a boolean algebra, you have an unsound algebra. And that holds globally. So, please don't think that assume(true==false) is a test of a condition, it is just a definition that you impose on the equality relation (that also, by incident, happens to make the algebra unsound) If you special case assume(false) and assert(false) then you can no longer use deduction properly and it essentially becomes an aberration, syntactical sugar, that needs special casing everywhere. It would be much better to just halt compilation if you at compile time can evaluate X==false for assume(X) or assert(X). Why let this buggy code live? If it failed at compile time then let the compilation fail! This would work better with CTFE. " unreachable" is an alternative if you want to be explicit about it and matches __builtin_unreachable et al.
Aug 06 2014
next sibling parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim Grøstad 
wrote:
 On Wednesday, 6 August 2014 at 17:59:06 UTC, Marc Schütz wrote:
 The crux is the axiom that is being defined. When you write 
 `assume(condition)`, the axiom is not:

    "`condition` is true."

 but:

    "When control flow reaches this point, then `condition` is 
 true."

 It's not an unconditionally true condition :-P
Assume(X) does not provide a condition. It defines a proposition/relation to be true.
Well, let's call it proposition then...
 If you define a relation between two constants then it has to 
 hold globally. Otherwise they are not constant…
Yes, but as I wrote above, we're not defining a relation between two constants ("true == false"), we define the following axiom: "When control flow reaches this point, then true == false." Because true is not equal to false, it follows that the first part of the proposition cannot be true, meaning control flow will not reach this point.
 Assume(P) defines that the proposition holds. If it does not 
 involve variables, then it will be free to move anywhere by the 
 rules of Hoare-logic (and propositional logic)? If 
 assume(PI==3.14…) can move everywhere, by the rules, then so 
 can assume(true==false).
See above. Of course we could define our `assume(P)` to define `P` as an axiom directly, but this would be much less useful, because it would have exactly the consequences you write about. And it would be a lot more consistent, too. Surely you wouldn't want `assume(x == 42)` to mean "x is always and everywhere equal to 42", but just "x is equal to 42 when control flow passes this point".
 You surely don't want to special case "true==false" in the 
 hoare logic rules?

 Please note that it is perfectly fine to define "true==false", 
 but you then have to live by it, that is, you no longer have a 
 boolean algebra, you have an unsound algebra.  And that holds 
 globally. So, please don't think that assume(true==false) is a 
 test of a condition, it is just a definition that you impose on 
 the equality relation (that also, by incident, happens to make 
 the algebra unsound)

 If you special case assume(false) and assert(false) then you 
 can no longer use deduction properly and it essentially becomes 
 an aberration, syntactical sugar, that needs special casing 
 everywhere.

 It would be much better to just halt compilation if you at 
 compile time can evaluate X==false for assume(X) or assert(X). 
 Why let this buggy code live? If it failed at compile time then 
 let the compilation fail! This would work better with CTFE.

 " unreachable" is an alternative if you want to be explicit 
 about it and matches __builtin_unreachable et al.
See above, no special treatment is necessary.
Aug 06 2014
next sibling parent "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 19:18:30 UTC, Marc Schütz wrote:
 Assume(P) defines that the proposition holds. If it does not 
 involve variables, then it will be free to move anywhere by 
 the rules of Hoare-logic (and propositional logic)? If 
 assume(PI==3.14…) can move everywhere, by the rules, then so 
 can assume(true==false).
See above. Of course we could define our `assume(P)` to define `P` as an axiom directly, but this would be much less useful, because it would have exactly the consequences you write about. And it would be a lot more consistent, too. Surely you wouldn't want `assume(x == 42)` to mean "x is always and everywhere equal to 42", but just "x is equal to 42 when control flow passes this point".
This is unclear. What I wanted to write is: "It would be more consistent to use the definition of `assume` that I propose.".
Aug 06 2014
prev sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 19:18:30 UTC, Marc Schütz wrote:
 On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim
 Yes, but as I wrote above, we're not defining a relation 
 between two constants ("true == false"), we define the 
 following axiom:

     "When control flow reaches this point, then true == false."

 Because true is not equal to false, it follows that the first 
 part of the proposition cannot be true, meaning control flow 
 will not reach this point.
But you are defining an axiom, not evaluating, that is how the optimizer can use it for deduction. Think of how Prolog works.
 See above. Of course we could define our `assume(P)` to define 
 `P` as an axiom directly, but this would be much less useful, 
 because it would have exactly the consequences you write about. 
 And it would be a lot more consistent, too. Surely you wouldn't 
 want `assume(x == 42)` to mean "x is always and everywhere 
 equal to 42", but just "x is equal to 42 when control flow 
 passes this point".
I think there is a misunderstanding here. If you have: uint x=0; then that invokes many axioms defined by the language: uint x=0; assume(x exists from here) assume(any value assigned to x has to be in the range [0,0xffffffff]) assume(x==0) assume(type(x)=='uint') assume(…etc…) So if you then do: x=x+1 assert(x==1) You have to move the assert upwards (3+ steps) and see if it satisfied by any of the axioms you run into. 3: assert(x==0) //covered by axiom(x==0), x==1 is satisfied 2: assert(x+1-1==1-1) 1: assert(x+1==1) x=x+1 assert(x==1) Without the "uint x=0;" you would then have moved all the way up to the global scope (conceptually speaking) and not been able to find any axioms matching 'x'. If you assume(x==0) on the other hand, then you don't need the other axioms at all. It is instantly satisfied. No need to prove anything.
 See above, no special treatment is necessary.
I don't follow. If you use assert(false) to signify anything special beyond requesting a proof or assume(false) for anything beyond defining an axiom, then you are special casing.
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
Please also remember that they are all "constants" in math, but 
variables are constants that are automatically renamed for 
convinience…

uint x=0;
x=x+1;
x=x*2;

is…

uint x0=0;
x1=x0+1;
x2=x1*2;

perhaps that makes it more clear.
Aug 06 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 20:01:04 UTC, Ola Fosheim Grøstad 
wrote:
 Please also remember that they are all "constants" in math, but 
 variables are constants that are automatically renamed for 
 convinience…

 uint x=0;
 x=x+1;
 x=x*2;

 is…

 uint x0=0;
 x1=x0+1;
 x2=x1*2;

 perhaps that makes it more clear.
As you may recall, this is also the common representation in compilers: http://en.wikipedia.org/wiki/Static_single_assignment_form
Aug 06 2014
prev sibling parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim Grøstad
wrote:
 On Wednesday, 6 August 2014 at 17:59:06 UTC, Marc Schütz wrote:
 The crux is the axiom that is being defined. When you write 
 `assume(condition)`, the axiom is not:

    "`condition` is true."

 but:

    "When control flow reaches this point, then `condition` is 
 true."

 It's not an unconditionally true condition :-P
Assume(X) does not provide a condition. It defines a proposition/relation to be true. If you define a relation between two constants then it has to hold globally. Otherwise they are not constant… Assume(P) defines that the proposition holds. If it does not involve variables, then it will be free to move anywhere by the rules of Hoare-logic (and propositional logic)? If assume(PI==3.14…) can move everywhere, by the rules, then so can assume(true==false).
Ah, I had a different understanding of assume, i.e. placing an assume(A) at some point in code adds not the axiom A, but rather the axiom "control flow reaches this spot => A". So if there was a different operator, assume_here() or so, with the semantics that I incorrectly assumed for assume(), could the optimizer insert assume_here() for assert() ?
Aug 06 2014
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
 Ah, I had a different understanding of assume, i.e. placing an
 assume(A) at some point in code adds not the axiom A, but rather
 the axiom "control flow reaches this spot => A".
(Your understanding is the conventional one.)
Aug 06 2014
next sibling parent reply "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
 On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
 Ah, I had a different understanding of assume, i.e. placing an
 assume(A) at some point in code adds not the axiom A, but 
 rather
 the axiom "control flow reaches this spot => A".
(Your understanding is the conventional one.)
Yeah, the one with control flow is really the only useful way to define it, at least for use in an imperative language. If you can only write assumes which are globally valid, then you can't refer to local variables in the expression. That makes it pretty useless. As for assume(0), in the control flow interpretation it makes perfect sense: Assuming control flow reaches here, false = true. So by contradiction, "control flow reaches here" is false, i.e. that point is unreachable. see again the __assume extension in the Microsoft c++ compiler: http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 22:03:11 UTC, David Bregman wrote:
 As for assume(0), in the control flow interpretation it makes 
 perfect sense: Assuming control flow reaches here, false = 
 true. So by contradiction, "control flow reaches here" is 
 false, i.e. that point is unreachable.

 see again the __assume extension in the Microsoft c++ compiler: 
 http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx
From the docs: «The __assume(0) statement is a special case.» So, it does not make perfect sense. If it did, it would not be a special case?
Aug 06 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Thursday, 7 August 2014 at 03:54:12 UTC, Ola Fosheim Grøstad 
wrote:
 «The __assume(0) statement is a special case.»

 So, it does not make perfect sense. If it did, it would not be 
 a special case?
It doesn't have to be a special case if you define it in the right way - in terms of control flow. Then the interpretation of assume(false) as unreachable follows quite naturally: instead of defining assume(x) to mean that x is an axiom, define assume(x) to mean that P=>x is an axiom, where P is the proposition that control flow reaches the assume statement. so assume(false) actually means P=>false, or simply !P and !P means !(control flow reaches the assume), as desired.
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 06:04:38 UTC, David Bregman wrote:
 On Thursday, 7 August 2014 at 03:54:12 UTC, Ola Fosheim Grøstad 
 wrote:
 «The __assume(0) statement is a special case.»

 So, it does not make perfect sense. If it did, it would not be 
 a special case?
It doesn't have to be a special case if you define it in the right way - in terms of control flow. Then the interpretation of assume(false) as unreachable follows quite naturally: instead of defining assume(x) to mean that x is an axiom, define assume(x) to mean that P=>x is an axiom, where P is the proposition that control flow reaches the assume statement. so assume(false) actually means P=>false, or simply !P and !P means !(control flow reaches the assume), as desired.
Let's try the opposite way instead: assume(Q) if(B1){ if(B2){ } } implies: assume(Q) if(B1){ assume(B1&&Q) if(B2){ assume(B1&&B2&&Q) } } So your P in the inner if statement is B1&&B2. However assume(P&&false) is still a fallacy… Or?
Aug 07 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Thursday, 7 August 2014 at 07:53:44 UTC, Ola Fosheim Grøstad 
wrote:
 On Thursday, 7 August 2014 at 06:04:38 UTC, David Bregman wrote:
 On Thursday, 7 August 2014 at 03:54:12 UTC, Ola Fosheim 
 Grøstad wrote:
 «The __assume(0) statement is a special case.»

 So, it does not make perfect sense. If it did, it would not 
 be a special case?
It doesn't have to be a special case if you define it in the right way - in terms of control flow. Then the interpretation of assume(false) as unreachable follows quite naturally: instead of defining assume(x) to mean that x is an axiom, define assume(x) to mean that P=>x is an axiom, where P is the proposition that control flow reaches the assume statement. so assume(false) actually means P=>false, or simply !P and !P means !(control flow reaches the assume), as desired.
Let's try the opposite way instead: assume(Q) if(B1){ if(B2){ } } implies: assume(Q) if(B1){ assume(B1&&Q) if(B2){ assume(B1&&B2&&Q) } } So your P in the inner if statement is B1&&B2. However assume(P&&false) is still a fallacy… Or?
If you use the definition of assume that I gave, assume(P && false) declares the axiom P => (P && false) which is again equivalent to !P.
Aug 07 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 14:09:26 UTC, David Bregman wrote:
 If you use the definition of assume that I gave, assume(P && 
 false) declares the axiom

 P => (P && false)

 which is again equivalent to !P.
Well, P=>(P&&X) is equivalent to P=>X. But you are allowed to have "false" in the preconditions, since we only are interested in preconditions => postconditions assume(input!=0) is ok… it does not say unreachable. It says, postconditions are not required to hold for input==0…
Aug 07 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 15:35:30 UTC, Ola Fosheim Grøstad 
wrote:
 assume(input!=0) is ok… it does not say unreachable.
 It says, postconditions are not required to hold for input==0…
And… assume(false) is a precondition that says that you don't have to care about the postconditions at all… Basically, "assume anything"…
Aug 07 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Thursday, 7 August 2014 at 15:35:30 UTC, Ola Fosheim Grøstad 
wrote:
 On Thursday, 7 August 2014 at 14:09:26 UTC, David Bregman wrote:
 If you use the definition of assume that I gave, assume(P && 
 false) declares the axiom

 P => (P && false)

 which is again equivalent to !P.
Well, P=>(P&&X) is equivalent to P=>X.
Right. So if X is false, the axiom we declare is !P, not "false" or "a fallacy".
 But you are allowed to have "false" in the preconditions, since 
 we only are interested in

 preconditions => postconditions
That's ok. There is no contradiction if P is false. False => X is true for any X, so the axiom we declare is just a tautology. So is the control flow definition / unreachability argument clear now?
 assume(input!=0) is ok… it does not say unreachable.
 It says, postconditions are not required to hold for input==0…
 And… assume(false) is a precondition that says that you don't 
 have to care about the postconditions at all… Basically, 
 "assume anything"…
I don't get this part, maybe you can reword it if I haven't already answered the question.
Aug 07 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
 Right. So if X is false, the axiom we declare is !P, not 
 "false" or "a fallacy".
But Pn is always true where you assume…?
 False => X is true for any X, so the axiom we declare is just a 
 tautology.
I don't follow. If any assumption is false then anything goes…
 So is the control flow definition / unreachability argument 
 clear now?
Nope.
 assume(input!=0) is ok… it does not say unreachable.
 It says, postconditions are not required to hold for 
 input==0…
 And… assume(false) is a precondition that says that you don't 
 have to care about the postconditions at all… Basically, 
 "assume anything"…
I don't get this part, maybe you can reword it if I haven't already answered the question.
assume(true) r = calc() assert(specification_test(r)) //required to hold for any situation assume(false) r=calc() //r can be anything // input!=0 assume(input!=0) // true r=calc(input) assert(specification(input)==r) // required to hold for input!=0 //input=0 assume(input!=0) // false r=calc(input) assert(specification(input)==r) // may or may not hold
Aug 07 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Thursday, 7 August 2014 at 16:56:01 UTC, Ola Fosheim Grøstad 
wrote:
 On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
 Right. So if X is false, the axiom we declare is !P, not 
 "false" or "a fallacy".
But Pn is always true where you assume…?
No. Remember P is "control flow can reach this assume". If the assume is unreachable, then P is false. The compiler doesn't always know that P is false though, so we can use assume(false) to supply that as an axiom. Here's an example: x = rand() & 3; // x is 0,1,2 or 3. switch(x) { case 0: foo(); case 1: bar(); case 2: baz(); case 3: qux(); default: assume(false); // hopefully redundant with a decent compiler. } now the compiler can optimize this down to {foo, bar, baz, qux}[x](); or even better, a computed jump.
 False => X is true for any X, so the axiom we declare is just 
 a tautology.
I don't follow. If any assumption is false then anything goes…
Using my definition of assume, the axiom declared is P=>x. If P is false, then the axiom declared is false => x, which is true for any x. http://en.wikipedia.org/wiki/Truth_table#Logical_implication
 So is the control flow definition / unreachability argument 
 clear now?
Nope.
Ok, is it clear now? If not, which parts are not clear?
Aug 07 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 17:38:22 UTC, David Bregman wrote:
 Using my definition of assume, the axiom declared is P=>x. If P 
 is false, then the axiom declared is false => x, which is true 
 for any x.
I don't see how this will work out. If it is truly unreachable then you don't need any assume, because then you can assert anything. Therefore you shouldn't. valid: assume(true) while(true){} assert(angels_love_pixiedust) //proven true now… But there are alternatives to HL that I don't know much about. You might want to look at "Matching Logic Reachability". Looks complicated: http://fsl.cs.illinois.edu/pubs/rosu-stefanescu-2012-fm.pdf
 Ok, is it clear now? If not, which parts are not clear?
It doesn't make any sense to me since I don't see how you would discriminate between your Ps. {P1} while(true) skip; endwhile {P2} How do you define P1 and P2 to be different?
Aug 07 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad 
wrote:
 I don't see how this will work out. If it is truly unreachable 
 then you don't need any assume
I just gave you a concrete example of where assume(false) might be useful for optimizing a switch statement. Just because it is truly unreachable doesn't mean the compiler is aware of that.
 It doesn't make any sense to me since I don't see how you would 
 discriminate between your Ps.

 {P1}
 while(true) skip; endwhile
 {P2}

 How do you define P1 and P2 to be different?
I'm not sure how you'd define them to be the same. They're different lines of code, for one thing.
Aug 07 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 18:20:20 UTC, David Bregman wrote:
 On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad 
 wrote:
 I just gave you a concrete example of where assume(false) might 
 be useful for optimizing a switch statement.
But to me it sounds dangerous if it actually is reachable or if the compiler somehow think it is. So you should use halt() if it should be unreachable, and use unreachable() if you know 100% it holds. Encouraging assume(false) sounds like an aberration to me. You need to provide proofs if you attempt using assume(X) and assert(false). This is valid, but it is derived, not postulated: assume(P) while(false){ assume(false) // anything goes is acceptable over S here S… // since it never happens… assert(P) // valid since the assumption is false } assert(P) // valid since the content is just a noop When you postulate without proving you open a can of worms: assume(P) while(B){ assume(false) // woops! Should have been assume(B&&P) S… // ohoh we just stated anything goes in here… assert(P) // invalid } assert(P) // invalid since the loop invariant doesn't hold.
 How do you define P1 and P2 to be different?
I'm not sure how you'd define them to be the same. They're different lines of code, for one thing.
I don't believe there "is" such a thing as lines of code. We are doing math. Everything just "is". We don't have code, we have mathematical dependencies/relations. P1 and P2 are propositions, so what are the content of those? The ones you use for your P1=>X and P2=>Y? You have to define newassume(P,X)===assume(P=>X). But what is P? Anyway, you don't need those… You can use a regular assume(false), but not for indicating unreachable. You indicate that the postcondition does not have to hold. Otherwise you will run into trouble. But if you think about while() as a short-hand that is expanded into pure math, then it makes sense. If you have while(true){} then the loop cannot generate new mathematical constants… Thus it cannot be a source for new unique propositions that let you discriminate between before and after entering the loop? Or?
Aug 07 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Thursday, 7 August 2014 at 19:41:44 UTC, Ola Fosheim Grøstad 
wrote:
 On Thursday, 7 August 2014 at 18:20:20 UTC, David Bregman wrote:
 On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim 
 Grøstad wrote:
 I just gave you a concrete example of where assume(false) 
 might be useful for optimizing a switch statement.
But to me it sounds dangerous if it actually is reachable or if the compiler somehow think it is.
It is dangerous, and shouldn't be used lightly. That's what started this whole thread.
 So you should use halt() if it should be unreachable,
Not if your goal is to completely optimize away any unreachable code.
 and use unreachable() if you know 100% it holds.
This is just another name for the same thing, it isn't any more or less dangerous.
 Encouraging assume(false) sounds like an aberration to me.
If you accept my definition of assume there is no problem with it, it just means unreachable. I showed how this follows naturally from my definition.
 You need to provide proofs if you attempt using assume(X) and 
 assert(false).
There is no mechanism for providing proofs or checking proofs in D.
 How do you define P1 and P2 to be different?
I'm not sure how you'd define them to be the same. They're different lines of code, for one thing.
I don't believe there "is" such a thing as lines of code. We are doing math. Everything just "is". We don't have code, we have mathematical dependencies/relations.
Well, any correct mathematical formalism of the code must preserve its semantics, so it doesn't really matter which one we talk about. Different lines (or basic blocks, I guess is the right term here) can have different reachability, so you could just give each one its own P.
 P1 and P2 are propositions, so what are the content of those? 
 The ones you use for your P1=>X and P2=>Y?
This is just an implementation detail of the compiler. Probably each basic block has its own P, which is conservatively approximated with some data flow analysis. (Disclaimer: I am not a compiler expert)
 Anyway, you don't need those… You can use a regular 
 assume(false), but not for indicating unreachable. You indicate 
 that the postcondition does not have to hold. Otherwise you 
 will run into trouble.

 But if you think about while() as a short-hand that is expanded 
 into pure math, then it makes sense. If you have while(true){} 
 then the loop cannot generate new mathematical constants… Thus 
 it cannot be a source for new unique propositions that let you 
 discriminate between before and after entering the loop? Or?
Sorry, I don't understand much of this. Anyways, I don't have much more time to keep justifying my definition of assume. If you still don't like mine, maybe you can give your definition of assume, and demonstrate how that definition is more useful in the context of D.
Aug 07 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 23:13:15 UTC, David Bregman wrote:
 and use unreachable() if you know 100% it holds.
This is just another name for the same thing, it isn't any more or less dangerous.
Of course it is. unreachable() could lead to this: f(){ unreachable} g(){...} f: g: machinecode assume(false) just states that the post condition has not been proved/tested/verified yet. That does not signify that no code will reach it. It just means that the returned value is uncertain. It does not mean that the code will never be executed. It is also dangerous to mix them up since CTFE can lead to assume(false). If you want safety and consistence you need to have a designated notation for unreachable.
 Encouraging assume(false) sounds like an aberration to me.
If you accept my definition of assume there is no problem with it, it just means unreachable. I showed how this follows naturally from my definition.
Your "definition" is lacking. It mixes up two entirely different perspectives, the deductive mode and the imperative mode of reasoning.
 You need to provide proofs if you attempt using assume(X) and 
 assert(false).
There is no mechanism for providing proofs or checking proofs in D.
Actually, unit tests do. D just lacks the semantics to state that the input accepted by the precondition has been fully covered in unit tests.
 Well, any correct mathematical formalism of the code must 
 preserve its semantics, so it doesn't really matter which one 
 we talk about.
Preserve the semantics of the language, yes. For pure functions there is no difference. And that is generally what is covered by plain HL. The code isn't modified, but you only prove calculations, not output.
 Different lines (or basic blocks, I guess is the right term 
 here) can have different reachability, so you could just give 
 each one its own P.
"basic blocks" is an artifact of a specific intermediate representation. It can cease to exist. For instance MIPS and ARM have quite different conditionals than x86. With a MIPS instruction set a comparison is an expression returning 1 or 0 and you can get away from conditionals by multiplying successive calculations with it to avoid branch penalties. This is also a common trick for speeding up SIMD… Hoare Logic deals with triplets: precondition, statement, postcondition. (assume,code,assert) You start with assume(false), then widen it over the code until the assert is covered for the input you care about.
 P1 and P2 are propositions, so what are the content of those? 
 The ones you use for your P1=>X and P2=>Y?
This is just an implementation detail of the compiler. Probably each basic block has its own P, which is conservatively approximated with some data flow analysis. (Disclaimer: I am not a compiler expert)
Oh, there is of course no problem by inserting a unreachable barrier-like construct when you have proven assume(false), but it is a special case. It is not an annotation for deduction.
 Anyways, I don't have much more time to keep justifying my 
 definition of assume. If you still don't like mine, maybe you 
 can give your definition of assume, and demonstrate how that 
 definition is more useful in the context of D.
assume(x) is defined by the preconditions in Hoare Logic triplets. This is what you should stick to for in(){} preconditions. A backend_assume(x) is very much implementation defined and is a precondition where the postconditions is: program(input) == executable(input) for all x except those excluded by backend_assume. However an assume tied to defining a function's degree of verification is not a backend_assume. That is where D risk going seriously wrong: conflating postconditions (assert) with preconditions (assume) and conflating local guarantees (by unit tests or proofs) with global optimization and backend mechanisms (backend_assume).
Aug 09 2014
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08/09/2014 09:26 PM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= 
<ola.fosheim.grostad+dlang gmail.com>" wrote:
 On Thursday, 7 August 2014 at 23:13:15 UTC, David Bregman wrote:
 and use unreachable() if you know 100% it holds.
This is just another name for the same thing, it isn't any more or less dangerous.
Of course it is. unreachable() could lead to this: f(){ unreachable} g(){...} f: g: machinecode assume(false) just states that the post condition has not been proved/tested/verified yet. That does not signify that no code will reach it.
Formally, that's what it assumes to be the case. If you can prove 'false', this means that the code is unreachable. if(Q){ ⦃ Q ⦄ if(¬Q){ ⦃ Q ∧ ¬Q ⦄ ⦃ false ⦄ // this means 'unreachable' assert(false); // goes through } } After assuming 'false' you can prove false. ⦃ false ⦄ still means 'unreachable' if it is 'assume'd. (Yes, of course it can also be read as 'inconsistent', if the code is actually reachable, but proving code 'unreachable' which can actually be reached also just means that the reasoning and the assumptions were 'inconsistent'. You can also read 'inconsistent' as: 'this program will never actually be executed', etc. David's interpretation of the formalism is adequate.)
 Encouraging assume(false) sounds like an aberration to me.
If you accept my definition of assume there is no problem with it, it just means unreachable. I showed how this follows naturally from my definition.
Your "definition" is lacking. It mixes up two entirely different perspectives, the deductive mode and the imperative mode of reasoning.
I think you should elaborate on this a little if you want to make a point. E.g. I don't think that such an opposition of 'reasoning modes' even exists.
 Hoare Logic deals with triplets: precondition, statement, postcondition. 
(assume,code,assert)
'assume' and 'assert' are "statement"s: ⦃ P ∧ Q ⦄ // ← precondition assert(Q); // ← statement ⦃ P ⦄ // ← postcondition 'assume' is just a dual concept: ⦃ P ⦄ // ← precondition assume(Q); // ← statement ⦃ P ∧ Q ⦄ // ← postcondition There is nothing 'lacking' here, right?
Aug 09 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Saturday, 9 August 2014 at 20:22:36 UTC, Timon Gehr wrote:
 Formally, that's what it assumes to be the case. If you can 
 prove 'false', this means that the code is unreachable.
No, if you prove false that means either that it is nonterminating or that it cannot be proved by the the assumptions, hence the assumptions need strengthening.
         ⦃ Q ∧ ¬Q ⦄
         ⦃ false ⦄     // this means 'unreachable'
         assert(false); // goes through
implication is not equivalence
 After assuming 'false' you can prove false.
 ⦃ false ⦄ still means 'unreachable' if it is 'assume'd.
False only means that the postcondition does not hold. If the precondition is false then the triplet is valid i.e. correct.
 (Yes, of course it can also be read as 'inconsistent', if the 
 code is actually reachable, but proving code 'unreachable'
No, you can have this: main(){ Precondition(false) Stuff() Postcondition(anything) } This states that Stuff has not yet been verified for any input. It does not state that Stuff will never execute.
 Your "definition" is lacking. It mixes up two entirely 
 different perspectives,
 the deductive mode and the imperative mode of reasoning.
I think you should elaborate on this a little if you want to make a point. E.g. I don't think that such an opposition of 'reasoning modes' even exists.
Of course it does, that is why Hoare Logic and SSA exist. Deduction lacks a notion of time.
 ⦃ P ∧ Q ⦄  // ← precondition
 assert(Q); // ← statement
 ⦃ P ⦄      // ← postcondition
Makes no sense. Assert is not an imperative statement, it is an annotation. It is meta.
Aug 09 2014
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08/10/2014 04:40 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= 
<ola.fosheim.grostad+dlang gmail.com>" wrote:
 On Saturday, 9 August 2014 at 20:22:36 UTC, Timon Gehr wrote:
 Formally, that's what it assumes to be the case. If you can prove
 'false', this means that the code is unreachable.
No, if you prove false that means either that it is nonterminating
I.e. everything afterwards is unreachable.
         ⦃ Q ∧ ¬Q ⦄
         ⦃ false ⦄     // this means 'unreachable'
         assert(false); // goes through
implication is not equivalence
Do you agree we indeed have equivalence for those programs with an empty precondition?
 or that it cannot be proved by the the assumptions, hence the assumptions
 need strengthening.
 ...
'false' is the strongest statement. Why would you need to strengthen assumptions?
 (Yes, of course it can also be read as 'inconsistent', if the code is
 actually reachable, but proving code 'unreachable'
No, you can have this: main(){ Precondition(false) Stuff() Postcondition(anything) } This states that Stuff has not yet been verified for any input. It does not state that Stuff will never execute. ...
If the precondition is actually assumed to hold for all executions of the program, a precondition of 'false' means that the program never executes. Maybe you don't assume this, but internally to the logic, this is what happens: You verify the postcondition under the assumption of the precondition. I.e. in this case you verify the postcondition of the program under the assumption that it never executes. Of course you may still execute such a program, but the ⦃ ⦄ assertions become irrelevant to this execution. Note that an optimizer needs to be able to use deduced facts for program transformations, or it is useless. To an optimizer, a contradiction means 'unreachable'. There are no non-trivial preconditions (in your sense, i.e. the program still may have interesting behaviour if they are violated) on the program used to deduce those facts. Do you agree that _if_ 'assume' is to be seen as an optimizer hint, then 'assume(false)' means 'assume unreachable'?
 Your "definition" is lacking. It mixes up two entirely different
 perspectives,
 the deductive mode and the imperative mode of reasoning.
I think you should elaborate on this a little if you want to make a point. E.g. I don't think that such an opposition of 'reasoning modes' even exists.
Of course it does, that is why Hoare Logic and SSA exist.
They exist for the virtue of being convenient formalisms for some applications, but they can be embedded into e.g. set theory just fine.
 Deduction lacks a notion of time.
 ...
What is 'a notion of time' and how does HL provide it?
 ⦃ P ∧ Q ⦄  // ← precondition
 assert(Q); // ← statement
 ⦃ P ⦄      // ← postcondition
Makes no sense.
It is a definition. If you actually want to understand David's point you should digest it. Does ⦃ false ⦄ abort; ⦃ P ⦄ make sense to you? The assert(Q); statement is equivalent to if(¬Q) abort;
 Assert is not an imperative statement,
Yes, it may be seen to be.
 it is an annotation. It is meta.
If it is part of the program it is not 'meta'. Here, there is a distinction between: assert(P) // statement and ⦃ P ⦄ // "meta" even though both are commonly called 'assertions'. assert(P); is a statement and hence it needs to be given a semantics, e.g. an axiomatic semantics or by rewriting, as above. (BTW: This is not about being right or wrong. It is about understanding each other's statements in the right context.)
Aug 10 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Sunday, 10 August 2014 at 13:47:45 UTC, Timon Gehr wrote:
 No, if you prove false that means either that it is 
 nonterminating
I.e. everything afterwards is unreachable.
Depends on your take on it. If you support non-deterministic computations (e.g. Ada's "select") then non-termination is treated like bottom. So you can have infinite_recursion() or terminates() => terminates() So unreachable in terms of machine-language, sure, but not in terms of execution flow.
 Do you agree we indeed have equivalence for those programs with 
 an empty precondition?
You mean "false" or "true"?
 or that it cannot be proved by the the assumptions, hence the 
 assumptions
 need strengthening.
 ...
'false' is the strongest statement. Why would you need to strengthen assumptions?
If you succeed in proving the postcondition to be false then the postcondition does not hold and you have to strengthen the precondition or else the triplet is invalid/incorrect. If the precondition is defined false then the postcondition is not required to hold. It is not covered by the proof/verification/specification and the triplet is valid/provably correct. So if the precondition is defined false then the program is a priori proved correct to the specification, i.e. the specification does not require any guarantees for the result.
 If the precondition is actually assumed to hold for all 
 executions of the program, a precondition of 'false' means that 
 the program never executes.
That is the responsibility of the caller. It is the caller's responsibility to uphold the precondition in order to get guaranteed results. But you could have multiple pairs of preconditions/postconditions. E.g. you could for a generic function have different pairs for int/float/double or have a separate pair for termination, etc. Or have one set that specifies what is covered by unit-tests, what is vetted by review, what is totally unknown… You could have different types of guarantees for a library and users could take advantage of it based on the requirements for the application (high security vs computer game).
 Maybe you don't assume this, but internally to the logic, this 
 is what happens: You verify the postcondition under the 
 assumption of the precondition. I.e. in this case you verify 
 the postcondition of the program under the assumption that it 
 never executes.
It is not always possible to prove termination, so that would be unfortunate. It would be more useful to be able to restrict the precondition to what you cover by unit-tests. Or to have multiple sets of pre/postconditions (proven-by-machine vs vetted-by-review). Then if you can prove that the caller fulfills the precondition you are able to optimize based on the pre/post condition and assume the post-condition if it is machine-verified. That would give new optimization possibilities. That does not mean that you should never be able to use a function outside the verified range (by machine proof), but then you need to assert the results at runtime if you want verified correctness.
 Of course you may still execute such a program, but the ⦃ ⦄ 
 assertions become irrelevant to this execution.
Not really, they could still trap.
 Note that an optimizer needs to be able to use deduced facts 
 for program transformations, or it is useless. To an optimizer, 
 a contradiction means 'unreachable'.
No, to an optimizer a contradiction means "all bets are off for the postcondition to hold": program(x) != executable(x) That is why __assume(P) must always hold on any reachable path (e.g. any path that the optimizer considers to be a target for optimization). But __assume is not a regular precondition, it has a counterpart in the optimization invariant (postcondition): program(x) == executable(x), x not creating contradictions by __assume(…) The optimizer is presuming that anything goes as long as this optimization invariant can be upheld. This is not a postcondition specified by the programmer at the meta-level. It is implicit. And the optimizer does not check the implicit precondition, at all…
 to deduce those facts. Do you agree that _if_ 'assume' is to be 
 seen as an optimizer hint, then 'assume(false)' means 'assume 
 unreachable'?
No. I think the optimizer should only use assumptions when they are guaranteed to hold by the caller or the language axioms. Or in the rare case by other machine verifiable axioms (specifications for hardware registers etc).
 Of course it does, that is why Hoare Logic and SSA exist.
They exist for the virtue of being convenient formalisms for some applications, but they can be embedded into e.g. set theory just fine.
Not sure what you mean by this and how this relates to imperative programming.
 Deduction lacks a notion of time.
 ...
What is 'a notion of time' and how does HL provide it?
It doesn't. Which is why it trips when you don't prove termination. But HL does not do program transformations.
 The assert(Q); statement is equivalent to

 if(¬Q) abort;
Not if assert() is considered meta-level. However, since a triplet is tied to an entity/function/module, it would be ok to throw an exception as long as it isn't caught in the module covered by the pre/postcondition triplet if it does not have any side effects. If you don't reach the postcondition it does not matter.
 Assert is not an imperative statement,
Yes, it may be seen to be.
That would be an aberration, because the specification should either be independent of the implementation or generate the implementation… If the specification is considered part of the program then you will run into problems if there are contradictions.
 assert(P); is a statement and hence it needs to be given a 
 semantics, e.g. an axiomatic semantics or by rewriting, as 
 above.
Well, in C it is a statement by implementation, but it is always meant to not have side effects and one should be able to compile with NDEBUG with no difference in program behaviour. So, even though it is implemented as a macro it has always had the status of an annotation.
 (BTW: This is not about being right or wrong. It is about 
 understanding each other's statements in the right context.)
I think the whole game changes when Walter wants to optimize based on the annotations… Then you need to be very careful unless you want to amplify bugs rather than improve the overall performance of the program (speed + correct behaviour). So then the distinction between specification and implementation, proven and vetted, becomes even more important. Since D has unit tests as a formalism, then it would be a shame to not use it to verify contracts in a way that could provide safe optimization possibilities rather than relying on programmers being able to write provably correct code in a predictable manner, which just ain't gonna happen.
Aug 10 2014
prev sibling parent reply "Kagamin" <spam here.lot> writes:
On Sunday, 10 August 2014 at 02:40:31 UTC, Ola Fosheim Grøstad 
wrote:
 Of course it does, that is why Hoare Logic and SSA exist. 
 Deduction lacks a notion of time.
Logic is ordered, and we have a notion of order because we know time, which is the only obviously ordered thing in nature. So in a sense any logic has time in its foundation and math can do the reverse: represent time in declarative manner.
Aug 11 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Tuesday, 12 August 2014 at 04:50:15 UTC, Kagamin wrote:
 Logic is ordered, and we have a notion of order because we know 
 time, which is the only obviously ordered thing in nature. So 
 in a sense any logic has time in its foundation and math can do 
 the reverse: represent time in declarative manner.
No, there is no order to boolean expressions. Deduction can be performed bottom up. Imperative programs rely on top down execution due to side effects. Recall that all pure functions over finite types can be implemented as tables. A table lookup is O(1). No time.
Aug 11 2014
parent reply "Kagamin" <spam here.lot> writes:
On Tuesday, 12 August 2014 at 05:47:22 UTC, Ola Fosheim Grøstad 
wrote:
 On Tuesday, 12 August 2014 at 04:50:15 UTC, Kagamin wrote:
 Logic is ordered, and we have a notion of order because we 
 know time, which is the only obviously ordered thing in 
 nature. So in a sense any logic has time in its foundation and 
 math can do the reverse: represent time in declarative manner.
No, there is no order to boolean expressions. Deduction can be performed bottom up.
A true reversal would be when preconditions are derived from postconditions.
 Recall that all pure functions over finite types can be 
 implemented as tables. A table lookup is O(1). No time.
That's different logic, and algorithmic complexity is time.
Aug 12 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Tuesday, 12 August 2014 at 08:07:01 UTC, Kagamin wrote:
 A true reversal would be when preconditions are derived from 
 postconditions.
That's how you conduct a proof…
 Recall that all pure functions over finite types can be 
 implemented as tables. A table lookup is O(1). No time.
That's different logic, and algorithmic complexity is time.
Not at all. You can create a boolean expression for every bit of output and evaluate it only using NAND gates (or NOR). Not practical, but doable…
Aug 12 2014
parent reply "Kagamin" <spam here.lot> writes:
On Tuesday, 12 August 2014 at 09:17:54 UTC, Ola Fosheim Grøstad 
wrote:
 On Tuesday, 12 August 2014 at 08:07:01 UTC, Kagamin wrote:
 A true reversal would be when preconditions are derived from 
 postconditions.
That's how you conduct a proof…
A proof usually flows from causes to consequences, the reverse (induction) is ambiguous. Ordering is more fundamental: you can define or redefine it, but it will remain, one can't think outside of this formalism.
 Not at all. You can create a boolean expression for every bit 
 of output and evaluate it only using NAND gates (or NOR). Not 
 practical, but doable…
Mathematics is pretty aware of differences between algorithms, and proving their equivalence is non-trivial.
Aug 12 2014
parent "Ola Fosheim Gr" <ola.fosheim.grostad+dlang gmail.com> writes:
On Tuesday, 12 August 2014 at 14:43:23 UTC, Kagamin wrote:
 A proof usually flows from causes to consequences, the reverse 
 (induction) is ambiguous.
If a deterministic imperative program is ambigious then there is something wrong. So no, ambiguity is not the problem. The size if the search space is. The preconditions are "the ambiguity" which the theorem prover try to find...
 Ordering is more fundamental: you can define or redefine it, 
 but it will remain, one can't think outside of this formalism.
Explain.
 Not at all. You can create a boolean expression for every bit 
 of output and evaluate it only using NAND gates (or NOR). Not 
 practical, but doable…
Mathematics is pretty aware of differences between algorithms, and proving their equivalence is non-trivial.
Define non-trivial. We were talking about the nature of finite computations. They are all trivial. Algorithms are just compression of space.
Aug 12 2014
prev sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
 On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
 Ah, I had a different understanding of assume, i.e. placing an
 assume(A) at some point in code adds not the axiom A, but 
 rather
 the axiom "control flow reaches this spot => A".
(Your understanding is the conventional one.)
Not right. You need to take into account that assume() provides a mathematical definition, it isn't an imperative. That would make no sense. So there is no control flow, only mathematical dependencies. You only deal with constants. "Variables" are just a tool for automatic labeling of constants. You would not be able to use logic otherwise. "Control flow" is embedded in the dependencies and relationships between the constants. j=0 for(i=0; i<3;++i){j+=i} Is just a short-hand for: j0 = 0 i0 = 0 j1 = j0 + i0 i1 = 1 j2 = j1 + i1 i2 = 2 j3 = j2 + i2 If you map this out as a graph you get the dependencies (mirroring "control flow"). Hoare-logic provide means to reason about the short-hand notation and make transformations on it. What is unconventional about this?
Aug 06 2014
parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
On Thursday, 7 August 2014 at 03:51:02 UTC, Ola Fosheim Grøstad
wrote:
 On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
 On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
 Ah, I had a different understanding of assume, i.e. placing an
 assume(A) at some point in code adds not the axiom A, but 
 rather
 the axiom "control flow reaches this spot => A".
(Your understanding is the conventional one.)
Not right. You need to take into account that assume() provides a mathematical definition, it isn't an imperative. That would make no sense. So there is no control flow, only mathematical dependencies.
But control flow can introduce mathematical dependencies. E.g. for assert the code if(a) { assert(b); ... } is not equivalent to assert(b); if(a) { ... } but not because the assertion depends on a different incarnation of "b", but because it also depends on "a", so it is like assert(!a || b); if(a) { ... } If assume is independent of control flow, then clearly this cannot be related to assert. But I think the proposal was not to replace assert with the textbook definition of assume, rather to use the information in asserts to optimize the code. So if assume doesn't work, what about assume_here() ?
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 05:41:22 UTC, Matthias Bentrup 
wrote:
 If assume is independent of control flow, then clearly this
 cannot be related to assert.
Well, both assume and assert are "independent" of control flow since you don't have execution or control flow in mathematics. The dependency is tied to the "renaming of variables into constants" which allows Hoare-Logic to work on variables, not only constants. However, for proper constants, you don't need that limit for neither assert nor assume? if(B){ assume(B && PI==3.14) } else { assume(!B && PI==3.14) // must hold here too since it is a constant } apply hoare logic rule for if: if this holds: {B ∧ P} S {Q} , {¬B ∧ P } T {Q} then this holds: {P} if B then S else T endif {Q} which gives: assume(PI==3.14) f(B){ assume(PI==3.14) } else { assume(PI==3.14) } assume(PI==3.14) (Usually you only have assume at the top in the preconditions, since you otherwise don't get a proof :-).
Aug 06 2014
parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
On Thursday, 7 August 2014 at 06:32:18 UTC, Ola Fosheim Grøstad 
wrote:
 On Thursday, 7 August 2014 at 05:41:22 UTC, Matthias Bentrup 
 wrote:
 If assume is independent of control flow, then clearly this
 cannot be related to assert.
Well, both assume and assert are "independent" of control flow since you don't have execution or control flow in mathematics. The dependency is tied to the "renaming of variables into constants" which allows Hoare-Logic to work on variables, not only constants. However, for proper constants, you don't need that limit for neither assert nor assume? if(B){ assume(B && PI==3.14) } else { assume(!B && PI==3.14) // must hold here too since it is a constant } apply hoare logic rule for if: if this holds: {B ∧ P} S {Q} , {¬B ∧ P } T {Q} then this holds: {P} if B then S else T endif {Q} which gives: assume(PI==3.14) f(B){ assume(PI==3.14) } else { assume(PI==3.14) } assume(PI==3.14) (Usually you only have assume at the top in the preconditions, since you otherwise don't get a proof :-).
So the D function (note that "a" is constant) int silly() { enum int a = 1; if( a == 2 ) { assert( a == 2 ); } return a; } has undefined semantics (at least in debug mode), because it contains a false assertion ? That is not my understanding of assert.
Aug 07 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 08:12:23 UTC, Matthias Bentrup 
wrote:
 So the D function (note that "a" is constant)

 int silly() {
   enum int a = 1;
   if( a == 2 ) {
     assert( a == 2 );
   }
   return a;
 }

 has undefined semantics (at least in debug mode), because it 
 contains a false assertion ?
It isn't reachable so it is not part of the program? If you support generic programming you probably should limit proofs to reachable portions of library code. However the specification or the implementation of it appears to be flawed, so perhaps it should be considered incorrect if this was in application code. You usually try to prove post conditions in terms of pre conditions. The invariants, variants and asserts are just tools to get there. So this is not a typical issue.
Aug 07 2014
parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
On Thursday, 7 August 2014 at 08:35:21 UTC, Ola Fosheim Grøstad 
wrote:
 On Thursday, 7 August 2014 at 08:12:23 UTC, Matthias Bentrup 
 wrote:
 So the D function (note that "a" is constant)

 int silly() {
  enum int a = 1;
  if( a == 2 ) {
    assert( a == 2 );
  }
  return a;
 }

 has undefined semantics (at least in debug mode), because it 
 contains a false assertion ?
It isn't reachable so it is not part of the program? If you support generic programming you probably should limit proofs to reachable portions of library code. However the specification or the implementation of it appears to be flawed, so perhaps it should be considered incorrect if this was in application code. You usually try to prove post conditions in terms of pre conditions. The invariants, variants and asserts are just tools to get there. So this is not a typical issue.
So reachability has an influence, but control flow hasn't ?
Aug 07 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Thursday, 7 August 2014 at 08:52:43 UTC, Matthias Bentrup 
wrote:
 So reachability has an influence, but control flow hasn't ?
You have to define what you want to prove. 1. The post condition to hold? 2. A sound specification to be fully implemented? 3. That executed code is tested when it executes, but ignore that important code should have been executed instead. (1) and (2) is what program verification and aims for. (1) is what design by contract tries to establish. (3) is weak and what c-asserts do.
Aug 07 2014
prev sibling parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 16:00:33 UTC, Ola Fosheim Grøstad 
wrote:
 On Wednesday, 6 August 2014 at 15:36:52 UTC, Marc Schütz wrote:
 This is an assume, not an assert.
Not sure what you mean. An assume is an assert proven (or defined) to hold. It can be a proven theorem which has been given the status of an axiom. It is known to keep the algebraic system sound. If you claim that something unsound is proven then all bets are off everywhere?
I guess we're talking past each other. You were saying that Hoare logic doesn't work with non-terminating loops, and I was responding that there was no non-terminating loop in the example. That's all there is to it. To clarify: The assume condition wasn't `false`, it was `!running`. There is a situation in which this is true, namely when `running` is false at the point where the assume is. Because the variable isn't changed in the loop, it follows that it's also true before the loop. I see no contradiction here.
Aug 06 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 17:03:44 UTC, Marc Schütz wrote:
 I guess we're talking past each other. You were saying that 
 Hoare logic doesn't work with non-terminating loops, and I was 
 responding that there was no non-terminating loop in the 
 example. That's all there is to it.
Oh well, but a terminating loop that does not change the condition is just an empty statement. So then you have basically proved that it isn't a loop… ;)
Aug 06 2014
parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
On Wednesday, 6 August 2014 at 17:08:18 UTC, Ola Fosheim Grøstad
wrote:
 On Wednesday, 6 August 2014 at 17:03:44 UTC, Marc Schütz wrote:
 I guess we're talking past each other. You were saying that 
 Hoare logic doesn't work with non-terminating loops, and I was 
 responding that there was no non-terminating loop in the 
 example. That's all there is to it.
Oh well, but a terminating loop that does not change the condition is just an empty statement. So then you have basically proved that it isn't a loop… ;)
I still can't see how you can infer that the assume(!running) which clearly holds after the loop also holds before the loop.
Aug 06 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 17:19:45 UTC, Matthias Bentrup 
wrote:
 I still can't see how you can infer that the assume(!running)
 which clearly holds after the loop also holds before the loop.
It holds if the loop does not change running, trivially? But then you no longer have a loop. Note also that you can implement an if construct from while this way: while(B){ S; B=false; } If that was the case, then you could not infer anything about B before the while.
Aug 06 2014
prev sibling parent reply "Matthias Bentrup" <matthias.bentrup googlemail.com> writes:
On Wednesday, 6 August 2014 at 15:29:13 UTC, Ola Fosheim Grøstad
wrote:
 On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup 
 wrote:
 is equivalent to

  while(running) {
    ...don't assign to running, don't break...
  }
  assume(!running);
You have to prove termination to get there? Plain Hoare logic cannot deal with non-terminating loops. Otherwise you risk proving any theorem below the loop to hold?
I'm pretty sure that running is false when the program reaches the end of the while loop, whether it is assigned in the loop or not. I only added the "don't assign to running" to make the example match your pattern.
Aug 06 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Wednesday, 6 August 2014 at 16:42:57 UTC, Matthias Bentrup 
wrote:
 I'm pretty sure that running is false when the program reaches
 the end of the while loop, whether it is assigned in the loop or
 not. I only added the "don't assign to running" to make the
 example match your pattern.
Well, if you don't assign to it in the loop, and it is known to terminate, then "running" is provably false before the loop for sure? But then it isn't a loop… It is an empty statement: skip, NOP…
Aug 06 2014
prev sibling parent Artur Skawina via Digitalmars-d <digitalmars-d puremagic.com> writes:
On 08/06/14 17:02, Matthias Bentrup via Digitalmars-d wrote:
 But even if there is no explicit assert()/assume() given by the developer, I
guess the optimizer is free to insert assumes that are provably correct, e.g.
 
   while(running) {
     ...don't assign to running, don't break...
   }
 
 is equivalent to
 
   while(running) {
     ...don't assign to running, don't break...
   }
   assume(!running);
In the "running==true" case that 'assume' will never be reached...
 is equivalent to
 
   assume(!running);
   while(running) {
     ...don't assign to running, don't break...
   }
... so, no, this transformation is not a valid one.
 So I take the compiler is allowed to throw away code without any asserts
already ?
It can do whatever it wants, as long as the observable behavior does not change. `Assume` removes that restriction as soon as a failing assert is reached. artur
Aug 06 2014
prev sibling parent Jeremy Powers via Digitalmars-d <digitalmars-d puremagic.com> writes:
 The main argument seems to revolve around whether this is actually a
change or not. In my (and others') view, the treatment of assert as 'assume' is not a change at all. It was in there all along, we just needed the wizard to tell us.
How can there be any question? This is a change in the compiler, a change in the docs, change in what your program does, change of the very bytes in the executable. If my program worked before and doesn't now, how is that not a change? This must be considered a change by any reasonable definition of the word change. I don't think I can take seriously this idea that someone's unstated, unmanifested intentions define change more so than things that are .. you know.. actual real changes.
Yes, sorry, there will be actual consequences if the optimizations are implemented. What I meant with the somewhat facetious statement was that there is no semantic change - broken code will still be broken, it will just be broken in a different way. If you subscribe to the idea that a failed assertion indicates all subsequent code is invalid, then subsequent code is broken (and undefined, if the spec says it is undefined). The change would be clarifying this in the spec, and dealing with the fallout of previously broken-but-still-working code behaving differently under optimization. At least, that's how I understand it... I hope I an not mischaracterizing others' positions here (let me know, and I'll shut up).
 Well I think I outlined the issues in the OP. As for solutions, there
have been some suggestions in this thread, the simplest is to leave things as is and introduce the optimizer hint as a separate function, assume(). I don't think there was any argument presented against a separate function besides that Walter couldn't see any difference between the two behaviors, or the intention thing which doesn't really help us here.
An argument against the separate function: we already have a function, called assert. Those that want the nonoptimizing version (a disable-able 'if false throw' with no wider meaning) should get their own method darnit. I guess the only real argument against it is that pre-existing asserts
 contain significant optimization information that we can't afford to not
 reuse.
Yessss. This gets to the argument - asserts contain information about the program. Specifically, a statement about the valid program state at a given point. So we should treat them as such.
 But this is a claim I'm pretty skeptical of.
Ah man, thought I had you.
 Andrei admitted it's just a hunch at this point. Try looking through your
 code base to see how many asserts would be useful for optimizing.
Ironically, I don't tend to use asserts at all in my code. I do not want code that will throw or not throw based on a compiler flag. Why am I even arguing about this stuff? If asserts were used for optimizing, I would look at actually using them more. (Can we programmatically (sp?) identify and flag/resolve
 issues that occur from a mismatch of expectations?)
I'm not an expert on this, but my guess is it's possible in theory but would never happen in practice. Such things are very complex to implement, if Walter won't agree to a simple and easy solution, I'm pretty sure there's no way in hell he would agree to a complex one that takes a massive amount of effort.
If gcc et all do similar optimizations, how do they handle messaging?
Aug 06 2014
prev sibling parent "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 01:11:55 UTC, Jeremy Powers via 
Digitalmars-d wrote:
 That's in the past. This is all about the pros and cons of 
 changing it now
 and for the future.
The main argument seems to revolve around whether this is actually a change or not. In my (and others') view, the treatment of assert as 'assume' is not a change at all. It was in there all along, we just needed the wizard to tell us.
This is already the first misunderstanding: The argument is about whether it's a good idea, not whether it's newly introduced or has been the intended meaning since assert's conception.
 The below can safely be ignored, as I just continue the pedantic
 discussions....


 OK, but my point was you were using a different definition of 
 undefined
 behavior. We can't communicate if we aren't using the same 
 meanings of
 words.
Yes, very true. My definition of undefined in this case hinges on my definition of what assert means. If a failed assert means all code after it is invalid, then by definition (as I interpret the definition) that code is invalid and can be said to have undefined behaviour. That is, it makes sense to me that it is specified as undefined, by the spec that is incredibly unclear. I may be reading too much into it here, but this follows the strict definition of undefined - it is undefined because it is defined to be undefined. This is the 'because I said so' defense.
Of course you can define your own concept and call it "undefined", but I don't see how it matters. The concept described by the usual definition of "undefined" still exists, and it still has very different implications than your concept has. To give a more practical example: You're writing an authentication function. It takes a username and a password, and returns true or false, depending on whether the password is correct for this username. Unfortunately, the verification algorithm is wrong: due to an integer overflow in the hash calculation, it rejects some valid passwords, but never accepts invalid ones. The program is clearly incorrect, but its behaviour is still well-defined and predictable (overflow is not undefined in D). Now, if the flaw in the algorithm were due to an actual undefined operation, everything could happen, including the function accepting invalid passwords. I hope it's clear that this is a very different class of brokenness.
 My stance is that this new/old definition is a good thing, as 
 it matches
 how I thought things were already, and any code that surfaces 
 as broken
 because of it was already broken in my definition.  Therefore 
 this 'change'
 is good, does not introduce breaking changes, and arguments 
 about such
 should be redirected towards mitigation and fixing of 
 expectations.

 In an attempt to return this discussion to something useful, 
 question:

 If assert means what I think it means (and assuming we agree on 
 what the
 actual two interpretations are), how do we allay concerns about 
 it?  Is
 there anything fundamentally/irretrievably bad if we use this 
 new/old
 definition?  (Can we programmatically (sp?) identify and 
 flag/resolve
 issues that occur from a mismatch of expectations?)
My understanding (which is probably the same as that of most people participating in the discussion, because as I said above, I _don't_ think the argument is about a misunderstanding on this level): Walter's assert: * Expresses a statement that the programmer intends to be true. It is only checked in non-release mode. * The compiler can assume that it is true - even in release mode - because the programmer explicitly said so, and the compiler may not have figured it out by itself (similar to casts, which also express assumptions by the programmer that the compiler cannot know otherwise). * Asserting a condition that is false is undefined behaviour. The other assert: * Expresses a statement that the programmer intends to be true. It is only checked in non-release mode. * Because it is unlikely that the programmer has proved the correctness in the general case, the compiler must not assume it is true unless it can prove it to be, either at compile time, or with a runtime check. Release mode disables the runtime checks. * Asserting a condition that is false either raises an error at runtime, aborts compilation, or doesn't do anything. It never causes undefined behaviour by itself. As I already wrote elsewhere, an assert with the suggested/intended behaviour is a very dangerous tool that should not be used as widely as it is today. If the asserted condition is wrong (for whatever reason), it would create not just wrong behaviour, but undefined behaviour (as described above, not your concept). H.S. Teoh however suggested to extend compile time checking for assertions. I believe this is the way to go forward, and it has great potential. What I don't agree with, of course, is to just believe anything in the assertions to be true without verifying it.
Aug 06 2014
prev sibling parent reply Mike Parker <aldacron gmail.com> writes:
On 8/6/2014 8:18 AM, David Bregman wrote:

 This appears to be the root of the argument, and has been circled
 repeatedly... it's not my intent to restart another round of
 discussion on
 that well traveled ground, I just wanted to state my support for the
 definition as I understand it.
I disagree. I don't think the fact that some people already had the new definition in mind before is really all that relevant. That's in the past. This is all about the pros and cons of changing it now and for the future.
You keep going on the premise that your definition is the intended definition. I completely disagree. My understanding of assert has always been as Walter has described it. To me, *that* is the existing definition and yours is completely new. Nothing is being changed. He's just talking about starting to take advantage of it as he has always intended to. --- This email is free from viruses and malware because avast! Antivirus protection is active. http://www.avast.com
Aug 05 2014
next sibling parent "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 01:39:25 UTC, Mike Parker wrote:
 On 8/6/2014 8:18 AM, David Bregman wrote:

 This appears to be the root of the argument, and has been 
 circled
 repeatedly... it's not my intent to restart another round of
 discussion on
 that well traveled ground, I just wanted to state my support 
 for the
 definition as I understand it.
I disagree. I don't think the fact that some people already had the new definition in mind before is really all that relevant. That's in the past. This is all about the pros and cons of changing it now and for the future.
You keep going on the premise that your definition is the intended definition. I completely disagree. My understanding of assert has always been as Walter has described it. To me, *that* is the existing definition and yours is completely new. Nothing is being changed. He's just talking about starting to take advantage of it as he has always intended to.
No, intention is orthogonal to this. Again, this is all about the pros and cons of changing the *actual* semantics of assert.
Aug 05 2014
prev sibling parent reply "eles" <eles215 gzk.dot> writes:
On Wednesday, 6 August 2014 at 01:39:25 UTC, Mike Parker wrote:
 On 8/6/2014 8:18 AM, David Bregman wrote:
 You keep going on the premise that your definition is the 
 intended definition. I completely disagree. My understanding of 
 assert has always been as Walter has described it.
I did not use to think the same, but once Walter stated his vision of assert(), it was like a kind of revelation to me: why the optimizer won't make use of such obvious information like assert() provides just like asimple: if(x<5) { // you can safely optimize this code knowing (*assuming*) that always x<5 } But, what started to bother me lately and, I think, is the root of the problem: to have programmer code disabled by a compiler flag. I do not speak about boundschecking, where the code is never explicitely written by the programmer, but of real programmer code. Until now, versioning (or, in C/C++, the #ifdef) was the sole acceptable way to disable programmer code. The C assert slipped through as being based on a #ifdef or #if (I know good compilers will also optimize a if(0), but this is just because it happens to be obvious). OTOH, the D assert is no longer based (directly) on versioning, so having it disabled by a flag is not easily grasped. This, combined with the sudden revelation of the optimizer messing with it, produced a shock and this thread illustrates it. People are just to used to its secondary meaning from C, that is, besides testing conditions: "easily obtain a log of what and where was wrong". So, it was an assertion, but also a logging feature (albeit a fatal one). People got used with assert() becoming noop code in the release mode, just like they would disable the logs for release. The more I think about it, the more I feel like assert would be more naturally an annotation or a kind of versioning. Still, I cannot come with a clear cut proposition, as my mind is also entangled in old habits. One one hand, it feels natural as an instruction, on the other hand, being disable-able, maybe even ignorable (in release builds) and an invalidating point for the program logic*, it should belong somewhere else. *I think this is important: is not only a tested condition that is then handled, but a tested condition exposing a "does not work as intended". It looks more like a kind of "this code should be unreachable".
Aug 05 2014
parent "eles" <eles215 gzk.dot> writes:
On Wednesday, 6 August 2014 at 02:43:17 UTC, eles wrote:
 On Wednesday, 6 August 2014 at 01:39:25 UTC, Mike Parker wrote:
 On 8/6/2014 8:18 AM, David Bregman wrote:
 *I think this is important: is not only a tested condition that 
 is then handled, but a tested condition exposing a "does not 
 work as intended". It looks more like a kind of "this code 
 should be unreachable".
nitpicking: is not "my program does not behave like expected (for example, because the config file is broken)" but "my code wasn't supposed to say that and I did not mean to write such code"
Aug 05 2014
prev sibling parent "David Bregman" <drb sfu.ca> writes:
On Tuesday, 5 August 2014 at 18:19:00 UTC, Jeremy Powers via 
Digitalmars-d wrote:
 This has already been stated by others, but I just wanted to 
 pile on - I
 agree with Walter's definition of assert.

 2. Semantic change.
 The proposal changes the meaning of assert(), which will 
 result in
 breaking existing code.  Regardless of philosophizing about 
 whether or not
 the code was "already broken" according to some definition of 
 assert, the
 fact is that shipping programs that worked perfectly well 
 before may no
 longer work after this change.
Disagree. Assert (as I always understood it) means 'this must be true, or my program is broken.' In -release builds the explicit explosion on a triggered assert is skipped, but any code after a non-true assert is, by definition, broken. And by broken I mean the fundamental constraints of the program are violated, and so all bets are off on it working properly. A shipping program that 'worked perfectly well' but has unfulfilled asserts is broken - either the asserts are not actually true constraints, or the broken path just hasn't been hit yet.
This is the 'already broken' argument, which I mentioned in the quote above. This kind of change could never be made in C or C++, because there is too much legacy code that depends on it. Perhaps D can still afford to break this because it's still a young language. That is a strength of young languages. If you believe in this case that the upside justifies the breakage, by all means, just say so and accept the consequences. Don't try to escape responsibility by retroactively redefining previously working code as broken :)
 Looking at the 'breaking' example:

 assert(x!=1);
 if (x==1) {
  ...
 }

 If the if is optimized out, this will change from existing 
 behaviour.  But
 it is also obviously (to me at least) broken code already.  The 
 assert says
 that x cannot be 1 at this point in the program, if it ever is 
 then there
 is an error in the program.... and then it continues as if the 
 program were
 still valid.  If x could be one, then the assert is invalid 
 here.  And this
 code will already behave differently between -release and 
 non-release
 builds, which is another kind of broken.
Not everything that breaks will be so obvious as that. It can get much more hairy when assumptions propagate across multiple levels of inlining. Also, some code purposely uses that pattern. It is (or rather, was) valid for a different use case of assert.
 3a. An alternate statement of the proposal is literally "in 
 release mode,
 assert expressions introduce undefined behavior into your code 
 in if the
 expression is false".
This statement seems fundamentally true to me of asserts already, regardless of whether they are used for optimizations. If your assert fails, and you have turned off 'blow up on assert' then your program is in an undefined state. It is not that the assert introduces the undefined behaviour, it is that the assert makes plain an expectation of the code and if that expectation is false the code will have undefined behaviour.
This is not the standard definition of undefined behavior. With regular assert, execution is still well defined. If you want to know what happens in release mode when the assert condition is not satisfied, all you need to do is read the source code to find out. With assume, if the condition is not satisfied, there is no way to know what will happen. _anything_ can happen, it can even format your hard drive. That's true undefined behavior.
 3b. Since assert is such a widely used feature (with the 
 original
 semantics, "more asserts never hurt"), the proposal will 
 inject a massive
 amount of undefined behavior into existing code bases, greatly 
 increasing
 the probability of experiencing problems related to undefined 
 behavior.
I actually disagree with the 'more asserts never hurt' statement. Exactly because asserts get compiled out in release builds, I do not find them very useful/desirable. If they worked as optimization hints I might actually use them more. And there will be no injection of undefined behaviour - the undefined behaviour is already there if the asserted constraints are not valid.
This uses your own definition of UB again, it isn't true for the regular definition.
  Maybe if the yea side was consulted, they might easily agree 
 to an
 alternative way of achieving the improved optimization goal, 
 such as
 creating a new function that has the proposed semantics.
Prior to this (incredibly long) discussion, I was not aware people had a different interpretation of assert. To me, this 'new semantics' is precisely what I always thought assert was, and the proposal is just leveraging it for some additional optimizations. So from my standpoint, adding a new function would make sense to support this 'existing' behaviour that others seem to rely on - assert is fine as is, if the definition of 'is' is what I think it is.
That doesn't mean you don't have buggy asserts in your code, or buggy assers in libraries you use (or the standard library), so you are not immune from undefined behavior.
Aug 05 2014
prev sibling next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
(limited connectivity for me)

For some perspective, recently gcc and clang have introduced 
optimizations based on undefined behavior in C/C++. The undefined 
behavior has been interpreted by modern optimizers as "these cases will 
never happen". This has wound up breaking a significant amount of 
existing code. There have been a number of articles about these, with 
detailed explanations about how they come about and the new, more 
correct, way to write code.

The emerging consensus is that the code breakage is worth it for the 
performance gains. That said, I do hear what people are saying about 
potential code breakage and agree that we need to address this properly.
Aug 05 2014
next sibling parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Tue, Aug 05, 2014 at 11:35:14AM -0700, Walter Bright via Digitalmars-d wrote:
 (limited connectivity for me)
 
 For some perspective, recently gcc and clang have introduced
 optimizations based on undefined behavior in C/C++. The undefined
 behavior has been interpreted by modern optimizers as "these cases
 will never happen". This has wound up breaking a significant amount of
 existing code. There have been a number of articles about these, with
 detailed explanations about how they come about and the new, more
 correct, way to write code.
And I'd like to emphasize that code *should* have been written in this new, more correct way in the first place. Yes, it's a pain to have to update legacy code, but where would progress be if we're continually hampered by the fear of breaking what was *already* broken to begin with?
 The emerging consensus is that the code breakage is worth it for the
 performance gains. That said, I do hear what people are saying about
 potential code breakage and agree that we need to address this
 properly.
The way I see it, we need to educate D users to use 'assert' with the proper meaning, and to replace all other usages with alternatives (perhaps a Phobos function that does what they want without the full implications of assert -- i.e., "breaking" behaviour like influencing the optimizer, etc.). Once reasonable notice and time has been given, I'm all for introducing optimizer hinting with asserts. I think in the long run, this will turn out to be an important, revolutionary development not just in D, but in programming languages in general. T -- Ignorance is bliss... until you suffer the consequences!
Aug 05 2014
next sibling parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Tuesday, 5 August 2014 at 19:14:57 UTC, H. S. Teoh via 
Digitalmars-d wrote:
T

--
Ignorance is bliss... until you suffer the consequences!
(sic!)
Aug 05 2014
prev sibling parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/5/2014 12:13 PM, H. S. Teoh via Digitalmars-d wrote:
 The way I see it, we need to educate D users to use 'assert' with the
 proper meaning,
I agree. We're starting with improving the spec wording.
 I think in the
 long run, this will turn out to be an important, revolutionary
 development not just in D, but in programming languages in general.
I agree. It also opens the door for programmers providing simple, checkable hints to the optimizer. I don't know how far we can go with that, but I suspect significant opportunity.
Aug 05 2014
prev sibling parent "David Bregman" <drb sfu.ca> writes:
On Tuesday, 5 August 2014 at 18:35:32 UTC, Walter Bright wrote:
 (limited connectivity for me)

 For some perspective, recently gcc and clang have introduced 
 optimizations based on undefined behavior in C/C++. The 
 undefined behavior has been interpreted by modern optimizers as 
 "these cases will never happen". This has wound up breaking a 
 significant amount of existing code. There have been a number 
 of articles about these, with detailed explanations about how 
 they come about and the new, more correct, way to write code.

 The emerging consensus is that the code breakage is worth it 
 for the performance gains.

 That said, I do hear what people are saying about potential 
 code breakage and agree that we need to address this properly.
Well, then at least we agree there is some kind of tradeoff being made here if the definition of assert is changed: potential performance vs a bunch of negatives. In my estimation, the upside is small and the tradeoff is not close to being justified. If performance is a top goal, there are many other things that could be done which have lesser (or zero) downsides. Just to give one example, addition of a forceinline attribute would be of great assistance to those attempting to micro optimize their code. And of course, adding this as a new function instead of redefining an existing one would eliminate the code breakage and C compatibility issues. The undefined behavior issue would remain, but at least defining assume as system would alleviate the safe issue somewhat (there could still be leaks due to inlining), and make it more clear to users that it's a dangerous feature. It would also make it more searchable, for code auditing purposes. Anyways, if I have at least made you and others aware of all the downsides, and all the contradictions of this proposal with D's stated goals, then I guess I have done my part for this issue.
Aug 05 2014
prev sibling next sibling parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Tue, Aug 05, 2014 at 11:18:46AM -0700, Jeremy Powers via Digitalmars-d wrote:
 This has already been stated by others, but I just wanted to pile on -
 I agree with Walter's definition of assert.
 
 2. Semantic change.
 The proposal changes the meaning of assert(), which will result in
 breaking existing code.  Regardless of philosophizing about whether
 or not the code was "already broken" according to some definition of
 assert, the fact is that shipping programs that worked perfectly
 well before may no longer work after this change.
Disagree. Assert (as I always understood it) means 'this must be true, or my program is broken.' In -release builds the explicit explosion on a triggered assert is skipped, but any code after a non-true assert is, by definition, broken. And by broken I mean the fundamental constraints of the program are violated, and so all bets are off on it working properly. A shipping program that 'worked perfectly well' but has unfulfilled asserts is broken - either the asserts are not actually true constraints, or the broken path just hasn't been hit yet.
Exactly. I think part of the problem is that people have been using assert with the wrong meaning. In my mind, 'assert(x)' doesn't mean "abort if x is false in debug mode but silently ignore in release mode", as some people apparently think it means. To me, it means "at this point in the program, x is true". It's that simple. Now if it turns out that x actually *isn't* true, then you have a contradiction in your program logic, and therefore, by definition, your program is invalid, which means any subsequent behaviour is undefined. If you start with an axiomatic system where the axioms contain a contradiction, then any results you derive from the system will be meaningless, since a contradiction vacuously proves everything. Similarly, any program behaviour that follows a false assertion is undefined, because one of the "axioms" (i.e., assertions) introduces a contradiction to the program logic.
 Looking at the 'breaking' example:
 
 assert(x!=1);
 if (x==1) {
  ...
 }
 
 If the if is optimized out, this will change from existing behaviour.
 But it is also obviously (to me at least) broken code already.  The
 assert says that x cannot be 1 at this point in the program, if it
 ever is then there is an error in the program.... and then it
 continues as if the program were still valid.  If x could be one, then
 the assert is invalid here.  And this code will already behave
 differently between -release and non-release builds, which is another
 kind of broken.
Which is what Walter has been saying: the code is *already* broken, and is invalid by definition, so it makes no difference what the optimizer does or doesn't do. If your program has an array overrun bug that writes garbage to an unrelated variable, then you can't blame the optimizer for producing a program where the unrelated variable acquires a different garbage value from before. The optimizer only guarantees (in theory) consistent program behaviour if the program is valid to begin with. If the program is invalid, all bets are off as to what its "optimized" version does.
 3a. An alternate statement of the proposal is literally "in release
 mode, assert expressions introduce undefined behavior into your code
 in if the expression is false".
This statement seems fundamentally true to me of asserts already, regardless of whether they are used for optimizations. If your assert fails, and you have turned off 'blow up on assert' then your program is in an undefined state. It is not that the assert introduces the undefined behaviour, it is that the assert makes plain an expectation of the code and if that expectation is false the code will have undefined behaviour.
I agree.
 3b. Since assert is such a widely used feature (with the original
 semantics, "more asserts never hurt"), the proposal will inject a
 massive amount of undefined behavior into existing code bases,
 greatly increasing the probability of experiencing problems related
 to undefined behavior.
I actually disagree with the 'more asserts never hurt' statement. Exactly because asserts get compiled out in release builds, I do not find them very useful/desirable. If they worked as optimization hints I might actually use them more. And there will be no injection of undefined behaviour - the undefined behaviour is already there if the asserted constraints are not valid.
And if people are using asserts in ways that are different from what it's intended to be (expressions that must be true if the program logic has been correctly implemented), then their programs are already invalid by definition. Why should it be the compiler's responsibility to guarantee consistent behaviour of invalid code?
 Maybe if the yea side was consulted, they might easily agree to an
 alternative way of achieving the improved optimization goal, such as
 creating a new function that has the proposed semantics.
Prior to this (incredibly long) discussion, I was not aware people had a different interpretation of assert. To me, this 'new semantics' is precisely what I always thought assert was, and the proposal is just leveraging it for some additional optimizations. So from my standpoint, adding a new function would make sense to support this 'existing' behaviour that others seem to rely on - assert is fine as is, if the definition of 'is' is what I think it is.
Yes, the people using assert as a kind of "check in debug mode but ignore in release mode" should really be using something else instead, since that's not what assert means. I'm honestly astounded that people would actually use assert as some kind of non-release-mode-check instead of the statement of truth that it was meant to be. Furthermore, I think Walter's idea to use asserts as a source of optimizer hints is a very powerful concept that may turn out to be a revolutionary feature in D. It could very well develop into the answer to my long search for a way of declaring identities in user-defined types that allow high-level optimizations by the optimizer, thus allowing user-defined types to be on par with built-in types in optimizability. Currently, the compiler is able to optimize x+x+x+x into 4*x if x is an int, for example, but it can't if x is a user-defined type (e.g. BigInt), because it can't know if opBinary was defined in a way that obeys this identity. But if we can assert that this holds for the user-defined type, e.g., BigInt, then the compiler can make use of that axiom to perform such an optimization. This would then allow code to be written in more human-readable forms, and still maintain optimal performance, even where user-defined types are involved. While manually-written code generally doesn't need this kind of optimization (instead of writing x+x+x+x, just write 4*x to begin with), this becomes an important issue with generic code and metaprogramming. The generic version of the code may very well be w+x+y+z, which cannot be reduced to n*x, so when you instantiate that code for the case where w==x==y==z, you have to pay the penalty of genericity. But we can eliminate this cost if we can tell the compiler that when w==x==y==z, then w+x+y+z == 4*x. Then we don't have to separately implement this special case in order to achieve optimal performance, but we will be able to continue using the generic, more maintainable code. Something like this will require much more development of Walter's core concept than currently proposed, of course, but the current proposal is an important step in this direction, and I fully support it. T -- There are 10 kinds of people in the world: those who can count in binary, and those who can't.
Aug 05 2014
next sibling parent reply "Araq" <rumpf_a web.de> writes:
 Furthermore, I think Walter's idea to use asserts as a source of
 optimizer hints is a very powerful concept that may turn out to 
 be a
 revolutionary feature in D. It could very well develop into the 
 answer
 to my long search for a way of declaring identities in 
 user-defined
 types that allow high-level optimizations by the optimizer, thus
 allowing user-defined types to be on par with built-in types in
 optimizability.
The answer to your search is "term rewriting macros (with sideeffect and alias analysis)" as introduced by Nimrod. Watch my talk. ;-) 'assume' is not nearly powerful enough for this and in no way "revolutionary".
Aug 05 2014
parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/5/2014 12:25 PM, Araq wrote:
 'assume' is not nearly powerful enough for this and in no way "revolutionary".
More in the near-term realm of possibility are asserts that constrain the range of values for a variable, which can subsequently eliminate the extra code needed to handle the full range of the type. One case is the one that started off this whole discussion - constraining the range of values so that an overflow-checking-multiply need not actually check the overflow, because an overflow might be impossible. This kind of situation can come up in generic code, where the generic code is written conservatively and defensively, then relying on the caller to provide a few asserts which will in effect "customize" the generic code. What's exciting about this is it'll give us a lever we can use to generate better code than other languages are capable of.
Aug 05 2014
prev sibling next sibling parent reply Ary Borenszweig <ary esperanto.org.ar> writes:
On 8/5/14, 3:55 PM, H. S. Teoh via Digitalmars-d wrote:
 On Tue, Aug 05, 2014 at 11:18:46AM -0700, Jeremy Powers via Digitalmars-d
wrote:
 Furthermore, I think Walter's idea to use asserts as a source of
 optimizer hints is a very powerful concept that may turn out to be a
 revolutionary feature in D.
LLVM already has it. It's not revolutionary: http://llvm.org/docs/LangRef.html#llvm-assume-intrinsic By the way, I think Walter said "assert can be potentially used to make optimizations" not "Oh, I just had an idea! We could use assert to optimize code". I think the code already does this. Of course, we would have to look at the source code to find out... By the way, most of the time in this list I hear "We could use this and that feature to allow better optimizations" and no optimizations are ever implemented. Look at all those pure nosafe nothrow const that you have to put and yet you don't get any performance boost from that.
Aug 05 2014
next sibling parent "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Tuesday, 5 August 2014 at 20:09:44 UTC, Ary Borenszweig wrote:
 By the way, most of the time in this list I hear "We could use 
 this and that feature to allow better optimizations" and no 
 optimizations are ever implemented. Look at all those  pure 
 nosafe nothrow const that you have to put and yet you don't get 
 any performance boost from that.
Hmm... I've never seen these annotations as a performance feature. They're there to help writing correct programs. If this allows some performance gains, great, but IMHO it's not their primary purpose.
Aug 05 2014
prev sibling next sibling parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Tue, Aug 05, 2014 at 05:09:43PM -0300, Ary Borenszweig via Digitalmars-d
wrote:
 On 8/5/14, 3:55 PM, H. S. Teoh via Digitalmars-d wrote:
On Tue, Aug 05, 2014 at 11:18:46AM -0700, Jeremy Powers via Digitalmars-d wrote:
Furthermore, I think Walter's idea to use asserts as a source of
optimizer hints is a very powerful concept that may turn out to be a
revolutionary feature in D.
LLVM already has it. It's not revolutionary: http://llvm.org/docs/LangRef.html#llvm-assume-intrinsic
Even better, so there's precedent for this. Even if it's only exposed at the LLVM level, rather than the source language. Introducing this at the source language level (like proposed in D) is a good step forward IMO.
 By the way, I think Walter said "assert can be potentially used to
 make optimizations" not "Oh, I just had an idea! We could use assert
 to optimize code". I think the code already does this. Of course, we
 would have to look at the source code to find out...
If the code already does this, then what are we arguing about?
 By the way, most of the time in this list I hear "We could use this
 and that feature to allow better optimizations" and no optimizations
 are ever implemented. Look at all those  pure nosafe nothrow const
 that you have to put and yet you don't get any performance boost from
 that.
Automatic attribute inference is the way to go. More and more, I'm beginning to be convinced that manually-specified attributes are a dead end. Having said that, though, I'm pretty sure the compiler could (and should) do more with pure/nothrow/const, etc.. I think it may already be taking advantage of nothrow/const (nothrow elides throw/catch scaffolding, e.g., which could be important in high-performance inner loops). With pure the current situation could be improved, since it currently only has effect when you call the same pure function multiple times within a single expression. But there are lots more things that could be done with it, e.g., memoization across different statements in the function body. PR's would be welcome. ;-) T -- What do you mean the Internet isn't filled with subliminal messages? What about all those buttons marked "submit"??
Aug 05 2014
parent Ary Borenszweig <ary esperanto.org.ar> writes:
On 8/5/14, 5:26 PM, H. S. Teoh via Digitalmars-d wrote:
 On Tue, Aug 05, 2014 at 05:09:43PM -0300, Ary Borenszweig via Digitalmars-d
wrote:
 On 8/5/14, 3:55 PM, H. S. Teoh via Digitalmars-d wrote:
 On Tue, Aug 05, 2014 at 11:18:46AM -0700, Jeremy Powers via Digitalmars-d
wrote:
 Furthermore, I think Walter's idea to use asserts as a source of
 optimizer hints is a very powerful concept that may turn out to be a
 revolutionary feature in D.
LLVM already has it. It's not revolutionary: http://llvm.org/docs/LangRef.html#llvm-assume-intrinsic
Even better, so there's precedent for this. Even if it's only exposed at the LLVM level, rather than the source language. Introducing this at the source language level (like proposed in D) is a good step forward IMO.
 By the way, I think Walter said "assert can be potentially used to
 make optimizations" not "Oh, I just had an idea! We could use assert
 to optimize code". I think the code already does this. Of course, we
 would have to look at the source code to find out...
If the code already does this, then what are we arguing about?
Exactly. I think the OP doesn't know that Walter wasn't proposing any semantic change in assert. Walter was just stating how assert works for him (or should work, but probably some optimizations are not implemented). We should ask Walter, but I think he's offline...
Aug 05 2014
prev sibling parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/5/2014 1:09 PM, Ary Borenszweig wrote:
 On 8/5/14, 3:55 PM, H. S. Teoh via Digitalmars-d wrote:
 On Tue, Aug 05, 2014 at 11:18:46AM -0700, Jeremy Powers via Digitalmars-d
wrote:
 Furthermore, I think Walter's idea to use asserts as a source of
 optimizer hints is a very powerful concept that may turn out to be a
 revolutionary feature in D.
LLVM already has it. It's not revolutionary: http://llvm.org/docs/LangRef.html#llvm-assume-intrinsic
That's a language extension. A language extension is not a language feature. But it is strong evidence supporting my assertion that these sorts of things are inexorably coming. As bearophile posted, Microsoft also has such an intrinsic for their C++.
 By the way, I think Walter said "assert can be potentially used to make
 optimizations" not "Oh, I just had an idea! We could use assert to optimize
 code". I think the code already does this. Of course, we would have to look at
 the source code to find out...
It is hardly a new idea, or my idea. I got it from this 1981 book: http://www.amazon.com/Program-Flow-Analysis-Application-Prentice-Hall/dp/0137296819/ which I've had a copy of since '82 or so. My notions on asserts being contracts, regardless of switch settings, date to a similar time, see "Object Oriented Software Construction", a 1985 book.
 By the way, most of the time in this list I hear "We could use this and that
 feature to allow better optimizations" and no optimizations are ever
 implemented. Look at all those  pure nosafe nothrow const that you have to put
 and yet you don't get any performance boost from that.
Not only is that currently quite incorrect, don't put the chicken before the egg. The 'nothrow', etc., feature must exist before it can be taken advantage of.
Aug 05 2014
prev sibling parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Tuesday, 5 August 2014 at 18:57:40 UTC, H. S. Teoh via 
Digitalmars-d wrote:
 Exactly. I think part of the problem is that people have been 
 using
 assert with the wrong meaning. In my mind, 'assert(x)' doesn't 
 mean
 "abort if x is false in debug mode but silently ignore in 
 release mode",
 as some people apparently think it means. To me, it means "at 
 this point
 in the program, x is true".  It's that simple.
A language construct with such a meaning is useless as a safety feature. If I first have to prove that the condition is true before I can safely use an assert, I don't need the assert anymore, because I've already proved it. If it is intended to be an optimization hint, it should be implemented as a pragma, not as a prominent feature meant to be widely used. (But I see that you have a different use case, see my comment below.)
 The optimizer only guarantees (in theory)
 consistent program behaviour if the program is valid to begin 
 with. If
 the program is invalid, all bets are off as to what its 
 "optimized"
 version does.
There is a difference between invalid and undefined: A program is invalid ("buggy"), if it doesn't do what it's programmer intended, while "undefined" is a matter of the language specification. The (wrong) behaviour of an invalid program need not be undefined, and often isn't in practice. An optimizer may only transform code in a way that keeps the resulting code semantically equivalent. This means that if the original "unoptimized" program is well-defined, the optimized one will be too.
 Yes, the people using assert as a kind of "check in debug mode 
 but
 ignore in release mode" should really be using something else 
 instead,
 since that's not what assert means. I'm honestly astounded that 
 people
 would actually use assert as some kind of 
 non-release-mode-check instead
 of the statement of truth that it was meant to be.
Well, when this "something else" is introduced, it will need to replace almost every existing instance of "assert", as the latter must only be used if it is proven that the condition is always true. To name just one example, it cannot be used in range `front` and `popFront` methods to assert that the range is not empty, unless there is an additional non-assert check directly before it.
 Furthermore, I think Walter's idea to use asserts as a source of
 optimizer hints is a very powerful concept that may turn out to 
 be a
 revolutionary feature in D. It could very well develop into the 
 answer
 to my long search for a way of declaring identities in 
 user-defined
 types that allow high-level optimizations by the optimizer, thus
 allowing user-defined types to be on par with built-in types in
 optimizability. Currently, the compiler is able to optimize 
 x+x+x+x into
 4*x if x is an int, for example, but it can't if x is a 
 user-defined
 type (e.g. BigInt), because it can't know if opBinary was 
 defined in a
 way that obeys this identity. But if we can assert that this 
 holds for
 the user-defined type, e.g., BigInt, then the compiler can make 
 use of
 that axiom to perform such an optimization.  This would then 
 allow code
 to be written in more human-readable forms, and still maintain 
 optimal
 performance, even where user-defined types are involved.
This is a very powerful feature indeed, but to be used safely, the compiler needs to be able to detect invalid uses reliably at compile time. This is currently not the case: void onlyOddNumbersPlease(int n) { assert(n % 2); } void foo() { onlyOddNumbersPlease(42); // shouldn't compile, but does } It would be great if this were possible. In the example of `front` and `popFront`, programs that call these methods on a range that could theoretically be empty wouldn't compile. This might be useful for optimization, but above that it's useful for verifying correctness. Unfortunately this is not what has been suggested (and was evidently intended from the beginning)...
Aug 05 2014
parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Tue, Aug 05, 2014 at 08:11:16PM +0000, via Digitalmars-d wrote:
 On Tuesday, 5 August 2014 at 18:57:40 UTC, H. S. Teoh via Digitalmars-d
 wrote:
Exactly. I think part of the problem is that people have been using
assert with the wrong meaning. In my mind, 'assert(x)' doesn't mean
"abort if x is false in debug mode but silently ignore in release
mode", as some people apparently think it means. To me, it means "at
this point in the program, x is true".  It's that simple.
A language construct with such a meaning is useless as a safety feature.
I don't see it as a safety feature at all.
 If I first have to prove that the condition is true before I can
 safely use an assert, I don't need the assert anymore, because I've
 already proved it.
I see it as future proofing: I may have proven the condition for *this* version of the program, but all software will change (unless it's dead), and change means the original proof may no longer be valid, but this part of the code is still written under the assumption that the condition holds. In most cases, it *does* still hold, so in general you're OK, but sometimes a change invalidates an axiom that, in consequence, invalidates the assertion. Then the assertion will trip (in non-release mode, of course), telling me that my program logic has become invalid due to the change I made. So I'll have to fix the problem so that the condition holds again.
 If it is intended to be an optimization hint, it should be implemented
 as a pragma, not as a prominent feature meant to be widely used. (But
 I see that you have a different use case, see my comment below.)
And here is the beauty of the idea: rather than polluting my code with optimization hints, which are out-of-band (and which are generally unverified and may be outright wrong after the code undergoes several revisions), I am stating *facts* about my program logic that must hold -- which therefore fits in very logically with the code itself. It even self-documents the code, to some extent. Then as an added benefit, the compiler is able to use these facts to emit more efficient code. So to me, it *should* be a prominent, widely-used feature. I would use it, and use it a *lot*.
The optimizer only guarantees (in theory) consistent program
behaviour if the program is valid to begin with. If the program is
invalid, all bets are off as to what its "optimized" version does.
There is a difference between invalid and undefined: A program is invalid ("buggy"), if it doesn't do what it's programmer intended, while "undefined" is a matter of the language specification. The (wrong) behaviour of an invalid program need not be undefined, and often isn't in practice.
To me, this distinction doesn't matter in practice, because in practice, an invalid program produces a wrong result, and a program with undefined behaviour also produces a wrong result. I don't care what kind of wrong result it is; what I care is to fix the program to *not* produce a wrong result.
 An optimizer may only transform code in a way that keeps the resulting
 code semantically equivalent. This means that if the original
 "unoptimized" program is well-defined, the optimized one will be too.
That's a nice property to have, but again, if my program produces a wrong result, then my program produces a wrong result. As a language user, I don't care that the optimizer may change one wrong result to a different wrong result. What I care about is to fix the code so that the program produces the *correct* result. To me, it only matters that the optimizer does the Right Thing when the program is correct to begin with. If the program was wrong, then it doesn't matter if the optimizer makes it a different kind of wrong; the program should be fixed so that it stops being wrong.
Yes, the people using assert as a kind of "check in debug mode but
ignore in release mode" should really be using something else
instead, since that's not what assert means. I'm honestly astounded
that people would actually use assert as some kind of
non-release-mode-check instead of the statement of truth that it was
meant to be.
Well, when this "something else" is introduced, it will need to replace almost every existing instance of "assert", as the latter must only be used if it is proven that the condition is always true. To name just one example, it cannot be used in range `front` and `popFront` methods to assert that the range is not empty, unless there is an additional non-assert check directly before it.
I don't follow this reasoning. For .front and .popFront to assert that the range is non-empty, simply means that user code that attempts to do otherwise is wrong by definition, and must be fixed. I don't care if it's wrong as in invalid, or wrong as in undefined, the bottom line is that code that calls .front or .popFront on an empty range is incorrectly written, and therefore must be fixed. If I were to implement ranges in assembly language, for example, I would not write .front or .popFront to check for emptiness before performing operations, because that introduces needless overhead in correct programs. In incorrect programs, it will crash (horribly), but that's just the consequence of the program being incorrect. Adding a check for emptiness does not help fix incorrectness -- you will still get a wrong result. The only difference is an exception instead of a crash -- nicer, I'll concede, but either way, you're not getting the correct result. Now, during development, I might add emptiness checks to my assembly language range program for the purpose of locating incorrectly-written parts of the program. But before I ship the product, I'd better make darned sure that I've eliminated every bug that I can find, and convinced myself that the program will operate correctly. If I can't even convince myself that the program is correct, I have no business shipping it to customers. But if I've convinced myself that it is correct, then I might as well disable the emptiness checks so that my product will deliver top performance -- since that wouldn't be a problem in a correct program.
Furthermore, I think Walter's idea to use asserts as a source of
optimizer hints is a very powerful concept that may turn out to be a
revolutionary feature in D. It could very well develop into the
answer to my long search for a way of declaring identities in
user-defined types that allow high-level optimizations by the
optimizer, thus allowing user-defined types to be on par with
built-in types in optimizability. Currently, the compiler is able to
optimize x+x+x+x into 4*x if x is an int, for example, but it can't
if x is a user-defined type (e.g. BigInt), because it can't know if
opBinary was defined in a way that obeys this identity. But if we can
assert that this holds for the user-defined type, e.g., BigInt, then
the compiler can make use of that axiom to perform such an
optimization.  This would then allow code to be written in more
human-readable forms, and still maintain optimal performance, even
where user-defined types are involved.
This is a very powerful feature indeed, but to be used safely, the compiler needs to be able to detect invalid uses reliably at compile time. This is currently not the case: void onlyOddNumbersPlease(int n) { assert(n % 2); } void foo() { onlyOddNumbersPlease(42); // shouldn't compile, but does }
In theory, the optimizer could use CTFE to reduce the function call, and thereby discover that the code is invalid. We don't have that today, but conceivably, we can achieve that one day. But taking a step back, there's only so much the compiler can do at compile-time. You can't stop *every* unsafe usage of something without also making it useless. While the manufacturer of a sharp cutting tool will presumably do their best to ensure the tool is safe to use, it's impossible to prevent *every* possible unsafe usage of said tool. If the user points the chainsaw to his foot, he will lose his foot, and there's nothing the manufacturer can do to prevent this except shipping a non-functional chainsaw. If the user insists on asserting things that are untrue, there will always be a way to bypass the compiler's static checks and end up with undefined behaviour at runtime.
 It would be great if this were possible. In the example of `front` and
 `popFront`, programs that call these methods on a range that could
 theoretically be empty wouldn't compile. This might be useful for
 optimization, but above that it's useful for verifying correctness.
A sufficiently-aggressive optimizer might be able to verify this at compile-time by static analysis. But even that has its limits... for example: MyRange range; assert(range.empty); if (solveRiemannHypothesis()) // <-- don't know if this is true range.addElements(...); range.popFront(); // <-- should this compile or not?
 Unfortunately this is not what has been suggested (and was evidently
 intended from the beginning)...
I don't think static analysis is *excluded* by the current proposal. I can see it as a possible future enhancement. But the fact that we don't have it today doesn't mean we shouldn't step in that direction. T -- I've been around long enough to have seen an endless parade of magic new techniques du jour, most of which purport to remove the necessity of thought about your programming problem. In the end they wind up contributing one or two pieces to the collective wisdom, and fade away in the rearview mirror. -- Walter Bright
Aug 05 2014
parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Tuesday, 5 August 2014 at 21:17:14 UTC, H. S. Teoh via 
Digitalmars-d wrote:
 On Tue, Aug 05, 2014 at 08:11:16PM +0000, via Digitalmars-d 
 wrote:
 On Tuesday, 5 August 2014 at 18:57:40 UTC, H. S. Teoh via 
 Digitalmars-d
 wrote:
Exactly. I think part of the problem is that people have been 
using
assert with the wrong meaning. In my mind, 'assert(x)' 
doesn't mean
"abort if x is false in debug mode but silently ignore in 
release
mode", as some people apparently think it means. To me, it 
means "at
this point in the program, x is true".  It's that simple.
A language construct with such a meaning is useless as a safety feature.
I don't see it as a safety feature at all.
Sorry, I should have written "correctness feature". I agree that it's not very useful for safety per se. (But of course, safety and correctness are not unrelated.)
 If I first have to prove that the condition is true before I 
 can
 safely use an assert, I don't need the assert anymore, because 
 I've
 already proved it.
I see it as future proofing: I may have proven the condition for *this* version of the program, but all software will change (unless it's dead), and change means the original proof may no longer be valid, but this part of the code is still written under the assumption that the condition holds. In most cases, it *does* still hold, so in general you're OK, but sometimes a change invalidates an axiom that, in consequence, invalidates the assertion. Then the assertion will trip (in non-release mode, of course), telling me that my program logic has become invalid due to the change I made. So I'll have to fix the problem so that the condition holds again.
Well, I think it's unlikely that you actually did prove the assert condition, except in trivial situations. This is related to the discussion about the ranges example, so I'll respond there.
 If it is intended to be an optimization hint, it should be 
 implemented
 as a pragma, not as a prominent feature meant to be widely 
 used. (But
 I see that you have a different use case, see my comment 
 below.)
And here is the beauty of the idea: rather than polluting my code with optimization hints, which are out-of-band (and which are generally unverified and may be outright wrong after the code undergoes several revisions), I am stating *facts* about my program logic that must hold -- which therefore fits in very logically with the code itself. It even self-documents the code, to some extent. Then as an added benefit, the compiler is able to use these facts to emit more efficient code. So to me, it *should* be a prominent, widely-used feature. I would use it, and use it a *lot*.
I think this is where we disagree mainly: What you call facts is something I see as intentions that *should* be true, but are not *proven* to be so. Again, see below.
 
The optimizer only guarantees (in theory) consistent program
behaviour if the program is valid to begin with. If the 
program is
invalid, all bets are off as to what its "optimized" version 
does.
There is a difference between invalid and undefined: A program is invalid ("buggy"), if it doesn't do what it's programmer intended, while "undefined" is a matter of the language specification. The (wrong) behaviour of an invalid program need not be undefined, and often isn't in practice.
To me, this distinction doesn't matter in practice, because in practice, an invalid program produces a wrong result, and a program with undefined behaviour also produces a wrong result. I don't care what kind of wrong result it is; what I care is to fix the program to *not* produce a wrong result.
Please see my response to Jeremy; the distinction is important: http://forum.dlang.org/thread/hqxoldeyugkazolllsna forum.dlang.org?page=11#post-eqlyruvwmzbpemvnrebw:40forum.dlang.org
 An optimizer may only transform code in a way that keeps the 
 resulting
 code semantically equivalent. This means that if the original
 "unoptimized" program is well-defined, the optimized one will 
 be too.
That's a nice property to have, but again, if my program produces a wrong result, then my program produces a wrong result. As a language user, I don't care that the optimizer may change one wrong result to a different wrong result. What I care about is to fix the code so that the program produces the *correct* result. To me, it only matters that the optimizer does the Right Thing when the program is correct to begin with. If the program was wrong, then it doesn't matter if the optimizer makes it a different kind of wrong; the program should be fixed so that it stops being wrong.
We're not living in an ideal world, unfortunately. It is bad enough that programs are wrong as they are written, we don't need the compiler to transform these programs to do something that is still wrong, but also completely different. This would make your goal of fixing the program very hard to achieve. In an extreme case, a small error in several million lines of code could manifest at a completely different place, because you cannot rely on any determinism once undefined behaviour is involved.
Yes, the people using assert as a kind of "check in debug 
mode but
ignore in release mode" should really be using something else
instead, since that's not what assert means. I'm honestly 
astounded
that people would actually use assert as some kind of
non-release-mode-check instead of the statement of truth that 
it was
meant to be.
Well, when this "something else" is introduced, it will need to replace almost every existing instance of "assert", as the latter must only be used if it is proven that the condition is always true. To name just one example, it cannot be used in range `front` and `popFront` methods to assert that the range is not empty, unless there is an additional non-assert check directly before it.
I don't follow this reasoning. For .front and .popFront to assert that the range is non-empty, simply means that user code that attempts to do otherwise is wrong by definition, and must be fixed. I don't care if it's wrong as in invalid, or wrong as in undefined, the bottom line is that code that calls .front or .popFront on an empty range is incorrectly written, and therefore must be fixed.
Just above you wrote that you "may have proven the condition". But in code like the following, there cannot be a proof: property T front() { assert(!empty); return _other_range.front; } This is in the standard library. The authors of this piece of code cannot have proven that the user of the library only calls `front` on a non-empty range. Now consider the following example (mostly made up, but not unrealistic) that parses a text file (this could be a simple text-based data format): // ... // some processing // ... input.popFront(); // end of line? => swallow and process next line if(input.front == '\n') { // <- this is wrong input.popFront(); continue; } // ... // more code that doesn't call `input.popFront` // ... // more processing of input if(!input.empty) { // <- HERE // use input.front } With the above definition of `front`, the second check marked "HERE" can be removed by the compiler. Even worse, if you insert `writeln(input.empty)` before the check for debugging, it might also output "false" (depending on how far the compiler goes). Yes, this code is wrong. But it's an easy mistake to make, it might not be detected during testing because you only use correctly formatted input files, and it might also not lead to crashes (the buffer is unlikely to end at a boundary to unmapped memory). Now the assert - which is supposed to be helping the programmer write correct code - has made it _harder_ to detect the cause of an error. What's worse is that it also removed a check that was necessary. This check could have been inserted by the programmer because the section of the code is security relevant, and they didn't want to rely on the input file to be correct. The compiler has thereby turned a rather harmless mistake that would under normal circumstances only lead to an incorrect output into a potentially exploitable security bug.
 -- snip --
 But if I've convinced myself that it is
 correct, then I might as well disable the emptiness checks so 
 that my
 product will deliver top performance -- since that wouldn't be 
 a problem
 in a correct program.
The problem is, as I explained above, that it doesn't just disable the emptiness checks where the asserts are. A simple mistake can have subtle and hard to debug effects all over your program.
 In theory, the optimizer could use CTFE to reduce the function 
 call, and
 thereby discover that the code is invalid. We don't have that 
 today, but
 conceivably, we can achieve that one day.

 But taking a step back, there's only so much the compiler can 
 do at
 compile-time. You can't stop *every* unsafe usage of something 
 without
 also making it useless. While the manufacturer of a sharp 
 cutting tool
 will presumably do their best to ensure the tool is safe to 
 use, it's
 impossible to prevent *every* possible unsafe usage of said 
 tool. If the
 user points the chainsaw to his foot, he will lose his foot, 
 and there's
 nothing the manufacturer can do to prevent this except shipping 
 a
 non-functional chainsaw. If the user insists on asserting 
 things that
 are untrue, there will always be a way to bypass the compiler's 
 static
 checks and end up with undefined behaviour at runtime.
I wouldn't be so pessimistic ;-) I guess most assert conditions are simple, mostly just comparisons or equality checks of one value with a constant. This should be relatively easy to verify with some control/data flow analysis (which Walter avoided until now, understandably). But CTFE is on the wrong level. It could only detect some of the failed conditions. It needs to be checked on a higher lever, as real correctness proofs. If an assert conditions cannot be proved - because it's always wrong, or just sometimes, or because the knowledge available to the compiler is not enough - it must be rejected. Think of it like an extension of type and const checking.
 It would be great if this were possible. In the example of 
 `front` and
 `popFront`, programs that call these methods on a range that 
 could
 theoretically be empty wouldn't compile. This might be useful 
 for
 optimization, but above that it's useful for verifying 
 correctness.
A sufficiently-aggressive optimizer might be able to verify this at compile-time by static analysis. But even that has its limits... for example: MyRange range; assert(range.empty); if (solveRiemannHypothesis()) // <-- don't know if this is true range.addElements(...); range.popFront(); // <-- should this compile or not?
It shouldn't, because it's not provable. However, most asserts are far less involved. There could be a specification of what is guaranteed to work, and what all compilers must therefore support.
 Unfortunately this is not what has been suggested (and was 
 evidently
 intended from the beginning)...
I don't think static analysis is *excluded* by the current proposal. I can see it as a possible future enhancement. But the fact that we don't have it today doesn't mean we shouldn't step in that direction.
I just don't see how we're stepping into that direction at all. It seems like the opposite: instead of trying to prove the assertions statically, they're going to be believed without verification.
Aug 06 2014
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/6/2014 5:14 AM, "Marc Schütz" <schuetzm gmx.net>" wrote:
 We're not living in an ideal world, unfortunately. It is bad enough that
 programs are wrong as they are written, we don't need the compiler to transform
 these programs to do something that is still wrong, but also completely
 different. This would make your goal of fixing the program very hard to
achieve.
 In an extreme case, a small error in several million lines of code could
 manifest at a completely different place, because you cannot rely on any
 determinism once undefined behaviour is involved.
You are technically correct, and I used to worry about that. But after using assert()s for 30 years, I can only think of this happening once. assert()s tend to trip very shortly after the actual error occurred. Of course, there's a bit of an art to appropriate placement of those assert()s.
 It seems like
 the opposite: instead of trying to prove the assertions statically, they're
 going to be believed without verification.
The point of an assert is it is something the programmer says must be true, not the compiler.
Aug 06 2014
parent "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 22:31:00 UTC, Walter Bright wrote:
 On 8/6/2014 5:14 AM, "Marc Schütz" <schuetzm gmx.net>" wrote:
 We're not living in an ideal world, unfortunately. It is bad 
 enough that
 programs are wrong as they are written, we don't need the 
 compiler to transform
 these programs to do something that is still wrong, but also 
 completely
 different. This would make your goal of fixing the program 
 very hard to achieve.
 In an extreme case, a small error in several million lines of 
 code could
 manifest at a completely different place, because you cannot 
 rely on any
 determinism once undefined behaviour is involved.
You are technically correct, and I used to worry about that. But after using assert()s for 30 years, I can only think of this happening once. assert()s tend to trip very shortly after the actual error occurred. Of course, there's a bit of an art to appropriate placement of those assert()s.
But for those 30 years you only used asserts with the semantics they have in C, not with the semantics you want for D. I don't see how you can come to the conclusion that the same is true for the "new style" assertions. The problems with finding errors that I talk about are not because the cause of the error is far from the assert. They stem from the fact that - with the proposed semantics - the asserts themselves can influence code in different parts of the program, far away from both the cause of the error and the failed assert.
Aug 07 2014
prev sibling parent reply "Sean Kelly" <sean invisibleduck.org> writes:
So from a functional perspective, assuming this is a 
multithreaded app, what should the procedure be when an 
AssertError is thrown in some thread?
Aug 06 2014
next sibling parent reply "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 17:18:19 UTC, Sean Kelly wrote:
 So from a functional perspective, assuming this is a 
 multithreaded app, what should the procedure be when an 
 AssertError is thrown in some thread?
afaik, AssertError works the same as any other exception. If it reaches the top without being handled, then the entire app will be terminated including all the other threads.
Aug 06 2014
parent reply "Sean Kelly" <sean invisibleduck.org> writes:
On Wednesday, 6 August 2014 at 18:15:41 UTC, David Bregman wrote:
 On Wednesday, 6 August 2014 at 17:18:19 UTC, Sean Kelly wrote:
 So from a functional perspective, assuming this is a 
 multithreaded app, what should the procedure be when an 
 AssertError is thrown in some thread?
afaik, AssertError works the same as any other exception. If it reaches the top without being handled, then the entire app will be terminated including all the other threads.
Except that's not really how unhandled exceptions are treated in threads. They're stored by the thread and (optionally) re-thrown in the context of whatever thread calls join, if any thread calls join at all. The assumption at the time was that the joining thread cared about the state of the thread being joined and so re-throwing the exception was a way to communicate the error to the most interested party. So if the main thread joins a thread that terminated with an unhandled AssertError, the error will be re-thrown in the context of the main thread, which will in turn join all remaining running threads and wait for them to complete. This is the same behavior as if an AssertError is generated during normal processing of the main thread. But in neither case is the application forcibly terminated when an assertion failure occurs. So again, my question is twofold: what *should* happen, given this new treatment for assertions, and then *how* will we accomplish this? A multithreaded process is really pretty much equivalent to a bunch of standalone processes with shared memory. There is no facility for forcing a clean termination of another thread. The best I can think of would be to assume that std.concurrency is being used for multithreading and sort things out similar to the existing LinkTerminated signaling, but looking for a reasonable solution within Druntime would be tricky.
Aug 06 2014
next sibling parent reply "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 19:34:48 UTC, Sean Kelly wrote:
 On Wednesday, 6 August 2014 at 18:15:41 UTC, David Bregman 
 wrote:
 On Wednesday, 6 August 2014 at 17:18:19 UTC, Sean Kelly wrote:
 So from a functional perspective, assuming this is a 
 multithreaded app, what should the procedure be when an 
 AssertError is thrown in some thread?
afaik, AssertError works the same as any other exception. If it reaches the top without being handled, then the entire app will be terminated including all the other threads.
Except that's not really how unhandled exceptions are treated in threads. They're stored by the thread and (optionally) re-thrown in the context of whatever thread calls join, if any thread calls join at all. The assumption at the time was that the joining thread cared about the state of the thread being joined and so re-throwing the exception was a way to communicate the error to the most interested party. So if the main thread joins a thread that terminated with an unhandled AssertError, the error will be re-thrown in the context of the main thread, which will in turn join all remaining running threads and wait for them to complete. This is the same behavior as if an AssertError is generated during normal processing of the main thread. But in neither case is the application forcibly terminated when an assertion failure occurs.
Ah, I see. Then I apologize for giving incorrect information. I am not that familiar with threads in D yet and I assumed unhandled exceptions worked like C++. But if you already knew the answer then why were you asking?
 So again, my question is twofold: what *should* happen, given 
 this new treatment for assertions, and then *how* will we 
 accomplish this?  A multithreaded process is really pretty much 
 equivalent to a bunch of standalone processes with shared 
 memory.
  There is no facility for forcing a clean termination of 
 another thread.  The best I can think of would be to assume 
 that std.concurrency is being used for multithreading and sort 
 things out similar to the existing LinkTerminated signaling, 
 but looking for a reasonable solution within Druntime would be 
 tricky.
I think there is some kind of misunderstanding here, I have not proposed any new treatment for assertions. Walter's proposal only affects release mode, so it's not related to exceptions.
Aug 06 2014
parent reply "Sean Kelly" <sean invisibleduck.org> writes:
On Wednesday, 6 August 2014 at 20:22:58 UTC, David Bregman wrote:
 On Wednesday, 6 August 2014 at 19:34:48 UTC, Sean Kelly wrote:
 On Wednesday, 6 August 2014 at 18:15:41 UTC, David Bregman 
 wrote:
 On Wednesday, 6 August 2014 at 17:18:19 UTC, Sean Kelly wrote:
 So from a functional perspective, assuming this is a 
 multithreaded app, what should the procedure be when an 
 AssertError is thrown in some thread?
afaik, AssertError works the same as any other exception. If it reaches the top without being handled, then the entire app will be terminated including all the other threads.
Except that's not really how unhandled exceptions are treated in threads. They're stored by the thread and (optionally) re-thrown in the context of whatever thread calls join, if any thread calls join at all. The assumption at the time was that the joining thread cared about the state of the thread being joined and so re-throwing the exception was a way to communicate the error to the most interested party. So if the main thread joins a thread that terminated with an unhandled AssertError, the error will be re-thrown in the context of the main thread, which will in turn join all remaining running threads and wait for them to complete. This is the same behavior as if an AssertError is generated during normal processing of the main thread. But in neither case is the application forcibly terminated when an assertion failure occurs.
Ah, I see. Then I apologize for giving incorrect information. I am not that familiar with threads in D yet and I assumed unhandled exceptions worked like C++. But if you already knew the answer then why were you asking?
It seems like this change in treatment of assertion failures might require a change in runtime behavior as well. But I don't know exactly what people have in mind. Also, assuming that a change is expected, depending on what the desired effect is, I'm not sure I'll know how to do it.
 So again, my question is twofold: what *should* happen, given 
 this new treatment for assertions, and then *how* will we 
 accomplish this?  A multithreaded process is really pretty 
 much equivalent to a bunch of standalone processes with shared 
 memory.
 There is no facility for forcing a clean termination of 
 another thread.  The best I can think of would be to assume 
 that std.concurrency is being used for multithreading and sort 
 things out similar to the existing LinkTerminated signaling, 
 but looking for a reasonable solution within Druntime would be 
 tricky.
I think there is some kind of misunderstanding here, I have not proposed any new treatment for assertions. Walter's proposal only affects release mode, so it's not related to exceptions.
Well, it seems like the underlying idea is to treat assertion failures more strongly than we do now. So changes in how these are handled by the runtime might be a side effect of this proposal.
Aug 06 2014
parent reply "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 20:27:45 UTC, Sean Kelly wrote:
 Well, it seems like the underlying idea is to treat assertion 
 failures more strongly than we do now.  So changes in how these 
 are handled by the runtime might be a side effect of this 
 proposal.
Again, since Walter's proposal only affects release mode, I don't see how exceptions or the runtime are related. What am I missing? You agree assertion failures (AssertError) are only thrown in debug mode, right?
Aug 06 2014
parent reply "Sean Kelly" <sean invisibleduck.org> writes:
On Wednesday, 6 August 2014 at 21:16:42 UTC, David Bregman wrote:
 On Wednesday, 6 August 2014 at 20:27:45 UTC, Sean Kelly wrote:
 Well, it seems like the underlying idea is to treat assertion 
 failures more strongly than we do now.  So changes in how 
 these are handled by the runtime might be a side effect of 
 this proposal.
Again, since Walter's proposal only affects release mode, I don't see how exceptions or the runtime are related. What am I missing? You agree assertion failures (AssertError) are only thrown in debug mode, right?
In non-release mode, but yes. However: 4. An assert failure is a non-recoverable error. The compiler may assume that execution does not proceed after one is tripped. The language does allow attempts to shut a program down gracefully after one is tripped, but that must not be misconstrued as assuming that the program is in a valid state at that point. 5. assert(0); is equivalent to a halt, and the compiler won't remove it. Clearly, the intention is for assertion failures to terminate the program, but that isn't done now. Or at least this isn't done in the multithreaded case. So I was asking for clarification on what should be done on that end, and whether that behavior should inform how assert is treated from a language perspective.
Aug 06 2014
parent "David Bregman" <drb sfu.ca> writes:
On Wednesday, 6 August 2014 at 21:35:26 UTC, Sean Kelly wrote:
 On Wednesday, 6 August 2014 at 21:16:42 UTC, David Bregman 
 wrote:
 On Wednesday, 6 August 2014 at 20:27:45 UTC, Sean Kelly wrote:
 Well, it seems like the underlying idea is to treat assertion 
 failures more strongly than we do now.  So changes in how 
 these are handled by the runtime might be a side effect of 
 this proposal.
Again, since Walter's proposal only affects release mode, I don't see how exceptions or the runtime are related. What am I missing? You agree assertion failures (AssertError) are only thrown in debug mode, right?
In non-release mode, but yes. However: 4. An assert failure is a non-recoverable error. The compiler may assume that execution does not proceed after one is tripped. The language does allow attempts to shut a program down gracefully after one is tripped, but that must not be misconstrued as assuming that the program is in a valid state at that point. 5. assert(0); is equivalent to a halt, and the compiler won't remove it. Clearly, the intention is for assertion failures to terminate the program, but that isn't done now. Or at least this isn't done in the multithreaded case. So I was asking for clarification on what should be done on that end, and whether that behavior should inform how assert is treated from a language perspective.
Ah, ok. So it's an issue with the existing implementation not matching some other expectations, not related to the main topic of this thread. Sorry for the confusion. Anyway, Walter just replied to your first post, I'll defer to him on this.
Aug 06 2014
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/6/2014 12:34 PM, Sean Kelly wrote:
 There is no facility for forcing a clean termination of another
 thread.
Understood - so the only option is to force an unclean termination. Let me emphasize that when an assert trips, the program has failed. It is in an invalid, unknown, indeterminate state from that moment forward. Use enforce() for errors that are anticipated and cleanly recoverable, not assert().
Aug 06 2014
parent reply "Sean Kelly" <sean invisibleduck.org> writes:
On Wednesday, 6 August 2014 at 22:01:47 UTC, Walter Bright wrote:
 On 8/6/2014 12:34 PM, Sean Kelly wrote:
 There is no facility for forcing a clean termination of another
 thread.
Understood - so the only option is to force an unclean termination.
So in all cases, it seems like what we should be doing is call exit(1) or the equivalent and forego any attempt at cleanup. Otherwise an assertion failure in a spawned thread would be handled even more strongly than in the main thread. Alternately, if we build on std.concurrency we could have the next call to receive throw a FatalError or something to force it to terminate. But there's no telling how long this would be. I assume you prefer the forceful route.
 Let me emphasize that when an assert trips, the program has 
 failed. It is in an invalid, unknown, indeterminate state from 
 that moment forward.
I think in many cases the scope of possible invalid states can actually be determined given a reasonable understanding of the program. For example, if a thread within a safe app encounters an error, it might be possible to assert that the damage does not extend beyond the limits of data referenced by the thread. But I do appreciate the desire to not deal lightly with detected logic errors so I won't push the point.
 Use enforce() for errors that are anticipated and cleanly 
 recoverable, not assert().
Given what I said above, I'm inclined to say that enforce() should be used by in contracts and the like rather than assert(), and to save assert() for the situations where I'm certain there's absolutely nothing to be done. However, I think of enforce() to be more for run-time problems that might be corrected by trying again later with the same input. I'll have to give this some thought.
Aug 06 2014
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/6/2014 5:22 PM, Sean Kelly wrote:
 On Wednesday, 6 August 2014 at 22:01:47 UTC, Walter Bright wrote:
 On 8/6/2014 12:34 PM, Sean Kelly wrote:
 There is no facility for forcing a clean termination of another
 thread.
Understood - so the only option is to force an unclean termination.
So in all cases, it seems like what we should be doing is call exit(1) or the equivalent and forego any attempt at cleanup. Otherwise an assertion failure in a spawned thread would be handled even more strongly than in the main thread. Alternately, if we build on std.concurrency we could have the next call to receive throw a FatalError or something to force it to terminate. But there's no telling how long this would be. I assume you prefer the forceful route.
Yes, I prefer that.
 Let me emphasize that when an assert trips, the program has failed. It is in
 an invalid, unknown, indeterminate state from that moment forward.
I think in many cases the scope of possible invalid states can actually be determined given a reasonable understanding of the program. For example, if a thread within a safe app encounters an error, it might be possible to assert that the damage does not extend beyond the limits of data referenced by the thread.
I can't agree with that, especially not for the standard library.
 Use enforce() for errors that are anticipated and cleanly recoverable, not
 assert().
Given what I said above, I'm inclined to say that enforce() should be used by in contracts and the like rather than assert(), and to save assert() for the situations where I'm certain there's absolutely nothing to be done. However, I think of enforce() to be more for run-time problems that might be corrected by trying again later with the same input. I'll have to give this some thought.
Aug 06 2014
parent Johannes Pfau <nospam example.com> writes:
Am Wed, 06 Aug 2014 20:19:33 -0700
schrieb Walter Bright <newshound2 digitalmars.com>:

 On 8/6/2014 5:22 PM, Sean Kelly wrote:
 On Wednesday, 6 August 2014 at 22:01:47 UTC, Walter Bright wrote:
 On 8/6/2014 12:34 PM, Sean Kelly wrote:
 There is no facility for forcing a clean termination of another
 thread.
Understood - so the only option is to force an unclean termination.
So in all cases, it seems like what we should be doing is call exit(1) or the equivalent and forego any attempt at cleanup. Otherwise an assertion failure in a spawned thread would be handled even more strongly than in the main thread. Alternately, if we build on std.concurrency we could have the next call to receive throw a FatalError or something to force it to terminate. But there's no telling how long this would be. I assume you prefer the forceful route.
Yes, I prefer that.
I can see some benefits here, but how does this interact with asserts in unittests? You might special-case these, but it's also common practice to use these asserts not only in the main unittest function but also in helper functions.
Aug 07 2014
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/6/2014 10:18 AM, Sean Kelly wrote:
 So from a functional perspective, assuming this is a multithreaded app, what
 should the procedure be when an AssertError is thrown in some thread?
Print message, stop the process and all its threads. Rationale: the program is in an unknown, invalid state, which will include any thread (or process) that has access to memory shared with that failed thread. Attempting to continue operating is irresponsible if the program is doing or can do anything important.
Aug 06 2014
next sibling parent reply Johannes Pfau <nospam example.com> writes:
Am Wed, 06 Aug 2014 14:57:50 -0700
schrieb Walter Bright <newshound2 digitalmars.com>:

 On 8/6/2014 10:18 AM, Sean Kelly wrote:
 So from a functional perspective, assuming this is a multithreaded
 app, what should the procedure be when an AssertError is thrown in
 some thread?
Print message, stop the process and all its threads. Rationale: the program is in an unknown, invalid state, which will include any thread (or process) that has access to memory shared with that failed thread. Attempting to continue operating is irresponsible if the program is doing or can do anything important.
Again: unittests?
Aug 07 2014
next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/7/2014 12:54 AM, Johannes Pfau wrote:
 Again: unittests?
Asserts in unittests are not the same as asserts elsewhere. I wasn't a big fan of this, but I was probably the only one :-)
Aug 07 2014
parent reply "Daniel Murphy" <yebbliesnospam gmail.com> writes:
"Walter Bright"  wrote in message news:lrvglk$25dt$1 digitalmars.com...

 Asserts in unittests are not the same as asserts elsewhere. I wasn't a big 
 fan of this, but I was probably the only one :-)
This has the fun side-effect that asserts in unittest helper functions are fatal, while ones in the unittest body are not! And we've also got asserts in pre-conditions, which are recoverable by definition.
Aug 07 2014
next sibling parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Thu, Aug 07, 2014 at 07:29:43PM +1000, Daniel Murphy via Digitalmars-d wrote:
 "Walter Bright"  wrote in message news:lrvglk$25dt$1 digitalmars.com...
 
Asserts in unittests are not the same as asserts elsewhere. I wasn't
a big fan of this, but I was probably the only one :-)
This has the fun side-effect that asserts in unittest helper functions are fatal, while ones in the unittest body are not! And we've also got asserts in pre-conditions, which are recoverable by definition.
Huh, what? I thought asserts in pre-conditions are non-recoverable, because they imply that user code has broken the contract governing the use of that function. T -- Answer: Because it breaks the logical sequence of discussion. Question: Why is top posting bad?
Aug 07 2014
next sibling parent "Sean Kelly" <sean invisibleduck.org> writes:
On Thursday, 7 August 2014 at 15:21:14 UTC, H. S. Teoh via 
Digitalmars-d wrote:
 Huh, what? I thought asserts in pre-conditions are 
 non-recoverable,
 because they imply that user code has broken the contract 
 governing the use of that function.
I suspect this new treatment of assert will affect the way that people check for errors. For example, in the server apps I write, I don't always want a hard stop of the entire process if I detect a logic error because it provides a potential attack vector for a user to bring down an entire service. As soon as someone determines that a particular request kills all transactions on a process... This isn't just paranoia in a new direction either. The servers I work on are literally under constant attack by hackers. Largely botnets trying to crack passwords, but not exclusively that. And so I might want to at least drain out all pending requests before halting the process, or I might want to just kill the transaction that detected the logic error and leave everything running, assuming I can be sure that the potential collateral damage is local to the transaction (which is typically the case). Longer term, this new treatment of assert will probably encourage better program design which guarantees memory isolation by multiprocessing. I favor this direction, but messaging has a way to go first. And by extension, I do think that memory sharing in a language that allows direct memory access is the real risk. That a logic error might cause a thread / process to generate an invalid message is not an issue any more than it would be an issue to call a function with bad parameters. In both cases, the implication is that the caller is in an invalid state, not the callee. So long as there is no vector through which one context can alter the data accessed by another context without proper validation, the corruption cannot spread.
Aug 07 2014
prev sibling parent reply "Daniel Murphy" <yebbliesnospam gmail.com> writes:
"H. S. Teoh via Digitalmars-d"  wrote in message 
news:mailman.674.1407424873.16021.digitalmars-d puremagic.com...

 And we've also got asserts in pre-conditions, which are recoverable by
 definition.
Huh, what? I thought asserts in pre-conditions are non-recoverable, because they imply that user code has broken the contract governing the use of that function.
I meant asserts in pre-conditions when used with inheritance. It's a pass if any of the preconditions pass, so the compiler runs them in turn and catches all but the last.
Aug 07 2014
next sibling parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Fri, Aug 08, 2014 at 03:44:06AM +1000, Daniel Murphy via Digitalmars-d wrote:
 "H. S. Teoh via Digitalmars-d"  wrote in message
 news:mailman.674.1407424873.16021.digitalmars-d puremagic.com...
 
 And we've also got asserts in pre-conditions, which are recoverable
 by definition.
Huh, what? I thought asserts in pre-conditions are non-recoverable, because they imply that user code has broken the contract governing the use of that function.
I meant asserts in pre-conditions when used with inheritance. It's a pass if any of the preconditions pass, so the compiler runs them in turn and catches all but the last.
Oh, I see it now. Hmph. Now it's making me wonder if preconditions should be treated as a *single* assert outside the body of 'in{}', rather than allowing individual asserts inside. Perhaps the body of 'in{}' should return a boolean where false indicates a failed precondition, so that instead of writing: auto func(...) in { assert(cond1); assert(cond2); assert(cond3); } body { ... } you'd write instead: auto func(...) in { cond1 && cond2 && cond3 } body { ... } and the compiler translates this to: bool __func__in(...) { return cond1 && cond2 && cond3; } auto func(...) { assert(__func_in(...)); // body goes here } Well, technically it should be the caller that invokes __func_in(), but that's a different issue. T -- We are in class, we are supposed to be learning, we have a teacher... Is it too much that I expect him to teach me??? -- RL
Aug 07 2014
parent reply "Daniel Murphy" <yebbliesnospam gmail.com> writes:
"H. S. Teoh via Digitalmars-d"  wrote in message 
news:mailman.684.1407434193.16021.digitalmars-d puremagic.com...

 Hmph. Now it's making me wonder if preconditions should be treated as a
 *single* assert outside the body of 'in{}', rather than allowing
 individual asserts inside. Perhaps the body of 'in{}' should return a
 boolean where false indicates a failed precondition,
I think that ship has sailed.
Aug 08 2014
parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Fri, Aug 08, 2014 at 07:15:22PM +1000, Daniel Murphy via Digitalmars-d wrote:
 "H. S. Teoh via Digitalmars-d"  wrote in message
 news:mailman.684.1407434193.16021.digitalmars-d puremagic.com...
 
Hmph. Now it's making me wonder if preconditions should be treated as
a *single* assert outside the body of 'in{}', rather than allowing
individual asserts inside. Perhaps the body of 'in{}' should return a
boolean where false indicates a failed precondition,
I think that ship has sailed.
I know. It was more of a wish than anything. T -- Don't modify spaghetti code unless you can eat the consequences.
Aug 08 2014
parent reply "Vlad Levenfeld" <vlevenfeld gmail.com> writes:
On Friday, 8 August 2014 at 14:27:56 UTC, H. S. Teoh via 
Digitalmars-d wrote:
 On Fri, Aug 08, 2014 at 07:15:22PM +1000, Daniel Murphy via 
 Digitalmars-d wrote:
 "H. S. Teoh via Digitalmars-d"  wrote in message
 news:mailman.684.1407434193.16021.digitalmars-d puremagic.com...
 
Hmph. Now it's making me wonder if preconditions should be 
treated as
a *single* assert outside the body of 'in{}', rather than 
allowing
individual asserts inside. Perhaps the body of 'in{}' should 
return a
boolean where false indicates a failed precondition,
I think that ship has sailed.
I know. It was more of a wish than anything. T
Since the ship HAS sailed... why must contracts be elided with --release? Seems to me if asserts go away, then eliding in and out is redundant. It'd be nice if I could put all my recoverable pre and post conditions inside those blocks as well. Just for organization's sake.
Aug 08 2014
parent "Jonathan M Davis" <jmdavisProg gmx.com> writes:
On Friday, 8 August 2014 at 18:43:22 UTC, Vlad Levenfeld wrote:
 Since the ship HAS sailed... why must contracts be elided with 
 --release? Seems to me if asserts go away, then eliding in and 
 out is redundant. It'd be nice if I could put all my 
 recoverable pre and post conditions inside those blocks as 
 well. Just for organization's sake.
An in or out block could have other code which is doing work in preparation for asserting rather than just assertions, so leaving them in wouldn't make sense. - Jonathan M Davis
Aug 08 2014
prev sibling next sibling parent reply "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Thu, Aug 07, 2014 at 10:54:53AM -0700, H. S. Teoh via Digitalmars-d wrote:
 On Fri, Aug 08, 2014 at 03:44:06AM +1000, Daniel Murphy via Digitalmars-d
wrote:
 "H. S. Teoh via Digitalmars-d"  wrote in message
 news:mailman.674.1407424873.16021.digitalmars-d puremagic.com...
 
 And we've also got asserts in pre-conditions, which are recoverable
 by definition.
Huh, what? I thought asserts in pre-conditions are non-recoverable, because they imply that user code has broken the contract governing the use of that function.
I meant asserts in pre-conditions when used with inheritance. It's a pass if any of the preconditions pass, so the compiler runs them in turn and catches all but the last.
Oh, I see it now.
[...] P.S. The current implementation also does not distinguish between a broken contract vs. a bug or problem encountered by the contract code. For example: auto func(T...)(T args) in { assert(checkConsistency(args)); } body { ... } bool checkConsistency(T...)(T args) { int i; for (i=0; i < args.length; i++) { ... i = 1000; // suppose an inadvertent typo causes this } assert(i == args.length); // so this will fail ... return result; } Suppose the i=1000 line is a mistake by the programmer, so it's a genuine bug in checkConsistency. This would trip the assert in checkConsistency, which would throw an AssertError. But if it was called from the in-contract of func(), and func() is in a derived class for which the base class version of func() has an in-contract that passes, then we're basically swallowing the AssertError triggered by the failed malloc(), and thereby causing the program to continue running in an invalid state! Basically, the problem is that the in-contract can't tell the difference between a precondition failure (triggered by the outer assert) and a genuine program bug (triggered by the inner assert). This makes DbC in D really shaky. :-( T -- Freedom: (n.) Man's self-given right to be enslaved by his own depravity.
Aug 07 2014
parent "Daniel Murphy" <yebbliesnospam gmail.com> writes:
"H. S. Teoh via Digitalmars-d"  wrote in message 
news:mailman.689.1407436311.16021.digitalmars-d puremagic.com...

 P.S. The current implementation also does not distinguish between a
 broken contract vs. a bug or problem encountered by the contract code.
 For example:
Last time I checked it also treated OOM and access violation (on windows) as contract failure too. Any Throwable.
Aug 08 2014
prev sibling next sibling parent reply "Sean Kelly" <sean invisibleduck.org> writes:
On Thursday, 7 August 2014 at 17:44:02 UTC, Daniel Murphy wrote:
 "H. S. Teoh via Digitalmars-d"  wrote in message 
 news:mailman.674.1407424873.16021.digitalmars-d puremagic.com...

 And we've also got asserts in pre-conditions, which are 
 recoverable by
 definition.
Huh, what? I thought asserts in pre-conditions are non-recoverable, because they imply that user code has broken the contract governing the use of that function.
I meant asserts in pre-conditions when used with inheritance. It's a pass if any of the preconditions pass, so the compiler runs them in turn and catches all but the last.
Oh man, I forgot about this. I wonder how this works from a codegen perspective. Is precondition inheritance properly implemented yet?
Aug 07 2014
parent "Daniel Murphy" <yebbliesnospam gmail.com> writes:
"Sean Kelly"  wrote in message news:trnhymzwfkflgotxykmb forum.dlang.org...

 Oh man, I forgot about this.  I wonder how this works from a codegen 
 perspective.  Is precondition inheritance properly implemented yet?
Properly is a bit strong. It is somewhat implemented. I think there are still corner cases when some functions have no preconditions that people are still arguing over, but it does work for simple inheritance examples.
Aug 08 2014
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/7/2014 10:44 AM, Daniel Murphy wrote:
 I meant asserts in pre-conditions when used with inheritance.  It's a pass if
 any of the preconditions pass, so the compiler runs them in turn and catches
all
 but the last.
That's right, they are OR'd together.
Aug 09 2014
parent "H. S. Teoh via Digitalmars-d" <digitalmars-d puremagic.com> writes:
On Sat, Aug 09, 2014 at 05:54:21PM -0700, Walter Bright via Digitalmars-d wrote:
 On 8/7/2014 10:44 AM, Daniel Murphy wrote:
I meant asserts in pre-conditions when used with inheritance.  It's a
pass if any of the preconditions pass, so the compiler runs them in
turn and catches all but the last.
That's right, they are OR'd together.
Which is fine if they are evaluated as a single expression. The problem right now is that the OR is simulated by catching AssertErrors, which by definition only happens when the program in an invalid state, so the fact that this works at all is only a "lucky coincidence". :-( If you're "not so lucky" you end up catching a genuine program bug but ignoring it because the other condition in the simulated OR turned out to pass. This unfortunately puts DbC in D on rather shaky ground. T -- Кто везде - тот нигде.
Aug 09 2014
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/7/2014 2:29 AM, Daniel Murphy wrote:
 And we've also got asserts in pre-conditions, which are recoverable by
definition.
Pre-condition asserts are not recoverable.
Aug 09 2014
parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/9/2014 5:52 PM, Walter Bright wrote:
 On 8/7/2014 2:29 AM, Daniel Murphy wrote:
 And we've also got asserts in pre-conditions, which are recoverable by
 definition.
Pre-condition asserts are not recoverable.
Eh, ignore that.
Aug 09 2014
prev sibling parent reply "Sean Kelly" <sean invisibleduck.org> writes:
On Thursday, 7 August 2014 at 07:57:14 UTC, Johannes Pfau wrote:
 
 Attempting to continue operating is irresponsible if the 
 program is doing or can do anything important.
Again: unittests?
unittests shouldn't use assert. Or alternately, we can have onAssertError (the assertion failure callback) do something different if unit testing is taking place than when the program is actually running.
Aug 07 2014
parent David Gileadi <gileadis NSPMgmail.com> writes:
On 8/7/14, 9:51 AM, Sean Kelly wrote:
 On Thursday, 7 August 2014 at 07:57:14 UTC, Johannes Pfau wrote:
 Attempting to continue operating is irresponsible if the program is
 doing or can do anything important.
Again: unittests?
unittests shouldn't use assert. Or alternately, we can have onAssertError (the assertion failure callback) do something different if unit testing is taking place than when the program is actually running.
Considering that TDPL, Ali's Book[1] and dlang.org[2] all use assert when introducing unittest, I think the latter solution is probably the right one. [1] http://ddili.org/ders/d.en/unit_testing.html [2] http://dlang.org/unittest.html
Aug 07 2014
prev sibling parent reply "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Wednesday, 6 August 2014 at 21:57:50 UTC, Walter Bright wrote:
 On 8/6/2014 10:18 AM, Sean Kelly wrote:
 So from a functional perspective, assuming this is a 
 multithreaded app, what
 should the procedure be when an AssertError is thrown in some 
 thread?
Print message, stop the process and all its threads. Rationale: the program is in an unknown, invalid state, which will include any thread (or process) that has access to memory shared with that failed thread.
Strictly speaking we would need to kill only those threads. But I guess it wouldn't be worth the effort, because the remaining threads are most likely not expecting them to disappear and couldn't recover from this.
Aug 07 2014
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/7/2014 2:10 AM, "Marc Schütz" <schuetzm gmx.net>" wrote:
 On Wednesday, 6 August 2014 at 21:57:50 UTC, Walter Bright wrote:
 On 8/6/2014 10:18 AM, Sean Kelly wrote:
 So from a functional perspective, assuming this is a multithreaded app, what
 should the procedure be when an AssertError is thrown in some thread?
Print message, stop the process and all its threads. Rationale: the program is in an unknown, invalid state, which will include any thread (or process) that has access to memory shared with that failed thread.
Strictly speaking we would need to kill only those threads.
No, all the threads. Threads share memory, so corruption can spread from one to the next.
Aug 07 2014
parent "Marc =?UTF-8?B?U2Now7x0eiI=?= <schuetzm gmx.net> writes:
On Thursday, 7 August 2014 at 09:26:01 UTC, Walter Bright wrote:
 On 8/7/2014 2:10 AM, "Marc Schütz" <schuetzm gmx.net>" wrote:
 On Wednesday, 6 August 2014 at 21:57:50 UTC, Walter Bright 
 wrote:
 On 8/6/2014 10:18 AM, Sean Kelly wrote:
 So from a functional perspective, assuming this is a 
 multithreaded app, what
 should the procedure be when an AssertError is thrown in 
 some thread?
Print message, stop the process and all its threads. Rationale: the program is in an unknown, invalid state, which will include any thread (or process) that has access to memory shared with that failed thread.
Strictly speaking we would need to kill only those threads.
No, all the threads. Threads share memory, so corruption can spread from one to the next.
Yes, that's what I was saying: "those threads ... that ha[ve] access to memory shared with that failed thread". But even without real sharing of memory, a failed assertion in one thread might result from invalid data being sent to that thread from another one (via spawn or send). Better to just kill all threads.
Aug 07 2014