hoopl

hoopl copied to clipboard

Apparently the CheckpointingMonad wasn't actually used anywhere in the code (there were only a few instances). In particular the fixpoint algorithm did not use it at all.

Removing it seems like a reasonable idea (at least for now), since:

• it's not used,
• having it is confusing (both for developers and users),
• re-adding it's functionality might have performance implications and we don't yet have any reasonable benchmarks. So I'd prefer to first do some cleanup of the library & work on it's performance (e.g., adding some benchmarks) and only once everything starts to look good, consider adding new functionality.

Are we sure clients don't use it?

No I'm not sure about that (GHC doesn't seem to use it though). :-( Also, this would probably require a minor version bump.

But IMHO it still makes sense to make this change - if anyone is using this, then they probably expect the CheckpointingMonad to actually do something, but unless I'm missing something, restart or checkpoint are not used anywhere in the library. So the type signatures are actually pretty misleading here.

It (restart) was invoked in the initial implementation, but it was, accidentally?, removed in a Dataflow rewriting to improve performance.

Without CheckpointMonad, you still can write a correct analysis if you don't use a user-defined state Monad, which is likely true in the most cases. But the state of UniqueMonad cannot be restored in an analysis restart, this might not cause a lot of harm.

I think the benefit of CheckpointMonad could be big. It might be worth investigating this: using the original implementation, which still invokes restart, to write some analysis that need to restore states. I probably can give it a try in the following weeks.

It might be worth investigating this: using the original implementation, which still invokes restart, to write some analysis that need to restore states.

Do you think this could be related to issue #1 ?

Do you think this could be related to issue #1 ?

Using freshUniques from UniqueMonad to name new variables is not a good idea, as UniqueMonad is not restorable in restart.

It will be ideal if a state Monad which is also an instance of CheckpointMonad is used to name new variables.

Yes, I suspect issue #1 can be alleviated if a stateful CheckpointMonad instance supporting deterministic variable naming is used.

Edit: freshLabels -> freshUnqiues a stateful CheckpointMonad -> a stateful CheckpointMonad instance supporting deterministic variable naming.

I think CheckpointMonad would definitely useful! The fixpoint algorithm should definitely be fixed to use it.

I stumbled on the fact that Checkpoint is not used today and was confused as well.

If it can be used, what is a good use-case for it? I wanted to use checkpointing to speculate on loop optimisations in an IR, but I feel that this maybe very expensive (to copy the entire IR data structure).

I've been coming at the problem from the other direction, [trying to study an algebraic theory of patches] (https://github.com/bollu/deltas) --- since I believe that checkpointing will be too expensive space wise. I believe the correct trade-off is to perform some style of incremental computation. I'm now at the stage where I want to try and benchmark this. However, I couldn't find any examples that use Checkpoint :)

I'm hoping @michalt, @mlite , and @spacekitteh may have useful examples in mind?

Thanks!

I don't know what Checkpoint is for. But I do remember that we had the idea of "fuel" for Hoopl. The idea was that you could give Hoopl a certain amount of fuel. When it runs out, it stops rewriting. If some transformation introduces a bug, you can use binary-chop on the fuel supply to nail the precise before-and-after of the buggy rewrite.

I'm not sure if this has anything to do with Checkpoint. I suggest deleting it if unused; it's not much code!

@simonpj Indeed, fuel makes sense :) I wasn't sure what Checkpoint was doing. I presumed it was to be able to speculate on optimisations, but I couldn't find any such source.

The justification of Checkpoint Monad is in the original paper. Checkpoint Monad was used in the original Dataflow implementation and removed in the performance optimized Dataflow reimplementation. Checkpoint Monad can prevent infinite loop when rewriting has side-effect. It's not current used but it should be used.

@mlite where is the performance optimised version described?

Please check the revision history of Dataflow.hs. The performance optimization was needed for integrating Hoopl into GHC.

@mlite Sorry for pinging you after so long on this, but I just got the bandwidth to spelunk. Unfortunately, I am unable to find the relevant commit which mentions checkpoint. Could you tell me roughly what to grep / look for in the history to find this commit? Thanks a ton.

@michalt, did you get around to benching Checkpoint? I'd be interested in setting up benchmarks.

@bollu No, disabling Checkpoint happened way before I did anything with Hoopl. I'm guessing this happened around the time Hoopl started to be used in GHC (it was super slow, so some things were disabled, the fixpoint algorithm copied to GHC codebase, etc.). Have a look at: https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/HooplPerformance

@michalt That's very interesting, thanks. Is that the most up-to-date information available on Hoopl? (Is it still very expensive, for example?)

Checkout Simon Marlow’s commits. I believe he did the performance enhancement for Dataflow.hs

On Feb 11, 2019, at 12:54 PM, Siddharth [email protected] wrote:

@mlite Sorry for pinging you after so long on this, but I just got the bandwidth to spelunk. Unfortunately, I am unable to find the relevant commit which mentions checkpoint. Could you tell me roughly what to grep / look for in the history to find this commit? Thanks a ton.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.