Ecdar / Ecdar/Reveaal

Multithreading determinism

Open
#133 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Rust
Stars
4
Forks
6
PR merge metrics
No merged PRs in 30d

Description

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: https://github.com/Ecdar-SW5/Reveaal/pull/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.

Contributor guide

No contributing guide indexed for this repository

Research direction

Review PR 146 and the send_query/thread-pool path first. Reproduce the reported deadlock by submitting four determinism send_query requests to a four-thread pool. Done means determinism queries can be multithreaded without deadlocking while concurrent requests remain schedulable; preemption, prioritization, and load balancing are broader design work.

Written by the indexing model from the issue text.

Assessment

Tech stack
rust
Domain
distributed-systems
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
25/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.