Stream: Coq devs & plugin devs

Topic: Issue with universes in VM


view this post on Zulip Matthieu Sozeau (Apr 05 2024 at 16:14):

Dear devs, I'm nearing completion of a first version of algebraic universes everywhere in this PR: https://github.com/coq/coq/pull/18903

Even after rebasing I'm still hitting an issue with vm_compute, which I probably badly adapted to the move from only levels in instances to arbitray universes. Could someone knowledgeable help? @Pierre-Marie Pédrot or @Guillaume Melquiond I'm looking at you :)

view this post on Zulip Matthieu Sozeau (Apr 05 2024 at 16:14):

The issue can be reproduced by running bug_7723.v

view this post on Zulip Matthieu Sozeau (Apr 05 2024 at 16:16):

Other than that, I have a seemingly non-terminating Nia.v coqchk and float/specs.v takes ages, I'm a bit surprised that universes would be involved in that one.

view this post on Zulip Matthieu Sozeau (Apr 05 2024 at 16:16):

The rest of the test-suite passes

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 16:35):

there's a "todo fix MS" in vmbytegen, possibly the reason

view this post on Zulip Matthieu Sozeau (Apr 05 2024 at 19:54):

Precisely, I don’t know how to fix it

view this post on Zulip Gaëtan Gilbert (Apr 05 2024 at 20:11):

I guess you need to do something like in the Lsort case
it looks like structured constant Sort can be applied to an instance somehow? I don't understand how that would work so maybe not

view this post on Zulip Matthieu Sozeau (Apr 05 2024 at 20:12):

Yep it looks like it but I don’t know the code well enough

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 06:16):

If you describe what the algorithm for computing universes is, then I can guide you about coding it in the VM. Currently and roughly, an instance is just an array that is received and passed as part of the first argument (assuming polymorphism). When calling a function, a fresh array is built and every cell of it is either a straight copy of a cell from the instance received in argument or a global universe that is independent of the instance.

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 06:18):

What changed is that now the elements of the array are no longer just levels but structured algebraic universes (lists of levels + int increment), so I suppose there is something to perform to go under this structure

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 06:28):

Presumably, we could replicate what is done for the Sort atom here for each universe in the instance, where it seems to be compiled as a kind of closure (fun univ_inst -> Sort (univ)) and uses subst_instance_sort (in vmvalues.ml, L322) to get the instantiated sort

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 07:00):

I don't follow. Let us consider a simple case: Definition foo@{u1...} := bar@{u2...}. In your new system, what is the difference between u1 and u2 and how do you transform u1 into u2?

view this post on Zulip Gaëtan Gilbert (Apr 06 2024 at 07:07):

the difference is that we can write Definition foo@{u1 u2} := bar@{max(u1,u2+1)}

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 07:08):

Does max have some computational content here, or is it just an unevaluated pair?

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 07:09):

(And what about +1?)

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 07:17):

+k is a constructor basically, but sup does have some computational content: Universe.sup Set i = i and Universe.sup i j = Universe.sup j i (where = is value equality at the ML level). Universes implement this as a quotient, every call to sup sorts the resulting level + increment list, and Set is a unit for sup. max() represents the resulting supremum. When substituting we use sup to keep the representation canonical

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 07:21):

Is the canonicization something that needs to be performed at computation time (e.g., because universes would fill up memory otherwise), or does it matter only when leaving the VM?

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 07:22):

We could leave it to readback I think

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 07:23):

It's probably better to do it when testing for cumulativity. But for pure reduction I don't think it will matter much

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 09:10):

So, from a computational point of view, you only need the following primitives: 1. load the content of the k-th cell from the input instance array, 2. create a tagged tuple of arbitrary size (to denote either a maximum or a successor), 3. create an instance array. (And 1 and 3 already exist and are unchanged.) As far as I understand, you never need to perform any computation on those things; they are completely opaque and you only need to pack them together. Am I right?

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 09:18):

Yes, there’s no “elimination” form, they are just passed around and substituted

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 09:19):

Essentially I can think of the encoding of the tagged tuple as in the usual ML value representation of blocks (I know about the native one not the bytecode one)

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 10:00):

They are essentially the same. After all, they have to be, since the OCaml runtime, especially the GC, has no way to distinguish between native OCaml values, and those created by the VM. Moreover, it would be painful to feed values to the VM and to recover them from it, if they were not actual native OCaml values.

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 10:18):

In a nutshell, the VM is a one-register stack machine. For example, to create a three-field tuple which would end up in the register, the sequence of code would look like:

code_for_last_field...; Kpush;
code_for_middle_field...; Kpush;
code_for_first_field...; Kmakeblock (3, tag)

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 10:32):

Thanks, that should be enough info to get going!

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 10:42):

There is one peculiar thing you need to be aware of. You will see that lots of functions in the bytecode generator have a penultimate argument named sz. It corresponds to the number of elements that will be pushed on the stack by subsequent code. This information does not impact in any way the code generation, but it is critical since it is there to prevent buffer overflow. (In other words, if you get its computation wrong, your code will seem to work but it will silently corrupt memory.) So, you have to increase sz by the number of Kpush you are about to do. For example, in the sequence above, the code for computing the last field should be invoked with sz+2, while the code for the first field would just use sz.

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 10:43):

A function like comp_args takes care of those details for you.

view this post on Zulip Gaëtan Gilbert (Apr 06 2024 at 10:57):

maybe we should say that instances accumulate the instance to be substituted by (except for constant instances which accumulate nothing), like how sorts work, instead of working at the level of the instance elements
then I guess Vmvalues.uni_instance becomes something like fun v -> match whd_accu v [] with Vaccu (Ainstance u, []) -> u | _ -> assert false (mutually recursive with whd_accu)

view this post on Zulip Matthieu Sozeau (Apr 06 2024 at 11:00):

That may be simpler indeed

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2024 at 11:18):

This information does not impact in any way the code generation

Actually, it does, some instructions need it to know where they live relatively to the function frame.

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 11:25):

Oh right. How could I forgot about local variables...

view this post on Zulip Guillaume Melquiond (Apr 06 2024 at 11:26):

So, a miscalculation would presumably have very noticeable effects then.

view this post on Zulip Matthieu Sozeau (Apr 07 2024 at 16:52):

Actually I take back what I said before, there is computational content in universe substitution, as when you substitute u by i+1 in u+2 you should get i+3

view this post on Zulip Matthieu Sozeau (Apr 07 2024 at 16:53):

I don’t know if it is more sensible to implement it as Gaëtan suggest or really generating the bytecode for that calculation

view this post on Zulip Gaëtan Gilbert (Apr 07 2024 at 19:03):

I think the idea was to generate something like

type univ = Const of Universe.t | Max of univ * univ | Incr of univ * int

in the vm and normalize in readback

view this post on Zulip Matthieu Sozeau (Apr 08 2024 at 15:57):

That’s possible as well, indeed. With the help of Pierre-Marie, we devised a different compilation scheme that’s maybe more modular and efficient: at universe instance construction time we use a new instruction to make a universe out of arrays of universes and increments. The instruction calls back OCaml’s Univ.Universe primitives to get the canonical form.

view this post on Zulip Matthieu Sozeau (Apr 08 2024 at 15:59):

The PR now passes the test-suite, with a surprising slowdown in primfloats/specs.v The code I wrote is not optimized at all, on purpose ;)

view this post on Zulip Guillaume Melquiond (Apr 08 2024 at 16:23):

Are you talking about SpecFloat.v? There should be no occurrence of Type in that file. Everything should be living in Set. Or does Set no longer exist?

view this post on Zulip Guillaume Melquiond (Apr 08 2024 at 16:27):

Oh, sorry. I guess you are talking about primitive/float/specs.v.

view this post on Zulip Matthieu Sozeau (Apr 08 2024 at 16:31):

Yep

view this post on Zulip Guillaume Melquiond (Apr 08 2024 at 16:35):

It does contain some large lists living in Type, so I guess it generates a few hundreds of thousands of constraints, if not careful.


Last updated: Oct 13 2024 at 01:02 UTC