ASELSANMicrokernel
S150 · SOURCE-BOUND GATE EVIDENCE

K2: CNTVCT-kalibreli IPC deadline wall-clock SLA

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

S150Focused kod testiOperations id exactsource SHA exacttest target exact

operation: k2-ipc-deadline-clock-sla-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 öğesiL1–L152
kernel/src/ipc_deadline_clock.rs::DeadlineClockError
//! Allocation-free wall-clock calibration and latency budget for the shared
//! IPC deadline registry. The kernel supplies the authoritative generic-timer
//! frequency and period; this module keeps the arithmetic host-testable and
//! independent of AArch64 register access.

pub const NANOS_PER_SECOND: u64 = 1_000_000_000;

#[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: f12d622904a9file sha256: 4a68cb69f841
02 · Doğrulayan test kodu

Operations komutuna bağlı focused test

tam Rust öğesiL105–L116
simulation/tests/ipc_deadline_clock_sla.rs::production_sources_require_the_same_clock_budget_and_qemu_marker

#[test]
fn production_sources_require_the_same_clock_budget_and_qemu_marker() {
    assert!(TIMER.contains("pub const TICK_HZ: u64 = 100;"));
    assert!(IPC.contains("pub const IPC_DEADLINE_TICK_HZ: u64 ="));
    assert!(IPC.contains("pub const IPC_DEADLINE_FULL_TABLE_SERVICE_SLA_NS: u64 = 320_000_000;"));
    assert!(IPC.contains("DeadlineClockBudget::try_new("));
    assert!(MAIN.contains("run_qemu_s150_ipc_deadline_clock_sla"));
    assert!(MAIN.contains("FULL_TABLE_SLA_NS=320000000 SLA=PASS"));
    assert!(MAIN.contains("DISTINCT_SERVICE_IRQS=32"));
    assert!(SMOKE.contains("K2-S150"));
}
snippet sha256: 0cd9e3a35a20file sha256: 6540c76ec819
03 · Kapı kimlik kaydı

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

tam Operations kaydıL24057–L24166
website/src/lib/operations.ts::k2-ipc-deadline-clock-sla-partial
  {
    id: "k2-ipc-deadline-clock-sla-partial",
    date: "2026-08-24",
    sequence: 150,
    status: "passed",
    umbrella_status: "partial",
    title: "K2: CNTVCT-kalibreli IPC deadline wall-clock SLA",
    summary:
      "S150, S149'da soyut tick olarak kalan ortak allocation-free CALL/RECV/notification deadline bütçesini CNTVCT_EL0/CNTFRQ_EL0 ile gerçek ARM Generic Timer sayacına bağladı. QEMU'da CNTFRQ=62500000, TICK_HZ=100, quantum=10000000 ns, capacity=32 ve IRQ başına tek kayıt sözleşmesiyle 32 ayrı PPI27 IRQ'su ölçüldü: ilk-son retirement penceresi 310064992 ns, signed full-table SLA 320000000 ns ve SLA=PASS. ABI v1.3 değişmedi. Dar S150 kabulü PASS; product workload/uzun soak, fiziksel RPi latency ve Generic SMP açık olduğundan K2/K1/MEM0–MEM2 umbrella PARTIAL'dır.",
    evidence: [
      "Fail-closed bring-up iki RED aşamasını korur: clock authority modülü yokken kaynak testi derlenmedi; ilk QEMU entegrasyonu scheduler preemption nedeniyle `S150 missed a distinct service IRQ` panic'i verdi. İki koşuda da PASS iddia edilmedi.",
      "Ölçüm GIC EOI sonrasında ve scheduler preemption öncesindeki gerçek PPI27 IRQ yoluna taşındı; capacity=32, SERVICE_BUDGET_PER_IRQ=1 veya 320000000 ns SLA gevşetilmedi.",
      "ipc_deadline_clock_sla kaynak/model kapısı 9/9 PASS: zero/mismatched frequency, arithmetic overflow, counter regression, tick-span ve SLA aşımı fail-closed; counter→nanosecond dönüşümü u128 ara değer ve ceil yuvarlama kullanır.",
      "ABI UNCHANGED_V1_3: yeni syscall veya error yok; S144–S149 CALL/RECV/notification runtime yolları korunur.",
      "QEMU clock: CNTVCT_EL0, CNTFRQ=62500000, TICK_HZ=100, PERIOD_COUNTS=625000 ve QUANTUM_NS_CEIL=10000000.",
      "QEMU full-table ölçümü: CAPACITY=32, DISTINCT_SERVICE_IRQS=32, FIRST_TICK=141, LAST_TICK=172, TICK_SPAN=31, COUNTER_SPAN=19379062, MEASURED_NS_CEIL=310064992 ≤ FULL_TABLE_SLA_NS=320000000 ve SLA=PASS.",
      "REGISTERED=32, TIMED_OUT=32, ACTIVE_FINAL=0, GLOBAL_ACTIVE=0→0, ALLOCATION_FREE=YES, CPU0_ONLY=YES ve PHYSICAL_DEVICE_OPS=0.",
      "S129–S150 exact focused envanteri 39 binary / 242/242 PASS; ortak ABI/IPC kapısı 11 binary / 104/104 PASS.",
      "AArch64 board-qemu, board-rpi4, board-rpi5 ve board-rpi5+smp applicability 4/4 PASS.",
      "make verify-qemu PASS: strict ELF W^X 31/31, başarılı IPC reply 20/20, KERNEL_FAULTS=0 ve EXECUTOR=PASS.",
      "Sekiz saniyelik QEMU log'u 551194 B / SHA-256 8b2a1b266efb28b20507d41a25fd43cea2303d6267d56c139c98ea135e1172bb.",
      "Ham workspace 111 result group içinde 717 PASS + exact yedi tarihsel frozen G8h assertion FAIL verdi; log 118810 B / SHA-256 963e8af623c9d441431de88ecb1ffba28d9d92b15a3cb330122471b706883f09. Yalnız bu yedi exact dışlandığında 111 group / 717/717 PASS; full GREEN iddia edilmez.",
      "S124 fiziksel kanıtı tarihsel PASS olarak korunur: raw 20270 B / SHA-256 ee97d070741d5f7acd8ea7985d00ea54086e2fbaea54e1cc94619dd640bb4158, BOOT8H=1, validators 12/12, milestones 60/60 ve ARCHIVE/PROMOTION=PASS.",
      "Fiziksel runbook S124'te tamamlandı: Gücü kapat → SD kartı Pi'den çıkar → SD kartı Mac'e tak → yetkili write/verify/read-back → SD kartı Mac'ten güvenli çıkar → SD kartı güçsüz Pi'ye tak → UART capture pre-arm ve exact identity → Güç ver. S150'de physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S150=NO.",
      "PASS-dışı audit S150 dahil 149 kayıttır: 21 Kısmi + 7 Başarısız + 7 Gözlem = 35 literal tarihsel PASS-dışı; 47 Passed + 58 Verified + 9 Fixed = 114 kapalı/yeşil. S111–S112 ve S125–S150 toplam 28 dar PASS/umbrella-partial kaydı; kalan gerçek ileri çalışma 15 ana kabul bloğudur.",
      "Planlama tahmini S150 + (15 × 8–10 sıra) + 40–60 risk sırası = S310–360; risk-paylı merkez ≈S335. Taahhüt veya fiziksel PASS değildir ve tek başına yeni S151 işlemi oluşturmaz.",
      "Kalıcı kapsam: `docs/K2-S150-IPC-Deadline-Clock-SLA-Proof.md`.",
    ],
    commands: [
      "cargo test -p aselsan_microkernel_simulation --test ipc_deadline_clock_sla -- --test-threads=1",
      "cargo test -p aselsan_microkernel_simulation [39 exact focused test binary] -- --test-threads=1",
      "cargo test -p aselsan_microkernel_simulation [11 exact ABI/IPC test binary] -- --test-threads=1",
      "cargo check -p aselsan_kernel --target aarch64-unknown-none [board-qemu, board-rpi4, board-rpi5, board-rpi5+smp]",
      "make verify-qemu",
      "cargo test --workspace --no-fail-fast",
      "cargo test --workspace -- --test-threads=1 [seven exact historical --skip filters]",
      "cargo fmt --all -- --check",
    ],
    terminalSessions: [
      {
        id: "s150-red-missing-clock-authority",
        title: "Deadline clock authority: ilk fail-closed kaynak RED'i",
        commandLines: [
          "cargo test -p aselsan_microkernel_simulation --test ipc_deadline_clock_sla -- --test-threads=1",
        ],
        outputLines: [
          "error: unresolved ipc_deadline_clock module / production clock authority absent",
          "compile failed · no partial PASS accepted",
        ],
        exitCode: 101,
        outputMode: "selected",
      },
      {
        id: "s150-red-controller-preemption",
        title: "İlk QEMU: controller preemption ayrı IRQ gözlemini kırdı",
        commandLines: ["make verify-qemu"],
        outputLines: [
          "panic: S150 missed a distinct service IRQ",
          "Kern-A/Kern-B scheduler preemption observed · PASS not claimed",
          "fixture moved into real PPI27 IRQ path before scheduler preemption; SLA unchanged",
        ],
        exitCode: 2,
        outputMode: "selected",
      },
      {
        id: "s150-green-clock-sla-qemu",
        title: "Counter-kalibre 32 ayrı IRQ ve 320 ms SLA",
        commandLines: [
          "cargo test -p aselsan_microkernel_simulation --test ipc_deadline_clock_sla -- --test-threads=1",
          "cargo test -p aselsan_microkernel_simulation [39 exact focused test binary] -- --test-threads=1",
          "cargo test -p aselsan_microkernel_simulation [11 exact ABI/IPC test binary] -- --test-threads=1",
          "cargo check -p aselsan_kernel --target aarch64-unknown-none [4 profiles]",
          "make verify-qemu",
        ],
        outputLines: [
          "ipc_deadline_clock_sla: 9/9 PASS",
          "combined exact focused inventory: 242/242 PASS · 39 binaries",
          "focused ABI/IPC: 104/104 PASS · 11 binaries · AArch64 compile profiles: 4/4 PASS",
          "[K2-S150] ABI=UNCHANGED_V1_3 CLOCK=CNTVCT_EL0 CNTFRQ=62500000 TICK_HZ=100 PERIOD_COUNTS=625000 QUANTUM_NS_CEIL=10000000 CAPACITY=32 SERVICE_BUDGET_PER_IRQ=1 DISTINCT_SERVICE_IRQS=32 FIRST_TICK=141 LAST_TICK=172 TICK_SPAN=31 COUNTER_SPAN=19379062 MEASURED_NS_CEIL=310064992 FULL_TABLE_SLA_NS=320000000 SLA=PASS REGISTERED=32 TIMED_OUT=32 ACTIVE_FINAL=0 GLOBAL_ACTIVE=0->0 ALLOCATION_FREE=YES CPU0_ONLY=YES PHYSICAL_DEVICE_OPS=0 KERNEL_FAULTS=0 EXECUTOR=PASS",
          "QEMU smoke PASS: strict ELF W^X 31/31 · IPC reply 20/20 · S150 PASS",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "s150-workspace-independent-history-red",
        title: "Tam workspace: exact yedi tarihsel G8h assertion kırmızısı",
        commandLines: [
          "cargo test --workspace --no-fail-fast",
          "cargo test --workspace -- --test-threads=1 [seven exact historical --skip filters]",
        ],
        outputLines: [
          "full workspace: 111 result groups · 717 PASS · exactly 7 historical frozen G8h assertions FAIL",
          "excluding only those seven exact assertion names: 111 result groups · 717/717 PASS",
          "historical assertions were not relaxed · full-workspace GREEN is not claimed",
        ],
        exitCode: 101,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S150 dar deadline clock/SLA kabulünü yalnız gerçek IRQ yolundaki final ölçümle PASS eder. İlk derleme ve ilk QEMU koşuları RED olarak korunur; QEMU/host kanıtı Generic SMP veya fiziksel Raspberry Pi wall-clock PASS'i değildir.",
    limitations: [
      "Generic SMP cross-CPU timer/signal/revoke/wake/IPI/TLB/reaper arbitration matrisi kapanmadı.",
      "Production workload sizing, uzun saturation soak ve fiziksel RPi latency ölçümü açık kaldı.",
      "Cross-subsystem rollback, capability transferi, shared-memory loan ve ortak frame/cap/endpoint/ASID reconciliation kapsam dışıdır.",
      "Tam workspace exact yedi tarihsel frozen G8h identity/closure assertion'ı nedeniyle GREEN değildir; yalnız yedi exact assertion dışlandığında 717/717 PASS'tir.",
      "Fiziksel/device operations=0; RUNBOOK_EXECUTED_IN_S150=NO.",
    ],
  },
snippet sha256: ea343d427f60file sha256: 9726dbf00f84
Focused test komutu
cargo test -p aselsan_microkernel_simulation --test ipc_deadline_clock_sla -- --test-threads=1
proof: docs/K2-S150-IPC-Deadline-Clock-SLA-Proof.md
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 3050638b71a684d8f8f947a8a6faa237a17fa8db5dc0db04fb207b668b462af9