PLT-506: Case-of-case #5554

michaelpj · 2023-09-21T17:07:38Z

Based on #5551, look at the last commit if you're interested.

This is a bit tricky. The key is to extract out enough of the code for picking apart datatype match terms that the pass itself is comprehensible. We also need this because then we can abstract over builtin "matchers" also, which lets us handle e.g. the combination of Bool_match and ifThenElse1, which is very common.

There's a question of whether to only do it when we know it's a win. I've linked that to the conservative optimisation flag, which feels right. To my surprise, it seems to be generally better to just let it run regardless!

Improvements are, again, modest.

Pre-submit checklist:

Branch
- Tests are provided (if possible)
- Commit sequence broadly makes sense
- Key commits have useful messages
- Changelog fragments have been written (if appropriate)
- Relevant tickets are mentioned in commit messages
- Formatting, PNG optimization, etc. are updated
PR
- (For external contributions) Corresponding issue exists and is linked in the description
- Targeting master unless this is a cherry-pick backport
- Self-reviewed the diff
- Useful pull request description
- Reviewer requested

effectfully

Quite a diff! I've only had a very cursory look so far, I'd need a ticket and some allocated time to review this one properly.

plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs

effectfully · 2023-09-22T15:05:23Z

plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs

+defaultUniMatcherLike :: Map.Map DefaultFun (BuiltinMatcherLike DefaultUni DefaultFun)
+defaultUniMatcherLike = Map.fromList
+  [ (IfThenElse, BuiltinMatcherLike splitIfThenElse)
+  , (ChooseUnit, BuiltinMatcherLike splitChooseUnit)


Lists and pairs?

Lists we can do, for pairs we don't actually have a matcher function!

Lists we can do, for pairs we don't actually have a matcher function!

How come? How's MkCons a [a] so much different from MkPair a b? Isn't uncurry the matcher?

... oh wait, I think I get it. We have ChooseList, but no such builtin for pairs. This all is just so weird, we should have proper pattern matching builtins and forget about all this nonsense.

Yeah. And it's slightly weird to treat chooseList as a "matcher": I'd be treating it as a matcher with 0 arity branches, which is in fact fine, but is a little strange...

What about chooseData?

plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs

plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs

effectfully · 2023-09-22T16:30:32Z

plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs

+That is, this guarantees that case-of-known constructor will fire and get rid of one of the
+matches entirely, which is great.
+
+If we *don't* have this property, then case-of-case can duplicate code, making the program bigger.
+So the conservative option is to only do case-of-case when this is true.


Aha, here they are. Is case-of-case interleaved with case-of-known-constructor? If not, can there still be an exponential blowup in code size before case-of-known-constructor cleans everything up? Worth discussing in this Note I think.

Also note that I'm currently turning the non-conservative version on by default since it seems to help! I feel pretty nervous about that...

Good point about the interleaving: indeed, they run one after the other and only once in each simplifier iteration, so we should be safe, but worth pointing out.

only once in each simplifier iteration, so we should be safe

Can you still get an exponential blowup due to transformOf being a bottom-up traversal? First you duplicate some leaves, then you duplicate nodes storing the duplicated leaves, then you duplicate nodes storing the duplicated nodes etc.

No idea if it's how it actually works, but it's worth having some kind of a test.

Good point, that seems possible. Let me try and come up with a case where that could happen.

Yep, I can make it happen. I think if we're in conservative mode then COKC is still guaranteed to clear it up, so the worst that can happen is a big intermediate tree.

michaelpj · 2023-09-27T13:10:25Z

So I realised that

Roman is right, and case-of-case can create exponentially large programs in a single pass
Even if we only trigger it when the branch bodies are conapps, we can still get duplication (and hence exponential programs).

That means I don't think we can have a strictly conservative case-of-case at all (or we'd have to assert that the branch bodies were all distinct conapps, which seems annoying). I'm not totally sure what to do then: turn it off entirely when in conservative mode, and turn it on universally otherwise (just forgetting the conapps-only mode?).

michaelpj · 2023-09-27T13:22:52Z

See 7b5d40a#diff-680928a1ecce80bf52208060a33a06de83134a99e5265b40402cdd6354ebf8e7R133

effectfully · 2023-09-27T15:43:43Z

processTerm is a single step, right? And transformOf in caseOfCase performs it to the fixpoint. Can't you just interleave the step function of caseOfCase with the step function of COKC and run that to the fixpoint? Wasn't it what GHC was doing? Can't remember right now, but I recall this was in some paper, surely it's a solved problem.

michaelpj · 2023-09-27T16:21:18Z

processTerm is a single step, right? And transformOf in caseOfCase performs it to the fixpoint.

transformOf does not run it to fixpoint, but it does run it recursively bottom up, which is enough. That means you can generate duplicate code in the branches before then duplicating the branches, exponential goes brrr.

Can't you just interleave the step function of caseOfCase with the step function of COKC and run that to the fixpoint? Wasn't it what GHC was doing?

Hmmm maybe we could fuse the passes. I think the issue will be that case-of-case creates opportunities for COKC in a subterm of the term currently being processed, so naive fusion won't work.

We could directly call the COKC step from the case-of-case step if we think we've made an opportunity for it. That would avoid the problem partly, although if you look in the comment I added you'll see there's still a case where we can get duplication :(

bezirg · 2023-09-28T15:21:46Z

plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs

@@ -133,7 +137,7 @@ data CompilationCtx uni fun a = CompilationCtx {
 makeLenses ''CompilationCtx

 toDefaultCompilationCtx
-    :: (Default (PLC.BuiltinSemanticsVariant fun), Default (PLC.CostingPart uni fun))
+    :: (Ord fun, Default (PLC.BuiltinSemanticsVariant fun), Default (PLC.CostingPart uni fun))


Unrelated: This Default CostingPart always makes me uneasy. It sucks that we have to pass some fake (zero) "default" costing just so we can have a runtime available to hand over to the EvaluateBuiltins pass (and perhaps other passes as well)

Is there another way to do it? Costing is a part of the evaluation semantics of a builtin.

I guess in principle we could make it optional? But then we'd need to pass Maybe cost around in various places which would have overhead in the machine, so this seems better.

But the compiler does not make use of the costing part at all. It's just for compile-time evaluation, disregarding the costs (more precisely treating all as zero-cost)

I guess in principle we could make it optional?

@bezirg

But the compiler does not make use of the costing part at all. It's just for compile-time evaluation, disregarding the costs (more precisely treating all as zero-cost)

Good point, though. I'll think about it, thank you.

If you only need compile-time evaluation, you can use the first two fields of BuiltinMeaning like we do in the well-typed Hedgehog program generators for example. Although it's probably not a good idea, since you probably don't want to roll out your own lifting and unlifting logic etc. Maybe we should indeed have some middle-ground.

Although I still feel like insisting everywhere that costing is a part of operational semantics of builtins will save us so much trouble in the long run that it may not be optimal to break this rule even when it makes sense. I may be wrong about that in this particular case, though.

bezirg

I think this still needs a bit of code refactoring:

a) moving code to their "principal" modules,
b) redoing a bit processTerm because it was hard to follow
c) adding some more comments/haddocks

Overall, despite bing a tricky transformation, the golden results look correct. Kudos!

plutus-core/plutus-ir/src/PlutusIR/Compiler.hs

plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs

bezirg · 2023-09-28T17:19:50Z

plutus-core/plutus-ir/src/PlutusIR/Analysis/VarInfo.hs

@@ -144,8 +123,38 @@ bindingVarInfo = \case
        in VarsInfo (PLC.insertByName matcher info mempty) mempty
      constrArity constrTy =
        -- One parameter for all function type arguments
-        fmap (const TypeParam) (funTyArgs constrTy)
+        fmap (const TermParam) (funTyArgs constrTy)


What is happening here? Why TypeParam became TermParam?

It was wrong before! now it's still slightly wrong actually, but I'll fix it

bezirg · 2023-09-29T10:21:33Z

plutus-core/plutus-ir/src/PlutusIR/Arity.hs

+e.g. consider the term @let id = \x -> x in id@: the variable @id@ has syntactic
+arity @[]@, but does in fact need an argument before it does any work.
+-}
+type Arity = [Param]


I think Arity is a misnomer in this case. Arity supposed to be a number and this is clearly not a number. Suggestion SyntacticArgs or SyntacticParams?

I guess I think about it differently. For me arity is a "summary of how the function is going to be used in the program". As such it makes sense to me to include information about the parameters, because that's what you need!

plutus-core/plutus-ir/src/PlutusIR/Arity.hs

plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs

bezirg · 2023-09-29T13:18:14Z

plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs

+      TermAppContext <$> underBindersMaybe arity f branch <*> pure ann <*> go ctx arities
+    go _ _ = Nothing
+
+    -- I tried to come up with a way to do this in terms of the underBinders traversal


I don't get it. underbinders should just work since its a traversal with Maybe as the Applicative?

go (TermAppContext branch ann ctx) (arity:arities) = TermAppContext <$> underBinders arity f branch <*> pure ann <*> go ctx arities

bezirg · 2023-09-29T13:36:08Z

plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs

+-}
+
+{- Note [Case-of-case and conapps]
+Case-of-case will be much better if the bodies of the branches are all constructor applications.


It's not jus t"will be much better", but to me it seems caseofcase is only applied if all the branches are conapps, correct?

bezirg · 2023-09-29T13:43:02Z

plutus-tx-plugin/test/size/max.uplc-size.golden

That's nice, I wish i could see the simplified uplc here to enjoy the benefit of caseofcase+caseknown+inline!

effectfully · 2023-09-29T16:54:52Z

@michaelpj

Can't you just interleave the step function of caseOfCase with the step function of COKC and run that to the fixpoint? Wasn't it what GHC was doing?

Hmmm maybe we could fuse the passes. I think the issue will be that case-of-case creates opportunities for COKC in a subterm of the term currently being processed, so naive fusion won't work.

We could directly call the COKC step from the case-of-case step if we think we've made an opportunity for it. That would avoid the problem partly, although if you look in the comment I added you'll see there's still a case where we can get duplication :(

Thanks for the explanation. Can you then just create a let binding for each of the branches that get duplicated and let the inliner deal with it down the line? And maybe inlining + COKC is easier to arrange than case-of-case + COKC? "This is safe to inline, because it immediately reduces by COKC to an acceptable expression".

michaelpj · 2023-10-02T08:18:58Z

Can you then just create a let binding for each of the branches that get duplicated and let the inliner deal with it down the line?

Yeah, I was also wondering about this. This is essentially what GHC does with join points. In our case it's not "free" like join points are, but it might still be worth it. And it does avoid the exponential code problem. So maybe it is indeed the right thing to do. In fact, I already have most of the code there to do this...

And maybe inlining + COKC is easier to arrange than case-of-case + COKC? "This is safe to inline, because it immediately reduces by COKC to an acceptable expression".

Right, and that's a generally useful inlining heuristic that will help us anyway. For most cases we don't even need a new heuristic, though: in the non-duplicative cases the binding will be single-occurrence, so the inliner will already inline it.

This seems promising, I think I should try this.

michaelpj · 2023-10-02T15:28:20Z

For most cases we don't even need a new heuristic, though: in the non-duplicative cases the binding will be single-occurrence, so the inliner will already inline it.

No, this is totally wrong: we get one binding which is used in every case branch, so it will almost never be single-use. So we are unlikely to inline it currently, which is a bit of a problem. Boo.

michaelpj · 2023-10-02T16:06:47Z

I guess we could make a binding in conservative mode? That avoids the program growth problem, and currently won't optimize well, but maybe that's okay.

michaelpj · 2023-10-12T12:35:48Z

This is good to go now, I think.

We always do CoC if all the branches are distinct conapps, this is guaranteed to be good
If we don't know this, then we do it unless we are being conservative, in which case we bind it to a variable
- The conservative case is not a noticeable regression: it looked like it was but it was a weird interaction with the UPLC case-of-case. I checked without that and it's fine.
Refactored the code a bit following suggestions.

michaelpj requested review from bezirg, zliu41 and effectfully September 21, 2023 17:07

effectfully reviewed Sep 22, 2023

View reviewed changes

michaelpj force-pushed the mpj/case-of-case branch from 16155a3 to c04d00e Compare September 25, 2023 16:45

bezirg reviewed Sep 28, 2023

View reviewed changes

bezirg approved these changes Sep 29, 2023

View reviewed changes

michaelpj force-pushed the mpj/case-of-case branch 2 times, most recently from d67adc0 to 0ef014c Compare October 12, 2023 11:03

Case-of-case

e7b68f4

michaelpj force-pushed the mpj/case-of-case branch from 0ef014c to e7b68f4 Compare October 12, 2023 12:00

michaelpj marked this pull request as ready for review October 12, 2023 12:01

michaelpj enabled auto-merge (squash) October 12, 2023 12:35

michaelpj merged commit bde821a into master Oct 12, 2023
7 checks passed

michaelpj deleted the mpj/case-of-case branch October 12, 2023 17:07

effectfully mentioned this pull request Jun 25, 2024

PIR case-of-case is exponential and causes OOMs #6183

Open

PLT-506: Case-of-case #5554

PLT-506: Case-of-case #5554

Conversation

michaelpj commented Sep 21, 2023

effectfully left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michaelpj commented Sep 27, 2023

michaelpj commented Sep 27, 2023

effectfully commented Sep 27, 2023

michaelpj commented Sep 27, 2023

bezirg Sep 28, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bezirg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

effectfully commented Sep 29, 2023

michaelpj commented Oct 2, 2023

michaelpj commented Oct 2, 2023

michaelpj commented Oct 2, 2023

michaelpj commented Oct 12, 2023

bezirg Sep 28, 2023 •

edited

Loading