[shalashaska117]

Closes #979.

The detached timer thread read the instruction limits from env.options on every tick, so it could read freed Options during global cleanup. reinitialise() now passes the time and simulated instruction limits to the thread. The instruction limit lives in an atomic in Timer, because main sets it after parsing under --parsing_does_not_count; with that flag the timer starts without one. An unlimited budget now stays unlimited after parsing; before, it became the parsing cost and the run stopped right after parsing.

Checks:

• The new unit test, which clears env.options after the timer starts, fails on master and passes here.
• All 105 CTest suites pass in Debug with CHECK_LEAKS=ON and under ASan/UBSan. Release sanity passes. 14 CLI cases pass in Debug, Release and ASan/UBSan.
• With an injected instruction counter, Debug and Release enforce -i 5 only after parsing and keep an unlimited budget unlimited. There is no hardware counter here, so real instruction counting is untested.

[MichaelRawson]

If this is the right approach, happy to review and merge. However, would it not be easier to load the required fields from env.options into the thread on timer startup as local variables? This approach seems complex.

[shalashaska117]

@MichaelRawson Thanks, that would be simpler. The catch is that --parsing_does_not_count changes the instruction limit after the timer starts, so a startup snapshot would miss those updates. Stopping and joining the timer preserves that behavior and ensures it cannot access env.options after cleanup. That's why I went with this approach.

[quickbeam123]

Please note that --parsing_does_not_count is a hack that should not stand in the way of a clean solution of more the official parts of the code base. (Without trying to delve into the details, there are probably ways to achieve the effect of --parsing_does_not_count in a way that interferes better with what you are trying to achieve?)

[shalashaska117]

@quickbeam123 Agreed. I will investigate adapting parsing_does_not_count so the timer can own its limits, and verify that the simpler approach remains safe during shutdown.

[quickbeam123]

Sorry to start thinking more deeply about this only now, but what is it exactly we are trying to fix with this change?

What bad will happen if Timer reads env.options after global cleanup? Isn't the whole process by then (almost) dead anyway?

I mean, we know this is a grey (if not black) area, but the current timer solution works for our purposes: it allows us to stop at any point in the main code (ideally also print some statistics) without having to spread bailout checks across every place in the code base that can in principle run for more than 0.000s, which I think would be the only correct way.

The bottom line: maybe let's not waste energy on fixing somethings that not pragmatically broken?

[shalashaska117]

@quickbeam123 Current master still allows the timer to read freed Options during cleanup, as reproduced under Valgrind. A late timeout can also access destroyed statistics and potentially crash during shutdown; I have reproduced that failure only in a controlled cleanup test, not in ordinary runs.

The PR stops the timer before global destruction and removes these shutdown accesses while retaining asynchronous timeout enforcement, without adding bailout checks throughout the prover. The demonstrated benefit is eliminating the reported memory errors; preventing abnormal shutdown is a further benefit, but I have no evidence of incorrect solver results caused by this issue.

[quickbeam123]

Current master still allows the timer to read freed Options during cleanup, as reproduced under Valgrind.

Could we briefly discuss the exact execution there?

Normally, I would assume, we call Timer::disableLimitEnforcement(); to prevent that from happening, at least on success. (A success that's too late to disable would count as not success and once past that point, could never get interrupted. Am I missing something here, or was that example a non-success?)

[shalashaska117]

@quickbeam123 You're right that once the main thread has acquired EXIT_LOCK, the timer cannot proceed with timeout reporting. My previous reply should have separated that from the Options reads.

The reproduction in #979 is a successful solve of cnf(a,axiom,$true)., with -t 0 and Debug cleanup enabled. disableLimitEnforcement() locks EXIT_LOCK, but the timer loop reads env.options->instructionLimit() and simulatedInstructionLimit() outside that lock. Those reads continue even when both limits are zero.

So the sequence is: the main thread disables enforcement, cleanup deletes Options, and a subsequent timer tick reads the freed object. No timeout needs to occur.

The controlled timeout-during-cleanup test does not call disableLimitEnforcement(), so it does not demonstrate a reporting crash after a success protected by that lock. The demonstrated issue on the successful path is the invalid reads reported by Valgrind.

[quickbeam123]

Thank you, @shalashaska117 , for pointing me to #979, which I should have read first, sorry.

But CHECK_LEAKS hasn't been used for at least a decade (as far as I know). Maybe the least invasive and least complex change is to declare it deprecated, or simply delete it... @MichaelRawson what do you think?

[MichaelRawson]

I'm fine with deleting CHECK_LEAKS, I've never used it. Vampire leaks like a sieve even with CHECK_LEAKS; one thing we could do is try to clean this up, but it would be a lot of effort for little (or even negative) performance.

I see Martin's point and it would be very hard for a compiler to exploit this into something suprising, but let's not do illegal things where we can avoid it. The thing I don't understand about this patch is that EXIT_LOCK should handle all of this, the bug is just that we read from env.options in timer_thread before acquiring the lock: so why all this extra complexity?

We don't want to acquire EXIT_LOCK on every timer iteration. So I'd expect only to change timer_thread to

[[noreturn]] void timer_thread()
{
  unsigned timeLimit = env.options->timeLimitInDeciseconds();
  unsigned instrLimit = env.options->instructionLimit();
  unsigned simulatedInstrLimit = env.options->simulatedInstructionLimit();
  while(true) {
    if(timeLimit && Timer::elapsedDeciseconds() >= timeLimit) {
      limitReached(TIME_LIMIT);
    }

#if VAMPIRE_PERF_EXISTS
    if(instrLimit || simulatedInstrLimit) {
      Timer::updateInstructionCount();
      if (instrLimit && LAST_INSTRUCTION_COUNT_READ >= MEGA*(long long)instrLimit) {
        limitReached(INSTRUCTION_LIMIT);
      }
    }
#endif

    // doesn't matter if we 'sleep in' a bit, we get the real time from the system clock
    std::this_thread::sleep_for(TICK_INTERVAL);
  }
  ASSERTION_VIOLATION
}

so that all the options get loaded into the thread's locals. With a suitable comment, of course. What did I miss? (other than parsing_does_not_count, let's deal with that once I understand this).

[shalashaska117]

@MichaelRawson You didn't miss anything on the #979 path: your version fixes it, and I've reduced the PR to it. Two details:

• I pass the limits from reinitialise() instead of reading them at the top of timer_thread. With --parsing_does_not_count, main zeroes the instruction limit right after starting the timer, and a read on the new thread races with that write: with -i 1000, the thread in your version read 0 in 93 of 100 runs, so no instruction limit was enforced.
• parsing_does_not_count also raises the limit after parsing, which a copy would miss, so that one limit is an atomic in Timer that main sets after parsing. An unlimited budget now stays unlimited; master turned it into the parsing cost.

Deleting CHECK_LEAKS is fine with me, but it wouldn't fix this: ~Environment() deletes options in every build.

Not covered: modes that never call disableLimitEnforcement(), such as --mode clausify, can still hit the time limit during cleanup and report from freed env.statistics. The window is tiny, so I left it out.

[MichaelRawson]

This is really nice, thanks for the update! This also handles the parsing_does_not_count logic nicer than I thought it could be done, bravo.