But you also support addition types of annotation I presume that could help with more extensive analysis like with shared memory structures etc ? It's a difficult problem to think through. The problems I saw with analysis were with memory allocator implementations 1/
Conversation
and streams interfaces with dynamic memory structures. Shared memory is also subject to race condition issues and other runtime scenarios that makes it difficult for static analysis. I'm sure these are well known issues but I'm a frustrated with language designer's 2/
2
notion of concurrency. It's overly simplistic. Also, last comment on this matter, I find that messaging based kernels emphasis function oriented program structures vs data oriented ones. It's makes implementation of code for shared structures obtuse here. 3/
3
In Rust, the language has a concept of types that are thread safe and can be shared, along with types that are safe to send between threads. For example, Rc<T> uses non-atomic reference counting and isn't Send. Arc<T> is a Send variant. Mutex<T> is a Sync variation of RefCell<T>.
1
1
So you can use Arc<Mutex<T>> for thread-safe shared mutable data. It also supports sharing mutable data between threads via atomics or without any synchronization at all via the standard reference safety system which enforces that mutable references do not alias anything else.
2
1
So for example you can divide up an array into non-overlapping mutable slices (pointer + length views) sent to different threads with their lifetimes constrained by the compiler to not outlive the data. It prevents data races (not higher level race conditions) in the type system.
2
1
Things like that are decent initial step but as programmer with kernel background, not picking a fight here, type systems can be abused by inexperienced programmers. Sometimes type systems aren't the most direct or sustainable way of writing that type of code
2
Linux kernel driver layers can have rather complicated nested structures. Some are a hybrid of of two subsystems like USB and ALSA (audio). Both have smaller structures inside them per each subsystems. In the case of a class compliant USB audio driver, both subsystems 1/
2
This is just a bad driver model. There's no reason for a driver to have any complex data structures or structure lifetimes. Hardware is highly finite and static.
2
The OS infrastructure using/interfacing with the drivers should be the component responsible for awareness of connections between hardware/drivers, user or kernel space consumers using the hardware, etc. and driver should have no access to these structures.
1
Rust discourages having shared ownership (Rc, Arc), but there end up being use cases for it. It just isn't the normal way to design / implement things. It's painful to use Rust if you don't design things around simple ownership models because it forces it to be verified as safe.
The code is very clean if you have unique ownership and use lots of lightweight references. If you have complex data structures, like linked data structures with cycles and mutability, you are forced into using Rc / RefCell or a similar approach which really discourages doing it.
1
So for example, if you have a nice recursive tree data structure, you can represent that with the nodes as Box<T>, which is a uniquely owned dynamic allocation. If you want to have cycles back from the children to the parent nodes, you need Rc<T> with Weak<T> for parent pointers.
1
Show replies