4 ms·

> Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc/borrow sense. Those are somewhat equivalent. I'd like to have static

by klabb3 2y ago

> Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc/borrow sense. Those are somewhat equivalent. I'd like to have static deadlock analysis in Rust. If you had that, I think you could get safe back-pointers, too. If you can prove that all borrow and upgrade calls can't fail, you can eliminate most reference counts. That gives you free interior mutability when that's possible. I’m not a formal verification guy, but I don’t think locks in the traditional sense is helpful. No compiler will give you anything useful to work with wrt locks. You just accept and live with the danger. In fact, locks and ref counts are runtime constructs in Rust. Imo it “goes against” even Rust’s own strong principles of single ownership - these things are shared mutable state. Arc broke Rusts RAII model so much that they had to remove scoped threads (which needs destructors to run before end-of-scope). Anyway, rust aside. Global refcounts have cyclic and leak issues that again are global. I don’t think we can necessarily get rid of them, but I do believe containing them is better, eg with arena-style scoping. As for locks my gut feeling is we need an asymmetric data structure, for instance a channel. In eg Go you can break a channel into sender and receiver, and have the sender goroutine do `defer close(ch)` which is guaranteed to run if the rest of thread finishes, even if there’s a panic. Doesn’t necessarily have to be channels but separating the roles (reader-writer / producer-consumer) is much easier to reason about, and that probably helps formal analysis too.

zozbot234 2y ago
Scoped threads have been reintroduced to Rust since ver 1.63, released in August 2022. There's also significant interest in introducing true linear types to Rust, where destructors would be guaranteed to run - however the changes required for that are large and will probably have to be introduced in a new Rust edition.
- the_mitsuhiko 2y ago
  > however the changes required for that are large and will probably have to be introduced in a new Rust edition. Or more likely: never. The odds of linear types making it into the language are non existing from what I can tell.
  - CooCooCaCha 2y ago
    Unfortunately rust language development has practically ground to a halt. There is a trickle of work but it’s highly unlikely that major language features will happen any time soon.
    - estebank 2y ago
      I'm not sure what you mean. There are fewer flashy announcements for things that block people, but development continues unabated, with large refactors that enable things that weren't possible before. Things like Return Position Impl Trait In Traits, Derefs in patterns, a new trait system checker, enhancement to const eval, generators and that's just of the top of my head. Not everything is gonna land soon, but development is happening. The major language feature work is happening, they just are large enough or contentious enough that stabilizing them will take time.
      - CooCooCaCha 2y ago
        Oh please, they’ve landed a few nice things but larger items like generators are likely not coming soon. Just look at the async roadmap for example, how many years has it been and how much progress has been made? As someone who is firmly in the Rust community it’s annoying how everyone seems to know this but you can’t fucking talk about it. I can’t tell you how many times I’ve seen passive aggressive comments like “this would be much easier if we had variadics… maybe someday”
        estebank 2y ago
        > landed a few nice things but larger items like generators are likely not coming soon. Generators got blocked on settling AsyncIterator/Stream. The work for it is happening. It's taken too long, but not because people are sitting on their thumbs. > Just look at the async roadmap for example, how many years has it been and how much progress has been made? Hard things are hard and take time. > As someone who is firmly in the Rust community it’s annoying how everyone seems to know this but you can’t fucking talk about it. You can say whatever you want to say, everyone can. But expect pushback from the people pulling the cart when you state that the cart isn't moving just because it isn't moving as fast as you want in the exact direction you want. Just take a damn glance at the review queue, or even the release notes. A ton of work is being done, of different levels of difficulty and the things that aren't stabilized quickly is because they have research-level open questions. > I can’t tell you how many times I’ve seen passive aggressive comments like “this would be much easier if we had variadics… maybe someday” I don't know why you read that as passive-aggressive, but I certainly see your reply as dickish.
- klabb3 2y ago
  > Scoped threads have been reintroduced to Rust Right, but those are a mere shadow of what they used to be, which was JoinHandle with a lifetime parameter. You can’t build a thread pool or async runtime with static borrowing across tasks, which makes the use case very narrow. > There's also significant interest in introducing true linear types to Rust, where destructors would be guaranteed to run I’m glad to hear that. I’ve always hoped it’s possible to introduce non-breaking through a new auto trait but there are many delicate details around unwinds and such that may be gnarly. As well as an accumulated dependence on Arcs in library code.
Animats 2y ago
> I’m not a formal verification guy, but I don’t think locks in the traditional sense is helpful. No compiler will give you anything useful to work with wrt locks. You just accept and live with the danger. Deadlock analysis is well understood. You have to prove that locks get locked in the same order regardless of the path taken. That can be easy or hard. In many cases, if you have the call graph annotated with where locks are set and cleared, you can try to prove that the program is deadlock-free. I'd like to see Rust tools to help with that.
- klabb3 2y ago
  Right, but that’s a global property of everything that uses the lock, so if you’re writing a library you'd have to run the analysis against real or synthetic call graphs. Plus it’s very easy to accidentally break that property if you’re not using it in an analysis-friendly way, no? Instead, role-separated data structures like eg channels, run-once-functions and atomic value swaps can - due to their constraints - make them harder to use in ways that break analysis, and can be analyzed locally. Say eg my library is acting as a producer. Ideally I can check that I am producing 0-N items and that it closes the channel. Analyzing the consumer can be deferred and decoupled, which is good because it may not exist yet.

by klabb3 2y ago

zozbot234 2y ago

Scoped threads have been reintroduced to Rust since ver 1.63, released in August 2022. There's also significant interest in introducing true linear types to Rust, where destructors would be guaranteed to run - however the changes required for that are large and will probably have to be introduced in a new Rust edition.

the_mitsuhiko 2y ago
> however the changes required for that are large and will probably have to be introduced in a new Rust edition. Or more likely: never. The odds of linear types making it into the language are non existing from what I can tell.
- CooCooCaCha 2y ago
  Unfortunately rust language development has practically ground to a halt. There is a trickle of work but it’s highly unlikely that major language features will happen any time soon.
  - estebank 2y ago
    I'm not sure what you mean. There are fewer flashy announcements for things that block people, but development continues unabated, with large refactors that enable things that weren't possible before. Things like Return Position Impl Trait In Traits, Derefs in patterns, a new trait system checker, enhancement to const eval, generators and that's just of the top of my head. Not everything is gonna land soon, but development is happening. The major language feature work is happening, they just are large enough or contentious enough that stabilizing them will take time.
    - CooCooCaCha 2y ago
      Oh please, they’ve landed a few nice things but larger items like generators are likely not coming soon. Just look at the async roadmap for example, how many years has it been and how much progress has been made? As someone who is firmly in the Rust community it’s annoying how everyone seems to know this but you can’t fucking talk about it. I can’t tell you how many times I’ve seen passive aggressive comments like “this would be much easier if we had variadics… maybe someday”
      - estebank 2y ago
        > landed a few nice things but larger items like generators are likely not coming soon. Generators got blocked on settling AsyncIterator/Stream. The work for it is happening. It's taken too long, but not because people are sitting on their thumbs. > Just look at the async roadmap for example, how many years has it been and how much progress has been made? Hard things are hard and take time. > As someone who is firmly in the Rust community it’s annoying how everyone seems to know this but you can’t fucking talk about it. You can say whatever you want to say, everyone can. But expect pushback from the people pulling the cart when you state that the cart isn't moving just because it isn't moving as fast as you want in the exact direction you want. Just take a damn glance at the review queue, or even the release notes. A ton of work is being done, of different levels of difficulty and the things that aren't stabilized quickly is because they have research-level open questions. > I can’t tell you how many times I’ve seen passive aggressive comments like “this would be much easier if we had variadics… maybe someday” I don't know why you read that as passive-aggressive, but I certainly see your reply as dickish.
klabb3 2y ago
> Scoped threads have been reintroduced to Rust Right, but those are a mere shadow of what they used to be, which was JoinHandle with a lifetime parameter. You can’t build a thread pool or async runtime with static borrowing across tasks, which makes the use case very narrow. > There's also significant interest in introducing true linear types to Rust, where destructors would be guaranteed to run I’m glad to hear that. I’ve always hoped it’s possible to introduce non-breaking through a new auto trait but there are many delicate details around unwinds and such that may be gnarly. As well as an accumulated dependence on Arcs in library code.

Animats 2y ago

> I’m not a formal verification guy, but I don’t think locks in the traditional sense is helpful. No compiler will give you anything useful to work with wrt locks. You just accept and live with the danger. Deadlock analysis is well understood. You have to prove that locks get locked in the same order regardless of the path taken. That can be easy or hard. In many cases, if you have the call graph annotated with where locks are set and cleared, you can try to prove that the program is deadlock-free. I'd like to see Rust tools to help with that.

klabb3 2y ago
Right, but that’s a global property of everything that uses the lock, so if you’re writing a library you'd have to run the analysis against real or synthetic call graphs. Plus it’s very easy to accidentally break that property if you’re not using it in an analysis-friendly way, no? Instead, role-separated data structures like eg channels, run-once-functions and atomic value swaps can - due to their constraints - make them harder to use in ways that break analysis, and can be analyzed locally. Say eg my library is acting as a producer. Ideally I can check that I am producing 0-N items and that it closes the channel. Analyzing the consumer can be deferred and decoupled, which is good because it may not exist yet.