Move interrupted check lower in NonIncrementalSolver to avoid race conditions

[jad-hamza]

@samarion I'm moving the interrupt check a bit later to avoid the case where we could get interrupted right after the if check.

[samarion]

Maybe use some synchronization primitive in that case? You might run into JVM cache inconsistency issues otherwise.

[jad-hamza]

Which one do you think? I was having a look at AtomicReference, and store both the currentSolver and interrupt in a pair here, but I don't think it's ideal when you want to set just one component.

[samarion]

I think we can just use a synchronized block and make sure modifications of interrupted and currentSolver are atomic. Something like:

def interrupt(): Unit = {
  val optSolver = synchronized {
    interrupted = true
    currentSolver
  }
  for (solver <- optSolver) solver.interrupt()
}

override def check(config: CheckConfiguration): config.Response[Model, Assumptions] = {
  assert(currentSolver.isEmpty, ...)
  val newSolver = underlying()
  try {
    val runCheck = synchronized {
      currentSolver = Some(newSolver)
      !interrupted
    }
    if (runCheck) {
      ...

[jad-hamza]

I think we can just use a synchronized block and make sure modifications of interrupted and currentSolver are atomic.

Thanks, should be good now

[jad-hamza]

Thanks :)