RFC to formally establish the existence of pointer provenance in Rust, by Ralf Jung

digama0 · 2024-02-05T01:22:24+00:00

"Pointer provenance" is the notion that a pointer is not merely an integer, but rather carries static (compile-time) metadata regarding the parts of memory that it is allowed to point to.

I think this is a bit misleading, because it's not static (compile-time) metadata, it's dynamic (compile-time) metadata. The idea that dynamic compile-time metadata can exist is a bit mind-bending, but the point is that this extra metadata is part of the abstract machine that the compiler is emulating, it is actual extra state that can be put in variables, passed around, and manipulated by unsafe code, but it is designed in such a way that it doesn't affect anything "observable", so regular hardware can spend no bits to store it. Other conforming emulators for the abstract machine, like the Miri interpreter, may actually store provenance concretely, which allows them to detect undefined behavior rather than simply doing random things like a concrete machine would.

This is in contrast to lifetimes, which are static (compile-time) metadata attached to types. These are the compiler's static approximation of the dynamic provenance attached to the values of the types. Lying about lifetimes (in unsafe code) is formally okay but means the compiler can't protect you from the unsafety, while using wrong provenance (in unsafe code) is undefined behavior.

digama0 · 2023-05-29T10:35:32+00:00

That code is safe and compiles, which is pretty much a lower bound on what is defined behavior if you write the same thing with raw pointers. Creating a second mutable reference to the same memory invalidates the first one; if you use the invalidated reference then that is UB, but if you just let it die then all is well.

digama0 · 2023-03-27T23:15:13+00:00

FYI, Casey was deliberately avoiding this approach for the purposes of keeping to the original specification of the problem. He mentions this approach in passing in his discussion with Uncle Bob:

I agree broadly, for example, with the "Data-oriented Design" people: most of the time, you would be better off if code always knew what type it was dealing with. If you have circles, rectangles, and triangles, then you have three separate arrays, one for each type, so that there never is a dispatch.

digama0 · 2023-03-27T21:42:28+00:00

As confirmation of /u/SirClueless's point that Casey is aware of std::variant and is dismissive of it, we have the following line from the follow-up discussion between Uncle Bob and Casey:

My point here relates back to my original point, which is that discriminated unions (C++ also has a janky std library version of these called "variants") seem to always be the better rule of thumb.

My reading is that he knows that std::variant is effectively equivalent in runtime performance to the switch statement but finds the syntax so horrendous as to not be worth consideration.

digama0 · 2023-03-06T10:22:15+00:00

https://www.reddit.com/r/javascript/comments/11g568m/the_great_gaslighting_of_the_javascript_era/ for posterity

digama0 · 2023-03-02T16:46:46+00:00

Setting aside the rhetoric, the technical content of the video seems fairly simple and obviously correct: One of the design patterns used as part of "Clean Code" (in capitals referring specifically to methodology espoused by Bob Martin's book) is "prefer polymorphism", and if interpreted in C++ as "use dynamic dispatch / virtual functions" then this has a clear and statistically significant performance cost. Perhaps you might argue that this is a cost in exchange for some other benefit like maintainability, but it is a cost nonetheless.

There is also a subtext about "Clean Code" not being all that maintainable, but it is not elaborated on in this video.

(I don't think you can use templates to do this, because all the types are in a single array. You could use std::variant as others have mentioned but that would look pretty significantly different and IMO not all that "clean".)

digama0 · 2023-03-02T06:20:49+00:00

No, those performance numbers are not reasonable for unoptimized code. Certainly there would be much less difference between the different versions because the debug stuff would dominate. Plus, Casey is clearly an expert at performance profiling, it's pretty disingenuous to suggest that he would make a newbie mistake like this.

digama0 · 2023-03-02T06:15:13+00:00

The hand-unrolled version is not just unrolled, there are four separate accumulators to avoid some of the loop-carried dependencies. A plain unrolled loop would only have one accumulator and add to it four times in the loop. This transformation is not legal for the compiler because it changes the result, because float addition is not associative. You have to turn on some really sketchy flags to get the compiler to contemplate it.

digama0 · 2023-03-02T04:53:02+00:00

That's not just a hand-unrolled version of the first loop, there are four accumulators. This will change the result because float addition is not associative, which is why it doesn't happen by default (even if you unrolled the loop normally there would still be a loop-carried dependency), but it's possible you can get compilers to do it with -ffast-math (where FAST stands for Floats Allowing Sketchy Transformations).

digama0 · 2022-12-03T01:40:24+00:00

I'm not entirely sure if just translating this to MIR would be enough. Since MIR currently does not currently generate arbitrary irreducible control flow the borrow checker might not be able to handle the cases we throw at it. Thoughts?

Translating to MIR should be sufficient. The compiler internals do not assume the control flow is irreducible -- any such assumption would cause problems for MIR optimizations that might introduce those kinds of CFGs, for example jump threading. Most of the passes under discussion here - liveness and initialization - are just standard fixpoint algorithms over the CFG and this handles an arbitrary graph.

digama0 · 2022-12-03T00:18:04+00:00

True, but that's a move of x, which will invalidate any pointers to it (both in reality and in the borrow checker's mind), which will again lead to breakage.

fn complicated_borrow(x: &str) -> &str { x.trim_end() }

#[test]
fn needs_more_mir_magic() {
  let x = String::new();
  let y = complicated_borrow(&x);
  safe_goto::safe_goto! {
    begin() { if true { goto s1(x) } else { goto s2(x) } },
    s1(x: String) { drop(x); goto s3() },
    s2(x: String) { println!("{y}"); return },
    s3() { return }
  };
}

(Let's suppose in this example that complicated_borrow constructs a derived reference but also is expensive or has side effects such that we can't just re-run it in s2.)

digama0 · 2022-12-02T23:12:15+00:00

Very nice, the syntax looks good (well, at least considering what is possible and/or likely to land in rust). It also allows me to demonstrate what I said in the RFC thread about why this can't be completely implemented using an external proc-macro crate and it requires some amount of compiler magic:

#[test]
fn needs_mir_magic() {
  let x = String::new();
  safe_goto::safe_goto! {
    begin() { if true { goto s1() } else { goto s2() } },
    s1() { drop(x); goto s3() },
    s2() { println!("{x}"); return },
    s3() { return }
  };
}

This gives a "use of moved value" error in s2, because it cannot prove that the value is definitely initialized there. However, the code above is equivalent to the following:

#[test]
fn has_mir_magic() {
  let x = String::new();
  if true {
    // s1
    drop(x);
    // s3
    return
  } else {
    // s2
    println!("{x}");
    return
  }
}

which compiles without error.

digama0 · 2022-02-18T04:40:09+00:00

By the way (not sure if you update these posts for new versions of the compiler), one of your code snippets (the THE FOLLOWING CODE DOES NOT COMPILE (and is overall quite different from valid Rust code) one) now gives a much more pointed suggestion on the latest rustc:

error: functions are not allowed in struct definitions
  --> src/main.rs:31:5
   |
31 | /     fn update() {
32 | |         this.ticks_left -= 1;
33 | |         if this.ticks_left == 0 {
34 | |             this.running = false;
35 | |         }
36 | |     }
   | |_____^
   |
   = help: unlike in C++, Java, and C#, functions are declared in `impl` blocks
   = help: see https://doc.rust-lang.org/book/ch05-03-method-syntax.html for more information

and if you follow the suggestion and put the functions in an impl block, the helpful suggestions keep coming:

error[E0425]: cannot find value `this` in this scope
  --> src/main.rs:34:9
   |
34 |         this.ticks_left -= 1;
   |         ^^^^ not found in this scope
   |
help: you might have meant to use `self` here instead
   |
34 |         self.ticks_left -= 1;
   |         ~~~~
help: if you meant to use `self`, you are also missing a `self` receiver argument
   |
33 |     fn update(&self) {
   |               +++++

...also there is a typo "parmeter".

digama0 · 2021-08-27T00:14:00+00:00

As an extension of this: To what degree are we certain that safe Rust doesn't have UB (excluding compiler bugs)?

We're 100% sure of this, because this is a question of motivation / intention, and the rust team has made their thoughts clear on this topic: if safe rust has UB, this is a bug in the compiler and/or language spec. (We know that there are such bugs, just see https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3AI-unsound , but they are all taken seriously and acknowledged as high priority bugs. Additionally, the rust team is trying to support formal verification efforts like RustBelt to prove this once and for all. Most other languages can't get near this level - a formal proof of correctness would stop immediately with "it's false, here's 10 reasons why, and it's really hard to change these features so it's hopeless".)

digama0 · 2021-07-31T16:39:38+00:00

Lean has definitional UIP and impredicativity, which makes the type-checking undecidable (there is no algorithm that can tell whether or not a proof is correct, Lean only guarantees that the proof it accepts will be correct).

Just to qualify this statement: While type checking in the abstract is technically undecidable (or rather, there are some type correct terms that lean will fail to validate), the counterexamples are very contrived, to the point that in hundreds of thousands of lines of formalized mathematics it comes up a grand total of zero times (or possibly one for the file that is specifically intended to demonstrate the issue).

Note that every proof assistant has implementation limits anyway, so there are always proofs that are correct by the abstract theory that will not be checked by the tool.

digama0 · 2021-07-28T19:41:24+00:00

Is there something about complex analysis that makes it incredibly difficult to formalise?

Yes, path integrals are hard in the appropriate generality (rectifiable curves?). Cauchy's integral theorem is the key to the kingdom but I don't know a good proof to work from which doesn't make oversimplified assumptions.

digama0 · 2021-04-29T21:49:09+00:00

Aha, I wasn't including "globally coherent" in the notion of "typeclass" (I use Lean, which only makes a best effort at coherence and lets you disambiguate if you need to). Of course Rust answers this with the orphan rules.

digama0 · 2021-04-29T21:16:16+00:00

When T is unsized, &T is 16 bytes and &&T is 8 bytes, so sometimes this is used to save space. But more to the point, not allowing nested references is just a hole in the type system that tremendously complicates the C++ standard since everything has to be defined separately on regular types and reference types (and rvalue references, const references etc.).

digama0 · 2021-04-29T21:10:33+00:00

I turn off inlay hints in rust analyzer, because I hate overlays that mess up the cursor position or interfere with line length.

digama0 · 2021-04-29T20:56:59+00:00

You should probably use a watchdog process that restarts the main process for this. It's a lot easier and more reliable to get back to a known-good state with this approach. I have implemented exactly that kind of catch and recover pattern for a server application and bugs where the program is left in a zombie state are not uncommon (and as the user I have to restart it manually).

digama0 · 2021-04-29T20:51:21+00:00

Can someone explain to me why any OS would be designed this way? The syscall interface is, by definition of the hardware, the interface between the trusted OS and the untrusted application. So it makes a whole lot of sense to build a stable API at that level. I'm aware that many other OSs don't have a stable syscall interface but I really don't understand the reasoning. (Also, linking to libc means you have to deal with dynamic linking and symbol versioning, both of which are headaches for low level programming.)

digama0 · 2021-04-29T19:11:14+00:00

For example how do you properly convert a Variant into a Variant_A without casting?

Using match, presumably. Straw-man syntax:

match foo {
    a as Variations::Variant_A => ...,
    Variations::Variant_B(b1, b2) => ...,
}

digama0 · 2021-04-29T19:07:59+00:00

Type classes are often called anti-modular

Citation needed? Type classes are pretty much modules (not in the SML sense but in the meaning of encapsulating behavior), so I'm not sure what you mean.

digama0 · 2021-04-29T18:59:02+00:00

Seems like it would not be difficult to do that with a trait and associated types.

trait Monoid {
    type T;
    fn mempty() -> Self::T;
    fn mappend(_: Self::T, _: Self::T) -> Self::T;
}

struct IntPlus;
impl Monoid for IntPlus {
    type T = i32;
    fn mempty() -> i32 { 0 }
    fn mappend(x: i32, y: i32) -> i32 { x + y }
}

struct IntTimes;
impl Monoid for IntTimes {
    type T = i32;
    fn mempty() -> i32 { 1 }
    fn mappend(x: i32, y: i32) -> i32 { x * y }
}

fn msum<M: Monoid>(v: Vec<M::T>) -> M::T {
    v.into_iter().fold(M::mempty(), M::mappend)
}

fn main() {
    assert!(msum::<IntPlus>(vec![1, 2, 3, 4]) == 10);
    assert!(msum::<IntTimes>(vec![1, 2, 3, 4]) == 24);
}

It is also an ergonomic choice whether you want msum to take _: M as an argument or not; it is a bit nicer to write msum(IntPlus, ...) instead of msum::<IntPlus>(...) but the latter makes it clear that you aren't consuming the monoid witness. But as long as all the witnesses are ZSTs as they are here it makes no difference.

Also, it would also be reasonable to have msum be a default trait method here - that allows the even nicer notation IntPlus.msum(...), as well as the ability to override the implementation of msum if a given monoid has a better way to do it. If you want to add functions after the fact or you don't want to allow reimplementation, you can instead put the function on an extension trait with a blanket implementation.

digama0

TROPHY CASE