3 ms·

This seems cool, but this blog article doesn't really delve into what the "provably" part is -- I can see how the structure they're describing of having process

by abeppu 5y ago

This seems cool, but this blog article doesn't really delve into what the "provably" part is -- I can see how the structure they're describing of having processors handle GC for a collection of heaps which are structurally linked might make GC more efficient, but they don't really talk about what is proved or how. I guess, even from a practical perspective, how does this end up comparing with GC in something like the JVM with functional languages like scala?

Jtsummers 5y ago
Near the top there's a link to a paper which seems to go into more technical detail: https://dl.acm.org/doi/10.1145/3434299 https://dl.acm.org/doi/10.1145/3434299 Context around the link: > In our POPL 2021 paper (which won a Distinguished Paper award), we proposed a specific heap scheduler and showed that it yields provable work and space bounds. I haven't read it yet, but this is where their claims of being provably space-efficient seems to come from. EDIT: A quick read later, section 6 is where they prove their claim. It's efficient when compared to equivalent sequential execution.
- chriswarbo 5y ago
  > It's efficient when compared to equivalent sequential execution. It looks like they're comparing against MLton, which is interesting since it performs whole-program optimisation. That makes their speedups even more impressive!
  - Athas 5y ago
    MPL is based on MLton, so they also do whole-program optimisation (the same one, in fact).
    - chriswarbo 5y ago
      Yes, but I imagine traditional compiler optimisations like inlining, unrolling, etc. are easier to apply to serial code.
      - Athas 5y ago
        Well, to the compiler, the parallelism probably just looks like an opaque call to a higher-order function. The bulk of the program will still be serial code, which will be subject to all the normal optimisations. I talked a bit with one of the main authors of MPL, and he mentioned that the existing optimisation passes in MLton just kept working without any nontrivial modifications.

by abeppu 5y ago

Jtsummers 5y ago

Near the top there's a link to a paper which seems to go into more technical detail: https://dl.acm.org/doi/10.1145/3434299 https://dl.acm.org/doi/10.1145/3434299 Context around the link: > In our POPL 2021 paper (which won a Distinguished Paper award), we proposed a specific heap scheduler and showed that it yields provable work and space bounds. I haven't read it yet, but this is where their claims of being provably space-efficient seems to come from. EDIT: A quick read later, section 6 is where they prove their claim. It's efficient when compared to equivalent sequential execution.

chriswarbo 5y ago
> It's efficient when compared to equivalent sequential execution. It looks like they're comparing against MLton, which is interesting since it performs whole-program optimisation. That makes their speedups even more impressive!
- Athas 5y ago
  MPL is based on MLton, so they also do whole-program optimisation (the same one, in fact).
  - chriswarbo 5y ago
    Yes, but I imagine traditional compiler optimisations like inlining, unrolling, etc. are easier to apply to serial code.
    - Athas 5y ago
      Well, to the compiler, the parallelism probably just looks like an opaque call to a higher-order function. The bulk of the program will still be serial code, which will be subject to all the normal optimisations. I talked a bit with one of the main authors of MPL, and he mentioned that the existing optimisation passes in MLton just kept working without any nontrivial modifications.