4 ms·
(co-author of the OCaml memory model paper here) The details of the 'LDRF' (local data race freedom) property are described in detail here: https://anil.recoil
by avsm 5y ago
(co-author of the OCaml memory model paper here)
The details of the 'LDRF' (local data race freedom) property are described in detail here:
https://anil.recoil.org/papers/2018-pldi-memorymodel.pdf https://anil.recoil.org/papers/2018-pldi-memorymodel.pdf
The performance numbers are in the paper abstract: "our evaluation demonstrates that it is possible to balance a comprehensible memory model with a reasonable (no overhead on x86, ~0.6% on ARM) sequential performance trade-off in a mainstream programming language". It's a little higher on PowerPC but still very usable, and RISC-V overheads should be roughly comparable to ARM.
- gadmm 5y agoAs the paper clarifies, this is for the performance of non-atomic read/writes in sequential setting. The paper left the performance evaluation for atomic read/writes to future work. Is there any indication yet regarding the performance in a parallel setting compared to weaker guarantees?
- avsm 5y agoThat's right -- we first wanted to establish that existing OCaml code wouldn't be adversely impacted. There are various efforts ongoing to build interested (locked and lock-free) concurrent data structures, so that will inform the parallel performance results. Nothing published yet.
- nextaccountic 5y agoDoes this feature inhibit any kind of optimization that current compilers could perform?
- gadmm 5y agoAccording to the paper “any compiler optimisation that breaks the load-to-store ordering is disallowed.”