Researchers at the University of Virginia, the University of Michigan and other institutions wrote a paper included in the proceedings of the USENIX Symposium on Operating Systems Design and Implementation, OSDI, of July 2025. It proposes deriving what it calls semantic checkers from a distributed system's existing tests, to catch failures in which "various defects can cause a system to silently violate its semantics without explicit errors." Parts of the paper follow, not the whole.
Failures Without Explicit Errors
The paper gives an instance. A distributed message service whose publish API promises at-most-once delivery may deliver some message twice. Failures of this kind lead to "severe consequences including data loss, wrong results, inconsistency, and vulnerabilities," and the harm spreads to applications that rely on the affected semantics.
With no explicit error signal, such failures escape existing failure detectors. With few error messages, developers are "clueless in debugging failures." Ideally, bugs causing silent failures "should be eliminated in testing." But "it is elusive to eliminate all bugs in production distributed systems."
Checks That Know the System
So the paper argues for runtime verification: a safeguard that continuously monitors a deployed distributed system and quickly detects silent failures. At its center are semantic checkers, which validate the system's semantics, such as at-most-once delivery. The paper distinguishes them from generic checks, for example for CPU usage, timeouts and exceptions.
Because semantic checkers "require system-specific knowledge, the conventional wisdom is that they have to be written manually." For a large distributed system, the paper says, that is "a daunting task."
From Tests to Checkers
The researchers observe that a distributed system's test cases "often contain valuable information about the system semantics". The paper then asks, "if existing tests contain expressive checks, why do they still fail to prevent silent failures?" Its answer is that such tests are tied to specific input in a fixed setup, while in production the same semantics can be violated by different bugs, triggered by other inputs and dynamic conditions.
Often, the tests knew what correct looked like. They asked the question only for the input they were written for, and production brings other inputs.
The researchers built a framework, T2C, that uses static and dynamic analysis to turn a test into a runtime checker. The checkers it makes can then be deployed with the system to production, and can detect new semantic violations under workloads different from the original tests. T2C also "performs multi-level validation on the synthesized checkers to ensure they are valid." On four widely used distributed systems, it transformed 672 test cases into what the paper calls "verified semantic checkers."
What It Caught, What It Missed, and the Limits
The researchers reproduced 20 user-reported production silent failures, and the checkers detected 15 of them "in a median of 0.188 seconds." Most of the test cases those checkers came from "were added by developers long before the failures."
T2C missed five, which the paper calls "unsurprising since T2C cannot guarantee detecting all silent failures." For those, either the system lacked tests that covered the violated semantics, or a related test had no useful assertions, or the test workloads were "written in a spaghetti style (usually a result of several ad-hoc patches) that are hard to generalize."
The method, the paper says, "relies on certain assumptions on test quality." Its measures against side effects, static analysis to exclude dangerous system operations and a cross-validation step to filter out poorly generalized checkers, "do not fully guarantee generated checkers side-effect free." And the researchers "consider initially deploying T2C in testing or pre-production environments (e.g., staging deployment) to be a practical way of gaining confidence before production deployment."
Sources
- Researchers at the University of Virginia, the University of Michigan and other institutions, in the Proceedings of the 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI '25). Deriving Semantic Checkers from Tests to Detect Silent Failures in Production Distributed Systems. July 2025. peer-reviewed paper