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 dd. 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 eEe \in E.

  • Init random priority p(ei),eiE;Init PriorityQueue queue\text{Init random priority } p(e_i), \forall e_i \in E; \text{Init PriorityQueue queue}
  • queue.enqueue(ei),eiEqueue.enqueue(e_i), \forall e_i \in E
  • while !queue.empty():\text{while }!queue.empty():
    • e:=queue.pop()e := queue.pop()
    • execute(e)\text{execute(e)}
    • queue.updatePriorityUniformly({ejej races with 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.

Check out my latest posts!


# Problem Even when requirements are clear, verifying software correctness and ensuring our code works in all scenarios without affecting existing logic can be challenging. This is more apparent on ‘hot’ codes: Excerpts of code that got updated often due to its status as a new base logic or due to ...
Improving Software Testability with Math

Improving Software Testability with Math

Blog
# Introduction Database normalization is a fundamental process in database design, ensuring data integrity and minimizing redundancy. Despite its theoretical foundations, practical implications and occurrences of different normal forms in real-world databases are underexplored. Our recent work addre...
Testing DB Normalization Theory vs Practice - FDSampleRush

Testing DB Normalization Theory vs Practice - FDSampleRush

ProjectResearchPaper
# Overview From full stack development, data management, automation, random hops on other teams’ meetings, to realizing that people having double eyelid (or lack thereof) is a thing, I have expanded my knowledge and honed my SWE skills by a lot during my 6-month internship at ShopBack. This article ...
My ShopBack Adventure

My ShopBack Adventure

Blog
#### Tl;dr: CS3210, under Prof. Cristina Carbunaru, is a solid introduction to parallel systems with a focus on theoretical understanding. The course covers various parallel computing models, architectures, and basics. While the lectures may seem basic for those with prior knowledge, the tutorials a...
Parallel Computing: CS3210 Review

Parallel Computing: CS3210 Review

Course Review