ASELSANMicrokernel
S151 · SOURCE-BOUND GATE EVIDENCE

K2: bounded IPC deadline workload replay

Operations --test hedefi → simulation public mod ipc_deadline_clock bağı → kaynak kesiti Bu sayfa yalnız S151 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S151Focused kod testiOperations id exactsource SHA exacttest target exact

operation: k2-ipc-deadline-workload-replay-partial

uygulama/model · focused test · Operations · 3 exact excerpt

sequence-bound=true · implementation-bound=true
01 · Testin bağlı olduğu uygulama/model kodu

Kapının yürüttüğü gerçek kaynak

tam Rust öğesiL7–L152
kernel/src/ipc_deadline_clock.rs::DeadlineClockBudget

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum DeadlineClockError {
    ZeroCounterFrequency,
    ZeroTickRate,
    ZeroPeriod,
    CounterFrequencyBelowTickRate,
    PeriodMismatch { expected: u64, observed: u64 },
    ZeroCapacity,
    ZeroServiceBudget,
    ArithmeticOverflow,
    CounterRegressed,
    ServiceTickSpanMismatch { expected: u64, observed: u64 },
    LatencySlaExceeded { measured_ns: u64, sla_ns: u64 },
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct DeadlineClockBudget {
    pub counter_hz: u64,
    pub tick_hz: u64,
    pub period_counts: u64,
    pub capacity: usize,
    pub service_budget_per_irq: usize,
    pub service_turns: usize,
    pub quantum_ns_ceil: u64,
    pub full_table_service_sla_ns: u64,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct DeadlineLatencyObservation {
    pub tick_span: u64,
    pub distinct_service_irqs: usize,
    pub counter_span: u64,
    pub measured_ns_ceil: u64,
    pub sla_ns: u64,
    pub slack_ns: u64,
}

impl DeadlineClockBudget {
    pub fn try_new(
        counter_hz: u64,
        tick_hz: u64,
        period_counts: u64,
        capacity: usize,
        service_budget_per_irq: usize,
    ) -> Result<Self, DeadlineClockError> {
        if counter_hz == 0 {
            return Err(DeadlineClockError::ZeroCounterFrequency);
        }
        if tick_hz == 0 {
            return Err(DeadlineClockError::ZeroTickRate);
        }
        if period_counts == 0 {
            return Err(DeadlineClockError::ZeroPeriod);
        }
        if capacity == 0 {
            return Err(DeadlineClockError::ZeroCapacity);
        }
        if service_budget_per_irq == 0 {
            return Err(DeadlineClockError::ZeroServiceBudget);
        }

        let expected_period = counter_hz / tick_hz;
        if expected_period == 0 {
            return Err(DeadlineClockError::CounterFrequencyBelowTickRate);
        }
        if period_counts != expected_period {
            return Err(DeadlineClockError::PeriodMismatch {
                expected: expected_period,
                observed: period_counts,
            });
        }

        let service_turns = capacity
            .checked_add(service_budget_per_irq - 1)
            .ok_or(DeadlineClockError::ArithmeticOverflow)?
            / service_budget_per_irq;
        let quantum_ns_ceil = ceil_mul_div_u64(period_counts, NANOS_PER_SECOND, counter_hz)
            .ok_or(DeadlineClockError::ArithmeticOverflow)?;
        let full_table_service_sla_ns = quantum_ns_ceil
            .checked_mul(
                u64::try_from(service_turns).map_err(|_| DeadlineClockError::ArithmeticOverflow)?,
            )
            .ok_or(DeadlineClockError::ArithmeticOverflow)?;

        Ok(Self {
            counter_hz,
            tick_hz,
            period_counts,
            capacity,
            service_budget_per_irq,
            service_turns,
            quantum_ns_ceil,
            full_table_service_sla_ns,
        })
    }

    /// Convert counter ticks with ceil rounding so an observed duration is
    /// never understated. `None` means the nanosecond result cannot fit u64.
    pub fn counts_to_ns_ceil(self, counts: u64) -> Option<u64> {
        ceil_mul_div_u64(counts, NANOS_PER_SECOND, self.counter_hz)
    }

    /// Validate the first-to-last service window of one initially full table.
    /// One exact record must be retired on each consecutive service IRQ, so
    /// N turns span N-1 tick intervals. The SLA remains the conservative N
    /// quantum envelope and all conversion rounds upward.
    pub fn validate_full_table_observation(
        self,
        first_service_tick: u64,
        last_service_tick: u64,
        first_service_count: u64,
        last_service_count: u64,
    ) -> Result<DeadlineLatencyObservation, DeadlineClockError> {
        let expected_tick_span = u64::try_from(self.service_turns - 1)
            .map_err(|_| DeadlineClockError::ArithmeticOverflow)?;
        let observed_tick_span = last_service_tick.wrapping_sub(first_service_tick);
        if observed_tick_span != expected_tick_span {
            return Err(DeadlineClockError::ServiceTickSpanMismatch {
                expected: expected_tick_span,
                observed: observed_tick_span,
            });
        }
        let counter_span = last_service_count
            .checked_sub(first_service_count)
            .ok_or(DeadlineClockError::CounterRegressed)?;
        let measured_ns_ceil = self
            .counts_to_ns_ceil(counter_span)
            .ok_or(DeadlineClockError::ArithmeticOverflow)?;
        if measured_ns_ceil > self.full_table_service_sla_ns {
            return Err(DeadlineClockError::LatencySlaExceeded {
                measured_ns: measured_ns_ceil,
                sla_ns: self.full_table_service_sla_ns,
            });
        }

        Ok(DeadlineLatencyObservation {
            tick_span: observed_tick_span,
            distinct_service_irqs: self.service_turns,
            counter_span,
            measured_ns_ceil,
            sla_ns: self.full_table_service_sla_ns,
            slack_ns: self.full_table_service_sla_ns - measured_ns_ceil,
        })
    }
}
snippet sha256: d7851da79028file sha256: 4a68cb69f841
02 · Doğrulayan test kodu

Operations komutuna bağlı focused test

tam Rust öğesiL104–L121
simulation/tests/ipc_deadline_workload_replay.rs::replay_is_bounded_and_does_not_claim_unproven_scope

#[test]
fn replay_is_bounded_and_does_not_claim_unproven_scope() {
    assert!(IPC.contains("pub const IPC_DEADLINE_WORKLOAD_REPLAY_ROUNDS: usize = 4;"));
    assert!(IPC.contains("pub const IPC_DEADLINE_EXTENDED_REPLAY_ROUNDS: usize = 8;"));
    assert!(IPC.contains("pub const IPC_DEADLINE_LONGER_BOUNDED_REPLAY_ROUNDS: usize = 16;"));
    assert!(IPC.contains("pub const IPC_DEADLINE_MAX_BOUNDED_REPLAY_ROUNDS: usize = 32;"));
    assert!(MAIN.contains("run_qemu_s151_ipc_deadline_workload_replay();"));
    assert!(MAIN.contains("run_qemu_s152_ipc_deadline_extended_replay();"));
    assert!(MAIN.contains("run_qemu_s153_ipc_deadline_longer_bounded_replay();"));
    assert!(MAIN.contains("run_qemu_s154_ipc_deadline_max_bounded_replay();"));
    assert!(MAIN.contains("ROUNDS={} FULL_TABLES={} RETIRED={} MAX_MEASURED_NS_CEIL={}"));
    assert!(MAIN.contains("not long-duration"));
    assert!(SMOKE.contains("K2-S151"));
    assert!(SMOKE.contains("K2-S152"));
    assert!(SMOKE.contains("K2-S153"));
    assert!(SMOKE.contains("K2-S154"));
}
snippet sha256: e703130e0915file sha256: feb6feb7e21d
03 · Kapı kimlik kaydı

Operations sıra, kimlik ve başlık bağı

tam Operations kaydıL23981–L24056
website/src/lib/operations.ts::k2-ipc-deadline-workload-replay-partial
  {
    id: "k2-ipc-deadline-workload-replay-partial",
    date: "2026-08-24",
    sequence: 151,
    status: "passed",
    umbrella_status: "partial",
    title: "K2: bounded IPC deadline workload replay",
    summary:
      "S151, S150 CNTVCT/CNTFRQ-kalibreli 32-slot deadline SLA'sını aynı production no_std registry üzerinde dört ardışık tam-dolum/boşaltım çevriminde tekrarlar. Dört tablo, 128 retirement, IRQ başına tek kayıt ve her çevrimde 320 ms full-table SLA PASS oldu; ABI v1.3 değişmedi. Dar replay kabulü PASS, Generic SMP ve ürün/workload eşikleri açık olduğu için K2/K1/MEM0–MEM2 umbrella durumu PARTIAL'dır.",
    evidence: [
      "ipc_deadline_workload_replay: 3/3 PASS; dört bounded gözlem penceresi, tek missed-tick/SLA overrun rejection ve source/QEMU wiring kapısı geçti.",
      "QEMU gerçek CNTVCT_EL0/CNTFRQ_EL0 otoritesinde ROUNDS=4, FULL_TABLES=4, RETIRED=128 ve MAX_MEASURED_NS_CEIL <= 320000000 üretti.",
      "Her replay çevrimi ortak deadline tablosunu ACTIVE=32'den ACTIVE=0'a döndürdü; global deadline snapshot 0→0 kaldı.",
      "ABI v1.3 ve mevcut CALL/RECV/notification syscall numaraları değişmedi; replay yeni admission veya ürün eşiği eklemedi.",
      "make verify-qemu: S151 bounded four-round deadline workload replay marker'ı PASS; mevcut W^X, IPC reply, RuntimePmm reclaim ve kernel-fault regresyonları da PASS.",
      "Cloudflare Pages deployment: https://527e71a6.aselsan-microkernel.pages.dev",
      "Custom domain canlı doğrulaması: /operations/, /timeline/ ve /yol-haritasi/ HTTP 200; üç rotada S151 marker'ı bulundu.",
      "S151 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S151=NO.",
      "Kalıcı kapsam: `docs/K2-S151-IPC-Deadline-Workload-Replay-Proof.md`.",
    ],
    commands: [
      "cargo test -p aselsan_microkernel_simulation --test ipc_deadline_workload_replay -- --test-threads=1",
      "make verify-qemu",
      "npm test && npm run lint && npx tsc --noEmit && npm run build",
      "npm run deploy",
      "curl -L --max-time 20 https://aselsan.kerege.net/{operations,timeline,yol-haritasi}/",
    ],
    terminalSessions: [
      {
        id: "s151-workload-replay-focused",
        title: "Bounded deadline workload replay kaynak/model kapısı",
        commandLines: [
          "cargo test -p aselsan_microkernel_simulation --test ipc_deadline_workload_replay -- --test-threads=1",
        ],
        outputLines: ["running 3 tests", "test result: ok. 3 passed; 0 failed"],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "s151-workload-replay-qemu",
        title: "Dört ardışık tam tablo ve 128 retirement QEMU kapısı",
        commandLines: ["make verify-qemu"],
        outputLines: [
          "QEMU smoke PASS: ... S151 bounded four-round deadline workload replay ...",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "s151-web-publication",
        title: "S151 web deployment ve custom-domain canlı doğrulaması",
        commandLines: [
          "npm test && npm run lint && npx tsc --noEmit && npm run build",
          "npm run deploy",
          "curl -L --max-time 20 https://aselsan.kerege.net/{operations,timeline,yol-haritasi}/",
        ],
        outputLines: [
          "249 tests passed; lint, TypeScript ve Next production build PASS",
          "Deployment complete · https://527e71a6.aselsan-microkernel.pages.dev",
          "custom domain: operations HTTP 200, timeline HTTP 200, yol-haritasi HTTP 200; S151 marker bulundu",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S151 bounded QEMU/host workload replay kabulüdür; uzun saturation soak, Generic SMP ve fiziksel Raspberry Pi workload latency PASS'i değildir.",
    limitations: [
      "Uzun süreli saturation soak ve production workload sizing henüz imzalanmadı; S151 yalnız dört bounded çevrimdir.",
      "İmzalı NORMAL/WARN/CRITICAL ürün eşikleri ve fiziksel RPi latency ölçümü kapsam dışıdır.",
      "Generic SMP cross-CPU timer/signal/revoke/wake/IPI/TLB/reaper arbitration matrisi kapanmadı.",
      "Cross-subsystem rollback, capability transferi, shared-memory loan ve ortak frame/cap/endpoint/ASID reconciliation kapsam dışıdır.",
      "Tam workspace tarihsel frozen G8h identity/closure assertion'ları nedeniyle GREEN değildir; bu kayıt onları gevşetmez.",
      "Fiziksel/device operations=0; RUNBOOK_EXECUTED_IN_S151=NO.",
    ],
  },
snippet sha256: 6e7b56b5df4ffile sha256: 9726dbf00f84
Focused test komutu
cargo test -p aselsan_microkernel_simulation --test ipc_deadline_workload_replay -- --test-threads=1
proof: docs/K2-S151-IPC-Deadline-Workload-Replay-Proof.md
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 3050638b71a684d8f8f947a8a6faa237a17fa8db5dc0db04fb207b668b462af9