Partial Order Aware Concurrency Sampling (POS) - Yuan, et al.

First Pass

Systematic testing of concurrent programs has been researched for quite some time and it is known to have the problem of state-space explosion whereby testing all possible interleaving of concurrent programs is exponential in the execution length. Deterministic Partial Order Reduction-based system has been used to reduce the state-space by minimizing the testing for equivalent execution schedules. As with common deterministic search algorithm, it often get stuck in some subspaces.

This article is a brief (first pass) of the following paper on POS:

Yuan, X., Yang, J., Gu, R. (2018). Partial Order Aware Concurrency Sampling. In: Chockler, H., Weissenbacher, G. (eds) Computer Aided Verification. CAV 2018. Lecture Notes in Computer Science(), vol 10982. Springer, Cham. https://doi.org/10.1007/978-3-319-96142-2_20

This paper expands upon some idea that instead of deterministically exploring the state-space, a randomized algorithm can be used instead.

Problem with current approaches

Prior POR works fail to show how the state-space reduction proof for deterministic algorithms can be applied to randomized algorithm, while the randomized approaches that use POR as a heuristic to avoid redundant exploration gave no formal probabilistic guarantee of error detection.

POS provides a formal proof of their probabilistic guarantee which shows that it is exponentially more efficient than random walk (which by itself has been shown to be better than most deterministic search algorithm).

The paper also compares POS to [[PCT - Ozkan|PCT]] as it is one of the randomized testing system that was able to give a probabilistic bound guarantee of error detection via its notion of strongly hitting schedules and a predefined bug depth $d$. We will not delve into these comparisons in this article as it serves as comparison and does not use partial order reduction.

How POS works

POS advertises its core algorithm as a "much more straightforward" system compared to prior POR work. Indeed, it is simple enough to be written in two sentences:

Each event is assigned with a random priority and, at each step, the event with the highest priority is executed. After each execution, all events that race with the executed event will be reassigned with a fresh random priority.

Following is a pseudocode for all events $e \in E$.

• $\text{Init random priority } p(e_i), \forall e_i \in E; \text{Init PriorityQueue queue}$
• $queue.enqueue(e_i), \forall e_i \in E$
• $\text{while }!queue.empty():$
  • $e := queue.pop()$
  • $\text{execute(e)}$
  • $queue.updatePriorityUniformly(\{e_j | e_j \text{ races with }e\})$

That's all for today bois. As promised, this is just a brief over first pass.