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)
  • [x] initial proof went through
  • [x] added to (modified) LVish API
  • [x] benchmark program runs
  • [ ] switch to CTrie to avoid gratuitiously non-performant version
  • [ ] thorough evaluation completed and performance within expectation
• Parallel fold (VerifiedMonoid)
  • [x] initial proof went through
  • [x] added to (modified) LVish API
  • [x] 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.