Optimizing Haskell Code for Runtime Verification: Part 2

This is the second part of our series on optimizing Haskell code for Runtime Verification series. If you haven’t had a chance to read the first part yet, you can find it here.

In this article, we will continue to describe the implementation of the solutions to the problems described in the previous article. Specifically, we will cover the completion of monomorphization and specialization, as well as the solution to the hashing performance issue in the Simplifier cache.

Monomorphization and specialization of Simplifier

In the first part, we discussed simplifying the codebase of the K Framework by unifying SMT and NoSMT. In this part, we continue the optimization process by removing the SimplifierT monad transformer and replacing it with a concrete Simplifier monad that is built on top of the new SMT. This simplification enables us to enhance performance by specializing and monomorphizing the MonadSimplify simplifier for a specific monad.

Simplifier

Previously, the Simplifier was implemented using a monad transformer, SimplifierT smt a, which was parameterized by the SMT solver type. The definition looked like this:

newtype SimplifierT smt a = SimplifierT (StateT SimplifierCache (ReaderT (Env (SimplifierT smt)) smt) a)

type Simplifier = SimplifierT SMT

The smt type variable could be instantiated to either SMT or NoSMT, depending on whether an external SMT solver was available. However, since SMT and NoSMT have been unified, we could now define the Simplifier as a base monad without the transformer:

newtype Simplifier a = Simplifier (StateT SimplifierCache (ReaderT Env SMT) a)

This new definition is simpler and allows us to remove the parameterization from Env.

We have also introduced a new function called liftSimplifier to the MonadSimplify class, similar to how we added liftSMT in the previous article:

class (MonadLog m, MonadSMT m) => MonadSimplify m where
    liftSimplifier :: Simplifier a -> m a
    default liftSimplifier ::
        (MonadTrans t, MonadSimplify n, m ~ t n) =>
        Simplifier a ->
        m a
    liftSimplifier = lift . liftSimplifier
    {-# INLINE liftSimplifier #-}

...

For the Simplifier instance of the MonadSimplify class, liftSimplifier can be defined simply as liftSimplifier = id. This allows us to lift Simplifier computations into any monad with a MonadSimplify instance.

trace-usage

Our next objective is to monomorphize the functions that contain the MonadSimplify constraint by substituting concrete types for the abstract type parameter m satisfying MonadSimplify. Then we aim to specialize the functions that contain the MonadSimplify constraint by putting the SPECIALIZE pragmas for such functions where monomorphization is impossible due to multiple types being substituted for the abstract ones during the run of the executable.

To aid in this process, we used a tool called trace-usage, which was mentioned in Findings section of previous article. We created a branch, where every function with MonadSimplify in its type signature is wrapped in Debug.Trace.Usage.traceUsage. The branch has been utilized to generate reports on what concrete types had been substituted when running the program.

The reports are structured as lines that look like this: N Module.function Type, where N represents the number of times the type Type has been instantiated when running the function Module.function. These reports provide insights into whether we can monomorphize the functions (if only one type is being instantiated) or specialize them (if at least two types are being instantiated). In the latter case, we need to select the types instantiated the most and place SPECIALIZE pragmas with the type signatures including the selected types.

The report generated using traceUsage revealed some very weird type instantiations, such as this example:

2 Kore.Builtin.Bool.unifyBoolAnd: UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (UnifierT (LogicT Simplifier)))))))))))))))))))))))))

We found that a pattern of heavily nested UnifierT types appears in almost every function that uses the MonadUnify constraint, which is essentially a combination of MonadSimplify and MonadLogic. The definition of UnifierT is as follows:

newtype UnifierT (m :: Type -> Type) a = UnifierT
    { getUnifierT ::
        ReaderT
            (ConditionSimplifier (UnifierT m))
            (LogicT m)
            a
    }

The MonadUnify class has no methods and is defined as:

class (MonadLogic unifier, MonadSimplify unifier) => MonadUnify unifier

The main purpose of MonadUnify is to abstract over a combination of MonadLogic and MonadSimplify constraints, and provide an error-handling mechanism for unification errors using ExceptT over UnificationError within a Simplifier monad.

Nested UnifierT

To investigate the root cause of the UnifierT nesting, we created a closed type family NotUnifierT:

type family NotUnifierT (m :: Type -> Type) :: Constraint where
    NotUnifierT (UnifierT m) = TypeError ( 'Text "Should not be UnifierT" ':$$: 'ShowType (UnifierT m))
    NotUnifierT _ = ()

This type family takes a type parameter m and returns a trivial constraint that is always satisfied if m is not UnifierT. However, if m is UnifierT, it returns a custom TypeError with the message “Should not be UnifierT” and the actual type that caused the error.

For more on type families in Haskell, check out our blog post: Type Families in Haskell: The Definitive Guide.

We added a NotUnifierT m constraint to the MonadUnify (UnifierT m) instance like this:

instance (MonadSimplify m, NotUnifierT m) => MonadUnify (UnifierT m)

This allows us to catch the situation where at least one level of nesting is present. If m is UnifierT, then we’re working in UnifierT (UnifierT n), which triggers our custom type error.

To address the circular dependencies caused by the imports of NotUnifierT in certain modules, we split the relevant declarations and definitions between the hs-boot files for Kore.Unification.UnifierT and Kore.Unification.NotUnifierT. Then we used {-# SOURCE #-} imports to these modules to break the circular dependencies in relevant places.

After adding the constraint to the relevant type signatures, we encountered the first instance of the custom type error in Kore.Simplify.Not.notSimplifier. The notSimplifier is defined as follows:

notSimplifier :: MonadSimplify simplifier => NotSimplifier simplifier
notSimplifier = NotSimplifier simplify

Here, simplify is a function used to simplify Not pattern in Kore language.

We observed that the notSimplifier was used in multiple places, and one such instance was in the termEqualsAnd function:

termEqualsAnd ::
    HasCallStack =>
    TermLike RewritingVariableName ->
    TermLike RewritingVariableName ->
    MaybeT (LogicT Simplifier) (Pattern RewritingVariableName)
termEqualsAnd p1 p2 =
    MaybeT $ run $ maybeTermEqualsWorker p1 p2
  where
    run it =
        (runUnifierT Not.notSimplifier . runMaybeT) it
            >>= Logic.scatter

    maybeTermEqualsWorker ::
        forall unifier.
        MonadUnify unifier =>
        TermLike RewritingVariableName ->
        TermLike RewritingVariableName ->
        MaybeT unifier (Pattern RewritingVariableName)
    maybeTermEqualsWorker =
        maybeTermEquals Not.notSimplifier termEqualsAndWorker

    termEqualsAndWorker ::
        forall unifier.
        MonadUnify unifier =>
        TermLike RewritingVariableName ->
        TermLike RewritingVariableName ->
        unifier (Pattern RewritingVariableName)
    termEqualsAndWorker first second =
        scatterResults
            =<< runUnification (maybeTermEqualsWorker first second)
      where
        runUnification = runUnifierT Not.notSimplifier . runMaybeT
        scatterResults =
            maybe
                (return equalsPattern)
                Logic.scatter
                . sequence

The function runUnification, which is defined in a where block of termEqualsAndWorker, has a type signature of MaybeT (UnifierT unifier) a -> unifier [a]. In this signature, unifier is constrained by MonadUnify in the termEqualsAndWorker. The only available instance of MonadUnify is UnifierT m, meaning that argument to runUnification must have at least one redundant UnifierT. Additionally, runUnification is called inside of termEqualsAndWorker, which is mutually recursive with maybeTermEqualsWorker. This mutual recursion was the main source of the nesting of UnifierT.

We replaced the runUnification function with runMaybeT in termEqualsAndWorker, and made a slight modification to scatterResults to match this change:

scatterResults = pure . fromMaybe equalsPattern . Logic.scatter

After implementing the change, we used our trace-usage utility and found that most of the nested UnifierTs had been removed. However, some functions still had an extra level of UnifierT.

We revisited the notSimplifier and traced its usage to identify the last remaining redundant layer of UnifierT. We observed two things. Firstly, the runUnifierT function takes notSimplifier as an argument of type MonadSimplify m => NotSimplifier (UnifierT m):

runUnifierT ::
    MonadSimplify m =>
    NotSimplifier (UnifierT m) ->
    UnifierT m a ->
    m [a]
runUnifierT notSimplifier = observeAllT . evalEnvUnifierT notSimplifier

Secondly, we noticed that the simplify function, used to define notSimplifier, eventually calls the termAnd function:

termAnd ::
    forall simplifier.
    MonadSimplify simplifier =>
    HasCallStack =>
    NotSimplifier (UnifierT simplifier) ->
    TermLike RewritingVariableName ->
    TermLike RewritingVariableName ->
    LogicT simplifier (Pattern RewritingVariableName)
termAnd notSimplifier p1 p2 =
    Logic.scatter
        =<< (lift . runUnifierT notSimplifier) (termAndWorker p1 p2)
  where
    termAndWorker ::
        TermLike RewritingVariableName ->
        TermLike RewritingVariableName ->
        UnifierT simplifier (Pattern RewritingVariableName)
    termAndWorker first second =
        maybeTermAnd notSimplifier termAndWorker first second
            & runMaybeT
            & fmap (fromMaybe andPattern)
      where
        andPattern = Pattern.fromTermLike (mkAnd first second)

Here, we also call runUnifierT, which requires NotSimplifier (UnifierT simplifier). However, in this case, simplifier is already specified as MonadSimplify m => UnifierT m. If we substitute this in the type signature of runUnifierT, we get:

runUnifierT :: MonadSimplify m => NotSimplifier (UnifierT (UnifierT m)) -> UnifierT (UnifierT m) a -> UnifierT m [a]

Therefore, termAndWorker has the type:

termAndWorker ::
    TermLike RewritingVariableName ->
    TermLike RewritingVariableName ->
    UnifierT (UnifierT simplifier) (Pattern RewritingVariableName)

In this case, runUnifierT removes the outer UnifierT, and the inner UnifierT belongs to notSimplifier, which calls this function.

To address this issue, we opted to eliminate UnifierT from NotSimplifier in the runUnifierT function, resulting in the following type signature:

runUnifierT :: MonadSimplify m => NotSimplifier m -> UnifierT m a -> m [a]

As a result of this modification, we needed to remove the UnifierT type variable from the definition of NotSimplifier in all other functions where notSimplifier was passed as an argument. Additionally, we changed NotSimplifier from a data type to a class to avoid the need for manual passing.

After implementing the changes, the trace-usage tool showed that there were no longer any nested UnifierT types in our code. This enabled us to monomorphize and specialize the simplifier type variables, which can improve performance. The compiler can now inline code of this functions, leading to additional optimizations.

Monomorphization and specialization

We used the trace-usage report to identify type variables that could be replaced with concrete types if only one type was instantiated during execution. For those whose type variables were instantiated to multiple different types, we added SPECIALIZE pragmas. We found that most functions could be monomorphized, and only a few required specialization. The process of monomorphization and specialization was divided into five pull requests: part 1, part 2, part 3, part 4, and part 5.

During this process, we also encountered cases of nested MaybeT and ReaderT caused by redundant maybeT and runReaderT calls, which added an unnecessary transformer layer in the argument. We resolved these issues by removing these redundant calls, which were straightforward solutions. We implemented these fixes in the pull requests titled Remove nested ReaderT and Remove nested MaybeT.

Summary

In this step, we simplified the types in codebase by introducing a concrete Simplifier monad to replace the SimplifierT transformer. This was possible because we had previously unified SMT and NoSMT. We also addressed the issues with nested transformers, which allowed us to monomorphize most of the type variables that were constrained by MonadSimplify. For functions not suitable for monomorphization, we added SPECIALIZE pragmas. This simplified the types and resulted in a speedup of approximately 15%.

In addition, the trace-usage report indicated that all type variables constrained by MonadUnify were instantiated to UnifierT Simplifier. However, we cannot monomorphize these type variables as it would create circular dependencies. Nonetheless, it is planned to replace UnifierT with a new implementation of the concrete Unifier monad on top of Simplifier, which will have a more principled implementation of the unification algorithm. The fact that all type variables constrained by MonadUnify are instantiated to UnifierT Simplifier is a positive indication towards this replacement.

Hashing problem

As we described in our previous blog post, although the cache was performing well with a high hit ratio, the lookup function was causing a bottleneck due to the time spent on hashing and comparing keys. To address this issue, there were two potential solutions: switch to a different data structure that avoids hashing and comparisons entirely or try to minimize the amount of time required to hash and compare keys by micro-optimizing the respective operations.

SimplifierChache

Let’s first take a look at what the cache looks like. SimplifierCache is a HashMap cache used to keep track of equations that have already been attempted but failed to apply:

newtype SimplifierCache = SimplifierCache
    { attemptedEquationsCache ::
        HashMap
            EvaluationAttempt
            (AttemptEquationError RewritingVariableName)
    }

The EvaluationAttempt data type is used as the key in the HashMap. It’s defined as a pair of an equation and a term:

data EvaluationAttempt = EvaluationAttempt
    { cachedEquation :: Equation RewritingVariableName
    , cachedTerm :: TermLike RewritingVariableName
    }
    deriving stock (Eq, Ord)
    deriving stock (GHC.Generic)
    deriving anyclass (Hashable)

The Equation data type is utilized to represent equational rules in K , which may take the form of either function definition or simplification rules. Its definition is as follows:

data Equation variable = Equation
    { requires :: !(Predicate variable)
    , argument :: !(Maybe (Predicate variable))
    , antiLeft :: !(Maybe (Predicate variable))
    , left :: !(TermLike variable)
    , right :: !(TermLike variable)
    , ensures :: !(Predicate variable)
    , attributes :: !(Attribute.Axiom Symbol variable)
    }

The TermLike data type serves as the internal representation of patterns, especially terms, in the Kore language. Under the hood, TermLike is essentially the Cofree data type from the free package. However, rather than defining a newtype over Cofree, TermLike is defined inline for performance reasons. This performance boost comes from the fact that the instances of the Recursive and Corecursive classes from the recursion-schemes package correspond to unwrapping and wrapping the newtype, respectively, which is done for free at runtime.

The definitions of TermLike, Recursive, and Corecursive are as follows:

newtype TermLike variable = TermLike
    { getTermLike ::
        CofreeF
            (TermLikeF variable)
            (TermAttributes variable)
            (TermLike variable)
    }

instance Recursive (TermLike variable) where
    project = getTermLike
    {-# INLINE project #-}

instance Corecursive (TermLike variable) where
    embed = TermLike
    {-# INLINE embed #-}

Cofree allows us to create a data structure that is both recursive and comonadic, which can be useful for representing data with a tree-like structure, such as abstract syntax trees. The basic idea is that we can attach annotations or metadata to the nodes of the tree while preserving the underlying structure, which makes it possible to define operations that traverse the tree while also accessing the annotations.

The TermLikeF type is a so-called base functor that is used to represent the structure of an abstract syntax tree. Its definition looks like this:

data TermLikeF variable child
    = AndF !(And Sort child)
    | ApplySymbolF !(Application Symbol child)
    | ApplyAliasF !(Application (Alias (TermLike VariableName)) child)
    | BottomF !(Bottom Sort child)
    | CeilF !(Ceil Sort child)
    | DomainValueF !(DomainValue Sort child)
    | EqualsF !(Equals Sort child)
    | ExistsF !(Exists Sort variable child)
    | FloorF !(Floor Sort child)
    | ForallF !(Forall Sort variable child)
    | IffF !(Iff Sort child)
    | ImpliesF !(Implies Sort child)
    | InF !(In Sort child)
    | MuF !(Mu variable child)
    | NextF !(Next Sort child)
    | NotF !(Not Sort child)
    | NuF !(Nu variable child)
    | OrF !(Or Sort child)
    | RewritesF !(Rewrites Sort child)
    | TopF !(Top Sort child)
    | InhabitantF !(Inhabitant child)
    | StringLiteralF !(Const StringLiteral child)
    | InternalBoolF !(Const InternalBool child)
    | InternalBytesF !(Const InternalBytes child)
    | InternalIntF !(Const InternalInt child)
    | InternalStringF !(Const InternalString child)
    | InternalListF !(InternalList child)
    | InternalMapF !(InternalMap Key child)
    | InternalSetF !(InternalSet Key child)
    | VariableF !(Const (SomeVariable variable) child)
    | EndiannessF !(Const Endianness child)
    | SignednessF !(Const Signedness child)
    | InjF !(Inj child)

The TermAttributes type is used to represent the attributes of a pattern that are collected during verification.

data TermAttributes variable = TermAttributes
    { termSort :: !Sort
    , termFreeVariables :: !(Attribute.FreeVariables variable)
    , termFunctional :: !Attribute.Functional
    , termFunction :: !Attribute.Function
    , termDefined :: !Attribute.Defined
    , termCreated :: !Attribute.Created
    , termSimplified :: !Attribute.Simplified
    , termConstructorLike :: !Attribute.ConstructorLike
    }

Replacing the data structure

One potential solution to this issue is to replace the existing HashMap data structure with a different one. In an attempt to address the problem, we initially tried to replace it with the strict Map data structure from the containers package, which would eliminate the need for hashing altogether. Despite the fact that this replacement eliminated the bottleneck caused by hashing, we discovered that it actually resulted in an overall performance degradation.

In our second attempt we opted to use the trie map data structure from the trie-simple package.

The trie data structure TMap c v is used to store a mapping from a list of characters to a value of some sort. This data structure is essentially isomorphic to the Map [c] v structure, but provides better querying efficiency compared to the latter.

In order to take advantage of the TMap data structure, we had to flatten our EvaluationAttempt data type manually, which is used as a key. For this purpose, we introduced a large data type called Component that describes every possible component of terms and predicates used in EvaluationAttempt:

data Component
    = CPredicate
    | CNoPredicate
    | CTermLike
    | CAxiom !(Axiom Symbol RewritingVariableName)
    | CElementalVariable !(Syntax.ElementVariable RewritingVariableName)
    | CSetVariable !(Syntax.SetVariable RewritingVariableName)
    | CSort !Sort
    | CSymbol !Symbol
    | CAnd
    | CApplySymbol
    | CApplyAlias !Syntax.Id
    | CBottom
    | CCeil
    | CDomainValue
    | CEquals
    | CExists
    | CFloor
    | CForall
    | CIff
    | CImplies
    | CIn
    | CMu
    | CNext
    | CNot
    | CNu
    | COr
    | CRewrites
    | CTop
    | CInhabitant
    | CStringLiteral !StringLiteral
    | CInternalBool !InternalBool
    | CInternalBytes !InternalBytes
    | CInternalInt !InternalInt
    | CInternalString !InternalString
    | CInternalList
    | CInternalMap !(InternalMap Key (TermLike RewritingVariableName))
    | CInternalSet !(InternalSet Key (TermLike RewritingVariableName))
    | CVariable !(Syntax.SomeVariable RewritingVariableName)
    | CEndianness !Endianness
    | CSignedness !Signedness
    | CInj !Syntax.Id

We also defined a function called flatten that maps the complex tree-like structure of the EvaluationAttempt data type to a flat list of Components.

Once again, we were successful in eliminating performance issues caused by hashing. However, we didn’t observe any noticeable improvement in performance due to the need for flattening keys.

Pre-hashing

To potentially address the performance issue, we considered pre-calculating the hashes and thus avoiding the repeated hashing of the same data. Initially, we opted to pre-hash the Equation data type by adding an additional field to store the pre-calculated hash:

data Equation variable = Equation
    { requires :: !(Predicate variable)
    , argument :: !(Maybe (Predicate variable))
    , antiLeft :: !(Maybe (Predicate variable))
    , left :: !(TermLike variable)
    , right :: !(TermLike variable)
    , ensures :: !(Predicate variable)
    , attributes :: !(Attribute.Axiom Symbol variable)
    , equationHash :: !Int
    }

Furthermore, we implemented a new data type called EquationNoHash, which mirrors the previous version of Equation without the equationHash field. To complement this, we also created a smart constructor for Equation that calculates the hash value of EquationNoHash:

{-# INLINE mkEquation' #-}
mkEquation' ::
    Hashable variable =>
    (Predicate variable) ->
    (Maybe (Predicate variable)) ->
    (Maybe (Predicate variable)) ->
    (TermLike variable) ->
    (TermLike variable) ->
    (Predicate variable) ->
    (Attribute.Axiom Symbol variable) ->
    Equation variable
mkEquation' req arg antiLeft left right ensures attrs eqHash  =
    Equation req arg antiLeft left right ensures attrs eqHash
        (hash $ EquationNoHash req arg antiLeft left right ensures attrs)

Thus, we could define a Hashable instance for Equation by directly accessing the equationHash field:

instance Hashable (Equation equation) where
    hashWithSalt _ = equationHash
    {-# INLINE hashWithSalt #-}

Unfortunately, pre-hashing the Equation data type improved the speed by only 1%.

As the next step, we attempted to pre-hash the TermLike data type. To achieve this, we added a new wrapper type called PreHashed to pre-hash the TermLike data type, and also included a smart constructor for it:

data PreHashed a = PreHashed
    { preHashed :: !a
    , preHash :: ~Int
    }
    deriving stock (Generic)
    deriving anyclass (NFData)

mkPreHashed :: Hashable a => a -> PreHashed a
mkPreHashed !a = PreHashed a (hash a)
{-# INLINE mkPreHashed #-}

This type is similar to the Data.Hashable.Hashed type, but it has a few differences:

• It has a lazy hash.
• It has a strict a.
• The Eq instance does not use the hash (to avoid evaluating it).

This change, however, resulted in a negligible impact with only a 0.33% overall speedup.

Our next attempt was to pre-compute hash for the term and store it in TermAttributes of TermLike. This pre-computed hash is then accessed by the Hashable instance rather than recursively traversing the TermLikeF data structure. To implement this, we added a new field termHash to TermAttributes to store the pre-computed hash value, just like we did for the Equation type:

data TermAttributes variable = TermAttributes
    { termSort :: !Sort
    , termFreeVariables :: !(Attribute.FreeVariables variable)
    , termFunctional :: !Attribute.Functional
    , termFunction :: !Attribute.Function
    , termDefined :: !Attribute.Defined
    , termCreated :: !Attribute.Created
    , termSimplified :: !Attribute.Simplified
    , termConstructorLike :: !Attribute.ConstructorLike
    , termHash :: Int -- caches the TermLikeF hash value for efficiency
    }

To compute the hash value using the hashWithSalt function, we used the pre-computed hash value stored in termHash, along with the provided salt value:

instance Hashable variable => Hashable (TermLike variable) where
    hashWithSalt salt (Recursive.project -> TermAttributes{termHash} :< _) =
        salt `hashWithSalt` termHash
    {-# INLINE hashWithSalt #-}

To produce the pre-computed hash value, we used the derived Hashable instance of TermLikeF, which will call hash on the respective sub-structure wrapped into one of the TermLikeF constructors. For all such sub-structures, the derived Hashable instance will then recurse into the contents, using the cached hashes directly instead of performing a deep recursion.

Although the change resulted in a 6% speedup, it also caused some integration tests to fail, and unfortunately, we were unable to find a way to fix them while keeping the pre-computed hash in TermAttributes.

So, to avoid storing pre-computed hash in TermAttributes, we cached the hash of the TermLikeF in the TermLike itself and extracted it in the Hashable instance instead of recursively traversing into the TermLikeF. To achieve this, we modified the TermLike definition:

data TermLike variable = TermLike__
    -- Some fields below are lazy to better match Cofree.
    { _tlAttributes :: ~(TermAttributes variable)
    , -- | A hash of _tlTermLikeF
      _tlHash :: ~Int
    , _tlTermLikeF :: ~(TermLikeF variable (TermLike variable))
    }

We replaced the CofreeF type with a record that includes the _tlHash field storing the pre-computed hash of _tlTermLikeF.

Here are the updated Hashable, Recursive, and Corecursive instances for the modified TermLike:

instance Eq variable => Hashable (TermLike variable) where
    hashWithSalt salt (TermLike__ _ hsh _) =
        salt `hashWithSalt` hsh
    {-# INLINE hashWithSalt #-}

instance Recursive (TermLike variable) where
    project = getTermLike
    project (TermLike__ attr _hash pat) = attr :< pat
    {-# INLINE project #-}

instance Corecursive (TermLike variable) where
    embed = TermLike
instance Hashable variable => Corecursive (TermLike variable) where
    embed (attr :< pat) = TermLike__ attr (hash pat) pat
    {-# INLINE embed #-}

In addition, a Lens' was added for editing the TermAttributes of a TermLike, which is more efficient than using project followed by embed because it avoids recomputing the hash on embed:

termLikeAttributes :: Lens' (TermLike variable) (TermAttributes variable)
termLikeAttributes =
    Lens.lens
        (\(TermLike__ attrs _ _) -> attrs)
        ( \(TermLike__ _ hsh termLikeF) attrs ->
            TermLike__ attrs hsh termLikeF
        )

Summary

To address this problem, we used pre-computation of the hash value to reduce the computational cost of computing the hash. In the case of the modified TermLike data structure, we pre-computed the hash value of the TermLikeF component and used it in the Hashable instance to avoid recomputing the hash. We also modified the Recursive and Corecursive type class instances to account for the pre-computed hash field in TermLike. In total, the changes above improve performance by approximately 10%.

Conclusion

In the second phase of our collaboration with Runtime Verification, we finished work on the problems described in the first article.

In the second part of the monomorphization and specialization task, we replaced SimplifierT with a concrete Simplifier monad. This was possible because we had unified SMT and NoSMT before. We also addressed the issues with nested transformers, which allowed us to monomorphize most of the type variables that were constrained by MonadSimplify. This not only simplified the types but also resulted in a 15% speedup. Moreover, we also cleaned up the code in preparation for the future replacement of the Unifier implementation.

The other task involved optimizing the cache by pre-computing the hash of keys. We modified the TermLike data type to include a pre-computed hash value of TermLikeF. This reduced the time spent on computing hash values, which resulted in a performance improvement of approximately 10%.

To ensure you don’t miss any of our future blog posts, stay updated by following us on Twitter or subscribe to our mailing list using the form below.