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

Copy input and output of provers to RAM #71

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

bclement-ocp
Copy link
Contributor

@bclement-ocp bclement-ocp commented Jun 7, 2023

This is the RAM disk part of #69, split off from #69

It includes the changes from #69 because there are multiple changes in Misc.ml and that would cause conflicts otherwise; hence, it should be merged after #69. The other two commits can be reviewed independently.

@bclement-ocp
Copy link
Contributor Author

Note: I am seeing some crashes with these changes that I thought I had eliminated, marking the PR as draft until I figure it out.

@bclement-ocp bclement-ocp marked this pull request as draft June 13, 2023 15:32
This changes the way Benchpress collects the prover's outputs from using
a pipe to using temporary files that are read once the prover is done.
On Unix systems, the temporary files default to being stored in
`/dev/shm`; on other platforms, the default temporary directory is used.

This ensures that the prover never gets stuck waiting for benchpress to
read from pipes, but more importantly minimises context switches between
the prover and benchpress.
This ensures that we don't benchmark the time it takes to load the
problem from disk, and helps minimise noise in situations of high disk
contention, and other noise from the filesystem cache.

We are still limited by the RAM bandwidth but… what can you do.

This is only effective on Unix (more precisely, on Unix systems where
`/dev/shm` is actually in RAM); on Windows the default temporary
directory will be used. To enable the same behavior on Windows, pass a
RAM disk as `--ramdisk` argument.

To disable the behavior on Linux, you can pass a directory that is not
in RAM to the `--ramdisk` argument. The files will still be copied.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant