Allocator-aware @safe reference counting is still not possible

[Paul Backus]

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?