Emilio Jesús Gallego Arias (Jan 11 2022 at 00:02): Emilio Jesús Gallego Arias (Jan 11 2022 at 00:02):https://github.com/ocaml/ocaml/pull/10831
Ali Caglayan (Jan 11 2022 at 10:00):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?
Emilio Jesús Gallego Arias (Jan 11 2022 at 10:25):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.
Emilio Jesús Gallego Arias (Jan 11 2022 at 10:25):Coq, with those disabled, seems to work fine for now on the limited testing multicore devs have done in my multicore branch
Guillaume Melquiond (Jan 11 2022 at 10:42):Why would VM not work with OCaml 5.0?
Pierre-Marie Pédrot (Jan 11 2022 at 10:42):It requires some changes w.r.t. closure representation IIRC
Pierre-Marie Pédrot (Jan 11 2022 at 10:44):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
Guillaume Melquiond (Jan 11 2022 at 10:45):My opinion has not changed. State threading is an awful paradigm and it has been a never-ending source of bugs in Coq already.
Pierre-Marie Pédrot (Jan 11 2022 at 10:46):yes, but this is not the goal of the PR
Guillaume Melquiond (Jan 11 2022 at 10:46):As for the change to closure representations, it was performed a few years ago already.
Pierre-Marie Pédrot (Jan 11 2022 at 10:46):the goal of the PR is to be able to make the VM state local and persistent
Guillaume Melquiond (Jan 11 2022 at 10:47):Yes, but you are doing it using state threading and I cannot agree to it.
Pierre-Marie Pédrot (Jan 11 2022 at 10:47):pff
Pierre-Marie Pédrot (Jan 11 2022 at 10:47):if I use a reference passing will you agree to merging it ASAP?
Pierre-Marie Pédrot (Jan 11 2022 at 10:48):this stuff will be needed if we want a multicore-capable VM notably
Guillaume Melquiond (Jan 11 2022 at 10:49):Yes, I will agree.
Pierre-Marie Pédrot (Jan 11 2022 at 10:49):tope-là, expect it in a couple of minutes
Emilio Jesús Gallego Arias (Jan 11 2022 at 11:35):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.
Guillaume Melquiond (Jan 11 2022 at 11:40):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.
Emilio Jesús Gallego Arias (Jan 11 2022 at 11:43):Even if the VM fix only takes a few person days, native seems that will require significant engineering time.
Guillaume Melquiond (Jan 11 2022 at 11:44):Sure, but I never talked about native.
Emilio Jesús Gallego Arias (Jan 11 2022 at 11:49):Guillaume Melquiond said:
Sure, but I never talked about native.
I did
Emilio Jesús Gallego Arias (Jan 11 2022 at 11:50):Note that I did not make an estimate of effort, I just wrote that for now, they don't work at all
Emilio Jesús Gallego Arias (Jan 11 2022 at 11:51):So today we have lost the ability to run Coq with OCaml master, which I ensured was possible quite a long time ago
Pierre-Marie Pédrot (Jan 11 2022 at 12:02):in the meantime we could make it easier to allow compiling Coq without native
Guillaume Melquiond (Jan 11 2022 at 12:04):Compilation is not the issue. As long as you do not call native_compute, it should work just fine.
Pierre-Marie Pédrot (Jan 11 2022 at 12:05):I'm pretty sure the infamous set_tag function was removed
Pierre-Marie Pédrot (Jan 11 2022 at 12:05):so Coq won't compile on OCaml 5.0
Pierre-Marie Pédrot (Jan 11 2022 at 12:05):(notwithstanding the other calls to Obj and friends that might have changed)
Guillaume Melquiond (Jan 11 2022 at 12:05):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?
Emilio Jesús Gallego Arias (Jan 11 2022 at 12:06):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
Pierre-Marie Pédrot (Jan 11 2022 at 12:07):hm, this precise part was tweaked recently though
Emilio Jesús Gallego Arias (Jan 11 2022 at 12:07):Are you guessing @Guillaume Melquiond or have you actually tried?
Guillaume Melquiond (Jan 11 2022 at 12:07):I am guessing. As you said yourself, Coq does not compile with OCaml trunk.
Emilio Jesús Gallego Arias (Jan 11 2022 at 12:11):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
Emilio Jesús Gallego Arias (Jan 11 2022 at 12:12):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
Emilio Jesús Gallego Arias (Jan 11 2022 at 12:12):A good start is the branch used in sandmark
Emilio Jesús Gallego Arias (Jan 11 2022 at 12:13):The diffs show everything that is broken
Enrico Tassi (Jan 11 2022 at 12:51):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 ?
Pierre-Marie Pédrot (Jan 11 2022 at 12:52):Representation of accumulators as closures with tag 0
Pierre-Marie Pédrot (Jan 11 2022 at 12:52):it's a problem with two constraints that can only solved that way in OCaml
Pierre-Marie Pédrot (Jan 11 2022 at 12:52):first constraint is that the accumulator is a function, because we don't want to wrap all applications in our own version of apply
Pierre-Marie Pédrot (Jan 11 2022 at 12:53):second constraint is that we can have efficient pattern-matching over accumulators
Pierre-Marie Pédrot (Jan 11 2022 at 12:53):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
Enrico Tassi (Jan 11 2022 at 12:54):so you are saying that we could de-optimize it a little
Pierre-Marie Pédrot (Jan 11 2022 at 12:54):de-optimizing is catastrophical
Pierre-Marie Pédrot (Jan 11 2022 at 12:54):it's like ten times as slow or so, hence with overheads taken into account not even clear to be competitive with the VM
Enrico Tassi (Jan 11 2022 at 12:59):You are are sayin that adding a | x when is_closure x -> to the matches makes it 10 times slower?
Pierre-Marie Pédrot (Jan 11 2022 at 13:00):yes
Pierre-Marie Pédrot (Jan 11 2022 at 13:00):tried and retried
Pierre-Marie Pédrot (Jan 11 2022 at 13:00):even with is_closure carefully written in C
Enrico Tassi (Jan 11 2022 at 13:00):How can it be? I expect most of the times you don't match an accumulator
Pierre-Marie Pédrot (Jan 11 2022 at 13:01):yes but it's always called because that's the first thing you test
Pierre-Marie Pédrot (Jan 11 2022 at 13:01):I would have expected branch prediction to be clever, but no
Enrico Tassi (Jan 11 2022 at 13:01):hum, which is the tag of closures?
Enrico Tassi (Jan 11 2022 at 13:02):why should it be the first case?
Pierre-Marie Pédrot (Jan 11 2022 at 13:02):247
Pierre-Marie Pédrot (Jan 11 2022 at 13:02):not first lexically, first as in we must check that the argument is an accumulator before doing anything
Enrico Tassi (Jan 11 2022 at 13:03):Hum, so it is not match Obj.magic thing_which_may_be_accu with K1 ... | K246 .. | x when is_closure x -> .. ?
Guillaume Melquiond (Jan 11 2022 at 14:01):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.
Gaëtan Gilbert (Jan 11 2022 at 14:07):because OCaml's standard library relies on it
How's that?
Guillaume Melquiond (Jan 11 2022 at 14:17):Cf CamlinternalOO.method_impl.
Gaëtan Gilbert (Jan 11 2022 at 14:23):the Closure _ as clo is a actually a value with closure_tag?
Enrico Tassi (Jan 11 2022 at 14:23):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")
Pierre-Marie Pédrot (Jan 11 2022 at 14:24):"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
Pierre-Marie Pédrot (Jan 11 2022 at 14:25):You can't write the K247 hack because this will fail at compile time
Pierre-Marie Pédrot (Jan 11 2022 at 14:25):OCaml will tell you there are too many constructors in the type
Enrico Tassi (Jan 11 2022 at 14:25):ok, that is what I meant, add a Fun case
Enrico Tassi (Jan 11 2022 at 14:26):And that is too much space overhead?
Guillaume Melquiond (Jan 11 2022 at 14:27):Gaëtan Gilbert said:
the
Closure _ as clois a actually a value with closure_tag?
Yes.
Pierre-Marie Pédrot (Jan 11 2022 at 14:29):@Enrico Tassi this is a catastrophe as well
Pierre-Marie Pédrot (Jan 11 2022 at 14:29):we need to reimplement the caml_apply dynamic dispatch in our own version of the runtime essentially
Guillaume Melquiond (Jan 11 2022 at 14:30):By the way, this whole discussion is kind of moot, because Gabriel's patch for unboxed constructors is ready, which will solve our issue.
Enrico Tassi (Jan 11 2022 at 14:30):ah ah ah, LOL
Enrico Tassi (Jan 11 2022 at 14:30):but I've learnt some stuff ;-)
Pierre-Marie Pédrot (Jan 11 2022 at 14:31):I am really unsure this will work
Pierre-Marie Pédrot (Jan 11 2022 at 14:31):unboxed constructors, that is
Pierre-Marie Pédrot (Jan 11 2022 at 14:31):because we gladly mess with the type system and this feature is typed-directed
Pierre-Marie Pédrot (Jan 11 2022 at 14:31):expect trouble ahead
Pierre-Marie Pédrot (Jan 11 2022 at 14:32):we're really playing with fire in the native compiler with Obj.magic but nobody seems to care
Enrico Tassi (Jan 11 2022 at 14:32):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.
Guillaume Melquiond (Jan 11 2022 at 14:32):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.
Pierre-Marie Pédrot (Jan 11 2022 at 14:33):@Guillaume Melquiond yes we do, because of large dependent elimination
Pierre-Marie Pédrot (Jan 11 2022 at 14:33):how would you translate a function of type forall b : bool, if b then nat else nat -> nat?
Pierre-Marie Pédrot (Jan 11 2022 at 14:33):the target of native compilation (and extraction, for that matter) is fundamentally untyped
Guillaume Melquiond (Jan 11 2022 at 14:34):It is already a function, you do not need to translate it. The issue is with inductive values, not functions.
Pierre-Marie Pédrot (Jan 11 2022 at 14:34):my point is that we still need to sprinkle Obj.magic everywhere
Guillaume Melquiond (Jan 11 2022 at 14:35):Sure, but we will no longer lie. When doing match Obj.magic, the list of constructors will exactly match the actual constructors.
Pierre-Marie Pédrot (Jan 11 2022 at 14:35):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"
Pierre-Marie Pédrot (Jan 11 2022 at 14:35):right
Enrico Tassi (Jan 11 2022 at 14:35):This is bullshit
Pierre-Marie Pédrot (Jan 11 2022 at 14:35):what's bullshit? that Obj.magic is not part of OCaml ?
Pierre-Marie Pédrot (Jan 11 2022 at 14:36):some people in the Linux kernel also have strong opinions about what C should be, and it's not what the standard says
Enrico Tassi (Jan 11 2022 at 14:36):yes, because it is.
Pierre-Marie Pédrot (Jan 11 2022 at 14:37):... until you start using flambda and then any optimization breaks your code ?
Pierre-Marie Pédrot (Jan 11 2022 at 14:37):we can't advocate for specs and formalizations on the one hand and blatantly ignore such issues on the other
Enrico Tassi (Jan 11 2022 at 14:37):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.
Pierre-Marie Pédrot (Jan 11 2022 at 14:38):... and I repeat, until the compiler understands that what you're doing is wrong
Enrico Tassi (Jan 11 2022 at 14:39):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).
Pierre-Marie Pédrot (Jan 11 2022 at 14:39)::shrug:
Enrico Tassi (Jan 11 2022 at 14:40):The type system is inherently incomplete, and can't be as smart as you want... so sometimes you cheat.
Enrico Tassi (Jan 11 2022 at 14:40):It is the reality
Pierre-Marie Pédrot (Jan 11 2022 at 14:40):but then you need a semantic model of your runtime
Enrico Tassi (Jan 11 2022 at 14:45):well, we have an operational one with a changelog... it is not too bad
Enrico Tassi (Jan 11 2022 at 14:54):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
Guillaume Melquiond (Jan 11 2022 at 15:00):My favorite example is the time (hopefully past) when when clauses were actually unsound.
Maxime Dénès (Jan 11 2022 at 16:29):I can confirm all these explicit encodings add a catastrophic overhead. I tried them during my thesis.
Maxime Dénès (Jan 11 2022 at 16:31):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?
Maxime Dénès (Jan 11 2022 at 16:32):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.
Guillaume Melquiond (Jan 11 2022 at 17:20):I am not sure there is an actual pull request yet. There is an RFC and a few published papers about it.
Paolo Giarrusso (Jan 11 2022 at 18:30):@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)
Paolo Giarrusso (Jan 11 2022 at 18:33):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)
Enrico Tassi (Jan 11 2022 at 19:29):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