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.
See #157, #462. Our current timer arranges for the process to be signalled with
SIGALRMevery 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:
TimerAPISome of the code needs close attention: I will flag the tricky bits with GitHub comments.