Bucketed trees

[dlesbre]

This adds generic bucketed maps (split one big map into n smaller ones using a bucket_id : int -> 0 .. (n-1) function. This is the trick currently used in codex's nonrelational constraint domain, which we've seen improve performance

This is still a WIP as it needs to support non-heterogeneous maps (and perhaps sets).

Overall I thinks the technique is good but it requires some changes of interface I'm not quite happy with.

• We now need a smaller version of BASE_MAP, which I've called BASE_MAP_INTERFACE for lack of imagination
• We also need a smaller version of NODE, with only the types and no constructors (except empty), which I've called MAP_TYPES.
• We'll also probably need smaller versions of MAP, SET and HETEROGENEOUS_SET which remove their BaseMap module and the pop_minimum/min_binding functions

[mlemerre]

Nice. Probably we need some comment on when one should use bucketing. I am confused about the cases where we gain performance. For instance, is it better to split the heteregenous map per type such that the map/merge code has a better branch predictor specialized to one type? Or is it just interesting to have fewer levels in the map, in which case we should have 16 buckets and distribute according to id%16?

[dlesbre]

Its a balancing act I think, hard to tell precisely without measuring it. In the non-relational domain, we use this with three buckets (one for boolean, one for integers and one for binary). I believe we gain since we have way fewer boolean than binary terms, but booleans are more frequently accessed.

Of course you also gain lookup speed by having shorter path (like if you use id%16), but that comes at the expense of copying a size 16 array every time you make a change. So read is cheaper, but write isn't.

Note that copying a size 16 array might still cheaper than copying four nested nodes though:

• a single allocation is required instead of four
• the data has better memory locality
• we only need one OCaml tag instead of three, so we increase the ratio of useful data/metadata
  However, if the array isn't full (many cells only contain empty), then the costs probably outweight the benefits (we would only copy one or two nested nodes in that case)

[mlemerre]

Another idea of improvement is to use a "compressed representation" for nodes, e.g. instead of storing InteriorNode(e,f,Leaf(a,b),Leaf(c,d)) in three memory blocks, we could use [| e;f;a;b;c;d; |], and use the tag field as a bitfield to know if we have leaves or nodes. The separation that we have between a node and the view of a node should make this easy.