On 27/07/16 00:56, Walter Bright wrote:
>
> What the assert(0) actually does is insert a HALT instruction, even when
> -release is used. The spec is poorly worded.

Does that mean D isn't meant to be used to develop code that will run in Ring-0?

Or do we treat it as a feature that kernel mode code continues execution after an assert(false)?

Shachar

On Wednesday, 27 July 2016 at 03:13:38 UTC, Shachar Shemesh wrote:
> Does that mean D isn't meant to be used to develop code that will run in Ring-0?

assert(0) is never supposed to actually happen...

Though, I do think it might be better to make it output `forever: hlt; jmp forever;` which I think is just three bytes, and it is supposed to be unreachable anyway... so that'd work in all cases.

On Wednesday, 27 July 2016 at 03:31:07 UTC, Adam D. Ruppe wrote:
> On Wednesday, 27 July 2016 at 03:13:38 UTC, Shachar Shemesh wrote:
>> Does that mean D isn't meant to be used to develop code that will run in Ring-0?
>
> assert(0) is never supposed to actually happen...
>
> Though, I do think it might be better to make it output `forever: hlt; jmp forever;` which I think is just three bytes, and it is supposed to be unreachable anyway... so that'd work in all cases.

Can you explain what's the difference ?

On 27/07/16 08:03, deadalnix wrote:
> On Wednesday, 27 July 2016 at 03:31:07 UTC, Adam D. Ruppe wrote:
>> On Wednesday, 27 July 2016 at 03:13:38 UTC, Shachar Shemesh wrote:
>>> Does that mean D isn't meant to be used to develop code that will run
>>> in Ring-0?
>>
>> assert(0) is never supposed to actually happen...

Then why do anything at all with it? assert(0) is something that the programmer *hopes* will never happen. The distinction is very important.

And defining it as issuing HLT, instead of according to what the effect of it should be, is a major problem in the spec, IMHO. (technically, it is not a problem with the D language published spec, as the spec's wording does not mandate it. It is a problem with D unpublished spec inside Walter's head. The D spec as published on that point is not great, but is not really the problem).

>>
>> Though, I do think it might be better to make it output `forever: hlt;
>> jmp forever;` which I think is just three bytes, and it is supposed to
>> be unreachable anyway... so that'd work in all cases.
>
> Can you explain what's the difference ?

Halt, or HLT, or other variations of it (e.g. invocation of a coprocessor instruction on ARM), is a command that tells the CPU to stop processing instructions until an interrupt arrives. It is usually employed by the kernel as the most basic form of power management, as the CPU will, sometimes, turn off the clock when it sees this command, thus saving power.

So, for most OSes, the idle process' implementation is:
loop: halt
      jump loop

Besides saving power, this also allows a virtual machine host to know when the guest does not need the CPU, and assign it elsewhere.

As should be obvious by now, this command is privileged. You are not allowed to decide, in a user space application, that the CPU should not do anything else. If you try to execute it from user mode, a "privileged instruction" exception is raised by the CPU, just like it would for any other privileged instruction.

It is this exception, rather than the command's intended use, that Walter is harnessing for assert(false). Walter is banking on the exception terminating the application. To that end, HLT could be replaced with any other privileged instruction with the exact same end result.

The problem (or rather, one of the many problems) is that if the CPU is in privileged mode, that exception will never arrive. The spec ala Walter says that's still okay, because a HALT was executed, and that's that. Anything else that the program does and you might not have expected it to is your own problem.

Most D programmers, however, expect the program not to continue executing past an assert(false). They might see it as a bug. Hence my question whether that means D is not meant for programming in privileged mode.

Shachar

On 7/26/2016 10:24 PM, Shachar Shemesh wrote:
> Most D programmers, however, expect the program not to continue executing past
> an assert(false). They might see it as a bug. Hence my question whether that
> means D is not meant for programming in privileged mode.

Obviously, HALT means any instruction of sequence of instructions that stops the program from running. Some machines don't even have a HLT instruction. Do you want to make a stab at writing this for the spec?

On 26.07.2016 21:11, Steven Schveighoffer wrote:
> On 7/26/16 2:44 PM, Timon Gehr wrote:
>> On 26.07.2016 17:44, Johan Engelen wrote:
>>> The compiler can assume it is unreachable code, but it has to keep it,
>>
>> That makes no sense. Those two statements are mutually exclusive.
>
> I thought that assert(0) means that the compiler does not need to check
> any validity of code after the assert. I'd reword Johan's statement to
> say that the compiler can assume the programmer thought this was
> unreachable,

The spec should have a formal interpretation, even if it is written down in prose. What is the formal mechanism by which a compiler can literally 'assume' "the programmer thought that..."?

The standard meaning of the phrase "the compiler can assume that.." is that the compiler can consider some set of logical statements to be true and it can hence transform the code such that it can prove that the transformations are equivalence-preserving given the truth of those statements.

In case the statements known to be true given the conditions under which a branch is executed become provably equivalent to false, the compiler knows that this branch is unreachable. It can then prove that all code in that branch is equivalent to no code at all and apply the transformation that removes all statements in the branch. This also goes in the other direction: "The compiler can assume it is unreachable code" is a way to say that it can assume that false is true within that branch.


> so it can just crash. It can't compile the crash out, or
> then the program is in an invalid state!
>
> This is not the user saying "I guarantee we won't go over the cliff",
> it's the user saying "If we get to this point, I have lost all
> guarantees of not going off the cliff, so shut off the engine". The
> compiler can make optimization assumptions for the code that *doesn't*
> take the branch, but it still needs the branch to make sure.
>
> -Steve

Yes, that would make sense, but according to Walter and Andrei, failing assertions are UB in -release:
http://forum.dlang.org/thread/jrxrmcmeksxwlyuitzqp@forum.dlang.org

assert(0) might or might not be special in this respect. The current documentation effectively states that a failing assert(0) is UB even if you /don't/ pass -release.

This needs to be specified very precisely. For me, there is not really a way to fill in the actually intended meaning using common sense, because some confirmedly conscious design choices in this area profoundly contradict common sense.

On 27.07.2016 07:50, Walter Bright wrote:
> On 7/26/2016 10:24 PM, Shachar Shemesh wrote:
>> Most D programmers, however, expect the program not to continue
>> executing past
>> an assert(false). They might see it as a bug. Hence my question
>> whether that
>> means D is not meant for programming in privileged mode.
>
> Obviously, HALT means any instruction of sequence of instructions that
> stops the program from running. Some machines don't even have a HLT
> instruction. Do you want to make a stab at writing this for the spec?
>

His argument is that DMD (also, the spec for x86) gets it wrong, because DMD emits HLT, and HLT is not actually designed to terminate the program.

On 27/07/16 08:50, Walter Bright wrote:
> On 7/26/2016 10:24 PM, Shachar Shemesh wrote:
>> Most D programmers, however, expect the program not to continue
>> executing past
>> an assert(false). They might see it as a bug. Hence my question
>> whether that
>> means D is not meant for programming in privileged mode.
>
> Obviously, HALT means any instruction of sequence of instructions that
> stops the program from running. Some machines don't even have a HLT
> instruction. Do you want to make a stab at writing this for the spec?
>

Current text (after the strange copying corruption):
> The expression assert(0) is a special case; it signies that it is unreachable code. Either
> AssertError is thrown at runtime if it is reachable, or the execution is halted (on the x86 processor,
> a HLT instruction can be used to halt execution). The optimization and code generation phases of
> compilation may assume that it is unreachable code.

Proposed text:
The expression assert(0) is a special case; it signifies code that should be unreachable. Either AssertError is thrown at runtime if reached, or the assert message printed to stderr and execution terminated. The optimization and code generation phases of the compilation may assume that any code after the assert(0) is unreachable.

Main differences:
* Some phrasing improvements
* Change the confusing "is unreachable" (so why bother?) with "should be unreachable", which stresses it's usefulness (and avoids the opinion, expressed in this thread, that reaching it is UB)
* Remove the recommendation to use HLT on X86, which, as discussed, is plainly wrong
* Define the behavior symptomatically, allowing both more certainty for programmers relying on the specs to know what will happen, and for compiler implementers more freedom to choose the correct way to achieve this effect and handle resulting bugs.
* Add the requirement that the assert message be printed for assert(0)

Shachar

On 7/26/2016 11:49 PM, Shachar Shemesh wrote:
> Current text (after the strange copying corruption):
>> The expression assert(0) is a special case; it signies that it is unreachable
>> code. Either
>> AssertError is thrown at runtime if it is reachable, or the execution is
>> halted (on the x86 processor,
>> a HLT instruction can be used to halt execution). The optimization and code
>> generation phases of
>> compilation may assume that it is unreachable code.
>
> Proposed text:
> The expression assert(0) is a special case; it signifies code that should be
> unreachable. Either AssertError is thrown at runtime if reached, or the assert
> message printed to stderr and execution terminated. The optimization and code
> generation phases of the compilation may assume that any code after the
> assert(0) is unreachable.
>
> Main differences:
> * Some phrasing improvements
> * Change the confusing "is unreachable" (so why bother?) with "should be
> unreachable", which stresses it's usefulness (and avoids the opinion, expressed
> in this thread, that reaching it is UB)
> * Remove the recommendation to use HLT on X86, which, as discussed, is plainly
> wrong
> * Define the behavior symptomatically, allowing both more certainty for
> programmers relying on the specs to know what will happen, and for compiler
> implementers more freedom to choose the correct way to achieve this effect and
> handle resulting bugs.
> * Add the requirement that the assert message be printed for assert(0)
>
> Shachar

Thank you. I'd prefer it to say something along the lines that it stops execution at the assert(0) in an implementation-defined manner. This leaves whether messages are printed or not, etc., up to the implementation. I don't think the spec should require more than that (for example, some uses may have no means to print an error message).

On 27/07/16 10:14, Walter Bright wrote:
> Thank you. I'd prefer it to say something along the lines that it stops
> execution at the assert(0) in an implementation-defined manner. This
> leaves whether messages are printed or not, etc., up to the
> implementation. I don't think the spec should require more than that
> (for example, some uses may have no means to print an error message).

I would ask that it at least be a "recommends". This message is muchu useful, and finding out it is not displayed in DMD release mode was a major disappointment.

Updated proposed text:
The expression assert(0) is a special case; it signifies code that should be unreachable. Either AssertError is thrown at runtime if reached or execution terminated. In the later case, it is recommended that the implementation print the assert message to stderr (or equivalent) before terminating. The optimization and code generation phases of the compilation may assume that any code after the assert(0) is unreachable.

Shachar