Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Levelized Files #154

Open
SSoelvsten opened this issue Oct 18, 2021 · 1 comment
Open

Levelized Files #154

SSoelvsten opened this issue Oct 18, 2021 · 1 comment
Labels
📁 internal This is where the ✨magic✨happens ✨ optimisation It's all about speed / space question Further information is requested

Comments

@SSoelvsten
Copy link
Owner

SSoelvsten commented Oct 18, 2021

Motivation

  1. A lot of our files are of the temporary read-once-and-produce-output type (specifically arc_file and node_file with move-semantics). Hence, to be able to squeeze more BDDs / ZDDs into a smaller disk, we should continually deallocate the input file.
  2. There is an upper limit to the file size for each file system, e.g. ext4 does not support files larger than 16 TiB.

Solution

The meta_file is turned into a list shared_ptr to files (or a file of files?). When a stream hooks into a read-once file, it removes the file for each level, when it has finished reading it.

Other Benefits

If there is one file per level and each node still points to the label rather than the level, then we can map labels to levels and that way support the swapping of two levels for variable reordering!

@SSoelvsten SSoelvsten added the ✨ optimisation It's all about speed / space label Oct 18, 2021
@SSoelvsten SSoelvsten added this to the Symbolic Model Checking milestone Oct 18, 2021
@SSoelvsten
Copy link
Owner Author

SSoelvsten commented Oct 28, 2021

Alternative: Incrementally Deallocate Temporary Files

A better alternative to solve motivation 1 and would also make everyone using TPIE love us is to delete the part of a file that already was read. Specifically, this was described by Mathias Rav in thomasmoelhave/tpie#227 .

@SSoelvsten SSoelvsten added the question Further information is requested label Mar 13, 2022
@SSoelvsten SSoelvsten changed the title Levelize the files Incrementally Deallocate Temporary Arc Files (Levelized Files) Mar 13, 2022
@SSoelvsten SSoelvsten changed the title Incrementally Deallocate Temporary Arc Files (Levelized Files) Incrementally Deallocate Temporary Files (Levelized Files) Jul 25, 2022
@SSoelvsten SSoelvsten changed the title Incrementally Deallocate Temporary Files (Levelized Files) Levelized Files Nov 15, 2022
@SSoelvsten SSoelvsten added the 📁 internal This is where the ✨magic✨happens label Nov 22, 2022
This was referenced Nov 24, 2022
@SSoelvsten SSoelvsten self-assigned this Dec 8, 2022
@SSoelvsten SSoelvsten removed their assignment Jan 13, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
📁 internal This is where the ✨magic✨happens ✨ optimisation It's all about speed / space question Further information is requested
Projects
None yet
Development

No branches or pull requests

1 participant