Kronologi Insiden: State-Space Explosion pada Engine Inferensi

Sebuah pembaruan model dan engine verifikasi formal (SMT/Lean prover wrapper) dirilis ke kluster produksi. Selang 12 menit pasca-rollout, kluster mengalami degradasi total pada pod worker inferensi matematika. Beban kerja ini bertugas membuktikan keabsahan teorem dan langkah derivasi simbolik yang dihasilkan oleh model bahasa (LLM).

Akar masalah berasal dari query inferensi tak terduga yang memicu combinatorial state-space explosion pada solver. Engine verifikasi mencoba mengevaluasi percabangan logika non-linear tanpa batas pencarian (search depth) yang ketat. Akibatnya:

  • CPU pod melonjak konstan ke 100% pada seluruh core yang dialokasikan.
  • Alokasi memori heap solver membengkak secara eksponensial dalam upaya melacak pohon bukti (proof search tree).
  • Linux OOM Killer menghentikan proses solver dengan status ExitCode: 137.
  • Worker daemon gagal memproses ACK/NACK pada antrean pesan, menyebabkan message redelivery loop yang menumbangkan worker lain secara berantai (cascading failure).

Diagnosa Berbasis Metrik: Prometheus & OpenTelemetry

Identifikasi masalah difokuskan pada tiga metrik inti: saturasi CPU/memori, latensi pemrosesan solver, dan antrean backlog.

1. Solver Latency Spikes

Tracing OpenTelemetry mencatat span solve_theorem tidak pernah selesai (mencapai batas default HTTP proxy 300 detik) atau terputus abruptly karena OOM. Metrik histogram Prometheus menunjukkan anomali tajam pada persentil ke-99:

# Query p99 latensi eksekusi solver per versi deployment
histogram_quantile(0.99, sum(rate(solver_execution_duration_seconds_bucket{job="math-solver"}[5m])) by (le, revision))

2. Memory Saturation & OOMKilled Pods

Metrik container dari cadvisor mengonfirmasi bahwa pod canary menghabiskan batas kuota memori (cgroup memory limit) sebelum sempat mengembalikan error ke client:

# Deteksi laju OOMKilled pada container
sum(increase(kube_pod_container_status_terminated_reason{reason="OOMKilled", pod=~"math-solver-canary-.*"}[5m])) by (pod) > 0

3. Queue Backlog Accumulation

Ketika worker terkunci dalam kalkulasi intensif, metrik antrean Redis/RabbitMQ menunjukkan divergensi tajam antara published messages dan acknowledged messages:

# Monitoring queue backlog / consumer lag
queue_messages_unacknowledged{queue="math_jobs"} > 50

Automated Canary Rollback dengan Argo Rollouts

Insiden ini berlangsung lebih lama dari yang seharusnya akibat deployment tradisional Kubernetes Deployment dengan strategi rolling update biasa. Pod baru lolos readiness probe awal karena probe hanya memeriksa status HTTP server, bukan kesiapan solver menerima beban berat.

Solusinya adalah mengadopsi Argo Rollouts dengan AnalysisTemplate berbasis Prometheus SLI. Jika latensi solver p99 melebihi ambang batas atau pod mengalami crash/OOM selama fase canary, rollout otomatis dibatalkan (aborted) dan trafik dialihkan kembali ke versi stabil.

Definisi AnalysisTemplate

apiVersion: argoproj.io/v1alpha1
kind: AnalysisTemplate
metadata:
  name: solver-health-analysis
  namespace: inference
spec:
  metrics:
  - name: p99-latency
    interval: 30s
    successCondition: result[0] < 5.0
    failureLimit: 2
    provider:
      prometheus:
        address: http://prometheus-k8s.monitoring.svc:9090
        query: |
          histogram_quantile(0.99, sum(rate(solver_execution_duration_seconds_bucket{pod=~"math-solver-canary-.*"}[1m])) by (le))
  - name: oom-rate
    interval: 30s
    successCondition: result[0] == 0
    failureLimit: 1
    provider:
      prometheus:
        address: http://prometheus-k8s.monitoring.svc:9090
        query: |
          sum(increase(kube_pod_container_status_terminated_reason{reason="OOMKilled", pod=~"math-solver-canary-.*"}[1m])) or vector(0)

Integrasi pada Rollout Resource

apiVersion: argoproj.io/v1alpha1
kind: Rollout
metadata:
  name: math-solver
  namespace: inference
spec:
  replicas: 10
  strategy:
    canary:
      steps:
      - setWeight: 10
      - pause: {duration: 5m}
      - analysis:
          templates:
          - templateName: solver-health-analysis
      - setWeight: 50
      - pause: {duration: 5m}
  template:
    spec:
      containers:
      - name: solver
        image: registry.internal/math-solver:v2.4.1
        resources:
          requests:
            cpu: "2"
            memory: "4Gi"
          limits:
            cpu: "4"
            memory: "8Gi"

Pencegahan dan Hardening Arsitektur

Rollback otomatis meminimalkan dampak, tetapi workload verifikasi formal membutuhkan pertahanan berlapis pada tingkat runtime engine dan konfigurasi kernel container.

1. Isolasi Subprocess & Engine Hard Timeout

Jangan menjalankan theorem prover langsung di dalam thread atau event-loop utama daemon HTTP/Queue. Eksekusi engine solver (seperti Z3, CVC5, atau Lean) harus dibungkus dalam proses terpisah dengan batas sumber daya eksplisit.

import subprocess
import resource

def run_solver_with_hard_limits(proof_script: str, timeout_seconds: int = 10, max_memory_mb: int = 4096) -> str:
    def set_limits():
        # Batasi memori virtual via cgroups/RLIMIT_AS
        max_bytes = max_memory_mb * 1024 * 1024
        resource.setrlimit(resource.RLIMIT_AS, (max_bytes, max_bytes))
        # Batasi waktu CPU
        resource.setrlimit(resource.RLIMIT_CPU, (timeout_seconds, timeout_seconds + 1))

    try:
        proc = subprocess.run(
            ["lean", "--run", "-"],
            input=proof_script,
            text=True,
            capture_output=True,
            timeout=timeout_seconds,  # Wall-clock timeout
            preexec_fn=set_limits
        )
        return proc.stdout
    except subprocess.TimeoutExpired:
        raise TimeoutError("State-space search exceeded wall-clock timeout limit")

Catatan: Parameter rlimit menjamin solver dimatikan oleh kernel OS jika mencoba mengalokasikan memori melebihi kuota worker, sehingga mencegah pod utama terbunuh oleh OOMKilled.

2. Engine-Level Parameters

Pada level solver (misal Z3 atau Lean), konfigurasi batasan komputasi internal harus selalu diterapkan selain batas waktu level OS:

  • Deterministic Resource Limit: Gunakan parameter seperti rlimit pada SMT solver. Tidak seperti waktu riil (wall-clock), rlimit berbasis langkah alokasi internal solver, sehingga deterministik dan tidak bergantung pada variasi beban CPU host.
  • Memory Cap Parameter: Pasang argumen -memory:MB untuk memicu pembersihan internal (garbage collection) sebelum menyentuh batas cgroup pod.

3. In-flight Concurrency & Load Shedding

Terapkan semaphore-based circuit breaker pada worker. Jika waktu eksekusi antrean rata-rata melampaui SLA (misal > 15 detik), sistem harus menolak beban baru secara adaptif menggunakan HTTP 429 Too Many Requests atau menjadwalkan ulang query pembuktian tersebut ke antrean komputasi asinkron berbiaya rendah (batch pool).