On Tue, Jun 07, 2016 at 07:00:13PM -0700, Charles Hixson via Digitalmars-d wrote:
> On 06/05/2016 09:17 PM, Adam D. Ruppe via Digitalmars-d wrote:
> > On Monday, 6 June 2016 at 02:30:55 UTC, Pie? wrote:
> > > Duh! The claim is made that D can work without the GC... but that's a red herring... If you take about the GC what do you have?
> > 
> > Like 90% of the language, still generally nicer than most the competition.
> > 
> > Though, I wish D would just own its decision instead of bowing to Reddit pressure. GC is a proven success in the real world with a long and impressive track record. Yes, there are times when you need to optimize your code, but even then you aren't really worse off with it than without it.
> > 
> Usually correct, but there are times when you want to suspend the garbage collection.  The problem is this should always be a scoped decision, because it's easy to accidentally leave it turned off, and then it's MUCH worse than not having it.

	auto myFunc(Args...)(Args args) {
		GC.disable();
		scope(exit) GC.enable();

		doStuff();
	}

On another note, I have found that strategic disabling of the GC and/or manually triggering GC.collect() at the right times, can give your programs a big boost in performance, typically around 20% to 50% depending on the specifics of your memory usage patterns. Arguably this should be automatic once D's GC is replaced with something better than the current implementation, but the point is that performance concerns over the GC aren't insurmountable, and the fix is often not even that complicated.

I think far too much energy has been spent arguing for a GC-less language than actually writing the code that would fix its associated performance issues, and my suspicion is that this is mostly caused by your typical C/C++ programmer mindset (of which I used to be a part) that's always obsessed about memory management, rather than any factual basis.


T

-- 
It said to install Windows 2000 or better, so I installed Linux instead.

On Tuesday, June 07, 2016 19:04:06 H. S. Teoh via Digitalmars-d wrote:
> I think far too much energy has been spent arguing for a GC-less language than actually writing the code that would fix its associated performance issues, and my suspicion is that this is mostly caused by your typical C/C++ programmer mindset (of which I used to be a part) that's always obsessed about memory management, rather than any factual basis.

One of the other big issues is that many of the companies which use D and have been active in the community have been doing _very_ high performance stuff where they can't afford the GC to kick in even occasionally for less than a hundred milliseconds (e.g. IIRC, Manu considering 10ms to be too long for what they were doing at Rememdy). When you start getting requirements that are that stringent, you start needing to not use the GC. And when some of the more visible users of D have requirements like that and raise issues about how the GC gets in their way, then it becomes a big deal even if it's not a problem for your average D user.

We need to support GC-less code, and we need to avoid using the GC in Phobos stuff where it's not necessary, since it will impede the high performance folks otherwise.  And doing some of the stuff like turning off the GC in specific code like you discussed will take care of many of the folks that would be affected by GC issues. But for your average D program, I really think that it's a non-issue, and as the GC situation improves, it will be even less of an issue.

So, to some extent, I agree that there's too much an issue made over the GC - especially by folks who aren't even using the language and pretty much just react negatively to the idea of the GC. But we do still need to do a better job of not requiring the GC when it's not actually needed as well as better supporting some of the GC-less paradigms like ref-counting.

- Jonathan M Davis

On Tue, Jun 07, 2016 at 07:24:55PM -0700, Jonathan M Davis via Digitalmars-d wrote:
> On Tuesday, June 07, 2016 19:04:06 H. S. Teoh via Digitalmars-d wrote:
> > I think far too much energy has been spent arguing for a GC-less language than actually writing the code that would fix its associated performance issues, and my suspicion is that this is mostly caused by your typical C/C++ programmer mindset (of which I used to be a part) that's always obsessed about memory management, rather than any factual basis.
> 
> One of the other big issues is that many of the companies which use D and have been active in the community have been doing _very_ high performance stuff where they can't afford the GC to kick in even occasionally for less than a hundred milliseconds (e.g. IIRC, Manu considering 10ms to be too long for what they were doing at Rememdy).

I'm pretty sure there are applications for which GC is verboten, such as high-performance game engines and what-not (but even for them, it's just the core code that needs to avoid GC; peripheral things like in-game scripting may actually be using a forced-GC scripting language -- it's just that you want to control certain core operations to be maximally performant).  But these are the exceptions rather than the norm.


[...]
> We need to support GC-less code, and we need to avoid using the GC in Phobos stuff where it's not necessary, since it will impede the high performance folks otherwise.  And doing some of the stuff like turning off the GC in specific code like you discussed will take care of many of the folks that would be affected by GC issues. But for your average D program, I really think that it's a non-issue, and as the GC situation improves, it will be even less of an issue.

Actually, I'm not sure how much of Phobos actually depends on the GC. Most of the stuff I use frequently are from std.range and std.algorithm, and we've pretty much gotten rid of GC-dependence from most of the stuff there.  Phobos modules that are GC-heavy ought to be avoided in high-performance code anyway; the only problematic case I can think of being std.string which greedily allocates. But we've been making progress on that over the past year or so by turning many of the functions into range-based algorithms rather than string-specific.

Lately I've been considering in my own code that a lot of things actually don't *need* the GC. Even things like string transformations generally don't need to allocate if they are structured to be a range-based pipeline, and the consumer (sink) processes the data as it becomes available instead of storing everything in intermediate buffers. Even if you do need to allocate some intermediate buffers these are generally well-scoped, and can be taken care of with malloc/free and scope(exit).  The only time you really need the GC is when passing around large recursive data structures with long lifetimes, like trees and graphs.


> So, to some extent, I agree that there's too much an issue made over the GC - especially by folks who aren't even using the language and pretty much just react negatively to the idea of the GC.

As Walter has said before: people who aren't already using the language are probably only using GC as an excuse to not use the language. They won't necessarily start using the language after we've bent over backwards to get rid of the GC. We should be paying attention to current users (and yes I know Manu has been clamoring for @nogc and he's a current user).


> But we do still need to do a better job of not requiring the GC when it's not actually needed as well as better supporting some of the GC-less paradigms like ref-counting.
[...]

IMO a lot of Phobos modules actually could become much higher-quality if rewritten to be GC-independent.  Some of the less-frequently used modules are GC-heavy not out of necessity but because of sloppy code quality, or because they were written prior to major D2 breakthroughs like ranges and templates / CT introspection.


T

-- 
The early bird gets the worm. Moral: ewww...

On Tuesday, June 07, 2016 21:00:06 H. S. Teoh via Digitalmars-d wrote:
> Actually, I'm not sure how much of Phobos actually depends on the GC. Most of the stuff I use frequently are from std.range and std.algorithm, and we've pretty much gotten rid of GC-dependence from most of the stuff there.  Phobos modules that are GC-heavy ought to be avoided in high-performance code anyway; the only problematic case I can think of being std.string which greedily allocates. But we've been making progress on that over the past year or so by turning many of the functions into range-based algorithms rather than string-specific.

As I understand it, the big problems relate to lambdas and closures and the like. As it stands, it's way too easy to end up allocating when using stuff like std.algorithm even though it doesn't obviously allocate. And on some level at least, I think that that's more an issue of language improvements than library improvements. But no, explicit use of the GC in Phobos is not particularly heavy. Array-related stuff often allocates, and the few places in Phobos that use classes allocate, but in general, Phobos really doesn't do much in the way explicit allocations. It's the implicit ones that are the killer.

- Jonathan M Davis

Jack Stouffer wrote:
> On Tuesday, 7 June 2016 at 13:39:19 UTC, Steven Schveighoffer wrote:
>> I just read elsewhere that a GSoC student is working to achieve the
>> goal of making the GC swappable and adding Reiner's precise scanning
>> GC. I consider this to be essential work, I hope we can get this
>> rolling soon!
>
> https://github.com/dlang/druntime/pull/1581
>

Feedback is greatly appreciated! If you have an opinion on how to implement user-selectable Garbage Collection algorithms, please chime in. That said, we may not include your feedback, being a GSoC project means that we will need to fast-track merges so as not to block the student. We'll listen, but we might push that really cool idea of yours off until after GSoC.

-- 
// Adam Wilson
// import quiet.dlang.dev;

On Wednesday, 8 June 2016 at 00:39:54 UTC, Walter Bright wrote:
> On the contrary, I think a formal proof would be very valuable. I am just skeptical of the notion that a proof is automatically correct. I've read about mistakes being found in many published mathematical proofs. I read somewhere that Hilbert made many mistakes in his proofs, even though the end results turned out correct.

Well, you cannot prevent errors in the requirements, but you can eliminate errors in the proof, so if the requirements are too complex  you have a bad deal. The theorem prover is separate from the proof verifier. It works like this:

1. Human specifies the requirements (e.g. assert(...) in D)

2. Theorem prover takes program + requirements + strategies (prodding the prover along the right track) and emits a loooong formal proof in a standard format.

3. The proof is handed to N independently implemented verifiers that checks the proof.

But that is impractical for typical user created program. You only want to do that once, for your backend or your type-system etc.

--

What you can do is, as you've stated before, transform your source code into a simpler form and verify that it only can lead to situations that are provably safe.

The advantage of this is that you also can prove that specific cases of pointer arithmetics are provably safe (say, fixed size array on the stack) thus reducing the need for @trusted.

The disadvantage is that it will slow down the compiler and make it more complicated, so why have it in the compiler and not as a separate program?

Make it a separate program so it works on uninstantiated code and prove libraries to be correctly marked @safe before they are uploaded to repositories etc.

If @safe does not affect code gen, why have it in the compiler?

On 08.06.2016 01:07, Andrei Alexandrescu wrote:
> On 6/8/16 12:53 AM, Timon Gehr wrote:
>> On 08.06.2016 00:47, Walter Bright wrote:
>>> On 6/7/2016 3:23 PM, Timon Gehr wrote:
>>>> Obviously they proved the virtual machine itself memory safe,
>>>
>>> As I recall, the proof was broken, not the implementation.
>>
>> Which time?
>
> That is an old result that has essentially expired and should not be
> generalized. See
> http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00849.html.

I think this can't be what Walter is referring to: "the type inference system for generic method calls was not subjected to formal proof. In fact, it is unsound,"

I.e. no proof, unsound.

> I assume the matter has been long fixed by now, do you happen to know?
> ...

I don't know.

BTW, Java's type system is unsound [1].

class Unsound {
    static class Bound<A, B extends A> {}
    static class Bind<A> {
        <B extends A> A bad(Bound<A,B> bound, B b) {return b;}
    }
    public static <T,U> U coerce(T t) {
        Bound<U,? super T> bound = null;
        Bind<U> bind = new Bind<U>();
        return bind.bad(bound, t);
    }
    public static void main(String[] args){
        String s=coerce(0);
    }
}


>>> People do
>>> make mistakes and overlook cases with proofs. There's nothing magical
>>> about them.
>>>
>>
>> Obviously, but there are reliable systems that check proofs
>> automatically.
>
> It is my opinion that writing off formal proofs of safety is a mistake.
> Clearly we don't have the capability on the core team to work on such.
> However, I am very interested if you'd want to lead such an effort.
>
>
> Andrei
>

I'll probably do it at some point. (However, first I need to figure out what the formal language specification should actually be, this is one reason why I'm implementing a D compiler.)


[1] https://www.facebook.com/ross.tate/posts/10102249566392775.

On 6/8/16 1:50 PM, Timon Gehr wrote:
> I'll probably do it at some point. (However, first I need to figure out
> what the formal language specification should actually be, this is one
> reason why I'm implementing a D compiler.)

That's very very promising. Looking forward to anything in that area! -- Andrei

On 08.06.2016 02:39, Walter Bright wrote:
> On 6/7/2016 4:07 PM, Andrei Alexandrescu wrote:
>> It is my opinion that writing off formal proofs of safety is a
>> mistake. Clearly
>> we don't have the capability on the core team to work on such.
>> However, I am
>> very interested if you'd want to lead such an effort.
>
> On the contrary, I think a formal proof would be very valuable. I am
> just skeptical of the notion that a proof is automatically correct. I've
> read about mistakes being found in many published mathematical proofs. I
> read somewhere that Hilbert made many mistakes in his proofs, even
> though the end results turned out correct.
>
>

Mathematicians use a semi-formal style of reasoning in publications. Most mistakes are minor and most mathematicians don't use tools (such as https://coq.inria.fr/) to verify their proofs like computer scientists often do when proving properties of formal systems.

The focus of Mathematics isn't necessarily on verification, it is usually on aesthetics, understanding, communication etc. Current tools are not particularly strong in such areas and it is often more tedious to get the proof through than it should be. And certainly Hilbert didn't have access to anything like them.

On 08.06.2016 01:59, Walter Bright wrote:
> ...
>
> I suspect D has long since passed point where it is too complicated for
> the rather limited ability of mathematicians to prove things about it.

The main reason why it is currently impractical to prove things about D is that D is not really a mathematical object. I.e. there is no precise spec.