LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

Impact of `seq` removal #572

Closed LeventErkok closed 3 years ago

LeventErkok commented 3 years ago

@doyougnu [I've merged the pull request, but keeping these items open here so we can get some numbers.]

I'm a little concerned regarding the removal of seq. If you read through Andy's original paper (http://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf), he explicitly says in Section 12 that forcing a seq is essential in capturing sharing. But perhaps you're right that since we're storing functions, it doesn't really matter if we seq or not; it's just added work with no benefit.

Still, I wonder if you can design an experiment to see if seq increases sharing or not. A simple way would be to simply count the number of hits in the lookup function and print them out as you run the same program twice. (In this case, we wouldn't want to be looking at the performance, but simply counting the hits.) If we can get some data to support removing seq has no impact in this case for recovering sharing, then I'd feel more comfortable.

Of course, we can always replace the list with the Seq, that'll always be fine. I'd also be interested in finding out how many long those chains ever get. (Perhaps do a run where you keep track of the length of the max chain and print at the end? That can also be very illuminating.)

doyougnu commented 3 years ago

linking to my comment about how the impact of seq removal for the unique case: https://github.com/LeventErkok/sbv/pull/571#issuecomment-751519401

Running a much smaller non-unique case now.

doyougnu commented 3 years ago

Code for the non-unique case:

  let go x acc = let s = x S..&& acc
                     in do S.constrain s
                           return s
      bad = S.sat $ do bs <- mapM (S.free . show) [1..10]
                       foldM go S.sTrue (take 5 bs)
                       foldM go S.sTrue bs

  print =<< show <$> bad

the seq results don't show any cache hits:

Size of Cache: 0
Size of elems: []
Miss
Size of Cache: 1
Size of elems: [1]
Size of Cache: 1
Size of elems: [1]
Miss
Size of Cache: 2
Size of elems: [1,1]
Miss
Miss
Size of Cache: 4
Size of elems: [1,1,1,1]
Size of Cache: 4
Size of elems: [1,1,1,1]
Size of Cache: 4
Size of elems: [1,1,1,1]
Miss
Size of Cache: 5
Size of elems: [1,1,1,1,1]
Miss
Miss
Size of Cache: 7
Size of elems: [1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 9
Size of elems: [1,1,1,1,1,1,1,1,1]
Size of Cache: 9
Size of elems: [1,1,1,1,1,1,1,1,1]
Size of Cache: 9
Size of elems: [1,1,1,1,1,1,1,1,1]
Size of Cache: 9
Size of elems: [1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 10
Size of elems: [1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 12
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 14
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 17
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 19
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 21
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 23
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 25
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 26
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 26
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 27
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 29
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 29
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 29
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 30
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 32
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 34
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 34
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 34
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 34
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 35
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 37
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 39
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 41
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 41
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 41
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 41
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 41
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 42
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 44
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 46
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 48
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 50
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 50
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 50
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 50
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 50
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 50
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 51
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 53
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 55
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 57
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 59
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 61
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 61
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 61
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 61
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 61
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 61
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 61
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 62
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 64
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 66
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 68
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 70
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 72
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 74
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 75
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 77
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 79
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 81
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 83
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 85
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 87
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 89
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 90
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 92
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 94
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 96
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 98
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 100
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 102
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 104
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 106
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 107
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 109
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 111
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 113
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 115
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 117
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 119
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 121
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 123
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 125
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Size of Cache: 126
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 128
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 130
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 132
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 134
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 136
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 138
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 140
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 142
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
"Satisfiable. Model:\n  1  = True :: Bool\n  2  = True :: Bool\n  3  = True :: Bool\n  4  = True :: Bool\n  5  = True :: Bool\n  6  = True :: Bool\n  7  = True :: Bool\n  8  = True :: Bool\n  9  = True :: Bool\n  10 = True :: Bool"
Benchmark auto: FINISH

We should see at least 5 Hit in the file.

the non-seq results show 21 caching hits:

Size of Cache: 0
Size of elems: []
Miss
Size of Cache: 1
Size of elems: [1]
Size of Cache: 1
Size of elems: [1]
Miss
Size of Cache: 2
Size of elems: [1,1]
Miss
Miss
Size of Cache: 4
Size of elems: [1,1,1,1]
Size of Cache: 4
Size of elems: [1,1,1,1]
Size of Cache: 4
Size of elems: [1,1,1,1]
Hit
Size of Cache: 4
Size of elems: [1,1,1,1]
Miss
Miss
Size of Cache: 6
Size of elems: [1,1,1,1,1,1]
Miss
Miss
Size of Cache: 8
Size of elems: [1,1,1,1,1,1,1,1]
Size of Cache: 8
Size of elems: [1,1,1,1,1,1,1,1]
Size of Cache: 8
Size of elems: [1,1,1,1,1,1,1,1]
Hit
Size of Cache: 8
Size of elems: [1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 10
Size of elems: [1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 12
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 12
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 12
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 12
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 14
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 16
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Miss
Size of Cache: 17
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 17
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 17
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 17
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Miss
Size of Cache: 18
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Miss
Size of Cache: 19
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 19
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 19
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 19
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Miss
Size of Cache: 20
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Miss
Size of Cache: 21
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 21
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 21
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 21
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Miss
Size of Cache: 22
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 24
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 24
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 24
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 24
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Miss
Size of Cache: 25
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 27
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 27
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 27
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 27
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 29
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 31
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 31
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 31
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 31
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 33
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 35
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 35
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 35
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 35
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 37
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 39
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 39
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 39
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 39
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 41
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
Size of Cache: 43
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Size of Cache: 43
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Hit
Size of Cache: 43
Size of elems: [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
Miss
Miss
"Satisfiable. Model:\n  1  = True :: Bool\n  2  = True :: Bool\n  3  = True :: Bool\n  4  = True :: Bool\n  5  = True :: Bool\n  6  = True :: Bool\n  7  = True :: Bool\n  8  = True :: Bool\n  9  = True :: Bool\n  10 = True :: Bool"
Benchmark auto: FINISH
doyougnu commented 3 years ago

I found this presentation by johan tibell on HashMap. Looks like the occurrence rate for collisions is ~32k per 2^24, so even with the tests I've run (up to 10k variables) its unlikely we'll ever see a collision. Either way its best to handle the case directly.

doyougnu commented 3 years ago

For the sake of completeness I went back and removed seq from the IntMap version. i.e.:

uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen getCache (Cached f) st = do
        let rCache = getCache st
        stored <- readIORef rCache
        let a = fmap S.length $ IMap.elems stored
        putStrLn $ "Size of Cache: " ++ show (IMap.size stored)
        putStrLn $ "Size of elems: " ++ show a
        sn <- makeStableName f
        let h = hashStableName sn
        let find ss = do i <- S.findIndexL (eqStableName sn . fstStrict) ss
                         sndStrict <$> S.lookup i ss
        case (h `IMap.lookup` stored) >>= find of
          Just r  -> putStrLn "Hit" >> return r
          Nothing -> do r <- f st
                        r `seq` R.modifyIORef' rCache (IMap.insertWith (S.><) h . pure $ SPair sn r)
                        putStrLn "Miss"
                        return r

This version doesn't exhibit the bug. Furthermore, it is closer to the original code and creates a smaller cache (again for 10k unique variables in query mode, notice this is 2k less than the hashmap):

Size of Cache: 39996

but more importantly the memory profile is better and we can avoid an extra dependency:

imap_no_seq.pdf

The spike in that profile is likely due to the printing in uncacheGen

I'm thinking of reverting the HashMap change back to IntMap but keeping the strict pair and sequences.

@LeventErkok what are your thoughts? I can issue a correcting PR in the next day or two this is an easy change.

LeventErkok commented 3 years ago

Yes, that sounds like a good option.

I was getting this bizarre error from doctest:

Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:23: failure in expression `checkArithOverflow midPointBroken'
expected: Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:35:28:+!: SInt32 addition overflows: Violated. Model:
            low  = 2147483647 :: Int32
            high = 2147483647 :: Int32
 but got: *** Exception: stack overflow

which worries me as well; since I can't replicate it if I run the same without doctest. Perhaps going back to IntMap will resolve this issue.

doyougnu commented 3 years ago

PR is up #573

LeventErkok commented 3 years ago

Great. Running test suite now.

doyougnu commented 3 years ago

Yes, that sounds like a good option.

I was getting this bizarre error from doctest:

Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:23: failure in expression `checkArithOverflow midPointBroken'
expected: Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:35:28:+!: SInt32 addition overflows: Violated. Model:
            low  = 2147483647 :: Int32
            high = 2147483647 :: Int32
 but got: *** Exception: stack overflow

which worries me as well; since I can't replicate it if I run the same without doctest. Perhaps going back to IntMap will resolve this issue.

perhaps this is from Sequence? Specifically from their docs:

The size of a Seq must not exceed maxBound::Int. Violation of this condition is not detected and if the size limit is exceeded, the behaviour of the sequence is undefined. This is unlikely to occur in most applications, but some care may be required when using ><, <*>, *>, or >>, particularly repeatedly and particularly in combination with replicate or fromFunction.
doyougnu commented 3 years ago

I think the overflow bug may be related to the increased laziness. Specifically I think removing seq is blowing up the stack with millions of nested thunks somehow.

I replaced the sequence with a list and still observed the issue so it isn't related to Seq.

But the fix I did find was adding back a seq before makeStableName. However, this would exacerbate the space leak I previously identified. So I'm running benchmarks now with sn <- f `deepseq` makeStableName f instead of seq to see if that fixes it.

Fingers crossed.

LeventErkok commented 3 years ago

Yeah, something is fishy here. I don't see why adding seq there would cause the space-leak in the first place. I don't see how deepSeq would be different than a regular seq on a function object; but maybe there's some interaction with the garbage-collector. Let's see what your experiment shows.

doyougnu commented 3 years ago

Ah deepseq exhibited the same memory leak behavior as seq. It is peculiar to me that this didn't come up with the booleans I've been testing with. So I think there is a leak around arithmetic somewhere and we are only catching it when it gets to the caching code. This would explain why seq behaves as it does and would explain why all the profiling points to the cache.

That this produces a stack overflow is a good sign IMHO there are several techniques for finding such leaks that Niel Mitchel has posted about. I'll give these a go tomorrow. I tried to get cabal to turn on profiling and it wasn't agreeing with me so I gave it a rest for the night.

LeventErkok commented 3 years ago

Interesting.. It baffles me why we have this leak, and I agree that it's not with the caching. Must be elsewhere. My concern is that it may not be a single point in the entire chain. But you're right, more digging is needed.

LeventErkok commented 3 years ago

@doyougnu I reverted the last two commits from the master as we dig down on this. Let's do the branch thing: When you're ready for changes to be pushed, push it to a branch and I'll merge when all is clean back to master.

doyougnu commented 3 years ago

update on this. I pulled the stack trace by linking with -xc RTS option. All plots and results are from running checkArithOverflow midPointBroken:

  Data.SBV.Core.Operations.liftSV2.c,
  called from Data.SBV.Core.Operations.liftSV2,
  called from Data.SBV.Core.Operations.liftSym2,
  called from Data.SBV.Core.Operations.svPlus,
  called from Data.SBV.Core.Model.+,
  called from Data.SBV.Tools.Overflow.checkOp2,
  called from Data.SBV.Tools.Overflow./!,
  called from Documentation.SBV.Examples.BitPrecise.BrokenSearch.midPointBroken,
  called from Data.SBV.Core.Symbolic.uncacheGen,
  called from Data.SBV.Core.Symbolic.uncache,
  called from Data.SBV.Core.Symbolic.outputSVal,
  called from Data.SBV.Core.Data.output,
  called from Data.SBV.Client.BaseIO.output,
  called from Data.SBV.Core.Symbolic.>>=,
  called from Data.SBV.Provers.Prover.sName_,
  called from Data.SBV.Core.Symbolic.>>,
  called from Data.SBV.Core.Symbolic.runSymbolic,
  called from Data.SBV.Provers.Prover.safeWith,
  called from Data.SBV.Provers.Prover.safe,
  called from Data.SBV.Client.BaseIO.safe,
  called from Documentation.SBV.Examples.BitPrecise.BrokenSearch.checkArithOverflow,
  called from Main.main

Looking at liftSV2.c we have:

liftSV2 :: (State -> Kind -> SV -> SV -> IO SV) -> Kind -> SVal -> SVal -> Cached SV
liftSV2 opS k a b = cache c
  where c st = do sw1 <- svToSV st a
                  sw2 <- svToSV st b
                  opS st k sw1 sw2

but sw1 and sw2 are leaking because they are passing to the continuation without being called for. Unfortunately adding strictness annotations or two seq's only here does nothing to the overflow or the heap profile.

I searched sbv for this pattern, i.e., having a where clause which is then passed to cache and there were 62 instances. I did my best to add strictness to cases such as sw1 and sw2 but it also had no effect. You can see another one of these patterns in liftQRem and the heap profile below is actually pointing to the mk closure in that function (note that these strictness annotations changed nothing):

liftQRem :: (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
liftQRem x y
  | isConcreteZero x
  = (x, x)
  | isConcreteOne y
  = (x, z)
  | True
  = ite (y .== z) (z, x) (qr x y)
  where qr (SBV (SVal sgnsz (Left a))) (SBV (SVal _ (Left b))) = let (q, r) = sQuotRem a b in (SBV (SVal sgnsz (Left q)), SBV (SVal sgnsz (Left r)))
        qr a@(SBV (SVal sgnsz _))      b                       = (SBV (SVal sgnsz (Right (cache (mk Quot)))), SBV (SVal sgnsz (Right (cache (mk Rem)))))
                where mk o st = do !sw1 <- sbvToSV st a
                                   !sw2 <- sbvToSV st b
                                   mkSymOp o st sgnsz sw1 sw2
        z = genLiteral (kindOf x) (0::Integer)

So I turned to heap profiling because it is likely that the same code would also be blowing up the heap. Here is the heap profile by cost-centre, i.e., the functions that are causing the heap to increase: image image

So the majority is coming from sAssert.r and liftSV2.c. So I tried to strictify sAssert.r. Note that this is the same pattern " do block to cache". Unfortunately this also had zero impact. I even tried removing the lazy list functions intercalate and map loc which will map with a lazy tuple, although it was a long shot because this code is just for error messages.

-- | Symbolic assert. Check that the given boolean condition is always 'sTrue' in the given path. The
-- optional first argument can be used to provide call-stack info via GHC's location facilities.
sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert cs msg cond x
   | Just mustHold <- unliteral cond
   = if mustHold
     then x
     else error $ show $ SafeResult ((locInfo . getCallStack) `fmap` cs, msg, Satisfiable defaultSMTCfg (SMTModel [] Nothing [] []))
   | True
   = SBV $ SVal k $ Right $ cache r
  where k     = kindOf x
        r st  = do !xsv <- sbvToSV st x
                   let !pc = getPathCondition st
                       -- We're checking if there are any cases where the path-condition holds, but not the condition
                       -- Any violations of this, should be signaled, i.e., whenever the following formula is satisfiable
                       !mustNeverHappen = pc .&& sNot cond
                   !cnd <- sbvToSV st mustNeverHappen
                   addAssertion st cs msg cnd
                   return xsv

        locInfo ps = intercalate ",\n " (map loc ps)
          where loc (!f, !sl) = concat [srcLocFile sl, ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f]

At this point I checked the types that were leaking, and there were no surprises: image image

The cache is taking up the heap space, you can see that the STABLE_NAMEs are a pretty significant portion of the heap which is surprising because this is a rather small example. I think this may be the profiler holding onto the names. The last thing I checked was the biography of this data. I was trying to answer what state the data is in when it is retained.

image image

from ghc's manual:

 typical heap object may be in one of the following four states at each point in its lifetime:

    The lag stage, which is the time between creation and the first use of the object,

    the use stage, which lasts from the first use until the last use of the object, and

    The drag stage, which lasts from the final use until the last reference to the object is dropped.

    An object which is never used is said to be in the void state for its whole lifetime.

A biographical heap profile displays the portion of the live heap in each of the four states listed above. 
Usually the most interesting states are the void and drag states: 
live heap in these states is more likely to be wasted space than heap in the lag or use states.

so the majority of this data being retained is Void meaning that these objects are never even used or called for. The last question was why is the data being retained? So I checked the retainer profile: image image

Again from ghc manual:

Retainer profiling is designed to help answer questions like “why is this data being retained?”. We start by defining what we mean by a retainer:

A retainer is either the system stack, an unevaluated closure (thunk), or an explicitly mutable object.

In particular, constructors are not retainers.

An object B retains object A if (i) B is a retainer object and (ii) object A can be reached by recursively following pointers starting from object B, but not meeting any other retainer objects on the way. Each live object is retained by one or more retainer objects, collectively called its retainer set, or its retainer set, or its retainers.

When retainer profiling is requested by giving the program the -hr option, a graph is generated which is broken down by retainer set. A retainer set is displayed as a set of cost-centre stacks; because this is usually too large to fit on the profile graph, each retainer set is numbered and shown abbreviated on the graph along with its number, and the full list of retainer sets is dumped into the file prog.prof.

Its likely we're only seeing the top most retainer with this last one. I can limit the retainer profile to drive down the retainer chain in the next few days.

What I think is happening is that performing f `seq` makeStableName f creates a dependency between f and the call to makeStableName, most of the time this is what we want because we want good stable names. But in this case f is most of the time a large monadic block of code. So this gets reduced to WHNF (probably a call to bind) and then because we need to keep the stable names in the cache we are keeping the thunks which represent these computations. If I redo the biography profile without f `seq` makeStableName f then we get this profile:

image image

where you can see that most of the heap is now INHERENT_USE rather than VOID which confirms that seq'ing is keeping these void objects around. This still doesn't give insight into the stack overflow but at least we have a better handle on what is happening under the hood. I think the next steps are to check the actual residency memory using top or ps or something similar. I want to see the stack with and without profiling turned on to check if that is the culprit (this is what we concluded last time, my only issue with this is that at the scale i'm using sbv I observed these heap explosions even with the profiling disabled). You'll notice that the y-axis changes for the last profile by ~2x. The inherent use portion is the run time system, if I profile using the -xt flag (show the memory used by the run time in the profile) then we'll see that this memory is all SYSTEM which means its from the runtime but apart from garbage collection, so we're probably looking at the profiling overhead: image image

So it seems like VOID is coming from liftCV2.c because INHERENT_USE became SYSTEM with the -xt flag.

LeventErkok commented 3 years ago

@doyougnu

Great analysis! It's still baffling me why that one seq is making so much difference and none of this seems to point to a single culprit. I attempted a few tests myself, which didn't reveal much. Still a mystery I suppose.

doyougnu commented 3 years ago

Hey Levent,

So i tried doing anything to change the profile and struck some gold:

uncacheGen :: NFData a => (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen getCache (Cached !f) st = do
        let rCache = getCache st
        stored <- readIORef rCache
        sn <- f `seq` makeStableName f
        let find ss = do !i <- S.findIndexL (eqStableName sn . fstStrict) ss
                         sndStrict <$> S.lookup i ss
            h = hashStableName sn
        case (h `IMap.lookup` stored) >>= find of
          Just r  -> return r
          Nothing -> do r <- f st
                        -- r `seq` R.modifyIORef' rCache (IMap.insertWith (S.><) h . pure $! SPair sn r)
                        return r

This is pretty course grained but I simply commented out the cache and got this profile: image image

Which is more what I would expect for really any of the documentation examples because it doesn't show a space leak. However this version still threw the stack overflow but this confirms that the heap issue is indeed separate from the stack overflow.

doyougnu commented 3 years ago

Ah I think I may have solved the heap issue (this is the third time I've said this though):

uncacheGen :: NFData a => (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen getCache (Cached !f) st = do
        let rCache = getCache st
        stored <- readIORef rCache
        sn <- f `seq` makeStableName f
        let find ss = do !i <- S.findIndexL (eqStableName sn . fstStrict) ss
                         sndStrict <$> S.lookup i ss
            h = hashStableName sn
        case (h `IMap.lookup` stored) >>= find of
          Just r  -> return r
          Nothing -> do r <- f st
                        r `seq`
                          R.modifyIORef' rCache (IMap.insertWith (S.><) h . pure $! SPair sn r)
                          `seq`
                          return r

Notice that I've tied the IORef to the return statement. Looks like this forces the thunk image image

and here is the biography profiles: image image

So most of the memory on the heap is from the runtime system INHERENT_USE, looks like we still have some VOID coming the actual code. I bet this is the profiler's reaction to the stack overflow.

If you could verify from your side. SBVBench should look like this:

module Main where

import           Gauge.Main.Options (defaultConfig, Config(..))

import Documentation.SBV.Examples.BitPrecise.BrokenSearch

main :: IO ()
main = do
  -- generate the benchmark file name
  -- let f = benchResultsFile "<your-test-name-here>"

  -- Your code on interest here
  putStrLn "running"
  checkArithOverflow midPointBroken

then you need to enable profiling with cabal. Either cabal v2-build --enable-profiling or using in a cabal.project.local file:

benchmarks: True
library-profiling: True
profiling: True
profiling-detail: all-functions

now we can run the bench:

cabal bench sbv:SBVBench --benchmark-options='+RTS -K64m -xc -s -hy -p -L150 -RTS'

-K64m sets the stack size -xc is print a stack trace on any exception -hy is construct the heap profile watching which types are on the heap -p is generate a .prof file to check the time and alloc spent in each function -L150 is set the labels in the heap profile to 150 characters.

the to make the heap profile run this:

hp2ps -M -c SBVBench.hp && ps2pdf SBVBench.ps && evince SBVBench.pdf

hp2ps -M -c is take the heap profile file and translate it to post script -M is put the legend on a separate page from the profile -c means to use color

psd2pdf translates the postscript to pdf evince is the program i'm using to view the pdfs

doyougnu commented 3 years ago

Yup I'm pretty sure the extra seq on modifyIORef is the real fix. I pulled from master and profiled nQueens 11: image image

using the -s RTS options reported this too 33Mb.

The seq version uses half as much memory:

Found: 2680 solution(s).
   2,301,573,936 bytes allocated in the heap
     275,087,008 bytes copied during GC
      15,127,192 bytes maximum residency (30 sample(s))
         114,024 bytes maximum slop
              14 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      2208 colls,     0 par    0.094s   0.094s     0.0000s    0.0003s
  Gen  1        30 colls,     0 par    0.207s   0.207s     0.0069s    0.0140s

  INIT    time    0.000s  (  0.000s elapsed)
  MUT     time    3.165s  (103.711s elapsed)
  GC      time    0.224s  (  0.223s elapsed)
  RP      time    0.000s  (  0.000s elapsed)
  PROF    time    0.078s  (  0.078s elapsed)
  EXIT    time    0.000s  (  0.000s elapsed)
  Total   time    3.467s  (104.012s elapsed)

  %GC     time       0.0%  (0.0% elapsed)

  Alloc rate    727,190,555 bytes per MUT second

  Productivity  93.5% of total user, 99.8% of total elapsed

image image

Notice the change in y-axis scale. Looks like there is another leak using a list of tuples somewhere. I've pushed the fix to the sbv/cacheFix branch if you want to play with it.

LeventErkok commented 3 years ago

Cool. Just so I understand, this still exhibits the stack-overflow problem, right? That's a real mystery to me.

doyougnu commented 3 years ago

Yes it is separate. Also a real mystery to me, and now I'm even more confused. Just as sanity checked out master and observed it using the benchmark setup I describe earlier. What's even more weird is that if I ran the doctest in the documentation file the it didn't appear the doctest simply passed with no violations detected.

I'm pretty confused with that one... Are you able to reproduce it on master when compiling not in ghci or through doctest?

LeventErkok commented 3 years ago

It would be good to understand the root cause of this, but If the doctest based violation is the only issue here, then we can perhaps simply not doctest that one example till a workaround is available.

doyougnu commented 3 years ago

Oh looks like my comment was confusing.

No I meant that: run in ghci or doctest --> no overflow compile and run in the benchmark --> overflow

I checkout out sbv-7.10 and ran the BrokenSearch with the benchmark suit with ghc-8.6.5 and it still threw a stack overflow:

Preprocessing benchmark 'SBVBench' for sbv-7.10..
Building benchmark 'SBVBench' for sbv-7.10..
[1 of 1] Compiling Main             ( SBVBenchSuite/SBVBench.hs, /home/doyougnu/Programming/sbv/dist-newstyle/build/x86_64-linux/ghc-8.8.4/sbv-7.10/b/SBVBench/build/SBVBench/SBVBench-tmp/Main.dyn_o )
[1 of 1] Compiling Main             ( SBVBenchSuite/SBVBench.hs, /home/doyougnu/Programming/sbv/dist-newstyle/build/x86_64-linux/ghc-8.8.4/sbv-7.10/b/SBVBench/build/SBVBench/SBVBench-tmp/Main.p_o )
Linking /home/doyougnu/Programming/sbv/dist-newstyle/build/x86_64-linux/ghc-8.8.4/sbv-7.10/b/SBVBench/build/SBVBench/SBVBench ...
Running 1 benchmarks...
Benchmark SBVBench: RUNNING...
running
SBVBench: Stack space overflow: current size 33568 bytes.
SBVBench: Relink with -rtsopts and use `+RTS -Ksize -RTS' to increase it.
Benchmark SBVBench: ERROR
cabal: Benchmarks failed for bench:SBVBench from sbv-7.10.

So this issue has been around since BrokenSearch was added. Thus I think we just discovered a new bug while trying to understand and fix the cache leak.

So here's a summary of the situation:

It would be good to know if the stack overflow is only observed in numeric problems or all problems so we could find a minimal case to reproduce the bug. I checked NQueens, Legato, MergeSort, PrefixSum and MultMask, each which worked without issue.

LeventErkok commented 3 years ago

Interesting! Good sleuthing there. In hindsight, I'm not surprised the two are rather irrelevant, though it baffles me how doctest survived till now. Also, looking at that particular example, it's such a simple thing I don't understand where the stack-overflow would come from in the first place. (It's literally an addition and a division.) There's nothing "deep" happening.

I'm willing to think that the stackoverflow we're getting is a weird combo of a GHC infelicity, exacerbated by the use of call-stacks maybe (to get the location information). That is, this could very well be reported as a GHC regression, but the toolchain involved is too messy to turn it into a nice bug report. I wonder if we can somehow replicate it in a minimum manner. (This can be really difficult to do so though.)

LeventErkok commented 3 years ago

@doyougnu

Interesting debugging/profiling technique: https://well-typed.com/blog/2021/01/first-look-at-hi-profiling-mode/

Apparently not yet available in GHC, but there's a way to get a version running. (Or we can wait and readdress this when it becomes part of a standard release.) Looks promising.

doyougnu commented 3 years ago

Oh yea i saw this yesterday and actually already tweeted about it.

Unfortunately I have to switch priorities for a journal submission at the end of the month, although I may have time to use the backported version this weekend. It should be pretty trivial to build it with nix and then I can point my sbv nix file to that particular ghc instance, keyword being should of course.

LeventErkok commented 3 years ago

@doyougnu I'm thinking of doing a release sometime this week, though there isn't any specific urgency. Should we wait till this ticket gets a closure?

doyougnu commented 3 years ago

Hey Levent,

Yea I was also wondering what to do with these results. Unfortunately I'm completely swamped and cannot commit any time to this quite yet. I'm sorry to make a mess and not have time to clean it!

I think you should go ahead with the release without including these changes. My thinking is that we should separate the seq related stuff from the stack overflow issue. With regard to the seq stuff, we know that adding and extra seq to the uncachegen plugs a pretty aggressive space leak at scale, but I'm a bit concerned that plugging the leak revealed the stack overflow issue. Furthermore, any code changes to the cache are pretty pervasive and so I want to do more testing before releasing it to the wild.

At the very least I would want to figure out the stack overflow problem with the extra seq before releasing it. I simply don't feel comfortable making a release where we have evidence of a fatal crash like a stack overflow. There are also several other performance tuning things left to do:

  1. Migrate more String to Text (I want to continue to do this because it'll increase throughput to the underlying solver)
  2. remove reverse's to take advantage of the Sequence in the state
  3. Strictify tuples, one of the benefits of plugging the cache memory leak is revealing other memory leaks, and this is one of them.
LeventErkok commented 3 years ago

Sounds good. I'll go ahead with the release, and this work can happen in its own time. Thanks for all the contributions.

LeventErkok commented 3 years ago

@doyougnu I don’t think there’ll be any work on this, and I lost the context. We can revisit if this proves to be an issue in the future again.

doyougnu commented 3 years ago

Hey Levent, yes, sorry for dropping this but I do intend to return to it. After a healthy break from finishing my phd. I'll probably submit a PR and reference this issue when that time comes.

LeventErkok commented 3 years ago

Sounds good! Feel free to reopen when that time arrives. Cheers.

cartazio commented 1 year ago

@doyougnu reminder about this follow on work you mentioned :)