PR #9 fixed stack-overflow crashes by making all list-utility functions tail recursive. The fix has two problems: the new code has no Coq proof, and tail recursion is enabled inefficiently by doing each list operation in reverse and then reversing the result.
This PR instead makes the whole serialize function in Coq produce reversed output, which means that the whole result comes out in reverse and just needs to be reversed once, but there was a redundant reversal after serialize already that could just be removed. The resulting code performs better and is now proved correct in Coq.
I wrote a crude benchmark to get some numbers. My benchmark took 17.1 seconds before this change and 9.2 seconds after. You can reproduce the benchmark numbers by applying this commit, running "make test" and inspecting the printed time it took to run the tests.
mzp
commented
8 years ago
PR #9 fixed stack-overflow crashes by making all list-utility functions tail recursive. The fix has two problems: the new code has no Coq proof, and tail recursion is enabled inefficiently by doing each list operation in reverse and then reversing the result.
This PR instead makes the whole serialize function in Coq produce reversed output, which means that the whole result comes out in reverse and just needs to be reversed once, but there was a redundant reversal after serialize already that could just be removed. The resulting code performs better and is now proved correct in Coq.
I wrote a crude benchmark to get some numbers. My benchmark took 17.1 seconds before this change and 9.2 seconds after. You can reproduce the benchmark numbers by applying this commit, running "make test" and inspecting the printed time it took to run the tests.