An official website of the United States government
Runtime verification (RV) found many bugs by monitoring passing tests in many open-source projects against formal specifications (specs). But, RV is often too slow for use in continuous integration. So, evolution-aware techniques were proposed to speed up RV by re-monitoring only a subset of specs affected by code changes. These techniques use coarse-grained class-level analyses, so they can sub-optimally and imprecisely re-monitor unaffected specs. We propose FineMOP to speed up evolution-aware RV by using fine-grained analyses to re-monitor fewer unaffected specs. The key idea is simple: changes often do not require re-monitoring specs that are only related to unchanged parts of changed classes. We im- plement six variants of three fine-grained analyses in FineMOP and evaluate them on 1,104 revisions of 68 open-source Java projects. Compared with two class-level techniques, FineMOP is up to 4.86x faster, re-monitors up to 81.04% fewer specs per revision, and finds 99.68% of all new violations that these techniques find. Also, FineMOP and Regression Test Selection (RTS) are complementary: combining FineMOP with RTS is faster than FineMOP or RTS alone.
more »
« less
This content will become publicly available on October 9, 2026
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Runtime verification (RV) monitors program executions for conformance with formal specifications (specs). This paper concerns Monitoring-Oriented Programming (MOP), the only RV approach shown to scale to thousands of open-source GitHub projects when simultaneously monitoring passing unit tests against dozens of specs. Explicitly storing traces—sequences of spec-related program events—can make it easier to debug spec violations or to monitor tests against hyperproperties, which requires reasoning about sets of traces. But, most online MOP algorithms are implicit trace, i.e. they work event by event to avoid the time and space costs of storing traces. Yet, TraceMOP, the only explicit-trace online MOP algorithm, is often too slow and often fails. We propose LazyMOP, a faster explicit-trace online MOP algorithm for RV of tests that is enabled by three simple optimizations. First, whereas all existing online MOP algorithms eagerly monitor all events as they occur, LazyMOP lazily stores only unique traces at runtime and monitors them just before the test run ends. Lazy monitoring is inspired by a recent finding: 99.87% of traces during RV of tests are duplicates. Second, to speed up trace storage, LazyMOP encodes events and their locations as integers, and amortizes the cost of looking up locations across events. Lastly, LazyMOP only synchronizes accesses to its trace store after detecting multi-threading, unlike TraceMOP’s eager and wasteful synchronization of all accesses. On 179 Java open-source projects, LazyMOP is up to 4.9x faster and uses 4.8x less memory than TraceMOP, finding the same traces (modulo test non-determinism) and violations. We show LazyMOP’s usefulness in the context of software evolution, where tests are re-run after each code change. LazyMOPeoptimizes LazyMOP in this context by generating fewer duplicate traces. Using unique traces from one code version, LazyMOPefinds all pairs of method 𝑚 and spec 𝑠, where all traces for 𝑠 in 𝑚 are identical. Then, in a future version, LazyMOPegenerates and monitors only one trace of 𝑠 in 𝑚. LazyMOPeis up to 3.9x faster than LazyMOP and it speeds up two recent techniques that speed up RV during evolution by up to 4.6x with no loss in violations.
more »
« less
- PAR ID:
- 10677091
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- Proceedings of the ACM on Programming Languages
- Volume:
- 9
- Issue:
- OOPSLA2
- ISSN:
- 2475-1421
- Page Range / eLocation ID:
- 3696 to 3725
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
In thetrace reconstruction problem, an unknown source stringx∈ {0,1}nis sent through a probabilisticdeletion channelthat independently deletes each bit with probability δ and concatenates the surviving bits, yielding atraceofx. The problem is to reconstructxgiven independent traces. This problem has received much attention in recent years both in the worst-case setting wherexmay be an arbitrary string in {0,1}n[7,8,10,11,12,23] and in the average-case setting wherexis drawn uniformly at random from {0,1}n[7,8,12,13,25]. This article studies trace reconstruction in thesmoothed analysissetting, in which a “worst-case” stringxworstis chosen arbitrarily from {0,1}n, and then a perturbed versionxofxworstis formed by independently replacing each coordinate by a uniform random bit with probability σ. The problem is to reconstructxgiven independent traces from it. Our main result is an algorithm that, for any constant perturbation rate 0< σ < 1 and any constant deletion rate 0 < δ < 1, uses poly(n) running time and traces and succeeds with high probability in reconstructing the stringx. This stands in contrast with the worst-case version of the problem, for which\(\text{exp}(\tilde{O}(n^{1/5}))\)is the best known time and sample complexity [8]. Our approach is based on reconstructingxfrom the multiset of its short subwords and is quite different from previous algorithms for either the worst-case or average-case versions of the problem. The heart of our work is a new poly(n)-time procedure for reconstructing the multiset of allO(logn)-length subwords of any source stringx∈ {0,1}ngiven access to traces ofx.more » « less
-
Trace replay is a common approach for evaluating systems by rerunning historical traffic patterns, but it’s not always possible to find suitable real-world traces at the desired level of system load. To experiment with different loads, one needs todownscalea trace to decrease the load orupscalea trace to artificially increase the load. This article expands upon our work,TraceUpscaler[92], by considering the interaction of upscaling and downscaling. In addition to evaluating upscaling with traces collected from a subset of the cluster, we also evaluate upscaling with traces that were downscaled with the state-of-the-art downscaling tool,TraceSplitter[91], to demonstrate that the upscaling and downscaling techniques are compatible and do not introduce unexpected artifacts in the scaling. In addition to comparing against prior approaches, we develop a novel upscaling technique,TraceOverlap, based on the idea of overlapping different time periods in a trace, where we identify the most similar time periods to overlap. Our evaluation demonstrates thatTraceUpscalerandTraceOverlapare both more accurate in maintaining latency characteristics than prior approaches, withTraceUpscalermatching the original trace latency more closely. Finally, we provide a unified framework,TraceScaler, that combinesTraceUpscalerwithTraceSplitterto provide experimenters a common tool for their trace scaling needs.more » « less
-
This paper is about semantic regular expressions (SemREs). This is a concept that was recently proposed by Smore (Chen et al. 2023) in which classical regular expressions are extended with a primitive to query external oracles such as databases and large language models (LLMs). SemREs can be used to identify lines of text containing references to semantic concepts such as cities, celebrities, political entities, etc. The focus in their paper was on automatically synthesizing semantic regular expressions from positive and negative examples. In this paper, we study themembership testing problem. First, we present a two-pass NFA-based algorithm to determine whether a stringwmatches a SemRErinO(|r|2|w|2+ |r| |w|3) time, assuming the oracle responds to each query in unit time. In common situations, where oracle queries are not nested, we show that this procedure runs inO(|r|2|w|2) time. Experiments with a prototype implementation of this algorithm validate our theoretical analysis, and show that the procedure massively outperforms a dynamic programming-based baseline, and incurs a ≈ 2 × overhead over the time needed for interaction with the oracle. Second, we establish connections between SemRE membership testing and the triangle finding problem from graph theory, which suggest that developing algorithms which are simultaneously practical and asymptotically faster might be challenging. Furthermore, algorithms for classical regular expressions primarily aim to optimize their time and memory consumption. In contrast, an important consideration in our setting is to minimize the cost of invoking the oracle. We demonstrate an Ω(|w|2) lower bound on the number of oracle queries necessary to make this determination.more » « less
-
Log-Structured Merge-tree-based Key-Value Stores (LSM-KVS) have been optimized and redesigned for disaggregated storage via techniques such as compaction offloading to reduce the network I/Os between compute and storage. However, the constrained memory space and slow flush at the compute node severely limit the overall write throughput of existing optimizations. In this paper, we proposeO3-LSM,a fundamental new LSM-KVS architecture, that leverages the shared Disaggregated Memory (DM) to support athree-layeroffloading, i.e., memtableOffloading, flushOffloading, and the existing compactionOffloading. Compared to the existing disaggregated LSM-KVS with compaction offloading only, O3-LSM maximizes the write performance by addressing the above issues. O3-LSM first leverages a novelDM-Optimized Memtableto achievedynamic memtable offloading,which extends the write buffer while enabling fast, asynchronous, and parallel memtable transmission. Second, we proposeCollaborative Flush Offloadingthat decouples the flush control plane from execution and supports memtable flush offloading at any node with dedicated scheduling and global optimizations. Third, O3-LSM is further improved with theShard-Level Optimization,which partitions the memtable into shards based on disjoint key-ranges that can be transferred and flushed independently, unlocking parallelism across shards. Besides, to mitigate slow lookups in the disaggregated setting, O3-LSM also employs an adaptiveCache-Enhanced Read Delegationmechanism to combine a compact local cache with DM-assisted memtable delegated read. Our evaluation shows that O3-LSM achieves up to4.5Xwrite,5.2XXrange query, and1.8Xpoint lookup throughput improvement, and up to76%P99 latency reduction compared with Disaggregated-RocksDB, CaaS-LSM, and Nova-LSM.more » « less
