search

xavierleroy / canonical-binary-tries

Coq development accompanying the paper "Efficient Extensional Binary Tries"
BSD 3-Clause "New" or "Revised" License
19 stars 2 forks source link

[FYI, do not merge as-is] Slightly faster variant of Sigma using a dedicated primitive record #4

Open andres-erbsen opened 7 months ago

andres-erbsen commented 7 months ago

FYI: I sketched some variants of the Sigma implementation as stand-ins for a similar design space in another library I am working on. Using a dedicated primitive record type does seem to give a speedup, but it is still slower than Original and Canonical.

Benchmarks with coq master:

coqtop -R . Tries -R mmaps MMaps -batch -load-vernac-source benchmark/Runbench.v
     = "PrimitiveRecord (repeated keys, x10)"
Finished transaction in 20.225 secs (19.499u,0.722s) (successful)
     = "Record (repeated keys, x10)"
Finished transaction in 22.648 secs (22.317u,0.327s) (successful)
     = "Sigma (repeated keys, x10)"
Finished transaction in 30.591 secs (30.194u,0.391s) (successful)
     = "Original (repeated keys, x10)"
Finished transaction in 5.367 secs (5.366u,0.s) (successful)
     = "Canonical (repeated keys, x10)"
Finished transaction in 6.524 secs (6.523u,0.s) (successful)

Benchmarks with https://github.com/silene/coq/tree/VMaccu2 https://github.com/coq/coq/pull/18917 (I am just an eager early user of this work-in-progress vm improvement; my experimentation here does not constitute any statement of readiness by its authors):

coqtop -R . Tries -R mmaps MMaps -batch -load-vernac-source benchmark/Runbench.v
     = "PrimitiveRecord (repeated keys, x10)"
Finished transaction in 7.77 secs (7.764u,0.004s) (successful)
     = "Record (repeated keys, x10)"
Finished transaction in 11.891 secs (11.889u,0.s) (successful)
     = "Sigma (repeated keys, x10)"
Finished transaction in 15.065 secs (15.054u,0.007s) (successful)
     = "Original (repeated keys, x10)"
Finished transaction in 5.366 secs (5.365u,0.s) (successful)
     = "Canonical (repeated keys, x10)"
Finished transaction in 6.505 secs (6.504u,0.s) (successful)

This PR includes unrelated changes blatantly hacking around https://github.com/xavierleroy/canonical-binary-tries/issues/1, but in principle I could clean it up.