7 ms·

I don't believe the argument is mistaken at all. Consider the interface of `uwu`. It takes two pointers with the extra promise that they do not alias each other

I don't believe the argument is mistaken at all. Consider the interface of `uwu`. It takes two pointers with the extra promise that they do not alias each other. When you call that function with two pointers that happen to be adjacent but non-overlapping, that promise is absolutely satisfied. The problems start with the notion of 'derived from' and pointer arithmetic. Obviously you can derive something from `y` that aliases `x` by subtracting the offset from `y`. But that's always true, and that – I believe – is the author's point. If you view this as 'derived from', you can never satisfy any restrict guarantee on a function whose implementation you have not carefully reviewed. As for having influence: Ralf Jung has written a PhD thesis on the correctness of Rust (including formal proof that the model is sound), so I'm inclined to believe people are willing to listen to him, and rightly so.

deleted 5y ago
[deleted]
xscott 5y ago
> It takes two pointers with the extra promise that they do not alias each other. ... and then promptly uses pointer arithmetic to create an alias. It violated the promise. > If you view this as 'derived from', you can never satisfy any restrict guarantee on a function whose implementation you have not carefully reviewed. This is C, not Rust. You aren't getting proofs without careful review. You're using "restrict" in order to ask the compiler to create a faster function on the promise that it will never be used in a way that the pointers alias. It's a promise that needs to be upheld within the function and for everyone who calls the function. Think of something like `memcpy` (overlaps not allowed) vs `memmove` (overlaps allowed). The compiler can make the first one faster, and it is your job to uphold the contract. > As for having influence: Ralf Jung has written a PhD thesis on the correctness of Rust Appeals to authority aren't motivating to me. I've known and worked with a whole lot of PhDs, and they aren't always right. In fact, frequently the ones I've known are overly confident when they step outside of their area of expertise.
- dthul 5y ago
  > and then promptly uses pointer arithmetic to create an alias. It violated the promise. afaik not creating aliased pointers is not a promise you make when marking a pointer as restrict. Only when using that aliased pointer for accesses (in the presence of modifications) can you actually break the promise. To quote cppreference: "During each execution of a block in which a restricted pointer P is declared (typically each execution of a function body in which P is a function parameter), if some object that is accessible through P (directly or indirectly) is modified, by any means, then all accesses to that object (both reads and writes) in that block must occur through P (directly or indirectly), otherwise the behavior is undefined"
  - xscott 5y ago
    > Only in the presence of accesses and modifications can you actually break the promise. Ok, creating aliases you don't use is probably fine. I should've worded that more carefully. However, the example code certainly modifies the same piece of memory from two different pointers, and so it broke the promise.
    - dthul 5y ago
      Yes, I think it boils down to whether creating a derived pointer from a restrict pointer and then using both is allowed. I just had a look at the C standard and I think it is allowed if the derived pointer is (what the standard calls) "based" on the restrict pointer (page 89, 6.7.3.1 paragraph 3: http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2310.pdf http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2310.pdf). The standard language is very dense but it makes it sound like the program presented in the article would not uphold this "based" property and so might be UB as you suspected.
      - ralfj 5y ago
        The standard defines "based on" by talking about hypothetical alternative executions where the original value has a different value. In those executions, the access in question does not even happen in my program. What this goes to show is that the definition in the standard is ill-formed -- this can happen because the standard is written in English rather than a formal, mathematical language. However, I think it is quite clear that the intention of the standard is to allow my program. It would certainly allow the alternative where the `if (xaddr == y2addr) {` is removed and its body (then-branch) put directly into the main function. It makes no sense to disallow this program just because it introduces an extra condition, ergo I claim this program has defined behavior.

deleted 5y ago

[deleted]

xscott 5y ago

> It takes two pointers with the extra promise that they do not alias each other. ... and then promptly uses pointer arithmetic to create an alias. It violated the promise. > If you view this as 'derived from', you can never satisfy any restrict guarantee on a function whose implementation you have not carefully reviewed. This is C, not Rust. You aren't getting proofs without careful review. You're using "restrict" in order to ask the compiler to create a faster function on the promise that it will never be used in a way that the pointers alias. It's a promise that needs to be upheld within the function and for everyone who calls the function. Think of something like `memcpy` (overlaps not allowed) vs `memmove` (overlaps allowed). The compiler can make the first one faster, and it is your job to uphold the contract. > As for having influence: Ralf Jung has written a PhD thesis on the correctness of Rust Appeals to authority aren't motivating to me. I've known and worked with a whole lot of PhDs, and they aren't always right. In fact, frequently the ones I've known are overly confident when they step outside of their area of expertise.

dthul 5y ago
> and then promptly uses pointer arithmetic to create an alias. It violated the promise. afaik not creating aliased pointers is not a promise you make when marking a pointer as restrict. Only when using that aliased pointer for accesses (in the presence of modifications) can you actually break the promise. To quote cppreference: "During each execution of a block in which a restricted pointer P is declared (typically each execution of a function body in which P is a function parameter), if some object that is accessible through P (directly or indirectly) is modified, by any means, then all accesses to that object (both reads and writes) in that block must occur through P (directly or indirectly), otherwise the behavior is undefined"
- xscott 5y ago
  > Only in the presence of accesses and modifications can you actually break the promise. Ok, creating aliases you don't use is probably fine. I should've worded that more carefully. However, the example code certainly modifies the same piece of memory from two different pointers, and so it broke the promise.
  - dthul 5y ago
    Yes, I think it boils down to whether creating a derived pointer from a restrict pointer and then using both is allowed. I just had a look at the C standard and I think it is allowed if the derived pointer is (what the standard calls) "based" on the restrict pointer (page 89, 6.7.3.1 paragraph 3: http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2310.pdf http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2310.pdf). The standard language is very dense but it makes it sound like the program presented in the article would not uphold this "based" property and so might be UB as you suspected.
    - ralfj 5y ago
      The standard defines "based on" by talking about hypothetical alternative executions where the original value has a different value. In those executions, the access in question does not even happen in my program. What this goes to show is that the definition in the standard is ill-formed -- this can happen because the standard is written in English rather than a formal, mathematical language. However, I think it is quite clear that the intention of the standard is to allow my program. It would certainly allow the alternative where the `if (xaddr == y2addr) {` is removed and its body (then-branch) put directly into the main function. It makes no sense to disallow this program just because it introduces an extra condition, ergo I claim this program has defined behavior.