A Reliable Non-Intrusive Runtime Verification Framework for Linearizability

Description

This dataset contains the source code, benchmarks, and experimental results for a framework designed to audit and verify the behavior of concurrent data structures in real time (Runtime Verification). When programming with multiple threads sharing memory, it is incredibly easy to introduce subtle race conditions that break linearizability (the golden rule that every concurrent operation must appear to take effect instantaneously in a logical, valid sequential order). Detecting these bugs with traditional testing (such as standard unit tests) is nearly impossible. Existing monitoring tools typically rely on intrusive instrumentation, such as bytecode weaving with AspectJ. By injecting significant extra code, they drastically alter thread timing and execution speed (overhead). This leads to two major issues: False Positives: The delay introduced by the tool changes the interleaving of threads, generating failure alarms for behaviors that would not actually happen in the original, uninstrumented code. False Negatives: This same delay can accidentally "mask" real bugs, causing threads to synchronize by chance, meaning the error never manifests while the tool is actively watching. We designed a framework that monitors the system under inspection as a black box (it does not modify the bytecode; it only requires the class name and its methods). To capture thread activity asynchronously and with an ultra-lightweight footprint, we implemented two distributed algorithms based on collect objects (concurrent memory reads that do not block the system): CollectFAInc: Uses a lightweight atomic operation (fetch-and-increment) to establish a global ordering of events. CollectRAW: Reconstructs the actual happens-before relation among threads by analyzing cross-thread memory snapshots. As a non-intrusive method that preserves original execution timings, the framework mathematically guarantees 0% false positives (zero false alarms) and drastically reduces false negatives, catching real concurrent bugs under high contention scenarios that traditional tools completely miss.

Steps to reproduce

1. Download and extract the provided repository ZIP file. 2. Ensure you have the required environment (Java and Maven) as specified in the enclosed README.md file. 3. Follow the step-by-step instructions in the README.md to compile the framework and execute the examples and experiments.

Institutions

• Universidad Nacional Autónoma de México

  Mexico City, Mexico City

Categories

Related Links

Licence