Progress on three benchmark categories

[rrnewton]

As we talked about in our last meeting (and in this whiteboard), we need to make independent progress in these three benchmark categories:

• Parallel insert (VerifiedOrd on keys)
  • initial proof went through
  • added to (modified) LVish API
  • benchmark program runs
  • switch to CTrie to avoid gratuitiously non-performant version
  • thorough evaluation completed and performance within expectation
• Parallel fold (VerifiedMonoid)
  • initial proof went through
  • added to (modified) LVish API
  • benchmark program runs
  • thorough evaluation completed and performance within expectation
• Mutation of a reduction variable (verified commuting operations)
  • initial proof went through
  • added to (modified) LVish API
  • benchmark program runs
  • thorough evaluation completed and performance within expectation

[vikraman]

PureSet scales poorly under concurrent insert. LVish has PureMap/CtrieMap, should we then benchmark PureMap/CtrieMap, or maybe PureSet/CtrieSet with CtrieSet k = CtrieMap k ()?

[vikraman]

@rrnewton CTrie doesn't need Ord on keys, so there's nothing to verify, it uses Hashable.