Valen's Memory Safety: A New Kind of Borrow Checking
verdagon.dev
  • lobsters__polywolf@crustaceanson.theshelf.topM
    1·
    26 days ago

    Last time I read https://verdagon.dev/blog/group-borrowing I was convinced that this approach works for simple structs + arrays where all fields are public, but would quickly become unwieldy for anything requiring “path abstraction” like a binary tree or linked list. Wildcard paths solve this complaint, neat! (I did not read the golden spike articles)

    Still a little nervous about “value invalidation” TOCTTOU for how this system deals with concurrency, seems shared-xor-mutable has a leg up there, but this is looking pretty nice for the single-threaded case.

    score 1 · canonical

    • lobsters__verdagon@crustaceanson.theshelf.topOPM
      1·
      26 days ago

      Thanks =) Another thing that will help with path abstraction is “associated groups/paths”, which are like associated types but for groups/paths.

      I think invalidation will work well with concurrency. The more I implement it, the more I’m discovering that invalidation and normal borrow checking are actually kind of the same thing (the difference between them lies elsewhere). So I think it’ll deal with concurrency the same way as normal borrow checking. Specifically:

      • If someone has a reference into some data that is currently being shared to another thread via structured concurrency, they won’t be able to mutate it during the structured concurrency.
      • If someone has a reference into some data that has been moved to another thread, they won’t be able to dereference it because, well, it’s been moved away.

      I’m having trouble putting it all in english, but I feel like a key here is that if a function (or scope?) has no mut effects, then it’s effectively taking an “immutable” reference. From that, all the normal shared-xor-mutable benefits apply.

      score 1 · canonical

      • lobsters__polywolf@crustaceanson.theshelf.topM
        1·
        26 days ago

        If someone has a reference into some data that is currently being shared to another thread via structured concurrency, they won’t be able to mutate it during the structured concurrency.

        This is what I’m saying: that sounds eerily similar to shared-xor-mutable :P

        It seems like one plan would be to:

        1. Define closure types that have/don’t have mut effects inside them
        2. Define structured concurrency to always take closures that don’t have mut effects inside them
        3. Define mutexes which can apply closures with mut effects without also being a mut effect externally.

        is that about right?

        score 1 · canonical