volta83

13 ms·

61.
by volta83 5y ago
> You're ignoring the case of a list being densely packed and embedded inside another data structure. No, I am not. This conversation is exclusively about non-intrusive doubly-linked lists. If you want to have a conversation about i
62.
by volta83 5y ago
Most of the unsafe code in libcore is proved in Iris. Some of the unsafe code in the standard library also. Some parts of crossbeam have pencil&paper proofs documented.
63.
by volta83 5y ago
> That O(1) splice must also be accompanied with an iteration. I don't think it necessarily must, but it tends to be. People tend to keep pointers to elements of the list all over the place, so if you have the right 3 pointers (bein
64.
by volta83 5y ago
Before I delve more, are you talking about `rotate` ? https://en.cppreference.com/w/cpp/algorithm/rotate Is that what you want?
65.
by volta83 5y ago
I've look at the literature every couple of years, and to the best of my knowledge, there is no paper proving that a subset of the Linux kernel RCU apis are sound. If you are aware of one, I am intrinsically interested in this topic.
66.
by volta83 5y ago
> I think you are not using 'proof' in the way that most people would understand it. I have corrected many math exams of students over the years. A "significant" amount of the "proofs" provided by the studen
67.
by volta83 5y ago
> You could technically interpret it as you did, but only a contrarian would do that. Or you could have been more clearer. I didn't intend any animosity, but you clearly do. > If you want more people to support rust I don't
68.
by volta83 5y ago
In C++, you have `std::optional<T>`. That's a type that either contains a `T` or contains nothing. In C++, sizeof(optional<T>) > sizeof(T) because the discriminat has to be stored somewhere. This is true even if, e.g., y
69.
by volta83 5y ago
> `unsafe { ... }` means "I hope you are convinced by my arguments in the surrounding comments, or better still in my POPL21 paper, that this is correct". I disagree here (and that's ok). The unsafe keyword tells Rust &quo
70.
by volta83 5y ago
> It is more like providing an "axiom" as the compiler won't be able to check it and instead has to assume that it true. I don't think one should see this as an axiom, although as you mention one could. If your unsafe
71.
by volta83 5y ago
You mentioned changing the order of two elements in a list, such that one comes after the other. With a vector of pointers to the elements (C++ std::vector<T*>) this can be easily done in O(1) as I explained above. If now that I'
72.
by volta83 5y ago
> Adding an unsafe block around a call to C code doesn't prove anything. I didn't say otherwise. What I said is that writing unsafe code is writing a proof that the code is correct. If the proof is incorrect, the behavior is un
73.
by volta83 5y ago
> I'm really tired of this motte and bailey stuff. Rust proponents say Rust gives you fine grained machine control and safety with no performance compromises, and then when you point out that the language doesn't quite live up
74.
by volta83 5y ago
> If you want good performance but don't care about precise control over the machine, write Java or C# or something high level like that. You'll be just as safe No, you aren't. None of these languages catch data-races, so
75.
by volta83 5y ago
> Would anybody use a doubly-linked list if they care about performance? That's probably the only reason to use them. If you don't care about performance there are simpler data-structures available. If you need to implement an
76.
by volta83 5y ago
SeL4 is not the Linux kernel and it doesn't use RCU. So yes, there is a correctness proof for a completely different operating system that does not use the one thing we are talking about here.
77.
by volta83 5y ago
TBH, while I can think of many layout optimizations that Rust does and C does not, I can't think of any that C or C++ do that Rust does not. In particular when it comes to unions which are heavily used in low-level code, Rust does opti
78.
by volta83 5y ago
I've also heard your claim many times, and every time I checked, replacing a doubly-linked list with something else improved performance by orders of magnitude. Particularly in video games. --- > The end result is that I now have th
79.
by volta83 5y ago
> The whole point is that the same thing (creating safe abstractions over unsafe code) is what developers have been doing with C for close to half a century. They have been trying to do this, but it doesn't work because C's sup
80.
by volta83 5y ago
> Lets say I have pointers two elements A and B in the list. I now want to say that B should come after A, I can do this easily in O(1) time with this with no overhead and all references sees this update instantly. You can do this with a
81.
by volta83 5y ago
The premise that Rust does not intend to replace C and C++ is not true. Rust is designed to mesh with existing C and C++ code bases well, which is why many large projects support writing code in Rust (Chrome, Firefox, Linux, Windows, etc.).
82.
by volta83 5y ago
The question is fair. Why would you want to use a non-intrusive doubly-linked list? AFAIK there is only one answer: you have very big objects and you need O(1) splice. If you don't have very big objects, or you don't need O(1), pr
83.
by volta83 5y ago
> The additional refcount takes space that could be used for the payload that now either needs to spill into the next cacheline or needs to be compressed further. It could, but since the cachelines are adjacents the prefetcher will pull
84.
by volta83 5y ago
> Also note that the author of the article is the actual inventor of RCU. I know, so? > On the other hand the author is probably saying that the kernel RCU C API itself has been proven correct, But this is not true right? There is no
85.
by volta83 5y ago
I know. So? How does that change anything? A doubly-linked list is already space inefficient, it adds 2 pointers per element. Using Rc + Weak adds one extra word per element to store the two (strong and weak) refcounts. So for a 64-bit type
86.
by volta83 5y ago
> You can, but not without introducing runtime overhead relative to C and C++, e.g., by forcing reference-counting where none would be necessary in C. The runtime overhead is minimal. 96% of it comes from the pointer indirection in the l
87.
by volta83 5y ago
> My take is that Rust is proposed based on the value proposition of its Safe Rust feature, but in the Linux kernel that feature has limited use. Where does your take come from? Everyone I've heard of proposing Rust for the Linux ke
88.
by volta83 5y ago
Using unsafe is like providing a "proof" that the code you write won't cause safe Rust to exhibit undefined behavior. Writing unsafe requires a certain degree of skill, because one needs a deep understanding about what guaran
89.
by volta83 5y ago
Arguably, that's just too hardcore. You can implement doubly-linked lists in safe Rust by using Rc and Weak, Option, and RefCell (or Arc and Mutex for a safe concurrent doubly-linked list). Learning about safe Rust is gentler and more
90.
by volta83 5y ago
> Given that DEC Alpha famously had difficulty with RCU, it is only reasonable to ask how Rust will do with it. > Including some wild speculation about how Rust's ownership model might be generalized I recommend starting with th

More ›