The Cyclone papers I gave you were evidence of precisely that. C lacks the syntax to guarantee that borrowed references are valid, but through extending C to support annotating references with lifetimes, static analysis could make guarantees about the lifetimes of their data.
Conversation
This Tweet was deleted by the Tweet author. Learn more
My entire point is that static analysis works much better when it's supported by the type system / language. External static analysis is greatly enhanced by a language providing stronger static guarantees that making code easier to analyze. It's easy to think about and evaluate.
2
1
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/
1
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
The ownership and move semantics mean you can send a type like Vec<T> (where T is also Send) between threads in safe code without copies. The vast majority of types are both Send and Sync. Can also share lightweight references across them via APIs where they get properly bounded.
1
1
The compiler enforces that &T does not outlive what it points out, which extends to other things like iterators (it prevents iterator invalidation), etc. &T can also guarantee immutability. &mut are non-aliasing mutable references. RefCell / Mutex are dynamically checked instead.