Coq Topic Working Group Multicore

Goals

We aim to port Coq to OCaml's multicore, and improve Coq's utilization of threading primitives.

Methodology

The primary goals are:

• to update Coq to use a functional / thread-safe handling of state.
• to increase the opportunities of local computation [for example w.r.t. universes]

People

• Emilio J. Gallego Arias
• Gaëtan Gilbert
• Pierre-Marie Pédrot

Miscellaneous links

• branch [current]: https://github.com/ejgallego/coq/tree/ocaml+multicore_remove_vm

• branch [broken]: https://github.com/ejgallego/coq/tree/ocaml+multicore

• bugs: https://github.com/ocaml-multicore/ocaml-multicore/issues/646

• https://github.com/ocaml-multicore/multicore-opam#install-multicore-ocaml

• https://github.com/ocaml-multicore/ocaml-multicore/

• https://github.com/ocaml-multicore/ocaml-multicore/blob/master/stdlib/domain.mli

• https://github.com/ocaml-multicore/domainslib

• https://github.com/ocaml-multicore/domainslib/blob/master/lib/task.mli

Meeting log and planning

Next meeting

2021-09-15

Porting of the VM / native to multicore

• porting the vm should be OK?

  Alloc_small needs some more parameters, not sure. Do we have bug for that in Coq already?

• `native seems more complex:

  • set_tag: PMP "easy" to solve
  • naked_pointers: No current solution

• PMP proposes to target "malfunction" as FL

How can Coq profit from threads?

• Could we delay QED?
  • what does the kernel w.r.t. universes constraints?
  • measure time spent in QED
  • seems not easy right now, kernel checking 100% sequential
• https://github.com/ppedrot/coq/tree/no-opaque-transitive-univs
• maybe use heuristics w.r.t. similar to STM?
• GG: make other tools to profit from multicore, for example coqdep
• Qed annotations? => Emilio doesn't like annotations.
• hashconsing et multicore? Weak hash table, how would it work? => Coq timings, fig 4 and 5 https://kcsrk.info/papers/retro-concurrency_pldi_21.pdf seems not to bad

PMP's plan of removing Future.t from the kernel?

• branch at https://github.com/ppedrot/coq/tree/move-opaque-out-of-kernel
• problem is how to design the API, so it is still "safe"
• at some point we need some safe async programming paradigm, let it be algebraic effects, monads, or anything else; hard choice to make, and pervades the system
• in general technical debt is a problem, maybe we should take Coq 9.0 more seriously?