4 ms·

Could you explain (in simple terms if possible) how the Multicore OCaml achieves a memory model which is much simpler on more efficient than in Java or C (menti

• jlouis 5y ago
  The key problem is program transformation, and in particular optimizations. Different CPUs/ISAs, and compilers, might want to transform your program to make it run faster. However, in the multi-core setting, data races pose bounds and limits on how much you can trigger those optimizations. The program doesn't generally execute sequentially in a way that can be entirely reasoned about. Instructions might be reordered for the sake of the program to run faster. Programmers can't work with that. So one proposes a memory model. Follow these rules, and our optimizations won't alter the behavior of the program. They kind-of describes what happens "in between" the critical sections of the program, hence the lack of a mutex mention. The paper presents a local property and then shows, formally, that this property is enough to guarantee an efficient memory model. That is, a model in which you can perform optimizations, while programmers can still reason about the programs behavior. The crux of the paper is that the property is local. This is new, because memory models which came before it are global: to reason about correctness, you have to consider the whole program, rather than consider a small (local) subset. OCaml requires more safety than most programming languages, so this is good for the fact that you can now compose local fragments of OCaml programs, without having to worry about a global safety property. The property is also simpler for programmers to reason about. The way you "use" the paper is that you adapt your optimizations to follow the property, and you make sure that the virtual memory model is implemented the same way on different architectures. Finally, the examples: they explore the idea of a local reasoning. In particular, they show why the (existing) global properties fail if you view them under the stronger requirement of local reasoning. It's the setup for the paper, since it means you can't just use the existing models. They need to be adapted if you want a more localized property.
• kcsrk 5y ago
  (One of the authors of the mentioned paper [1]) Firstly, if you are using high-level synchronisation mechanisms such as mutexes and condition variables, or higher-level concurreny libraries such as java.util.concurrent, you shouldn't worry about the memory model. C++, Java and OCaml ensure that properly synchronised programs do not exhibit surprising behaviours. Such programs have sequentially consistent semantics i.e, the observed behaviour is one of the permitted interleavings of the threads in the program. Rust inherits C++ memory model [2], but if you are using the safe subset, then you will never have to think about it. Memory model is important only to those who write the concurrency libraries. If you are still keen, read on. The OCaml memory model is certainly simpler than the C++ and Java memory model, but being more efficient is not one of our goals. C++ memory model permits a partially-ordered lattice of stronger memory accesses starting from access to non-atomic memory locations to sequentially consistent access with increasing cost as you move up the lattice. OCaml memory model only provides two -- atomic and non-atomic, representing approximately the top and the bottom of the lattice. OCaml memory model is also stronger than Java in that our data races are bound not-only in space like Java (data races on certain variables don't affect behaviours on other variables) but also in time (surprising behaviours stop affecting the program after the race ends unlike Java; see example 2 from [1]). This permits modular reasoning of racy and non-racy parts of the program which is not the case with C++ and Java. The catch is that we have to disallow load-to-store reordering to get the stronger guarantees. Relaxed memory models such as ARM and Power do in fact permit these reorderings, and we have to compile OCaml code (including sequential one) such that the load-to-store reordering is disallowed. This can be done fairly cheaply. It is free on x86 which doesn't perform load-to-store reorderings, and has a small cost (up to 3%) on ARM and Power architectures whose memory models permit load-to-store reorderings. [1] https://kcsrk.info/papers/pldi18-memory.pdf https://kcsrk.info/papers/pldi18-memory.pdf [2] https://doc.rust-lang.org/nomicon/atomics.html https://doc.rust-lang.org/nomicon/atomics.html
  • troutwine 5y ago
    > Rust inherits C++ memory model [2], but if you are using the safe subset, then you will never have to think about it. Small correction, atomics are part of the safe subset of Rust. At a certain point it's important to have a work-a-day knowledge of the memory model with regard to atomic numerics. Dealing with allocated types, now, that's a whole different area and is specialized knowledge.