Benchmarks

[DmxLarchey]

I created a first set of benchmarks that on can rune with sh benchmarks.sh. It seems that bfn_3q is linear while bfn_2l (although quicker) is not so linear. By linear, I mean in the number of nodes.

For some unknown reason, testing btrees of sizes over 60k yields stack-overflows ... do not know why. It is a bit of a low upper bound to evaluate the linearity of bfn_3q but if it were quadratic, we would have noticed. Not sure for n log n ...

[rmatthes]

You change the size of the tests but not the stack limit. Now, there is again stack overflow. Please commit your new stack limit - to master.

[DmxLarchey]

Could you write an ocaml benchmark that picks a random btree of size 2n+1 where n is chosen randomly between 2^4 and 2^20 (on a logarithmic scale) and then repeats benchmarking bfn_2l and bfn_3q over this random sequence so that we can draw some kind of graph of the per node execution times and check the linearity of our algos ?

[rmatthes]

I would have tried QCheck. But I am still on the side of understanding your implementation.

[DmxLarchey]

Why not QCheck ... for now I think the benchmarks are enough to ensure efficiency but I am not sure about the O(n) complexity ... looks as if there is some log n factor hidden somewhere. Do you think the Coq code of bfn_*_f should be beautified? By that I mean, to separate more the computational content from the proof obligations ?

[rmatthes]

I'll keep your question in mind during my study of your code.

[DmxLarchey]

I did (somewhat) beautifiy the proof of bfn_3q_f in the new file bfn_fifo_3q_full.v with some comments to explain how the proof is structured. Let me know if you find this style easier to understand.

[rmatthes]

Today, I have nearly no time for this project. The question arises if the lazy lists of Ocaml to which llist are extracted are really the lazy lists Okasaki bases his argument on. We should probably make "unit tests" on individual functions and not only on the whole breadth-first numbering.

[DmxLarchey]

If you want to understand the implementation/extraction of bfn_f, I strongly you to review the version in file bfn_fifo_3q_full.v which is now beautified and fully commented.

[DmxLarchey]

I have been running some benchmarks on random trees. By random tree, I mean:

• the size n is chosen randomly between a and b on a log scale
• then a random binary tree of size 2n+1 is build recursively by randomly splitting n into n=p+q+1 and recurse on p and q. Then I run bfn_[2l,3q] on that tree while measuring time. I measure the total time for bfn_* to run and divide it by the number of nodes to get a node-average output. The GC (garbage collector) is forced before each individual measurement to avoid random/unnecessary GC triggers.

For bfn_2l, below trees of size 2^13 ~ 8k nodes, the runtime is linear in the number of nodes with a time of 0.2µs per node. It seems the GC gets triggered above the 2^13 limit where we get a second near constant level of 0.6µs per node up-to a 2^16 limit. Above that limit, the GC seems to largely impact the runtime. See

For bfn_3q, below trees of size ~ 3k nodes, the runtime is linear in the number of nodes with a time of 1µs per node. It seems the GC gets triggered above the 3k limit where we get a second near constant level of 1.5µs per node up-to a 2^15 limit. Above that limit, the GC seems to largely impact the runtime. See

Two remarks:

• When the GC is not triggered, we witness O(n) runtime. Could we set the GC limits higher to check above 8k (resp. 3k) nodes ?
• When the GC is triggered, the runtime is not linear. The curve is distinct however so maybe we could guess an empirical runtime law ?