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

replace signal-based Timer with a ticking thread #577

Merged
merged 13 commits into from
Sep 2, 2024
Merged

Conversation

MichaelRawson
Copy link
Contributor

See #157, #462. Our current timer arranges for the process to be signalled with SIGALRM every millisecond, which is OK but not very portable and requires our code to be signal-safe, a concept which seems to be poorly specified/understood compared to thread safety.

This replaces the mechanism with an auxiliary thread per process that wakes up, checks resource limits, updates instruction counts, then sleeps for a millisecond or so. On process exit, this thread unceremoniously dies.

I don't have good intuition for how this performs. In principle this should be equal or better than the old mechanism. On my machine I get comparable numbers of generated clauses with a 10-second timeout, but the new implementation times out much more precisely.

Also:

  • remove some code that was only needed for the old implementation
  • simplify the Timer API
  • remove some manual "did we time out yet" code from random places - AFAIK this has not been useful since we implemented external timeout logic

Some of the code needs close attention: I will flag the tricky bits with GitHub comments.

CASC/PortfolioMode.cpp Outdated Show resolved Hide resolved
vampire.cpp Outdated Show resolved Hide resolved
@quickbeam123 quickbeam123 merged commit e5a912c into master Sep 2, 2024
1 check passed
@quickbeam123 quickbeam123 deleted the michael-timer branch September 2, 2024 07:16
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.

2 participants