https://github.com/ocaml/ocaml/pull/10831
I guess the obvious place to try it is the STM. IIRC there were some changes/cleanups to the STM that we wanted to carry out first however? Do we have any other places it might be applicable?
The STM can't profit from this without a rewrite, and there are other parts of Coq that would need significant work too due to global shared state.
But there is a much more pressing problem, and it is that VM / native won't work in 5.0 at all.
Coq, with those disabled, seems to work fine for now on the limited testing multicore devs have done in my multicore branch
Why would VM not work with OCaml 5.0?
It requires some changes w.r.t. closure representation IIRC
speaking of the VM, while I have your attention @Guillaume Melquiond https://github.com/coq/coq/pull/12640 was discussed at the last weekly call but you weren't there
My opinion has not changed. State threading is an awful paradigm and it has been a never-ending source of bugs in Coq already.
yes, but this is not the goal of the PR
As for the change to closure representations, it was performed a few years ago already.
the goal of the PR is to be able to make the VM state local and persistent
Yes, but you are doing it using state threading and I cannot agree to it.
pff
if I use a reference passing will you agree to merging it ASAP?
this stuff will be needed if we want a multicore-capable VM notably
Yes, I will agree.
tope-là, expect it in a couple of minutes
Guillaume Melquiond said:
Why would VM not work with OCaml 5.0?
Last time we tried it was using "private" stuff from the GC, but the code on both sides has changed considerably, my branch provides a point if someone is interested in trying to compile the C code again.
The GC might have changed considerably, but as far as the interpreter is concerned, there is nothing worrying. I participated in the review of the changes to the OCaml interpreter, and there is no reason it will be harder to adapt the Coq interpreter. Sure, it will not compile out of the box, but nothing that cannot be solved by adding #define Alloc_small
at the start of the file to account for the new argument to the macro.
Even if the VM fix only takes a few person days, native seems that will require significant engineering time.
Sure, but I never talked about native.
Guillaume Melquiond said:
Sure, but I never talked about native.
I did
Note that I did not make an estimate of effort, I just wrote that for now, they don't work at all
So today we have lost the ability to run Coq with OCaml master, which I ensured was possible quite a long time ago
in the meantime we could make it easier to allow compiling Coq without native
Compilation is not the issue. As long as you do not call native_compute
, it should work just fine.
I'm pretty sure the infamous set_tag function was removed
so Coq won't compile on OCaml 5.0
(notwithstanding the other calls to Obj and friends that might have changed)
Still there:
external set_tag : t -> int -> unit = "caml_obj_set_tag"
[@@ocaml.deprecated "Use with_tag instead."]
interesting, they don't plan to remove if from the 5.0 API then?
Guillaume Melquiond said:
Compilation is not the issue. As long as you do not call
native_compute
, it should work just fine.
It is an issue, to start with, due to static initializers in native coqc will just segfault
hm, this precise part was tweaked recently though
Are you guessing @Guillaume Melquiond or have you actually tried?
I am guessing. As you said yourself, Coq does not compile with OCaml trunk.
Pierre-Marie Pédrot said:
hm, this precise part was tweaked recently though
I actually saw it, but was not enough to fix the problem, a couple more remained, I have a tree that tried to fix it tho
I don't have the time these days to experiemnt, but I have spent quite some time messing with Coq and multicore so if anyone would like to go ahead I have git branches and notes around
A good start is the branch used in sandmark
The diffs show everything that is broken
What is the problem with native? I did port Elpi to 4.12+domains since it did segfault, but the only offender was the GC (I was reading the value of pointers, I guess I was messing the "domain" part of them). Using obj.magic and the like is just fine (I mean, if it was reasonable it still it).
What does native do which is unsafe? @Maxime Dénès ?
Representation of accumulators as closures with tag 0
it's a problem with two constraints that can only solved that way in OCaml
first constraint is that the accumulator is a function, because we don't want to wrap all applications in our own version of apply
second constraint is that we can have efficient pattern-matching over accumulators
in OCaml we can't pattern-match on the tag of a value directly so we hack this by setting the tag of accumulators to 0 by convention
so you are saying that we could de-optimize it a little
de-optimizing is catastrophical
it's like ten times as slow or so, hence with overheads taken into account not even clear to be competitive with the VM
You are are sayin that adding a | x when is_closure x ->
to the matches makes it 10 times slower?
yes
tried and retried
even with is_closure carefully written in C
How can it be? I expect most of the times you don't match an accumulator
yes but it's always called because that's the first thing you test
I would have expected branch prediction to be clever, but no
hum, which is the tag of closures?
why should it be the first case?
247
not first lexically, first as in we must check that the argument is an accumulator before doing anything
Hum, so it is not match Obj.magic thing_which_may_be_accu with K1 ... | K246 .. | x when is_closure x -> ..
?
Unfortunately, you need at least one extra constructor for the branch x when is_closure x
to be relevant, and the tag of this constructor needs to be ignored by OCaml. (Otherwise, the branch will be compiled to K0 ... when is_closure x
, which does not have the correct behavior.) The only case where it works (because OCaml's standard library relies on it) is when the remaining constructor is the only non-constant constructor. But that is not true for Coq; there usually are lots of block constructors.
because OCaml's standard library relies on it
How's that?
Cf CamlinternalOO.method_impl
.
the Closure _ as clo
is a actually a value with closure_tag?
I see thanks for the explanations. So it seems @Pierre-Marie Pédrot tried if is_closure x then .. else match x with K1 ..
. Did you also try K247 of Obj.t
? (I guess this is what you meant by "our own apply")
"our own apply" means that we compile function types to a sum type Accu of accu | Fun of Obj.t
and we dispatch depending on the tag
You can't write the K247 hack because this will fail at compile time
OCaml will tell you there are too many constructors in the type
ok, that is what I meant, add a Fun case
And that is too much space overhead?
Gaëtan Gilbert said:
the
Closure _ as clo
is a actually a value with closure_tag?
Yes.
@Enrico Tassi this is a catastrophe as well
we need to reimplement the caml_apply dynamic dispatch in our own version of the runtime essentially
By the way, this whole discussion is kind of moot, because Gabriel's patch for unboxed constructors is ready, which will solve our issue.
ah ah ah, LOL
but I've learnt some stuff ;-)
I am really unsure this will work
unboxed constructors, that is
because we gladly mess with the type system and this feature is typed-directed
expect trouble ahead
we're really playing with fire in the native compiler with Obj.magic but nobody seems to care
It is also moot partially moot because IMO we gain zero moving to multicore, so we lose very little to stay on 4.13 for a while.
Actually, we will not have to mess with the type system anymore. We will just systematically add a constructor Accu of t -> t
to every inductive type.
@Guillaume Melquiond yes we do, because of large dependent elimination
how would you translate a function of type forall b : bool, if b then nat else nat -> nat
?
the target of native compilation (and extraction, for that matter) is fundamentally untyped
It is already a function, you do not need to translate it. The issue is with inductive values, not functions.
my point is that we still need to sprinkle Obj.magic everywhere
Sure, but we will no longer lie. When doing match Obj.magic
, the list of constructors will exactly match the actual constructors.
as a famous OCaml dev whose name starts with Xavier and ends with Leroy would say: "repeat after me, Obj.magic is not part of OCaml"
right
This is bullshit
what's bullshit? that Obj.magic is not part of OCaml ?
some people in the Linux kernel also have strong opinions about what C should be, and it's not what the standard says
yes, because it is.
... until you start using flambda and then any optimization breaks your code ?
we can't advocate for specs and formalizations on the one hand and blatantly ignore such issues on the other
it's a mantra people akin to strong types repeat... it does not make it true. of course you have to use it knowing what you are doing.
... and I repeat, until the compiler understands that what you're doing is wrong
and use is only when necessary, but the whole bullshit about optimized one constructor GADTS just proves my point (the ones that looks like type theory Id).
:shrug:
The type system is inherently incomplete, and can't be as smart as you want... so sometimes you cheat.
It is the reality
but then you need a semantic model of your runtime
well, we have an operational one with a changelog... it is not too bad
Also, my ocaml code broke more times in its safe-and-sound part, than it its unsafe parts. Multicore is actually the very first time I have to change some unsafe code because it really became unsafe. I still recall the sound change that flipped the arguments of some set/map API, which started to iterate on the other set/map and made my code compile fine but never terminate... It's life
My favorite example is the time (hopefully past) when when
clauses were actually unsound.
I can confirm all these explicit encodings add a catastrophic overhead. I tried them during my thesis.
Guillaume Melquiond said:
By the way, this whole discussion is kind of moot, because Gabriel's patch for unboxed constructors is ready, which will solve our issue.
Is there an OCaml PR?
I don't think we need to panic anyway. In the worst case, we'll remove the native compiler until somebody finds the time to implement one that targets a lower level language.
I am not sure there is an actual pull request yet. There is an RFC and a few published papers about it.
@Enrico Tassi I'd expect you want a real semantic model like in RustBelt/NuPRL, an operational one is too cumbersome to reason about... but the bigger problem is that you might need a contract for the optimizer (and for undefined behavior?) similar to the C/C++ standard (or the WIP work on Rust Undefined Behavior by @Ralf Jung)
while the C and C++ standard have lots of accidental complexity, supporting low-level operations together with a high-level invariants (that an optimizer relies on) has lots of essential complexity (Robbert Krebbers's PhD thesis explains that nicely)
If I had to reason formally about that code, sure. What I meant is that we have one implementation which is known and documented, it is not like relying on undefined behavior every implementation has the freedom to implement differently. For that implementation many uses of Obj make sense, others don't. I'm not saying you must use the unsafe feature at all costs, just that pretending it has no practical use or reason to exist is, well, bar sport (PMU for the french) discussion (at least, this is my reading of "is not part of the ocaml language").
Last updated: Dec 05 2023 at 11:01 UTC