S139 · SOURCE-BOUND GATE EVIDENCE
K1/MEM0–MEM2/K2: çoklu OOM supervisor taşıması ve yarış kuralı
Operations --test hedefi → focused test içindeki include_str!/#[path] bağı → kaynak kesiti Bu sayfa yalnız S139 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.
S139Focused kod testiOperations id exactsource SHA exacttest target exact
operation: k1-mem0-mem1-mem2-k2-multi-event-oom-supervisor-transport-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–L67
kernel/src/main.rs::main.rs
//! ASELSAN Milli Telefon — gerçek aarch64 microkernel.
//!
//! M0 : bare-metal boot + PL011 UART
//! M1.1 : Exception Vector Table (VBAR_EL1) + trampolines
//! M1.2 : EC decode + BRK/SVC recover + panic on bad cases
//! M1.3 : GICv2 + ARM Virtual Timer (CNTV) using CVAL (low drift)
//! M1.4 : 100 Hz periodic tick + per-second drift measurement + irq_lock!
#![no_std]
#![no_main]
// The typed S401+ fail-closed error chain is intentionally deep. Production
// AArch64 builds need enough query headroom to lay it out while compiling the
// post-S430 acceptance callsites.
#![recursion_limit = "256"]
extern crate alloc;
use core::panic::PanicInfo;
mod arch;
// Hands-free altyapısı (radyo değişkeni DEĞİL): PM watchdog + UART 'R'.
#[cfg(all(feature = "board-rpi5", feature = "rpi5-auto-reset"))]
mod auto_reset;
mod board; // M8.1 — Board/Platform abstraction (QEMU vs RPi4 vs future SoC)
mod driver; // M8.1.2 — Mailbox, UART driver'ları vs. (RPi4 için kritik)
mod dt; // M9.1 — Device Tree Blob parser (RPi5 + telefon SoC hazırlığı)
mod elf; // M8 — ELF64 Loader (başlangıç)
#[allow(dead_code)]
mod elf_plan; // K1 — allocation-free validator + production ELF page plan
#[cfg(feature = "board-rpi5")]
mod g7c_contract;
#[cfg(feature = "board-rpi5")]
mod g7d_contract;
#[cfg(feature = "board-rpi5")]
mod g8_contract;
#[cfg(feature = "board-rpi5")]
mod g8b_contract;
#[cfg(feature = "board-rpi5")]
mod g8c_contract;
#[cfg(feature = "board-rpi5")]
mod g8d_contract;
#[cfg(feature = "board-rpi5")]
mod g8e_contract;
#[cfg(feature = "board-rpi5")]
mod g8f_contract;
#[cfg(feature = "board-rpi5")]
mod g8g_contract;
#[cfg(feature = "board-rpi5")]
mod g8h_contract;
#[cfg(feature = "board-rpi5")]
mod g8l_arch_execution_contract;
#[cfg(feature = "board-rpi5")]
mod g8l_authority_contract;
#[cfg(feature = "board-rpi5")]
mod g8l_irq_tlbi_wiring;
#[cfg(feature = "board-rpi5")]
mod g8l_runtime_contract;
#[cfg(feature = "board-rpi5")]
mod g8l_scheduler_admission;
#[cfg(feature = "board-rpi5")]
mod g8l_target_aarch64_dispatch;
#[cfg(feature = "board-rpi5")]
mod g8l_target_dispatch_admission;
#[cfg(feature = "board-rpi5")]
mod g8l_target_dispatch_callsite;
#[cfg(feature = "board-rpi5")]
mod g8l_target_dispatch_context_switch;snippet sha256: bb4040f314a8…file sha256: 3348a0639f2c…
02 · Doğrulayan test kodu
Operations komutuna bağlı focused test
tam Rust öğesiL133–L153
simulation/tests/runtime_oom_multi_event_transport.rs::s139_wires_the_broker_to_eight_real_calls_and_a_strict_el0_fifo_drain
#[test]
fn s139_wires_the_broker_to_eight_real_calls_and_a_strict_el0_fifo_drain() {
let mm = source("kernel/src/mm/mod.rs");
let main = source("kernel/src/main.rs");
let supervisor = source("userspace/oom_batch_supervisor/src/main.rs");
let binaries = source("userspace/mod.rs");
let makefile = source("Makefile");
assert!(mm.contains("pub mod runtime_oom_transport;"));
assert!(main.contains("qemu_s139_multi_event_caller"));
assert!(main.contains("TRANSPORT_OVERFLOW=QUEUE_FULL"));
assert!(main.contains("ENDPOINT_OVERFLOW=QUEUE_FULL"));
assert!(main.contains("ACK_AT_DEADLINE=ACK_WINS"));
assert!(main.contains("TIMEOUT_AFTER_DEADLINE=TIMEOUT_WINS"));
assert!(main.contains("LATE_ACK=STALE"));
assert!(supervisor.contains("[K1-MEM2-S139] STRICT EL0 FIFO DRAIN=8/8"));
assert!(supervisor.contains("cmp x20, #8"));
assert!(binaries.contains("OOM_BATCH_SUPERVISOR_BINARY"));
assert!(makefile.contains("userspace-oom-batch-supervisor"));
}snippet sha256: e5369f1c2c7a…file sha256: edfadc0505ad…
03 · Kapı kimlik kaydı
Operations sıra, kimlik ve başlık bağı
tam Operations kaydıL25426–L25548
website/src/lib/operations.ts::k1-mem0-mem1-mem2-k2-multi-event-oom-supervisor-transport-partial
{
id: "k1-mem0-mem1-mem2-k2-multi-event-oom-supervisor-transport-partial",
date: "2026-08-24",
sequence: 139,
status: "passed",
umbrella_status: "partial",
title: "K1/MEM0–MEM2/K2: çoklu OOM supervisor taşıması ve yarış kuralı",
summary:
"S139, S138 sonrasındaki delivery sınırına allocation-free capacity-8 RuntimeOomSupervisorTransport ekler. Sekiz immutable projection eşzamanlı in-flight olur; dokuzuncu enqueue broker snapshot'ını değiştirmeden QueueFull döner. Dokuz ayrı production kernel caller'ın ilk sekizi gerçek endpoint CALL'unda BlockedOnIpc olur, dokuzuncusu gerçek endpoint QueueFull alır. Ayrı strict RuntimePmm oom_batch_supervisor ordinary SYS_IPC_RECV/SYS_IPC_REPLY ile 1..8 FIFO'yu boşaltır ve sekiz one-shot reply verir. Exact ACK deadline tick'inde kazanır; timeout yalnız deadline sonrasında kazanır, aynı event taze delivery epoch ile retry edilir ve eski late ACK StaleLease olur. Runtime batch sekiz bağımsız victim iddia etmez: tek authoritative S138 completion event'inin sekiz transport projection'ıdır. Crash/restart recovery S140, genel IPC syscall timeout wiring, signed thresholds ve Generic SMP açık; K1/MEM0–MEM2/K2 PARTIAL.",
evidence: [
"RED source gate yeni modül yokken 0/7; GREEN `runtime_oom_multi_event_transport` 7/7 PASS.",
"İlk gerçek QEMU koşusu derived caller SEND grant generation'ını root endpoint generation'ına yanlış eşitledi; S139 caller SEND authority panic'i PASS üretmeden durdu. Non-zero canlı derived generation kullanıldı; root/grant/CNode/registry doğrulamaları korunur.",
"İkinci QEMU koşusunda panic yoktu ancak priority-4 strict supervisor sürekli Ready priority-0 task'lar arkasında çalışamadı; smoke yalnız tarihsel yedi reply gördü, S139 final marker'ı çıkmadı ve koşuyu reddetti.",
"Nihai IRQ-masked publication dokuz equal-priority caller'ı önce, strict supervisor'ı sonra yayımlar; task-id tie-break endpoint'i deterministic 8/8 doldurur ve hiçbir queue/timeout kapısı gevşetilmez.",
"S129–S139 exact `cargo test -- --list` envanteri 28 binary / 147 testtir; 147/147 PASS.",
"AArch64 board-qemu, board-rpi4, board-rpi5 ve board-rpi5+smp compile applicability 4/4 PASS.",
"QEMU controller/callers/supervisor=32/34..42/43; supervisor domain=1330597179, endpoint=26, capacity=8. BATCH=8/8, FIFO=1..8, REAL_KERNEL_CALLS/KERNEL_CALL_BLOCKED/REAL_EL0_RECV_REPLY/REPLY_ONESHOT=8/8.",
"Broker ve gerçek endpoint capacity+1'i mutasyonsuz QueueFull reddetti. ACK_AT_DEADLINE=ACK_WINS, TIMEOUT_AFTER_DEADLINE=TIMEOUT_WINS, LATE_ACK=STALE, RETRY=1, BROKER_ACK=10, BROKER_TIMEOUT=1 ve final BROKER_DRAINED=YES.",
"Strict supervisor quota 5→0; free 6139→6134→6139, active 5→10→5, SUPERVISOR_RECLAIM=5, OWNER_EP_CLEANUP=1, KERNEL_DIRECT_ACK=NO ve EXECUTOR=PASS.",
"QEMU strict ELF W^X 13/13, IPC reply 15/15, final RuntimePmm 6144→6144 / active 0→0 ve scheduler SEC5 birlikte PASS.",
"Tam workspace yalnız bağımsız frozen S96 exceptions.S SHA-256 uyuşmazlığında durdu: observed f7b47672…04fd, expected c0eed3e2…cb89; full GREEN iddia edilmedi.",
"Fiziksel operatör runbook'u görünürdür: Gücü kapat → SD kartı Pi'den çıkar → SD kartı Mac'e tak → yetkili yazma/doğrulama → SD kartı Mac'ten güvenli çıkar → SD kartı güçsüz Pi'ye tak → UART pre-arm/identity → Güç ver.",
"Runbook S139'da uygulanmadı: physical/device operations=0, S124 archive/promotion STOP, son fiziksel boot/runtime PASS S92 BOOT8G ve son storage/media PASS S119.",
"Güncel planlama tahmini S139 bazında R2 bitiş aralığı S323–379, risk-paylı merkez ≈S356'dır; taahhüt veya fiziksel PASS değildir.",
"Web kapıları 235/235 test, lint, TypeScript ve statik 23/23 route PASS verdi.",
"İlk S139 production yayını 9f432653.aselsan-microkernel.pages.dev üzerinde tamamlandı; özel alan adı cache-bust ile byte-exact doğrulandı: operations 4725593 B / d381e1cd…d2bd, timeline 508948 B / 36805450…0b83, yol-haritasi 509051 B / 690435a2…de16.",
"Kalıcı kapsam: `docs/K1-S139-Multi-Event-OOM-Supervisor-Transport-Proof.md`.",
],
commands: [
"cargo test -p aselsan_microkernel_simulation --test runtime_oom_multi_event_transport -- --test-threads=1",
"cargo test -p aselsan_microkernel_simulation [28 exact focused 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 -- --test-threads=1",
"cd website && npm test && npm run lint && npx tsc --noEmit && npm run build",
"cd website && npx wrangler pages deploy out --project-name=aselsan-microkernel --branch=main --commit-dirty=true",
],
terminalSessions: [
{
id: "s139-red-source-before-multi-event-broker",
title: "Capacity-8 broker kaynak kapısı: implementation öncesi RED",
commandLines: [
"cargo test -p aselsan_microkernel_simulation --test runtime_oom_multi_event_transport -- --test-threads=1",
],
outputLines: [
"runtime_oom_multi_event_transport: 0/7 PASS before implementation",
"compile error: kernel/src/mm/runtime_oom_transport.rs missing",
],
exitCode: 101,
outputMode: "selected",
},
{
id: "s139-fail-closed-derived-send-generation",
title: "İlk QEMU: derived SEND generation yanlış eşitliği reddedildi",
commandLines: ["make verify-qemu"],
outputLines: [
"panic: S139 caller SEND authority",
"QEMU smoke: FAIL-CLOSED · no S139 PASS",
],
exitCode: 2,
outputMode: "selected",
},
{
id: "s139-fail-closed-supervisor-starvation",
title: "İkinci QEMU: strict supervisor starvation marker'ı kapattı",
commandLines: ["make verify-qemu"],
outputLines: [
"panic absent, historical IPC reply count remained 7",
"S139 strict FIFO/final marker absent",
"QEMU smoke: FAIL-CLOSED · no S139 PASS",
],
exitCode: 2,
outputMode: "selected",
},
{
id: "s139-green-focused-aarch64-qemu",
title:
"Çoklu transport, gerçek endpoint taşması, yarış, AArch64 ve QEMU",
commandLines: [
"cargo test -p aselsan_microkernel_simulation [28 exact focused test binary] -- --test-threads=1",
"cargo check -p aselsan_kernel --target aarch64-unknown-none [4 profiles]",
"make verify-qemu",
],
outputLines: [
"runtime_oom_multi_event_transport: 7/7 PASS",
"combined exact focused inventory: 147/147 PASS · 28 binaries",
"AArch64 compile profiles: 4/4 PASS",
"website: 235/235 tests · lint PASS · TypeScript PASS · static routes 23/23",
"Cloudflare Pages initial production deployment: 9f432653.aselsan-microkernel.pages.dev",
"custom domain byte-exact: operations/timeline/yol-haritasi 3/3 PASS",
"[K1-MEM2-S139] supervisor strict spawn PASS id=43 pages=2 domain=1330597179 endpoint=26 owner=32 BOUNDED=8 BATCH=8 INITIAL_X0=YES W^X=YES",
"[K1-MEM2-S139] STRICT EL0 FIFO DRAIN=8/8",
"[K1-MEM2-S139] source_event=1 endpoint=26 supervisor=43 supervisor_domain=1330597179 BATCH=8/8 TRANSPORT_OVERFLOW=QUEUE_FULL ENDPOINT_OVERFLOW=QUEUE_FULL FIFO=1..8 REAL_KERNEL_CALLS=8 KERNEL_CALL_BLOCKED=8 REAL_EL0_RECV_REPLY=8/8 REPLY_ONESHOT=8/8 ACK_AT_DEADLINE=ACK_WINS TIMEOUT_AFTER_DEADLINE=TIMEOUT_WINS LATE_ACK=STALE RETRY=1 BROKER_ACK=10 BROKER_TIMEOUT=1 BROKER_DRAINED=YES SUPERVISOR_RECLAIM=5 OWNER_EP_CLEANUP=1 free=6139->6134->6139 active=5->10->5 KERNEL_DIRECT_ACK=NO EXECUTOR=PASS",
"QEMU smoke PASS: strict ELF W^X 13/13 · IPC reply 15/15 · S139 PASS",
],
exitCode: 0,
outputMode: "selected",
},
{
id: "s139-workspace-independent-history-red",
title: "Tam workspace: S139 dışı frozen S96 identity kırmızısı",
commandLines: ["cargo test --workspace -- --test-threads=1"],
outputLines: [
"rpi5_g8h_integration_source::wiring_does_not_mutate_timer_gic_boot_or_expand_runtime_scope: FAILED",
"S96 exceptions.S SHA-256: observed f7b47672...04fd, frozen expected c0eed3e2...cb89",
"full-workspace GREEN is not claimed",
],
exitCode: 101,
outputMode: "selected",
},
],
terminalSessionsNote:
"S139 tek authoritative completion event'ini sekiz transport projection'ıyla gerçek capacity-8 endpoint üzerinde taşır; sekiz concurrent blocked CALL, dokuzuncu QueueFull, strict EL0 FIFO drain ve ACK/timeout yarış kuralı kanıtlıdır. Sekiz independent victim iddiası yoktur; fiziksel runbook görünürdür ve uygulanmadı.",
limitations: [
"Runtime batch tek authoritative S138 source event'in sekiz distinct sequence/fingerprint projection'ıdır; sekiz independent concurrent victim/effect authority'si değildir.",
"Deadline/race broker ve QEMU acceptance düzeyinde gerçektir; genel IPC syscall blocking/timer cancellation yoluna bağlı değildir.",
"Supervisor crash/restart ve in-flight event recovery S140'a açıktır.",
"Product pressure eşikleri ölçülmüş veya imzalanmış değildir.",
"CPU0-only scheduler kanıtıdır; cross-CPU stop, migration-safe runqueue, TLB shootdown ve SMP reaper açıktır.",
"Capability transfer, shared-memory loan ve bütün legacy/kernel kaynak üreticilerinin ortak reconciliation'ı açıktır.",
"K1, MEM0, MEM1, MEM2 ve K2 COMPLETE değildir; S124 fiziksel archive/promotion STOP kalır.",
],
},snippet sha256: 56d8ce121d38…file sha256: 9726dbf00f84…
Focused test komutu
cargo test -p aselsan_microkernel_simulation --test runtime_oom_multi_event_transport -- --test-threads=1proof: docs/K1-S139-Multi-Event-OOM-Supervisor-Transport-Proof.md
Registry schema v5 · generator
website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06