paint-brush
Context-Bounded Verification of Liveness: A Strengthening Fairness to Progressive Runsby@multithreading

Context-Bounded Verification of Liveness: A Strengthening Fairness to Progressive Runs

tldt arrow

Too Long; Didn't Read

We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads.
featured image - Context-Bounded Verification of Liveness: A Strengthening Fairness to Progressive Runs
MultiThreading.Tech: #1 Publication on Concurrent Programming HackerNoon profile picture

This paper is available on arxiv under CC BY-NC-SA 4.0 DEED license.

Authors:

(1) Pascal Baumann, Max Planck Institute for Software Systems (MPI-SWS), Germany;

(2) Rupak Majumdar, Max Planck Institute for Software Systems (MPI-SWS), Germany;

(3) Ramanathan S. Thinniyam, Max Planck Institute for Software Systems (MPI-SWS), Germany;

(4) Georg Zetzsche, Max Planck Institute for Software Systems (MPI-SWS), Germany.

A STRENGTHENING FAIRNESS TO PROGRESSIVE RUNS

In this section we strengthen the notion of fairness for DCPS to progressiveness by proving Lemma 4.3.


Idea. To prove Lemma 4.3 we modify the DCPS A by giving every thread a bottom of stack symbol ⊥ and saving its context switch number in its top of stack symbol. We also save this number in the global state whenever a thread is active. This way we can still swap a thread out and back in again once it has emptied its stack, and we also can keep track of how often we need to repeat that, before we reach K context switches and allow it to terminate.


Furthermore, we also keep a subset A ′ of the global states of A in our new global states, which restricts the states that can appear when no thread is active. This way we can guess that a thread will be “stuck” in the future, upon which we terminate it instead (going up to K context switches first) and also spawn a new thread keeping track of its top of stack symbol in the bag. Then later we restrict the subset G ′ to only those global states that do not have Resume rules for the top of stack symbols we saved in the bag. This then verifies our guess of “being stuck”.