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