S152 · SOURCE-BOUND GATE EVIDENCE
K2: extended bounded IPC deadline replay
Operations --test hedefi → simulation public mod ipc_deadline_clock bağı → kaynak kesiti Bu sayfa yalnız S152 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.
S152Focused kod testiOperations id exactsource SHA exacttest target exact
operation: k2-ipc-deadline-extended-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: d7851da79028…file 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: e703130e0915…file sha256: feb6feb7e21d…
03 · Kapı kimlik kaydı
Operations sıra, kimlik ve başlık bağı
tam Operations kaydıL23923–L23980
website/src/lib/operations.ts::k2-ipc-deadline-extended-replay-partial
{
id: "k2-ipc-deadline-extended-replay-partial",
date: "2026-08-24",
sequence: 152,
status: "passed",
umbrella_status: "partial",
title: "K2: extended bounded IPC deadline replay",
summary:
"S152, S151'in aynı production no_std deadline tablosunu ve gerçek CNTVCT/CNTFRQ clock authority'sini sekiz ardışık tam-dolum/boşaltım çevrimine genişletir. ROUNDS=8, FULL_TABLES=8, RETIRED=256; her tablo 320 ms full-table SLA, ACTIVE=0 kapanışı ve global active=0→0 ile PASS oldu. ABI v1.3 değişmedi. Dar continuity kabulü PASS, uzun soak/product workload/Generic SMP açık olduğu için umbrella PARTIAL'dır.",
evidence: [
"ipc_deadline_workload_replay: 4/4 PASS; dört model kapısı ve S151/S152 source/QEMU wiring sözleşmesi geçti.",
"QEMU gerçek CNTVCT_EL0/CNTFRQ_EL0 otoritesinde ROUNDS=8, FULL_TABLES=8, RETIRED=256 ve son bağımsız koşuda MAX_MEASURED_NS_CEIL=312026000 <= 320000000 üretti.",
"Exact ABI/IPC envanteri 12 binary / 108/108, AArch64 board-qemu/board-rpi4/board-rpi5/board-rpi5+smp 4/4 PASS.",
"Ham workspace 112 grupta 724 PASS / aynı yedi tarihsel frozen G8h assertion FAIL; yalnız exact yedi isim dışlandığında 724/724 PASS. Tam-workspace GREEN iddia edilmedi.",
"Her çevrim 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; yeni admission veya ürün eşiği eklenmedi.",
"make verify-qemu: S151 bounded four-round ve S152 extended bounded eight-round deadline replay marker'ları PASS; mevcut regresyonlar da PASS.",
"S152 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S152=NO.",
"Kalıcı kapsam: `docs/K2-S152-IPC-Deadline-Extended-Replay-Proof.md`.",
],
commands: [
"cargo test -p aselsan_microkernel_simulation --test ipc_deadline_workload_replay -- --test-threads=1",
"make verify-qemu",
],
terminalSessions: [
{
id: "s152-extended-replay-focused",
title: "Extended bounded deadline replay kaynak/model kapısı",
commandLines: [
"cargo test -p aselsan_microkernel_simulation --test ipc_deadline_workload_replay -- --test-threads=1",
],
outputLines: ["running 4 tests", "test result: ok. 4 passed; 0 failed"],
exitCode: 0,
outputMode: "selected",
},
{
id: "s152-extended-replay-qemu",
title: "Sekiz ardışık tam tablo ve 256 retirement QEMU kapısı",
commandLines: ["make verify-qemu"],
outputLines: [
"[K2-S152] ... ROUNDS=8 FULL_TABLES=8 RETIRED=256 MAX_MEASURED_NS_CEIL=312026000 ... SLA=PASS ... EXECUTOR=PASS",
"QEMU smoke PASS: ... S152 extended bounded eight-round deadline replay ...",
],
exitCode: 0,
outputMode: "selected",
},
],
terminalSessionsNote:
"S152 bounded continuity 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ı; S152 sekiz 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_S152=NO.",
],
},snippet sha256: b2c943e0fca9…file sha256: 9726dbf00f84…
Focused test komutu
cargo test -p aselsan_microkernel_simulation --test ipc_deadline_workload_replay -- --test-threads=1proof: docs/K2-S152-IPC-Deadline-Extended-Replay-Proof.md
Registry schema v5 · generator
website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06