On Monday, 30 January 2023 at 18:59:38 UTC, Richard (Rikki) Andrew Cattermole wrote:
> I'm not expressing myself clearly enough but the goal posts I'm recommending are the same as at the start. Check as much as possible with @safe, but let data structures be responsible for as much of the life time guarantees wrt. allocators as possible.
>
[...]
> I'm half and half. Stuff like @localsafe would mean that I think that allocators should all be @system in API. I'm genuinely reconsidering it for my own because of this thread.
>
> But in terms of hard coding into the compiler std.allocators vs sidero.base.allocators yeah no. It shouldn't do that, which is what the quoted statement was about. If both API's match, then the compiler should treat them the same way in terms of lifetime management.

So, what, we should allow @safe data structures to call @system allocators and simply *assume* that the allocator implementation won't do anything weird? And if someone writes their own allocator implementation, and doesn't manually check that their @system code provides the guarantees that the data structures expect, we're ok with them getting memory corruption in @safe code?

To me this seems antithetical to the entire idea of @safe. It's what Walter calls "programming by convention," where the only thing standing between the user and disaster is programmer discipline. I do not think he or Atila would be willing to accept it (nor would I accept it in their place).

On 31/01/2023 10:34 AM, Paul Backus wrote:
> So, what, we should allow @safe data structures to call @system allocators and simply *assume* that the allocator implementation won't do anything weird? And if someone writes their own allocator implementation, and doesn't manually check that their @system code provides the guarantees that the data structures expect, we're ok with them getting memory corruption in @safe code?

If you can show me papers where mechanical checking of memory allocators take place without the use of proofing assistants, I'll be very interested in it.

My understanding is that the state of the art barely touches upon this subject even with proofing assistants, let alone without. I.e. https://surface.syr.edu/eecs_techreports/182/

So yes, if the state of the art literally requires proof assistants to verify that a memory allocator is doing the right thing at the bare minimum, then it absolutely is out of scope of D for the time being. But hey, if there is a known good solution here that we can implement, lets do that.

On Monday, 30 January 2023 at 21:54:44 UTC, Richard (Rikki) Andrew Cattermole wrote:
> On 31/01/2023 10:34 AM, Paul Backus wrote:
>> So, what, we should allow @safe data structures to call @system allocators and simply *assume* that the allocator implementation won't do anything weird? And if someone writes their own allocator implementation, and doesn't manually check that their @system code provides the guarantees that the data structures expect, we're ok with them getting memory corruption in @safe code?
>
> If you can show me papers where mechanical checking of memory allocators take place without the use of proofing assistants, I'll be very interested in it.

Once again, it seems that I have utterly failed to communicate the fundamental premise of this discussion. This has nothing to do with verifying the allocator's implementation (which I agree must be done by hand).

The problem is, if you are attempting to write a @safe data structure

1. You need the allocator to provide you with certain guarantees (i.e., it is safe to call deallocate as long as you satisfy preconditions A, B, and C).
2. If you accept arbitrary allocators supplied by users, you have no way to tell whether they provide those guarantees or not.

Forget the author of the allocator--he is completely irrelevant. What should the *data structure author* do in this scenario?

One possible answer is, "the data structure author should just assume that the guarantees are provided." This answer is not acceptable because it allows memory corruption to occur in @safe code.

Another possible answer is, "the data structure author should look for some kind of 'flag' or 'certificate' on the allocator that indicates it provides the necessary guarantees." This is a better answer, but not ideal, because it requires manual verification not just of @trusted code but also @system code, and the responsibility for that verification is divided between the data structure author and the allocator author.

Another possible answer is, "the data structure author should make a whitelist of allocators that he personally knows provide the necessary guarantees, and only trust allocators on that list." This is similar to the previous answer, but it places the all of the responsibility for verification on the author of the @trusted code (i.e., the data structure author), and does not rely on allocator authors to manually verify their @system code.

Another possible answer is, "the data structure author should not accept arbitrary allocators from users in the first place." This is a more restrictive compromise, but unlike the previous ones, it allows the data structure author to be certain that his @trusted code will not cause memory corruption.

Another possible answer is, "the data structure author should rely on the allocator author to provide a @safe interface." This is the best answer, but unfortunately it is not possible without new language features.

What I would like to hear from you is, what is *your* answer to this question? What do you think the author of the *data structure* should do?

On 31/01/2023 11:28 AM, Paul Backus wrote:
> What I would like to hear from you is, what is *your* answer to this
> question? What do you think the author of the *data structure* should do?

Pray that it will error or work correctly.

Unless Walter changes his opinion of DFA or says let's add a proofing engine to dmd, I do not think we are fixing this situation. I want to see this solved. But we have very little to lean on in the literature, if we manage to do it, good chance somebody is getting a PHD.

On 1/30/23 18:36, Paul Backus wrote:
> 
> As far as I am aware, it is impossible to have all three of the following:
> 
> 1. @safe containers.
> 2. User-supplied allocators.
> 3. No language changes.

Well, we have @system variables now, so we can have poor man's typestate together with poor man's move semantics [1], like already proposed by ntrel and Dukc.

Why is this scheme not workable? Isn't this exactly the kind of problem (non-trivial memory safety invariant) we invented `@system` variables to solve?

(With sumtype, I guess you can even move the flags to runtime (at the cost of template bloat exponential in the number of flags) to get poor man's dependent type state.)

[1]:
import core.stdc.stdlib;


void main(){
    import std.stdio;
    void foo()@safe{
        auto ptr0=fancyMalloc(16);
        writeln(ptr0.borrow((scope ptr){
            return cast(int)ptr;
        }));
        fancyFree(ptr0);
    }
    foo();
    void bar()@safe{
        auto ptr0=fancyMalloc(16);
        auto ptr1=ptr0.withAliasing.leak;
        // ok, leaking is safe
        writeln(ptr1);
    }
    bar();
    void baz()@safe{
        auto ptr0=fancyMalloc(16);
        auto ptr1=ptr0.withAliasing;
        // fancyFree(ptr1); // error, not isolated
    }
    baz();
    void qux()@safe{
        auto ptr0=fancyMalloc(16);
        auto ptr1=ptr0.withAliasing;
        // auto ptr2=ptr1.unsafeAddFlags!(PointerFlags.isolated); // error, unsafe
        // fancyFree(ptr2); // (ok)
    }
    qux();
    void flarp()@trusted{
        auto ptr0=fancyMalloc(16);
        auto ptr1=ptr0.withAliasing;
        auto ptr2=ptr1.unsafeAddFlags!(PointerFlags.isolated); // ok, and we can check it is fine
        fancyFree(ptr2); // (ok)
    }
    flarp();
    void bongo()@safe{
        auto ptr1=function()@trusted{
            auto ptr0=malloc(16);
            return ptr0.unsafeAddFlags!(PointerFlags.mallocd|PointerFlags.isolated); // ok, we can tell it is mallocd and isolated
        }();
        fancyFree(ptr1); // ok
    }
    bongo();
}

enum PointerFlags{
    none,
    mallocd=1,
    isolated=2,
}

struct Pointer(T,PointerFlags flags){
    private @system T* ptr;

    Pointer!(T,flags&~PointerFlags.isolated) withAliasing()@trusted{
        auto result=ptr;
        ptr=null;
        return typeof(return)(result);
    }
    static if(!(flags&PointerFlags.isolated)){
        T* leak()@trusted{
            auto result=ptr;
            ptr=null;
            return result;
        }
    }
    auto borrow(R)(scope R delegate(scope T*)@safe dg)@trusted{
        scope local=ptr;
        ptr=null;
        scope(exit) ptr=local;
        return dg(local);
    }
    auto borrow(R)(scope R delegate(scope T*)@system dg)@system{
        scope local=ptr;
        ptr=null;
        scope(exit) ptr=local;
        return dg(ptr);
    }
}
Pointer!(T,flags) unsafeAddFlags(PointerFlags flags,T)(ref T* ptr)@system{
    auto result=ptr;
    ptr=null;
    return typeof(return)(result);
}
Pointer!(T,newFlags|oldFlags) unsafeAddFlags(PointerFlags newFlags,T,PointerFlags oldFlags)(ref Pointer!(T,oldFlags) ptr)@system{
    auto result=ptr.ptr;
    ptr.ptr=null;
    return unsafeAddFlags!(newFlags|oldFlags)(result);
}

Pointer!(void, PointerFlags.mallocd|PointerFlags.isolated) fancyMalloc(size_t size)@trusted{
    return typeof(return)(malloc(size));
}
void fancyFree(ref Pointer!(void, PointerFlags.mallocd|PointerFlags.isolated) ptr)@trusted{
    if(!ptr.ptr) return;
    free(ptr.ptr);
    ptr.ptr=null;
}

On Monday, 30 January 2023 at 22:28:56 UTC, Paul Backus wrote:
> On Monday, 30 January 2023 at 21:54:44 UTC, Richard (Rikki) Andrew Cattermole wrote:
>> On 31/01/2023 10:34 AM, Paul Backus wrote:
>>> So, what, we should allow @safe data structures to call @system allocators and simply *assume* that the allocator implementation won't do anything weird? And if someone writes their own allocator implementation, and doesn't manually check that their @system code provides the guarantees that the data structures expect, we're ok with them getting memory corruption in @safe code?
>>
>> If you can show me papers where mechanical checking of memory allocators take place without the use of proofing assistants, I'll be very interested in it.
>
> Once again, it seems that I have utterly failed to communicate the fundamental premise of this discussion. This has nothing to do with verifying the allocator's implementation (which I agree must be done by hand).
>
> [snip]

But spelling it out in more detail will help for any future DIP.

I think part of the problem is the whole "can't prove a negative" of this. Or rather, being able to show that this is the smallest language change to enable @safe allocator-aware reference counting.

I was watching Walter's Q&A from the recent Dconf and one point he makes it that things are much easier for him to understand with code examples. Probably goes for others as well. I think being able to show simple versions of various attempts at @safe allocator-aware RC approaches that either don't work or are awkward to use might go a long way to convincing people.