Multithreading determinism

[mads256h]

When a send_query request is sent to Reveaal each request is enqueued on the thread pool.
This allows Reveaal to handle multiple queries at the same time.

However, we want to multithread single queries as well.
One query type we could multithread is the determinism query.
We have already multithreaded determinism in this pr: Ecdar-SW5#146
However, it does not work correctly as it has a deadlock.
Let's say the thread pool has 4 threads.
Then, if you queue 4 determinism queries quickly, each of these queries create new subtasks to multithread the single determinism query.
The deadlock occurs here when all threads work on a determinism send_query task, because each of these tasks will await their subtasks which will never finish as the threads are taking up awaiting their subtasks.

One way to fix this issue is to ask the thread pool how many threads are currently available.
When the determinism query spawns its subtasks, it will only spawn as many tasks as there are threads available.
This will fix the deadlock.
However, you need to take care that you aren't introducing a time-of-check-to-time-of-use (TOCTTOU) race condition.
As another thread can enqueue tasks between the check of how many threads are available, and when the subtasks are spawned.
Thus, the deadlock can still occur if that race condition exists.

There is one issue with this approach though.
If a thread becomes available, the thread will not be used to complete a running task.
This is a waste of resources.
One way to fix this could be that the thread pool controls spawning tasks.
This way, when a thread on the thread pool becomes available, it can enqueue another task to complete one of the current tasks faster.
It could also be beneficial to also let the thread pool stop running tasks.
This could be useful f.x. for the multithreaded determinism query, as one of its subtasks can be stopped to allow another send_query task to run, as that might be a better use of resources.
This would also allow the thread pool to prioritize tasks, and it could lead to making it load balance requests made by different users, so different users get a fair share of the available compute resources.