Document and scripts relating to CPS experiments with CEK machine #434
Conversation
There was a problem hiding this comment.
Amazing job. You seem to think it's not very useful, but it's very valuable and we can improve our evaluators based on what is implemented here (not to say you've already spotted at least two efficiency weak spots: slow exponentiation and slow generation of booleans). Comments:
- Is it possible to run this locally using some simple command? If so, it should be added to readme, cause I'm going to play with that
- The R scripts look very similar, can they be unified somehow?
- Writing Plutus Core by hand is a form of punishment. I'd be glad to generate you some programs (using the AST directly, so you'd get pretty much the same programs with no abstraction overhead) if you have any more of them.
- The PDF is marvelous!
- The version of the CEK machine with bangs is essentially the same version as the one without them, see below.
- The CPS-transformed CEK machine looks rather nice.
- The fact that the current CEK machine consumes less memory is interesting. I can't explain that at the moment.
|
|
||
|
|
||
| evalCek :: Closure -> Closure | ||
| evalCek !cl@(Closure term env) = |
There was a problem hiding this comment.
You force cl here by matching on it, hence ! does not add anything.
There was a problem hiding this comment.
-
I forgot to mention this, but if you look in RUNNING.md it tells you how to run the tests.
-
I tend to work with R by plotting things interactively and then hacking together a script to do it properly with labels on the axes and a legend and so on once I know what the data looks like. In this case, it happens that the results for the different experiments are similar enough that you can use more or less the same parameters for each graph, but in general that wouldn't happen. I think that unifying the scripts is maybe more effort than it's worth, since these particular things tend not to be too resuable (also, the R language is remarkably horrible). It may be overkill using R here, since it's really for doing statistical stuff like fitting models (and almost anything else you can think of), but I happen to be familiar with it so it was the easiest thing for me to use.
-
Yes, I think that's about as far as I want to go with writing my own Plutus Core; PlutusTx or PIR would probably be a lot better for generating complex benchmarks (and I think that's something we should do some time).
-
I just stuck in bangs everywhere to be absolutely sure that it was doing things in the right order, but yes, many could be omitted. I tried a version without any bangs, but I don't think it made any noticeable difference.
-
The CPS version was quite difficult to get right since you've just got a big chain of continuations and if something goes wrong it's very hard to work out what's wrong. It's much easier to see what's going on with the stack of frames, and maybe a positive outcome of this experiment is that it tells us that using that version isn't actually costing us a lot.
-
I also don't know why the current version is using less memory. It would be interesting to find out ...
| instantiateEvaluate | ||
| :: Type TyName () -> Closure -> Closure | ||
| instantiateEvaluate _ !(Closure (TyAbs _ _ _ body) env) = evalCek (Closure body env) | ||
| instantiateEvaluate ty !(Closure fun env) |
There was a problem hiding this comment.
Again, ! has no effect here.
| -- If succesful, proceed with either this same term or with the result of the computation | ||
| -- depending on whether 'BuiltinName' is saturated or not. | ||
| applyEvaluate :: Closure -> Closure -> Closure | ||
| applyEvaluate !(Closure funVal funEnv) !(Closure argVal argEnv) = |
| case funVal of | ||
| LamAbs _ name _ body -> evalCek $ Closure body (extendEnvironment name argVal argEnv funEnv) | ||
|
|
||
| _ -> let !term = Apply () funVal argVal in |
There was a problem hiding this comment.
term is by construction in WHNF and moreover, it's forced in the next line, hence ! has no effect here as well.
| Nothing -> | ||
| throw $ MachineException NonPrimitiveApplicationMachineError term | ||
| Just (IterApp headName spine) -> | ||
| case runQuote $! ((applyBuiltinName $! headName) $! spine) of |
There was a problem hiding this comment.
In runQuote $! the $! has no effect, because this thing is inside a pattern matching case. Forcing headName does not have any effect, because it's forced in applyBuiltinName anyway. Forcing spine does not do much, because you anyway only force to WHNF and the spine is forced in applyBuiltinName as well.
|
|
||
| -- | Evaluate a term using the CEK machine. May throw a 'MachineException'. | ||
| evaluateCek :: Term TyName Name () -> EvaluationResult | ||
| evaluateCek !term = |
There was a problem hiding this comment.
This only forces up to the outermost constructor, so does not do much.
| -- | Evaluate a term using the CEK machine. May throw a 'MachineException'. | ||
| evaluateCek :: Term TyName Name () -> EvaluationResult | ||
| evaluateCek !term = | ||
| let Closure result _ = evalCek $! Closure term (Environment IntMap.empty) |
There was a problem hiding this comment.
As above, Closure constructs a value in WHNF, so no need to force it.
| -- | Run a program using the CEK machine. May throw a 'MachineException'. | ||
| -- Calls 'evaluateCek' under the hood, so the same caveats apply. | ||
| runCek :: Program TyName Name () -> EvaluationResult | ||
| runCek !(Program _ _ term) = evaluateCek term |
There was a problem hiding this comment.
As in the first three comments.
| @@ -0,0 +1,22 @@ | |||
| n usr sys mem | |||
There was a problem hiding this comment.
Did you mean to check in the results?
There was a problem hiding this comment.
If you did, maybe we can generate the graphs during the build instead of checking them in?
There was a problem hiding this comment.
I just thought I'd save the results since there's more information in there than appears in the graphs. The graphs are generated using R (see RUNNING.md), and putting that into nix might be a bit heavyweight just to draw some graphs.This isn't a terribly important document anyway, so I don't know if it's worth complicating the build.
| @@ -0,0 +1,73 @@ | |||
| -- Preprocess this file with 'gpp -DARG=20 -DSIZE=4' to calculate fib(20), for example. | |||
There was a problem hiding this comment.
I really need to get you some PIR concrete syntax...
|
If you feel able to add a nix build for this then I think it's a good idea, otherwise I'll do it later. |
|
I'll take a look at that, since I should make an effort to get to grips with nix. Again, the document's not that important, so I thought just checking in a pre-built PDF would be the simplest thing to do. |
|
If we're not planning to work on it in future, then there's not much point checking the sources for the document into git, IMO (you could just email around the pdf!). If we are then I'd prefer to do it consistently! I would mildly prefer to generate the graphs, but I'm not going to make a fuss about it :) |
Some measurements of variations on the CEK machine. It doesn't tell us anything interesting, but it's probably worth recording anyway.