Performance improvements - HeisenbugLtd/spat GitHub Wiki

Parallelization

• Converting the JSON data into our internal data structure could also be done in parallel, i.e. collect the subtree data separately and then join the subtrees. This is probably only relevant for really large projects.

  • On my machine, parsing the SPARKNaCl results into JSON takes about 80-90 ms (compared to ~120 ms before the reading was parallelized), converting the JSON data into our tree is reported with about 60 ms. These are 14 files, so if that is any typical indication we're talking about a wall-clock time of about 10 ms per file for reading and converting the JSON data.

• [X] Done Reading the files can be done in parallel which (implemented for V0.9.3+)

• [X] Done This is pretty much a copy from my comment in issue #10: (implemented in V0.9.2)

  Right now, when printing entities filtered by --failed or --unproved, the decision if the entity's proof tree has failed attempts results in multiple calls to Has_Failed_Attempts, Is_Unproved which each cause more similar calls into all dependent objects. This should be optimized, so that such properties are only calculated once.

  • The data structure we have now is mostly a vector containing other vectors. It seems more logical to represent the whole structure as a multi way tree instead. SOLVED

  • This, of course, requires that all objects are derived from the same parent type, but that shouldn't be much of an issue. SOLVED

  • So, instead of trying to extend the "Vector" types to insert our cached information, we could instead insert some kind of meta element which caches all information from its siblings, or (maybe a better solution) insert the concerned elements as child nodes of this element: SOLVED

    root
    |—file_info_1
    | |—flow_info
    | | |—flow_object_1 [...]
    | | |—flow_object_2 [...]
    | | '— [...] 
    | |—proof_info
    | | |—proof_object_1 [...]
    | | '— [...]
    | [...]
    |—file_info_2 [...]
    |— [...]
    [...]
    

  • Ada.Containers.Multiway_Trees allows us to iterate through a whole (sub)tree or through siblings of a subtree, so all our iterator needs should be satisfied. SOLVED

  • It also completely eliminates the need to have multiple container types. UNSOLVED

  • The problem is sorting which we need within the children of a subtree. SOLVED

  • View conversions shouldn't be too much of a problem, all siblings in a particular subtree should be of the exact same type (except maybe for the info element?). SOLVED