Description

An important paradigm in parallel programming is the task-based paradigm, where each task creates subtasks and waits for their results.

It is not efficient to use a single big queue to store tasks/

The most efficient implementation of task-based programming is called work-stealing, where all idle "workers" (threads) steal tasks from busy workers.

The idea is that each worker has a special double-ended queue (deque). The worker adds and removes work from the head of the queue, while the thieves steal from the tail. Sometimes all the work in the queue is stolen and then the worker has to steal from other workers until the stolen task has been completed and the result of the task is given to the original owner.

So obviously the overhead of this queue in terms of communication between the workers/processor threads and the memory must be as low as possible and hence, such queues do not use global locking or mutexes but instead use special atomic instructions like "compare-and-swap" and memory fences in order to be correct.

This project is about proving of a work-stealing deque that every task that is put in the deque is eventually executed exactly once and that the correct result is returned to the owner. In other words: prove that the queue functions correctly.

You can do this using for example the VerCors tool set (a model checker for concurrent programs), or with LTSmin (a model checking tool set for transition systems), or with a SAT/SMT solver, or with Isabelle (a theory prover).

Final paper: https://drive.google.com/file/d/1WqsB8rMSeFtP2jvbuMl-vdxl14vTUXfw/view