4 ms·
This is interesting in that if you can use channels as described by the CSP book[1] you could build a kernel that is guaranteed to be free of concurrency bugs.
by robot 6y ago
This is interesting in that if you can use channels as described by the CSP book[1] you could build a kernel that is guaranteed to be free of concurrency bugs.
This would be important because even if you have proven the functional correctness of a kernel, that typically excludes the concurrency aspect.
[1] (https://www.cs.cmu.edu/~crary/819-f09/Hoare78.pdf https://www.cs.cmu.edu/~crary/819-f09/Hoare78.pdf)
- arianvanp 6y agoBut go doesn't provide channels in the CSP way nor does it do any model checking on it right? Like one thing it already gets wrong is that you can send mutable pointers around without clear ownership.
- sythe2o0 6y agoIf it's 'wrong' to be able to pass around mutable pointers, is the only language that is 'right' Rust? (and some Lisps maybe?)
- remexre 6y agoI think you can do "real" ownership in ATS; or check ownership with a static analysis tool in many languages, including C; and you should be able make a hacky version as a library that dies at runtime in any language with parametric polymorphism and modules. "Modern C++" too, ish. Which Lisps are you thinking of? CL and Scheme both allow having multiple copies of mutable objects.
- arianvanp 6y agoNo. For example Erlang only allows you to send immutable values around. For very good reason.
- pcwalton 6y agoIf "concurrency bugs" includes deadlocks, no, such a kernel would not be free of concurrency bugs. Any blocking receive operation on a channel can create deadlocks.
- robot 6y agoIt will be free of concurrency bugs including deadlocks. This is the promise of CSP. The requirement is data is shared only via blocking IPC and never directly using a lock. (and similarly one must not share a pointer to private data, as another poster has pointed out) You can compose small systems, even with multiple parties, prove they cannot deadlock, then make them a 'black box' with defined IO, and build larger, more complex systems with equal properties. The downside is you must guard every piece of shared data with a separate thread, but there may be ways to reduce the performance penalty.
- pcwalton 6y agoHow do you prevent process A from waiting on a receive from process B while process B waits on a receive from process A?