Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Builtins] Optimize 'MakeKnownM' #4587

Merged
merged 11 commits into from
May 11, 2022
114 changes: 88 additions & 26 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,18 @@ module PlutusCore.Builtin.KnownType
, throwKnownTypeErrorWithCause
, KnownBuiltinTypeIn
, KnownBuiltinType
, MakeKnownM
, MakeKnownM (..)
, ReadKnownM
, liftReadKnownM
, readKnownConstant
, MakeKnownIn (..)
, MakeKnown
, ReadKnownIn (..)
, ReadKnown
, makeKnownRun
, makeKnownOrFail
, readKnownSelf
) where

import PlutusPrelude (reoption)

import PlutusCore.Builtin.Emitter
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.Polymorphism
Expand Down Expand Up @@ -184,23 +182,89 @@ typeMismatchError uniExp uniAct = fromString $ concat
-- failure message and evaluation is about to be shut anyway.
{-# NOINLINE typeMismatchError #-}

{- Note [MakeKnownM and ReadKnownM being type synonyms]
Normally it's a good idea for an exported abstraction not to be a type synonym, since a @newtype@
is cheap, looks good in error messages and clearly emphasize an abstraction barrier. However we
make 'MakeKnownM' and 'ReadKnownM' type synonyms for convenience: that way we don't need to derive
a ton of instances (and add new ones whenever we need them), wrap and unwrap all the time
(including in user code), which can be non-trivial for such performance-sensitive code (see e.g.
'coerceVia' and 'coerceArg') and there is no abstraction barrier anyway.
-}

-- See Note [MakeKnownM and ReadKnownM being type synonyms].
-- | The monad that 'makeKnown' runs in.
type MakeKnownM = ExceptT KnownTypeError Emitter

-- See Note [MakeKnownM and ReadKnownM being type synonyms].
-- Equivalent to @ExceptT KnownTypeError Emitter@, except optimized in two ways:
--
-- 1. everything is strict
-- 2. has the 'MakeKnownSuccess' constructor that is used for returning a value with no logs
-- attached, which is the most common case for us, so it helps a lot not to construct and
-- deconstruct a redundant tuple
--
-- Moving from @ExceptT KnownTypeError Emitter@ to this data type gave us a speedup of 8% of total
-- evaluation time.
data MakeKnownM a
= MakeKnownFailure !(DList Text) !KnownTypeError
| MakeKnownSuccess !a
| MakeKnownSuccessWithLogs !(DList Text) !a

-- | Prepend logs to a 'MakeKnownM' computation and 'fmap' it.
fmapWithLogs :: DList Text -> (a -> b) -> MakeKnownM a -> MakeKnownM b
fmapWithLogs logs1 f = \case
MakeKnownFailure logs2 err -> MakeKnownFailure (logs1 <> logs2) err
MakeKnownSuccess x -> MakeKnownSuccessWithLogs logs1 (f x)
MakeKnownSuccessWithLogs logs2 x -> MakeKnownSuccessWithLogs (logs1 <> logs2) (f x)
{-# INLINE fmapWithLogs #-}

-- | Prepend logs to a 'MakeKnownM' computation.
withLogs :: DList Text -> MakeKnownM a -> MakeKnownM a
withLogs logs1 = \case
MakeKnownFailure logs2 err -> MakeKnownFailure (logs1 <> logs2) err
MakeKnownSuccess x -> MakeKnownSuccessWithLogs logs1 x
MakeKnownSuccessWithLogs logs2 x -> MakeKnownSuccessWithLogs (logs1 <> logs2) x
{-# INLINE withLogs #-}

instance Functor MakeKnownM where
-- Written out explicitly, because for some inexplicable reason GHC fails to inline
-- @fmapWithLogs mempty@ despite the pragma.
fmap _ (MakeKnownFailure logs err) = MakeKnownFailure logs err
fmap f (MakeKnownSuccess x) = MakeKnownSuccess (f x)
fmap f (MakeKnownSuccessWithLogs logs x) = MakeKnownSuccessWithLogs logs (f x)
{-# INLINE fmap #-}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All these INLINE annotations seem a little risky to me. If you have any substantial do block in MakeKnownM you're going to be at risk of exponential code bloat. Maybe we should just do INLINABLE?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why exponential? It's a constant factor: every call to >>= becomes, what, six pattern matches. Not too much of a deal, given that we don't do much in MakeKnownM and we want all of it to be efficient, apart from stuff in tests, but it's still not that much.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, you're right, it's not exponential. It would only become so if GHC got happy with case-of-case, which it's probably too smart to do. I'd be interested to know if performance is actually worse with INLINABLE.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, you're right, it's not exponential. It would only become so if GHC got happy with case-of-case, which it's probably too smart to do.

Hm, there's something to worry about here indeed. So let's say we didn't have MakeKnownSuccessWithLogs, then

(a >>= f) >>= g

would expand into

case (case a of
        MakeKnownFailure logs err -> MakeKnownFailure logs err
        MakeKnownSuccess x        -> f x) of
    MakeKnownFailure logs err  -> MakeKnownFailure logs err
    MakeKnownSuccess y         -> g y

which would be turned by case-of-case into

case a of
    MakeKnownFailure logs err ->
        case MakeKnownFailure logs err of
            MakeKnownFailure logs err  -> MakeKnownFailure logs err
            MakeKnownSuccess y         -> g y
    MakeKnownSuccess x        ->
        case f x of
            MakeKnownFailure logs err  -> MakeKnownFailure logs err
            MakeKnownSuccess y         -> g y

which would be turned by case-of-known-constructor into

case a of
    MakeKnownFailure logs err ->
        MakeKnownFailure logs err
    MakeKnownSuccess x        ->
        case f x of
            MakeKnownFailure logs err  -> MakeKnownFailure logs err
            MakeKnownSuccess y         -> g y

which is still perfectly linear.

But we do have MakeKnownSuccessWithLogs and so it is indeed very much possible we'll get duplication in the two success cases.

But then

  1. we do want the duplication, since it's important for this stuff to be as efficient as possible
  2. we won't actually get it, because our f and g are going to be known and so the case-of-known-constructor will save us

Really, I don't think we should worry about this. Especially compared to the ridiculous code bloats with meanings of builtins inlining all the way through the pipeline at each and every step until the very construction of EvaluationContext (we won't have any problems with MakeKnownM at any step, because the denotations have always been perfectly linear due to everything being fully known).

I'd be interested to know if performance is actually worse with INLINABLE.

It probably isn't any worse, but we're building quite a house of cards with all the optimizations here, I don't want to make it any more shaky unless we have to.


-- Written out explicitly just in case (see @fmap@ above for what the case might be).
_ <$ MakeKnownFailure logs err = MakeKnownFailure logs err
x <$ MakeKnownSuccess _ = MakeKnownSuccess x
x <$ MakeKnownSuccessWithLogs logs _ = MakeKnownSuccessWithLogs logs x
{-# INLINE (<$) #-}

instance Applicative MakeKnownM where
pure = MakeKnownSuccess
{-# INLINE pure #-}

MakeKnownFailure logs err <*> _ = MakeKnownFailure logs err
MakeKnownSuccess f <*> a = fmap f a
MakeKnownSuccessWithLogs logs f <*> a = fmapWithLogs logs f a
{-# INLINE (<*>) #-}

MakeKnownFailure logs err *> _ = MakeKnownFailure logs err
MakeKnownSuccess _ *> a = a
MakeKnownSuccessWithLogs logs _ *> a = withLogs logs a
{-# INLINE (*>) #-}

instance Monad MakeKnownM where
MakeKnownFailure logs err >>= _ = MakeKnownFailure logs err
MakeKnownSuccess x >>= f = f x
MakeKnownSuccessWithLogs logs x >>= f = withLogs logs $ f x
{-# INLINE (>>=) #-}

(>>) = (*>)
{-# INLINE (>>) #-}

-- Normally it's a good idea for an exported abstraction not to be a type synonym, since a @newtype@
-- is cheap, looks good in error messages and clearly emphasize an abstraction barrier. However we
-- make 'ReadKnownM' type synonyms for convenience: that way we don't need to derive all the
-- instances (and add new ones whenever we need them), wrap and unwrap all the time
-- (including in user code), which can be non-trivial for such performance-sensitive code (see e.g.
-- 'coerceVia' and 'coerceArg') and there is no abstraction barrier anyway.
-- | The monad that 'readKnown' runs in.
type ReadKnownM = Either KnownTypeError

-- | Lift a 'ReadKnownM' computation into 'MakeKnownM'.
liftReadKnownM :: ReadKnownM a -> MakeKnownM a
liftReadKnownM (Left err) = MakeKnownFailure mempty err
liftReadKnownM (Right x) = MakeKnownSuccess x
{-# INLINE liftReadKnownM #-}

-- See Note [Unlifting values of built-in types].
-- | Convert a constant embedded into a PLC term to the corresponding Haskell value.
readKnownConstant :: forall val a. KnownBuiltinType val a => val -> ReadKnownM a
Expand Down Expand Up @@ -253,15 +317,12 @@ class uni ~ UniOf val => ReadKnownIn uni val a where

type ReadKnown val = ReadKnownIn (UniOf val) val

makeKnownRun
:: MakeKnownIn uni val a
=> a -> (ReadKnownM val, DList Text)
makeKnownRun = runEmitter . runExceptT . makeKnown
{-# INLINE makeKnownRun #-}

-- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val
makeKnownOrFail = reoption . fst . makeKnownRun
makeKnownOrFail x = case makeKnown x of
MakeKnownFailure _ _ -> EvaluationFailure
MakeKnownSuccess val -> EvaluationSuccess val
MakeKnownSuccessWithLogs _ val -> EvaluationSuccess val
{-# INLINE makeKnownOrFail #-}

-- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
Expand All @@ -274,7 +335,7 @@ readKnownSelf val = either (throwKnownTypeErrorWithCause val) pure $ readKnown v
{-# INLINE readKnownSelf #-}

instance MakeKnownIn uni val a => MakeKnownIn uni val (EvaluationResult a) where
makeKnown EvaluationFailure = throwing_ _EvaluationFailure
makeKnown EvaluationFailure = MakeKnownFailure mempty KnownTypeEvaluationFailure
makeKnown (EvaluationSuccess x) = makeKnown x
{-# INLINE makeKnown #-}

Expand All @@ -291,7 +352,8 @@ instance
readKnown _ = throwing _UnliftingError "Panic: 'TypeError' was bypassed"

instance MakeKnownIn uni val a => MakeKnownIn uni val (Emitter a) where
makeKnown = lift >=> makeKnown
makeKnown a = case runEmitter a of
(x, logs) -> withLogs logs $ makeKnown x
{-# INLINE makeKnown #-}

instance
Expand Down
3 changes: 1 addition & 2 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ import PlutusCore.Builtin.TypeScheme
import PlutusCore.Core
import PlutusCore.Name

import Control.Monad.Except
import Data.Array
import Data.Kind qualified as GHC
import Data.Proxy
Expand Down Expand Up @@ -177,7 +176,7 @@ instance (res ~ res', Typeable res, KnownTypeAst (UniOf val) res, MakeKnown val

-- For deferred unlifting we need to lift the 'ReadKnownM' action into 'MakeKnownM',
-- hence 'liftEither'.
toDeferredF getRes = liftEither getRes >>= makeKnown
toDeferredF getRes = liftReadKnownM getRes >>= makeKnown
{-# INLINE toDeferredF #-}

-- | Every term-level argument becomes as 'TypeSchemeArrow'.
Expand Down
8 changes: 6 additions & 2 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
Original file line number Diff line number Diff line change
Expand Up @@ -102,10 +102,14 @@ data UnliftingMode
-- former by choosing the runtime denotation of the builtin (either '_broImmediateF' for immediate
-- unlifting or '_broDeferredF' for deferred unlifting, see 'UnliftingMode' for details) and by
-- instantiating '_broToExF' with a cost model to get the costing function for the builtin.
--
-- The runtime denotations are lazy, so that we don't need to worry about a builtin being bottom
-- (happens in tests). The production path is not affected by that, since 'BuiltinRuntimeOptions'
-- doesn't survive optimization.
data BuiltinRuntimeOptions n val cost = BuiltinRuntimeOptions
{ _broRuntimeScheme :: RuntimeScheme n
, _broImmediateF :: ToRuntimeDenotationType val n
, _broDeferredF :: ToRuntimeDenotationType val n
, _broImmediateF :: ~(ToRuntimeDenotationType val n)
, _broDeferredF :: ~(ToRuntimeDenotationType val n)
, _broToExF :: cost -> ToCostingType n
}

Expand Down
10 changes: 4 additions & 6 deletions plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -67,12 +67,10 @@ evalBuiltinApp
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
evalBuiltinApp term runtime@(BuiltinRuntime sch getX _) = case sch of
RuntimeSchemeResult -> do
let (errOrRes, logs) = runEmitter $ runExceptT getX
emitCkM logs
case errOrRes of
Left err -> throwKnownTypeErrorWithCause term err
Right res -> pure res
RuntimeSchemeResult -> case getX of
MakeKnownFailure logs err -> emitCkM logs *> throwKnownTypeErrorWithCause term err
MakeKnownSuccess x -> pure x
MakeKnownSuccessWithLogs logs x -> emitCkM logs $> x
_ -> pure $ VBuiltin term runtime

ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
Expand Down
2 changes: 1 addition & 1 deletion plutus-core/plutus-core/test/Evaluation/Spec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ prop_builtinEvaluation bn mkGen f = property $ do
MakeKnownM (Term uni fun)
go sch fn args = case (sch, args) of
(RuntimeSchemeArrow sch', a : as) -> do
res <- liftEither (fn a)
res <- liftReadKnownM (fn a)
go sch' res as
(RuntimeSchemeResult, []) -> fn
(RuntimeSchemeAll sch', _) -> go sch' fn args
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -569,11 +569,12 @@ evalBuiltinApp
evalBuiltinApp fun term runtime@(BuiltinRuntime sch getX cost) = case sch of
RuntimeSchemeResult -> do
spendBudgetCek (BBuiltinApp fun) cost
let !(errOrRes, logs) = runEmitter $ runExceptT getX
?cekEmitter logs
case errOrRes of
Left err -> throwKnownTypeErrorWithCause term err
Right res -> pure res
case getX of
MakeKnownFailure logs err -> do
?cekEmitter logs
throwKnownTypeErrorWithCause term err
MakeKnownSuccess x -> pure x
MakeKnownSuccessWithLogs logs x -> ?cekEmitter logs $> x
_ -> pure $ VBuiltin fun term runtime
{-# INLINE evalBuiltinApp #-}

Expand Down