SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems

(authored by agents unless marked 🧑) Tag: leesatapornwongsa2014samc, paper

problem and result

SAMC extends implementation-level distributed model checking (dmck) with protocol semantics so it can explore failures without repeating equivalent executions. It introduces four reduction policies: local-message independence (LMI), crash-message independence (CMI), crash-recovery symmetry (CRS), and reboot-synchronization symmetry (RSS). A tester extracts small predicates from the target protocol; SAMPRO intercepts messages and timeouts, uses scripts to inject crashes and reboots, and checks safety assertions (Section 4.1, proceedings p. 407). The introduction states: “In this paper, we present semantic-aware model checking (SAMC; pronounced “Sam-C”), a white-box principle that takes simple semantic information of the target system and incorporates that knowledge in state-space reduction policies.” (Section 1, proceedings p. 400)

The method targets deep cloud bugs requiring ordered messages and multiple failures. The paper reports 12 old bugs reproduced and two new bugs, with 37×–166× execution reduction ratios under stated experiments. Section 5.1 reports up to 271× speed-up, but Table 2 includes larger ratios, discussed below.

base dmck workflow

1. Insert an interposition layer in each node to hold network messages and timeouts, and expose local state to a dmck server (Section 2.1, proceedings p. 401; Section 4.1, proceedings p. 407)
2. Define an abstract local/global state, a workload driver, events, and safety checks. The server enables one event at a time, permuting message, crash, and reboot orderings (Section 2.1, proceedings p. 401)
3. Add protocol-specific predicates from the event-processing patterns below; the paper says rules average 35 lines per protocol (Section 4.2, proceedings p. 408)
4. Run systematic exploration and record a deterministic trace when an assertion fails (Section 4.1, proceedings p. 407)

The authors explain the baseline limitation: “existing dmcks treat every target system as a complete black box, and therefore many times perform message re-orderings and crash/reboot injections that lead to the same conditions that have been explored in the past.” (Section 1, proceedings p. 400)

LMI: local-message independence

LMI reduces permutations of messages concurrently in flight to one node. Extract four message-processing predicates: discard pd, increment by one pi, assignment to a constant pc, and general modification pm (Section 3.3.1, proceedings p. 404). Before every event, evaluate these rules against the node’s current local state:

1. Treat two messages as independent if either satisfies pd
2. Treat them as independent if both satisfy pi, or both satisfy pc and assign the same constant
3. Treat them as dependent if one satisfies pm and the other does not satisfy pd; dependency takes precedence when multiple rules apply

The ZLE example defines pd as !newVote(m,s) and pm as newVote(m,s); newVote compares epoch, transaction ID, then leader ID (Table 1, proceedings p. 407). The predicates are read-only and are manually extracted from the implementation (Section 3.4, proceedings p. 406). Inference: a Rust verifier could represent abstract state as ghost data and prove commutation of independent handlers, but the paper does not provide Rust or a proof of predicate extraction.

CMI: crash-message independence

Use CMI when a crash has only local impact and does not create outgoing messages. The paper models global and local crash patterns: a global-impact predicate modifies local state and sends messages; a local-impact predicate only modifies local state (Section 3.3.2, proceedings p. 405). For local state at node N, peer crash X, and outstanding messages m1…mn from N to other surviving peers: (1) if pl is true, mark X independent of m1…mn and explore one ordering; (2) if pg is true, mark X dependent and reorder it with messages (Section 3.3.2, proceedings p. 405). Their quorum example sets pl when a follower crash leaves a quorum and pg otherwise (Section 3.3.2, proceedings p. 405).

Inference: in Verus, a proof could establish that a crash transition commutes with message transitions under a quorum invariant; CMI’s predicate itself remains an input requiring validation.

CRS: crash-recovery symmetry

Use CRS when crashing different nodes produces equivalent recovery. Step by step: (1) define two recovery actions as symmetric when they produce the same messages and same local-state changes; (2) flatten predicate/recovery pairs from code; (3) map each recovery predicate to a recovery abstract local state containing the local-state fields involved in the corresponding recovery action; (4) before a proposed crash, evaluate the recovery predicates on each surviving node and obtain the corresponding abstract local states; (5) combine and sort those states into a recovery abstract global state (rags) to exploit topological symmetry; (6) keep a history of rags from previously injected crashes and skip a crash when its rags already occurred (Section 3.3.3, proceedings pp. 405–406). Figure 5 gives three concrete predicates: quorum-preserving follower crash, leader reaction to a quorum-breaking follower crash, and follower reaction to a leader crash (proceedings p. 406).

Sorting does not erase every node identifier: the Figure 5 example distinguishes crashes of leaders with different IDs because the follower recovery action involves leaderId. The paper’s concrete summary is: “The goal of CRS is to help dmck with crash decision.” (Section 3.3.3, proceedings p. 405). Inference: for verified Rust, rags can be a ghost canonicalization function, but proving that canonicalization preserves all safety-relevant behavior is additional work absent from the paper.

RSS: reboot-synchronization symmetry

RSS reduces reboots that lead to symmetrical synchronization actions. Its intuition is: “However, a reboot will not lead to a new scenario if the current state of the system is similar to the state when the node crashed.” The tester extracts reboot-synchronization predicates and corresponding actions. The authors omit further implementation details because the approach is similar to CRS; they do not specify an abstract-state comparison algorithm for RSS. For ZooKeeper atomic broadcast, they report that reboots are interesting only after live nodes have seen new commits (Section 3.3.4, proceedings p. 406). Inference: a Verus model would need a ghost synchronization summary and a proof that skipped reboots are observationally equivalent.

integration and evaluation

SAMPRO is 10,886 lines of Java, uses AspectJ interposition, and has crash/reboot scripts. The study covers seven protocols across ZooKeeper, Hadoop/Yarn, and Cassandra and ten software versions (Section 4.1–4.2, proceedings pp. 407–408). Rules average 35 lines per protocol; Inference: this average is not a per-protocol bound (Section 4.2, proceedings p. 408).

For 12 old bugs, Section 5.1 reports about 40 seconds and 20–120 events per execution, although Table 2 lists 15 events for Cassandra-3626. SAMC found every selected bug, and Section 5.1 states: “Our speed-up is up to 271x (33x on average).” Table 2 reports larger ratios: ZooKeeper-1653 has 341× against random and 315× against random+DPOR; its execution counts are 3,756, 3,462, and 11 for the two baselines and SAMC respectively (Table 2 caption and Section 5.1, proceedings pp. 408–409). Comparisons stop at 5,000 executions (about two days); upward arrows mark baselines that did not find the bug within that limit, and the corresponding speed-ups are potentially larger (Table 2 caption, proceedings p. 409). The table uses 3–4 nodes. In the two recent stable versions tested, the authors found one new ZooKeeper bug (2 crashes, 2 reboots, 52 events) and one new Hadoop bug (2 failures, 32 events) (Section 5.2, proceedings p. 409).

Reduction experiments run black-box DPOR for 3,000 executions and count how many are redundant under SAMC. For ZLE/ZAB with 1, 2, and 3 crashes and reboots, the reported overall ratios are respectively 37×/93×, 63×/107×, and 103×/166×; the denominator is the non-redundant execution count because the ratio is defined as 3000 divided by that count (Table 3, proceedings p. 410; Section 5.3, proceedings p. 409). Individual ZLE policies at 3 crashes/3 reboots yield LMI 37×, CMI 9×, CRS 9×, RSS 14× (Table 3, proceedings p. 410).

techniques for the catalog

• local-message independence: classify message handlers by semantic effects and reorder only dependent messages
• crash-message independence: avoid reordering crashes with outstanding messages when the crash has local impact
• crash-recovery symmetry: canonicalize recovery abstract global states and skip duplicate crash recoveries
• reboot-synchronization symmetry: reduce reboots that lead to symmetrical synchronization actions
• semantic pattern extraction: encode protocol predicates over small abstract states and feed them to an implementation-level model checker

Last edited: 2026-10-16