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

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.

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.

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.

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?

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() ?

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.)

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.

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.

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().