-
Notifications
You must be signed in to change notification settings - Fork 68
Safety of Stdlib under Multicore OCaml
What guarantees should Multicore OCaml provide when multiple domains concurrently use stdlib functionality?
Even with parallelism support, the majority of programs in OCaml will still be sequential. Hence, Multicore OCaml will not make the stdlib thread-safe by default as this would introduce overheads even for sequential programs.
For parallel programming, Multicore OCaml stdlib provides low-level interfaces such as the Atomic, Domain, Mutex and Condition modules, but we expect the users to utilise a higher-level library such as Domainslib. This is similar to the choice made by Java to have the parallel programming functionality under java.util.concurrent package.
OCaml encourages the use of mutability using ref cells, mutable record fields, and arrays. For parallel programs using such non-atomic mutable values, Multicore OCaml also ensures DRF-SC property -- any data race free program will have sequential consistency semantics. But given the need to preserve memory-safety in OCaml, unlike C++, and similar to Java, even racy programs have well-defined semantics that preserves memory-safety.
Consider the Queue module from stdlib. The queue is a mutable structure, and the documentation says that module is not thread-safe and must be protected with a Mutext.t. Failure to do so will lead to a crash (= segfault?). Multicore OCaml would aim to strengthen the guarantee such that the program will not crash. But lost updates and inconsistent internal states leading to unexpected results are still possible if two domains concurrently access the queue. (XXX KC: I don't think the current queue implementation as is can crash with multiple domains).
Another good example is the Lazy values. Lazy values are used to memoize expensive computations. They are implemented with unsafe features from the Obj module in stdlib. The lazy value implementation also non-trivially interacts with the GC marking activities. Using the stock OCaml version of Lazy under multiple domains would lead to crashes. To this end, Multicore OCaml has a new implementation of Lazy that does not crash when used with multiple domains.
Similarly, weak arrays and ephemerons have been re-implemented to be memory-safe, but one may observe non-trivial behaviours when weak arrays and ephemerons are updated concurrently by multiple domains due to the concurrent GC. It is recommended that weak arrays and ephemerons are properly synchronised using a Mutex.t if they need to be used with multiple domains.
Some stdlib functionality appear pure from their interfaces but may use global state to implement them. For example, Format module internally uses a queue for producing the formatted string. This causes an unexpected exception when Format.printf is used with multiple domains. Multicore OCaml will ensure that Format module will be thread-safe since the interface is observationally pure; the interface does not return a shared mutable value unlike say the queue module which returns the mutable queue. There are similar issues around Random and Filename.temp_file, which Multicore OCaml will make observationally pure.
Issues related to stdlib safety are tracked under a separate stdlib safety label.