Move unsat cache to Solvers.hs

[msooseth]

Description

This moves the UNSAT cache to a central location, in Solvers.hs. This means that UNSAT cache is filled and used even during interpretation. Also, one can simply use checkSatWithProps and the UNSAT cache will be there and working.

This also means that the unsat cache is now available to every place that calls checkSatWithProps, which also includes PleaseAskSMT, i.e. it will now work also when deciding on branches.

We now have a queue for the cache, and it is taken as priority before picking up any new task.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[gustavo-grieco]

Can checkSatWithProps be used to in verify so we can also benefit from caching?

[msooseth]

Can checkSatWithProps be used to in verify so we can also benefit from caching?

But we are already using it:

        -- Dispatch the remaining branches to the solver to check for violations
        --
        results <- withRunInIO $ \env -> flip mapConcurrently withQueries $ \(query, leaf) -> do
          res <- env $ checkSatWithProps solvers query
          when conf.debug $ putStrLn $ "   SMT result: " <> show (fst res)
          pure (fst res, leaf)

In fact, I made checkSat a sub-function of checkSatWithProps, and so, it cannot even be called anymore.

[msooseth]

@gustavo-grieco Basically, this PR is meant to replace all that cache in verify and elsewhere, so we have a single, unified cache.

[blishko]

Looks good, though I am wondering: How is this going to work? Wouldn't all SMT queries be put in the queue before the requests to add results to the cache?

Have you checked that this is working as expected?

[msooseth]

Have you checked that this is working as expected?

It certainly needs to be thought through. It does work sometimes for sure, but I agree that this needs more scrutiny. I wanna see how the ordering is done in this queue.

[msooseth]

I actually figured out why FIFO is correct for the equivalence checker! Kinda crazy. So:

So this:

       wrap <- pool numproc
       parMapIO (runOne env wrap) input

Creates e.g. 5 processes. Then immediately run 5 elements from input and block. Then when any has finished, it will pick up one more, and run that one. Etc. It does this in-order of the input. It will run 5 single tasks. Let's say all 5 are UNSAT. Let's say one finishes. It can only finish if it has already put the UNSAT cache element into the queue. Which means that when parMapIO sees that this thread has finished, it will pick up a new element, and put that task into the channel. But the cache task will be earlier in the channel! So the orchestrate will pick that up and deal with that first. Then it will pick up the next element to be processed.

What we need is a cache task channel that is priority, and does not block :)

[msooseth]

This is now ready for re-review. @blishko maybe you can take a peek?

[blishko]

This looks good!

I would still like to play with it a bit before we merge it.

[blishko]

This seems unrelated to the main point of the PR.
To me it seems better to write liftIO once. What is the problem with that?

[msooseth]

It's annoying. the checkSatWithProps needs the env. But it's ugly as-is, let me try to clean it up...

[msooseth]

OK, it should be cleaner now. Can you maybe re-check? It doesn't print the simplifying... line, but that's not that useful anyway I think. Otherwise, it should be cleaner now :)

[blishko]

Can you explain why you need STM (TChan) for the cache? Why the basic Chan is not sufficient?

[blishko]

I think this should be renamed, no? [Prop] is not the unsat cache. It is more like an Entry that should be added to unsat cache.

[msooseth]

Good point! Renamed it CacheEntry, I hope that works :)

[msooseth]

Can you explain why you need STM (TChan) for the cache? Why the basic Chan is not sufficient?

Yes! This queue needs to be nonblocking. The Chan queue doesn't have a non-blocking variant. STM.TChan has a non-blocking read operation:

      mx <- liftIO . atomically $ tryReadTChan cacheq
      case mx of
        Just (CacheEntry props)  -> deal with the entry...
        Nothing -> nothing in the queue, continue...

We need a non-blocking read operation, so we can start solving if there is nothing in the channel.

My understanding is that the other way of doing this is to use STM.TVar directly, which is what STM.TChan is using.

[blishko]

Right, that makes sense!