Skip to content

Commit

Permalink
[ Serialize ] Memoize A.QNames as a whole.
Browse files Browse the repository at this point in the history
Serialization of the std-lib is now TWICE as fast
(from 60s down to 30s). For example on
  https://code.google.com/p/agda/issues/detail?id=1533
serialization is FOUR times as fast (from 54s to 15s).

BEFORE maint$ make library-test
==============================

Finished README.
Total                      116,813ms
Miscellaneous                  687ms
Parsing                        511ms
Parsing.Operators            9,636ms
Import                         748ms
Deserialization                  4ms
Scoping                      3,346ms
Typing                      36,948ms
Termination                    638ms
Termination.Graph              133ms
Termination.RecCheck           652ms
Termination.Compare            144ms
Positivity                   2,490ms
Injectivity                    494ms
ProjectionLikeness              80ms
Coverage                     1,021ms
Highlighting                   305ms
Serialization               53,251ms
Serialization.Sort             291ms
Serialization.BinaryEncode   4,672ms
Serialization.Compress         746ms
ModuleName                       8ms

 133,716,008,712 bytes allocated in the heap
  13,239,588,424 bytes copied during GC
     703,106,800 bytes maximum residency (32 sample(s))
       8,151,504 bytes maximum slop
            1361 MB total memory in use (16 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     14669 colls,     0 par   19.245s  19.275s     0.0013s    0.2270s
  Gen  1        32 colls,     0 par   19.456s  19.504s     0.6095s    2.7494s

  INIT    time    0.000s  (  0.000s elapsed)
  MUT     time   77.727s  ( 78.116s elapsed)
  GC      time   38.701s  ( 38.779s elapsed)
  EXIT    time    0.296s  (  0.296s elapsed)
  Total   time  116.725s  (117.192s elapsed)

  %GC     time      33.2%  (33.1% elapsed)

  Alloc rate    1,720,319,039 bytes per MUT second

  Productivity  66.8% of total user, 66.6% of total elapsed

real	1m57.251s
user	1m56.725s
sys	0m0.448s

AFTER maint$ make library-test
==============================

Finished README.
Total                      83,215ms
Miscellaneous                 528ms
Parsing                       473ms
Parsing.Operators           9,336ms
Import                        914ms
Deserialization                 5ms
Scoping                     3,179ms
Typing                     29,480ms
Typing.OccursCheck          1,890ms
Termination                   504ms
Termination.Graph             117ms
Termination.RecCheck          725ms
Termination.Compare           198ms
Positivity                  2,666ms
Injectivity                   492ms
ProjectionLikeness             85ms
Coverage                      995ms
Highlighting                  320ms
Serialization              25,320ms
Serialization.Sort            217ms
Serialization.BinaryEncode  4,780ms
Serialization.Compress        974ms
ModuleName                      8ms

 109,823,929,840 bytes allocated in the heap
  12,698,461,640 bytes copied during GC
     543,366,680 bytes maximum residency (31 sample(s))
       3,559,128 bytes maximum slop
            1352 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1168 colls,     0 par   14.154s  14.187s     0.0121s    0.2196s
  Gen  1        31 colls,     0 par    6.388s   6.431s     0.2074s    0.6551s

  INIT    time    0.000s  (  0.000s elapsed)
  MUT     time   62.155s  ( 62.662s elapsed)
  GC      time   20.543s  ( 20.618s elapsed)
  EXIT    time    0.263s  (  0.263s elapsed)
  Total   time   82.961s  ( 83.543s elapsed)

  %GC     time      24.8%  (24.7% elapsed)

  Alloc rate    1,766,928,832 bytes per MUT second

  Productivity  75.2% of total user, 74.7% of total elapsed

real	1m23.606s
user	1m22.961s
sys	0m0.580s
  • Loading branch information
andreasabel committed Jun 4, 2015
1 parent a157a9a commit f7b47de
Showing 1 changed file with 19 additions and 27 deletions.
46 changes: 19 additions & 27 deletions src/full/Agda/TypeChecking/Serialise.hs
Expand Up @@ -33,15 +33,14 @@ module Agda.TypeChecking.Serialise
)
where

import GHC.Generics (Generic)

import Control.Applicative
import Control.Arrow (first, second)
import Control.DeepSeq
import qualified Control.Exception as E
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State.Strict

import Data.Array.IArray
import Data.Word
import qualified Data.ByteString.Lazy as L
Expand All @@ -60,8 +59,11 @@ import qualified Data.Binary.Put as B
import qualified Data.List as List
import Data.Function
import Data.Typeable ( cast, Typeable, typeOf, TypeRep )

import qualified Codec.Compression.GZip as G

import GHC.Generics (Generic)

import qualified Agda.Compiler.Epic.Interface as Epic

import Agda.Syntax.Common as Common
Expand Down Expand Up @@ -287,7 +289,7 @@ encode a = do
modifyStatistics $ Map.union stats
-- Encode hashmaps and root, and compress.
bits1 <- Bench.billTo [ Bench.Serialization, Bench.BinaryEncode ] $
returnForcedByteString $ B.encode (root, nL, sL, iL, dL)
returnForcedByteString $ B.encode (root, nL, sL, iL, dL, qL)
let compressParams = G.defaultCompressParams
{ G.compressLevel = G.bestSpeed
, G.compressStrategy = G.huffmanOnlyStrategy
Expand Down Expand Up @@ -419,34 +421,24 @@ decodeHashes s
decodeFile :: FilePath -> TCM (Maybe Interface)
decodeFile f = decodeInterface =<< liftIO (L.readFile f)


deriving instance Generic NamePart
deriving instance Generic C.Name
deriving instance Generic NameId
-- deriving instance Generic AbsolutePath -- in Agda.Utils.FileName
deriving instance Generic a => Generic (Position' a)
deriving instance Generic a => Generic (Interval' a)
deriving instance Generic a => Generic (Range' a)
deriving instance Generic Associativity
deriving instance (Generic a, Generic b) => Generic (Common.Arg a b)
deriving instance (Generic a, Generic b) => Generic (Common.Named a b)
deriving instance Generic GenPart
deriving instance Generic Fixity
deriving instance Generic Fixity'
deriving instance Generic A.Name
deriving instance Generic A.ModuleName
deriving instance Generic A.QName

-- Andreas, 2015-06-04 AIM XXI: Memoize A.QName
-- The following instances of Binary allow for a direct serialization of A.QName
-- this is needed for serialization of HashTable A.QName Int32.
instance Binary AbsolutePath
instance Binary NamePart
instance Binary C.Name
instance Binary NameId
instance Binary AbsolutePath
instance (Binary a) => Binary (Position' a)
instance (Binary a) => Binary (Interval' a)
instance (Binary a) => Binary (Range' a)
instance Binary Associativity
instance (Binary a, Binary b) => Binary (Common.Arg a b)
instance (Binary a, Binary b) => Binary (Common.Named a b)
instance (Generic a, Binary a) => Binary (Position' a)
instance (Generic a, Binary a) => Binary (Interval' a)
instance (Generic a, Binary a) => Binary (Range' a)
instance (Generic a, Binary a) => Binary (Common.Ranged a)
instance (Generic a, Binary a) => Binary (Common.ArgInfo a)
instance (Generic a, Generic b, Binary a, Binary b) => Binary (Common.Arg a b)
instance (Generic a, Generic b, Binary a, Binary b) => Binary (Common.Named a b)
instance Binary Common.Big
instance Binary Common.Relevance
instance Binary Common.Hiding
instance Binary GenPart
instance Binary Fixity
instance Binary Fixity'
Expand Down

0 comments on commit f7b47de

Please sign in to comment.