unhappy-path-audit

Unhappy Path Audit Skill

Core Logic (First Principles)

Unhappy path auditing = answering three propositions:

Key principle: Not "looks like it might leak/hang", but "prove it definitely leaks/hangs". Q1 includes ownership cardinality, not only the presence of a destructor. Q2 includes mutex, channel, callback, RPC, I/O, and retry dependencies, not only functions named Wait. Exhaust every bypass and release path before ruling.

---

Systematic Method (Drill-Down Algorithm)

Entry function
  └→ Layer 1: Execute Q1-Q3 on every resource/wait/accumulation point
      ├─ Termination condition satisfied at this layer → ✅, stop drill-down
      └─ Termination condition depends on a lower layer → ⬇ drill down to Layer 2
          └→ Recurse with Q1-Q3

Drill-Down Example

proxy.Close()
  └→ tunnel.Close()                 ← Q1: Destruction guaranteed? ✅ (defer)
      └→ pipe.kickoff() exit        ← Q2: io.EOF guaranteed? → depends on connection.Close()
          └→ connection.Close()     ← Q2: Close guaranteed? → depends on morpc readLoop detection
              └→ morpc readLoop     ← Q2: Condition for detecting close?
                  ├─ readTimeout > 0 → periodic return + detect → ✅
                  └─ readTimeout = 0 → forever blocked on conn.Read → ❌ Bug

---

Audit Workflow

Phase 1 — Scope Definition

Input: target module list
Actions:
  1. Trace the complete call chain from entry to exit
  2. Number layers: Layer 1, Layer 2, ... Layer N
  3. Mark each layer's concern dimensions (goroutine/connection/lock/memory/...)
  4. Draw resource ownership transfers and wait-for edges
  5. Mark restart/retry/pool generation boundaries
Output: audit scope matrix

Phase 2 — Per-Layer Audit

For each Layer:
  1. read_file ≤ 6 files (hard limit)
  2. Execute Q1-Q3 on this layer, including ownership cardinality and hidden wait edges
  3. Record verdict + layer number where termination condition is satisfied
  4. If termination depends on a lower layer → mark drill-down target, do not conclude at this layer
  5. Output this layer's audit table → then proceed to the next layer

Anti-false-positive rule: For every wait point, first exhaust all release paths (including defer, cancel watcher, timer goroutine). Follow indirect edges such as reject → mutex → owner → RPC; a control path is not fail-fast merely because it returns an error after the owner eventually releases it. Only rule it hung when every path is confirmed unreachable.

Phase 3 — Synthesis

1. Merge all layer audit tables
2. Extract failed Q1/Q2/Q3 items
3. Verify termination chain integrity (no break from entry to exit)
4. Apply Bug Claim Verification Checklist (see Critical Rules) to each candidate
5. Generate Issue templates for confirmed Bugs
Output: final risk matrix + Bug list

---

Output Format

Per-Layer Audit Table (Phase 2 output)

Layer N: [Module Name] ([File Name])

| Q | Proposition | Code Path | Verdict | Termination Layer |
|---|-------------|-----------|---------|-------------------|
| Q1 | creation→destruction | go xxx() → defer close() | ✅ | Layer N |
| Q2 | wait→termination | cond.Wait() → Broadcast | ✅ | Layer N (cancel watcher) |
| Q3 | accumulation→bound | channel | ✅ | Layer N |

Final Risk Matrix (Phase 3 output)

| # | Bug | Layer | Q | Severity | Issue |
|---|-----|-------|---|----------|-------|
| 1 | [description] | Layer X | Q2 | High | #12345 |

Termination Chain Verification (Phase 3 output)

Entry
  └→ Layer 1: destruction call ✅
      └→ Layer 2: wait released ✅
          └→ Layer 3: **BREAK** ← Q1 destruction unreachable

---

Critical Rules

Core Rules

1. Anti-confirmation-bias: prove "definitely leaks/hangs", not "looks like it might" — exhaust all bypass paths before ruling
2. Batch hard limit: ≤ 6 read_file per batch, must output audit conclusion for that batch before continuing
3. Exit self-check: before ending the turn confirm — ①conclusion in first paragraph ②audit table present ③Bug has Issue
4. Drill-down discipline: when termination condition is not satisfied, mark "pending drill-down", do not speculate at the current layer

Bug Claim Verification Checklist (BEFORE filing ANY bug)

Every bug claim MUST pass all 5 gates before being included in the final report:

Process rule: G1-G4 are per-bug gates applied during Phase 2→3 transition. G5 is a global gate applied after the full bug list is finalized. Any bug failing G1-G4 is discarded, not downgraded.

G1 Detail: Full-Graph Traversal

For every resource (fd, lock, goroutine, memory allocation), construct the complete directed ownership graph:

Creation Point ──transfer──→ Holder A ──transfer──→ Holder B ──transfer──→ ...
                                  │                    │
                                  ▼                    ▼
                              Reset()              Destroy()
                              Free()               FreeMemory()

Required actions per node:

1. Identify every transfer function (hand-off, assignment, message send)
2. For each transfer target, locate its destruction path
3. Verify destruction path is reachable on error branches too
4. Prove competing branches cannot both execute irreversible cleanup, unless the destructor itself is verified idempotent
5. Repeat until reaching a node with NO further transfer (terminal)

Stop condition: Graph is complete when every leaf is either (a) a verified destructor call, or (b) a GC-managed resource with bounded lifetime.

Q2 Detail: Wait-For And Control Paths

Construct a wait-for graph for each potentially blocking path:

caller -> mutex/channel/future -> owner/receiver -> RPC/I/O/callback -> release

Cancellation, close, abort, timeout, health-check, and rejection paths must be independent of the work they control. If such a path acquires a lock held across downstream work, sends into that work's queue, or synchronously waits for its cleanup, it inherits the downstream termination condition. Trace to the local edge that guarantees progress; a caller context alone is insufficient if the blocked primitive does not observe it.

For restart/retry/pooling, include generation edges: old callbacks and handles must terminate before reuse, and new state must remain unpublished until all admission gates are ready.

G3 Detail: Symmetry Check

For any variable V that exhibits growth (append, map[K]=V, channel send, allocation):

1. Find all assignments to V (grep V\s*=)
2. Confirm one of these assigns nil / empty / zero
3. Verify that assignment is ALWAYS reached before the variable goes out of scope

Common false positive: variable is reset in a function you haven't read yet (e.g., Reset(), Free(), cleanup()). Always search for these BEFORE filing a Q3 bug.

---

Appendix A: Module Threat Model Reference

A.1 Proxy / Execution Dispatch Layer

A.2 morpc / RPC Transport Layer

A.3 Compile / Remote Execution Layer

A.4 Pipeline / Computation Execution Layer

A.5 Txn / Transaction Layer

A.6 Lock Service Layer

A.7 Frontend / Session Layer

A.8 CN Lifecycle Layer

A.9 TAE / Storage Engine Layer (disttae)

A.10 Log Service / Replication Layer

A.11 Hakeeper / Gossip Membership Layer

---

Appendix B: Distributed Component Wait Termination Models

---

Appendix C: Common False Positive Patterns