Use local persistent data structures for VM global tables #12640
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Here is a bench: Some developments are very slightly slower, and mathcomp got quite faster for some reason. |
SkySkimmer
reviewed
Jul 4, 2020
proux01
reviewed
Jul 5, 2020
ppedrot
force-pushed
the
vm-persistent-global
branch
3 times, most recently
from
bdfc8a6
to
6aaff98
Compare
ppedrot
force-pushed
the
vm-persistent-global
branch
from
6aaff98
to
e78911e
Compare
|
This needs an assignee. @SkySkimmer maybe? |
ppedrot
force-pushed
the
vm-persistent-global
branch
from
e78911e
to
7f80042
Compare
ppedrot
force-pushed
the
vm-persistent-global
branch
from
7f80042
to
1886b5b
Compare
|
This is more for VM people. @maximedenes ? |
github-actions
bot
added
the
needs: rebase
ppedrot
force-pushed
the
vm-persistent-global
branch
from
1886b5b
to
6dd9ce1
Compare
coqbot-app
bot
removed
the
needs: rebase
Yes, I'll take it. |
github-actions
bot
added
the
needs: rebase
ppedrot
force-pushed
the
vm-persistent-global
branch
from
6dd9ce1
to
b950f6e
Compare
coqbot-app
bot
removed
the
needs: rebase
|
@maximedenes Done. |
ppedrot
force-pushed
the
vm-persistent-global
branch
from
b950f6e
to
8a4510c
Compare
This is only used for VM slots now. Instead of an imperative hashtable, we use a similar immutable structure.
We store the VM definitions inside a persistent array for efficiency while emulating immutability.
This prevents haphazard access to the global table.
We encapsulate types that are only used internally using opaque types.
ppedrot
force-pushed
the
vm-persistent-global
branch
from
7b58b74
to
48cecd8
Compare
|
@silene done, but I insist that this is a bad idea that will have to go away at some point anyways. |
|
I am confused. Are you talking about By the way, why did you remove the error message from |
Well, there is the infamous call to
I don't remember that part. Maybe it's raised elsewhere, maybe not, let me check. |
|
Nope, indeed the error message went away. I'll reintroduce it even though it's not clear that it's complete (e.g. why don't we also fail on section variables is a mystery). Currently the checks are spread around, there are calls in tactics.ml and vernacentries.ml, I think I'll go with the latter since it's a user-facing message. |
|
@silene fixed |
But the closure does not survive the call to |
Yes. We are interleaving steps of relocation computation with VM evaluation in the same call. There used to be a frightening comment about concurrent mutation of the bytecode, which was not true anymore since we switched to a pure string API. But still, the fact that we're calling arbitrary code when trying to find indices inside a table is not very reassuring to me. |
Do we? I thought the code was first fully relocating the bytecode and then evaluating it. Even with strong normalization, there should be no reason to relocate again some already relocated bytecode. |
|
I am not sure we're talking about the same thing, we should probably discuss it more interactively at some point. |
|
CI failure is real, it's perennial trying to set a Qed definition transparent. My my, I'll tweak this to the most stupid backwards compat patch ever so that we can fix the check in a distinct PR. |
The API let the user believe that there was a way to modify the opacity status of individual constants although this was a total lie.
Some of them were outdated, some of them were in French.
This is a purely diplomatic step, my personal belief is that this is marginally worse but I will not die on that hill.
ppedrot
force-pushed
the
vm-persistent-global
branch
from
ca60f1a
to
0a0b5dd
Compare
|
Hopefully we're good this time. |
silene
approved these changes
Jan 12, 2022
|
@coqbot merge now |
|
@silene: You can't merge the PR because you're not among the assignees. |
|
@coqbot merge now |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a PR I had lying on my drive, which is a first step towards being able to dynamically change the opacity of constants in the VM (#4476, #5660). In a nutshell, this removes the use of global mutable data structures used in the VM in favour of local persistent ones.
There is still a main global entry point to the table, but eventually it should be stored immutably in the kernel environment.