Cleanup & genericity

[DmxLarchey]

Having axiomaized fifos in fifo_axm.v, I have rewritten bf[rnt].v so that they use that axiomatization and extract properly.

Also, fifo_[triv,2lists,3llists].v contain realizations of these axioms and can be plugged as is instead of fifo_axm.v. Then of course Extraction provides the corresponding fifo implementation as well.

The final goal is a file fifo.v that contains a master switch like Require Export fifo_2lists so that we get full genericity.

I am going to create a cleanup PR that contains only clean code that we want to publish and remove dead ends and independant code.

[DmxLarchey]

I pushed a MAJOR cleanup in the cleanup branch. There is a clean dependancy_graph.txt. I should perhaps add a description file as well.

The code now focuses on generic implementation of BFT, BFN and BFR with abstract FIFOs. FIFOs can be realized with lists, pairs of lists, triples of lazy lists and all that is implemented as well.

The file fifo.v acts as a global centralized switch where one can choose an implementation on FIFOs that holds for the whole project.

I have also added yet another FIFO-free implementation of bft_f and bft which might be better than the one with niveaux ... niveaux_tree has been renamed as niveaux and niveaux has been renamed as niveaux_f for more coherent naming.

[DmxLarchey]

I forgot to say that this cleanup branch is intended to become the code which is going to be distributed with the article.

[DmxLarchey]

Created a new branch to separate bft_std from the other bft algos as well as a new dft file and a dft_bft_compare to compare the two specifications.

[rmatthes]

I reviewed the new branch that is only beneficial. I also made simple changes to it. Well worth merging into our other branches.

[rmatthes]

I merged it into cleanup and cleanup-with-modules.

[DmxLarchey]

I did look at your stats ... nice graphs trl_2l_vs_3q.pdf showing very well the O(n) complexity until the tree size reaches roughly 2^13 and then a quadratic runtine. The fact that 2l runs about five time quicker than 3ll is a bit hidden in the legend though.

The graph does not show quadratic as such but I did check that some time ago and I could recompute a good quadratic approximation of the curve. It is also interesting to show the number of minor gc calls in parallel. This is VERY telling.

[rmatthes]

How did you show those gc calls?

[DmxLarchey]

How did you show those gc calls?

In branch gctuning file try_random_log.ml

let mytime () = Sys.time ();;
let mygcstats () =
  let st = Gc.quick_stat ()      
  in (st.minor_collections,st.major_collections);;

let measure f =
  let (mi1,ma1) = mygcstats ()    in
  let t1  = mytime ()             in
  let r =  f ()                   in
  let t2 = mytime ()              in
  let (mi2,ma2) = mygcstats ()
in (t2 -.t1,r,mi2-mi1,ma2-ma1);;

See also https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html

[DmxLarchey]

Pushed title + abstract + plan in cleanup branch tex/abstract_plan.txt.