diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-11 11:27:15 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-11 11:27:15 +0200 |
commit | 16dec9697b06a7fbda0997ab0685ef24443c7d3a (patch) | |
tree | 1f85ee8f06535198d402ef9879883f3225291e6b /lib/heap.ml | |
parent | 35c36f80dcc1e61e3dae8bcce1da71b384904582 (diff) |
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
Diffstat (limited to 'lib/heap.ml')
0 files changed, 0 insertions, 0 deletions