3 ms·
People who aren't PL theorists understand the multicore benefits even if the retrofitting paper might be over their heads. On the other hand, the bounding data
by mbac32768 4y ago
People who aren't PL theorists understand the multicore benefits even if the retrofitting paper might be over their heads. On the other hand, the bounding data races in time and space paper/presentation is also a fairly significant change that I don't think the average dev has an easy to understand relationship with.
Anil covers it in a bit more plain English in this Signals and Threads episode. Here's a bit of the transcript, starting at about 50 minutes in:
https://signalsandthreads.com/what-is-an-operating-system/ https://signalsandthreads.com/what-is-an-operating-system/
> Ron: Do you have a pithy example of a pitfall in multicore Java that doesn’t exist in multicore OCaml?
> Anil: There’s something called a data race. And when you have a data race, this means that two threads of parallel execution are accessing the same memory at the same time. At this point, the program has to decide what the semantics are. In C++, for example, when you have a data race, it results in undefined behavior for the rest of the program, the program can do anything. Conventionally, daemons could fly out of your nose is an example of just what the compiler can do.
> In Java, you can have data races that are bounded in time so the fact that you change a value can mean later on in execution, because of the workings of the JVM, you can then have some kind of undefined behavior. It’s very hard to debug because it is happening temporally across executions of multiple threads.
> In OCaml, we guarantee that the program is consistent and sequentially consistent between data races. It’s hard to explain any more without showing you fragments of code. But conceptually, if there’s a data race in OCaml code, it will not spread in either space or time. In C++, if there’s a data race, it’ll spread to the rest of the codebase. In Java, if there’s a data race, it’ll spread through potentially multiple executions of that bit of code in the future.
> In OCaml, none of those things happen. The data race happens, some consequence exists in that particular part of the code but it doesn’t spread through the program. So if you’re debugging it, you can spot your data race because it happens in a very constrained part of the application and that modularity is obviously essential for any kind of semantic reasoning about the program because you can’t be looking in your logging library for undefined behavior when you’re working on a trading strategy or something else. It’s got to be in your face, at the point.
(and so on)
- jojohohanon 4y agoThis reminds of the worse is better debate. Specifically how the “better” crowd spent a lot of time trying to solve PCLSRing while the “worse” crowd just said: meh, throw an error and let the program figure it out. Previously https://news.ycombinator.com/item?id=20225555 https://news.ycombinator.com/item?id=20225555
- KMag 4y agoHonestly, the best of both worlds would have been to have the simple kernel implementation and put the boilerplate recovery code in the system libraries. For instance, libc's write() should handle interruption resumption, and libc should also provide a write_interruptable() (okay, appropriately shortened for the symbol limits in early linkers) to expose the raw system call in the uncommon case that the programmer wants to manually handle interruptions.
- rq1 4y agoAren’t these problems better resolved by linear types and alike? Successful implementations were made in several languages now.
- dan-robertson 4y agoI guess you still want well-defined semantics even if most users use some modes-based or other high-level api. Eg normal rust code gets to be ‘data race free’ but low level implementations of eg Arc could be racy if they were incorrect. But maybe the OCaml thing is more than just doing a good job of specifying semantics and there is some overhead in generated code because of it. I confess I haven’t looked into the details.
- tomp 4y agoCan you name a single successful implementation that can e.g. implement modern concurrent lock-free data structures without using `unsafe`?
- ghostwriter 4y agoATS has it [1], you can safely implement lock-free queues and ring buffers in it. [1] https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c3811.html https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML...