Conversation

This Tweet was deleted by the Tweet author. Learn more

Replying to

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

bill huey (hui)

Replying to

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

bill huey (hui)

Replying to

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

bill huey (hui)

Replying to

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

Replying to

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

Replying to

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

Replying to

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

bill huey (hui)

Replying to

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

Replying to

It's not something optional. In normal Rust code, you cannot break these rules. It's not something that you can accidentally bypass. The compiler guarantees that the code is memory safe including not having data races. In other cases, it helps a lot, but without guarantees.

2

1

Replying to

For example, the type system helps to avoid memory / resource leaks, since resources including memory are managed via deterministic destructors, ownership and move semantics. However, it doesn't consider leaking memory unsafe, and you can do things like making an Rc<T> cycle.

8:26 PM · Apr 18, 2019Twitter Web Client

bill huey (hui)

Replying to

Yeah, I honestly think that's one of the biggest problems with kernel, the inability to track references with any level of clarity

Replying to

Often the solution to an Rc<T> cycle would be using a weak reference via Weak<T>, which provides an `upgrade` method returning Option<Rc<T>>. It's a pure library feature, like the collections, which are all memory safe due to building on basic language features.

1