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
123 changes: 94 additions & 29 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,25 +13,25 @@
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE StrictData #-}

module PlutusCore.Builtin.KnownType
( KnownTypeError
, 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 +184,85 @@ 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
effectfully marked this conversation as resolved.
Show resolved Hide resolved
-- deconstruct a redundant tuple
--
-- Moving from @ExceptT KnownTypeError Emitter@ to this data type gave us a speedup of 8% of total
-- evaluation time.
--
-- Logs are represented as a 'DList', because we don't particularly care about the efficiency of
-- logging, since there's no logging on the chain and builtins don't emit much anyway. Otherwise
-- we'd have to use @text-builder@ or @text-builder-linear@ or something of this sort.
data MakeKnownM a
= MakeKnownFailure (DList Text) KnownTypeError
| MakeKnownSuccess a
| MakeKnownSuccessWithLogs (DList Text) a

-- | 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
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 = withLogs logs $ fmap f a
{-# INLINE (<*>) #-}

-- Better than the default implementation, because the value in the 'MakeKnownSuccess' case
-- doesn't need to be retained.
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
zliu41 marked this conversation as resolved.
Show resolved Hide resolved
{-# 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 @@ -232,9 +294,14 @@ class uni ~ UniOf val => MakeKnownIn uni val a where
-- The inverse of 'readKnown'.
makeKnown :: a -> MakeKnownM val
default makeKnown :: KnownBuiltinType val a => a -> MakeKnownM val
-- Forcing the value to avoid space leaks. Note that the value is only forced to WHNF,
-- so care must be taken to ensure that every value of a type from the universe gets forced
-- to NF whenever it's forced to WHNF.
-- Everything on evaluation path has to be strict in production, so in theory we don't need to
-- force anything here. In practice however all kinds of weird things happen in tests and @val@
-- can be non-strict enough to cause trouble here, so we're forcing the argument. Looking at the
-- generated Core, the forcing amounts to pulling a @case@ out of the 'fromConstant' call,
-- which doesn't affect the overall cost and benchmarking results suggest the same.
--
-- Note that the value is only forced to WHNF, so care must be taken to ensure that every value
-- of a type from the universe gets forced to NF whenever it's forced to WHNF.
makeKnown x = pure . fromConstant . someValue $! x
{-# INLINE makeKnown #-}

Expand All @@ -253,15 +320,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 +338,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 +355,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