ASELSANMicrokernel
S135 · SOURCE-BOUND GATE EVIDENCE

K1/MEM1–MEM2/K2: iki strict EL0 IPC peer teardown

Operations --test hedefi → focused test içindeki include_str!/#[path] bağı → kaynak kesiti Bu sayfa yalnız S135 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S135Focused kod testiOperations id exactsource SHA exacttest target exact

operation: k1-mem1-mem2-k2-strict-el0-peers-oom-teardown-partial

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

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

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

tam Rust öğesiL4302–L4320
kernel/src/task/scheduler.rs::qemu_s135_strict_peers_cancellation_state

/// S135 uses the same post-cancellation graph invariant, but both peers are
/// independently published RuntimePmm ELFs and must also be reclaimed.
#[cfg(feature = "board-qemu")]
pub(crate) unsafe fn qemu_s135_strict_peers_cancellation_state(
    caller_task: u64,
    responder_task: u64,
    endpoint_owner: u64,
    target_endpoint: crate::ui::capability::CapId,
    reply_cap_id: crate::ui::capability::CapId,
) -> bool {
    qemu_strict_peers_cancellation_state(
        caller_task,
        responder_task,
        endpoint_owner,
        target_endpoint,
        reply_cap_id,
    )
}
snippet sha256: aedad38bcd8afile sha256: 838dd474448c
02 · Doğrulayan test kodu

Operations komutuna bağlı focused test

tam Rust öğesiL90–L112
simulation/tests/runtime_oom_el0_responder_teardown.rs::observer_and_later_stack_require_exact_responder_bound_cancellation

#[test]
fn observer_and_later_stack_require_exact_responder_bound_cancellation() {
    let main = source("kernel/src/main.rs");
    let scheduler = source("kernel/src/task/scheduler.rs");

    let graph = function_from(
        &scheduler,
        "pub(crate) unsafe fn qemu_observe_delivered_ipc_syscalls",
        "pub(crate) unsafe fn qemu_s134_responder_cancellation_state",
    );
    assert!(graph.contains("snapshot.responder_task == Some(responder_task)"));
    assert!(graph.contains("TaskState::BlockedOnIpc"));
    assert!(graph.contains("ENDPOINT_SEND"));
    assert!(graph.contains("ENDPOINT_RECV"));
    assert!(graph.contains("responder.saved_user_gprs[7] == reply_cap_id"));

    assert!(main.contains("OWNED_EP=0 DRAINED_CALLS=0 RESPONDER_CALLS=1"));
    assert!(main.contains("EL0_CALL_RETURN=INVALID_CAPABILITY"));
    assert!(main.contains("EL0_RECV=DELIVERED GRAPH=ABSENT OWNER_EP_CLEANUP=1"));
    assert!(main.contains("qemu_s134_ipc_witnesses_observed"));
    assert!(main.contains("teardown_task_ipc_lifecycle(state.supervisor_task)"));
}
snippet sha256: 7a1e6e1f32bcfile sha256: 1892505d6a95
03 · Kapı kimlik kaydı

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

tam Operations kaydıL25902–L25999
website/src/lib/operations.ts::k1-mem1-mem2-k2-strict-el0-peers-oom-teardown-partial
  {
    id: "k1-mem1-mem2-k2-strict-el0-peers-oom-teardown-partial",
    date: "2026-08-23",
    sequence: 135,
    status: "passed",
    umbrella_status: "partial",
    title: "K1/MEM1–MEM2/K2: iki strict EL0 IPC peer teardown",
    summary:
      "S135, S134'te kalan legacy-root caller sınırını kaldırır. Caller ve responder artık ayrı standalone strict RuntimePmm ELF'tir; ikisi de publication öncesi saved x0 endpoint argümanı ve typed SEND/RECV grant'i alır; ordinary SYS_IPC_CALL caller'ı production reply/rendezvous grafiğinde park eder, ordinary SYS_IPC_RECV responder'a teslim eder. Read-only observer exact graph'tan sonra yalnız responder için taze OOM ticket'ı arm eder. Current responder teardown exact bir responder-bound reply'ı iptal edip strict caller'ı InvalidCapability ile döndürür; responder later-stack reaper, caller ise bounded handoff sonrası normal SYS_EXIT/reaper ile kendi 5 frame'ini bırakır. Domain quota'ları 0/0, free 6129→6134→6139, S135 active-allocation baseline 15→5, final smoke baseline 0; BOTH_STRICT=YES, GRAPH=ABSENT, OWNER_EP_CLEANUP=1. Gerçek supervisor endpoint transportu, production pressure trigger ve Generic SMP açık; K1/MEM0–MEM2/K2 PARTIAL.",
    evidence: [
      "Fail-closed build: standalone crate workspace kökünden manifest ile çağrıldığında crate-local AArch64 config yüklenmedi ve linker ADRP/GOT relocation'ını reddetti; production crate çalışma dizinindeki iki temiz release build PASS.",
      "Fail-closed runtime 1: caller ticket completion'dan önce normal exit/reclaim yaptığı için supervisor TeardownIncomplete panic etti; PASS üretilmedi.",
      "Fail-closed runtime 2: tek SYS_YIELD caller'ı yeniden seçebildi ve aynı panic'i üretti; bounded sekiz yield responder-only reconciliation'ı caller'ın unrelated normal reclaim'inden önce kesinleştirdi.",
      "GREEN `runtime_oom_el0_strict_peers_teardown` 5/5; S128–S135 scheduler/IPC/ASID/kmap/lifecycle birleşik focused matrisi 124/124 (24 grup) PASS.",
      "İki peer da standalone strict RuntimePmm ELF, independent domain ve publication öncesi initial x0 kullanır; graph fixture yoktur, ordinary SYS_IPC_CALL/SYS_IPC_RECV ve user-copy yolları çalışır.",
      "QEMU graph: caller/responder/owner/observer=26/27/25/28, domains=1330597174/1330597175, endpoint/reply=19/20; BOTH_STRICT/EL0_CALL/EL0_RECV/USER_COPY/CALLER_BLOCKED/RESPONDER_READY/BOUND/ARMED=YES.",
      "Responder exact bir bound reply'ı iptal etti; strict caller InvalidCapability marker'ı verdi ve normal reaper ile 5 frame bıraktı: OWNED_EP/DRAINED_CALLS/RESPONDER_CALLS=0/0/1 (RESPONDER_CALLS=1), STRICT_CALLER_RECLAIM=5.",
      "QEMU iki domain frame quota'sı 0/0, free 6129→6134→6139, ACTIVE_ALLOCATIONS=15→5 ve GLOBAL_BASELINE=PASS; bu 5 canlı allocation hello-stress'e aittir ve final smoke 6144→6144 / 0→0'a döner.",
      "QEMU strict ELF W^X 9/9; S130–S134 OOM regresyonları, final RuntimePmm 6144→6144 / active allocation 0→0, EL0 return x4096, IPC reply 3/3 ve scheduler SEC5 birlikte PASS.",
      "AArch64 board-qemu, board-rpi4, board-rpi5 ve board-rpi5+smp compile applicability 4/4 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.",
      "Web 231/231, lint, TypeScript ve statik 23/23 PASS; ilk S135 production yayını b698d366 kimliğiyle tamamlandı ve özel alan operations/timeline/yol-haritasi rotaları local output ile byte-exact eşleşti.",
      "Bu S135 kabulünde güç verme/kapatma, SD kartı Pi'den çıkarma/takma, SD kartı Mac'e takma, disk yazma, UART açma veya başka fiziksel/device işlemi yapılmadı.",
      "Kalıcı kapsam ve açık S136 supervisor-transport sınırı: `docs/K1-S135-Strict-EL0-IPC-Peers-Teardown-Proof.md`.",
    ],
    commands: [
      "cargo test -p aselsan_microkernel_simulation --test runtime_oom_el0_strict_peers_teardown -- --test-threads=1",
      "cargo test -p aselsan_microkernel_simulation --test aarch64_asid_encoding --test ipc_queue_source --test kernel_kmap_source --test memory_accounting --test memory_pressure --test runtime_allocation_token --test runtime_boot_authority --test runtime_boot_authority_fail_closed --test runtime_boot_authority_no_alloc --test runtime_domain_quota --test runtime_elf_reclaim_source --test runtime_memory_reconciliation --test runtime_oom_effect --test runtime_oom_scheduler_executor --test runtime_oom_current_deferred --test runtime_oom_live_ipc_teardown --test runtime_oom_el0_ipc_teardown --test runtime_oom_el0_responder_teardown --test runtime_oom_el0_strict_peers_teardown --test runtime_pressure_authority --test task_id_allocator --test task_lifecycle_source --test task_publication_source --test task_spawn_asid_source -- --test-threads=1",
      "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-qemu",
      "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi4",
      "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi5",
      "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi5,smp",
      "make verify-qemu",
      "cargo test --workspace -- --test-threads=1",
    ],
    terminalSessions: [
      {
        id: "s135-green-focused-two-strict-peers",
        title: "İki strict EL0 peer ve birleşik lifecycle kapıları",
        commandLines: [
          "cargo test -p aselsan_microkernel_simulation --test runtime_oom_el0_strict_peers_teardown -- --test-threads=1",
          "cargo test -p aselsan_microkernel_simulation [24 focused test binary] -- --test-threads=1",
        ],
        outputLines: [
          "runtime_oom_el0_strict_peers_teardown: 5/5 PASS",
          "combined focused matrix: 124/124 PASS · 24 groups",
          "graph injection: ABSENT · standalone strict caller + responder: PASS",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "s135-aarch64-qemu-two-strict-peers",
        title: "Dört AArch64 profil ve iki strict EL0 peer QEMU teardown",
        commandLines: [
          "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-qemu",
          "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi4",
          "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi5",
          "cargo check -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi5,smp",
          "make verify-qemu",
        ],
        outputLines: [
          "AArch64 compile profiles: 4/4 PASS",
          "[K1-MEM2-S135] caller strict spawn PASS id=26 pages=2 domain=1330597174 endpoint=19 INITIAL_X0=YES W^X=YES",
          "[K1-MEM2-S135] responder strict spawn PASS id=27 pages=2 domain=1330597175 endpoint=19 INITIAL_X0=YES W^X=YES",
          "[K1-MEM2-S135] delivered graph PASS caller=26 responder=27 owner=25 observer=28 endpoint=19 reply=20 BOTH_STRICT=YES EL0_CALL=YES EL0_RECV=YES USER_COPY=YES CALLER_BLOCKED=YES RESPONDER_READY=YES BOUND=YES ARMED=YES",
          "[K1-MEM2-S135] EL0 SYS_IPC_RECV DELIVERED=YES OOM_TRIGGER=YES",
          "[K1-MEM2-S135] STRICT EL0 SYS_IPC_CALL RETURN=INVALID_CAPABILITY",
          "[K1-MEM2-S135] responder=27 caller=26 owner=25 responder_domain=1330597175 caller_domain=1330597174 endpoint=19 reply=20 event=1 expected=5 observed=0 free=6129->6134->6139 OWNED_EP=0 DRAINED_CALLS=0 RESPONDER_CALLS=1 STRICT_CALLER_RECLAIM=5 CALLER_DOMAIN_FRAMES=0 RESPONDER_DOMAIN_FRAMES=0 ACTIVE_ALLOCATIONS=15->5 GLOBAL_BASELINE=PASS EL0_CALL_RETURN=INVALID_CAPABILITY EL0_RECV=DELIVERED BOTH_STRICT=YES GRAPH=ABSENT OWNER_EP_CLEANUP=1 CURRENT=YES LATER_STACK=YES ACK=YES REARM=2 LEVEL=NORMAL EXECUTOR=PASS",
          "QEMU smoke PASS: strict ELF W^X 9/9 + S130/S131/S132/S133/S134/S135 OOM runtime + regressions",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "s135-workspace-independent-history-red",
        title: "Tam workspace: S135 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:
      "S135 iki standalone strict RuntimePmm ELF peer'ın ordinary CALL/RECV, responder-bound cancellation, strict caller normal reclaim ve independently owned endpoint cleanup yolunu gerçek scheduler state'i üzerinde doğrular; fiziksel veya device işlemi yapılmadı.",
    limitations: [
      "Endpoint owner, observer ve OOM supervisor kernel task'tır; completion eventinin gerçek bounded endpoint transportu ve strict EL0 consumer'ı bağlı değildir.",
      "Successful SYS_WRITE tetikleyicisi production pressure daemon/timer yolu değildir.",
      "Carrier tek in-flight slotudur; multi-event queue/backpressure, timeout/race matrisi ve supervisor crash recovery yoktur.",
      "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: 5001060f6d8efile sha256: 9726dbf00f84
Focused test komutu
cargo test -p aselsan_microkernel_simulation --test aarch64_asid_encoding --test ipc_queue_source --test kernel_kmap_source --test memory_accounting --test memory_pressure --test runtime_allocation_token --test runtime_boot_authority --test runtime_boot_authority_fail_closed --test runtime_boot_authority_no_alloc --test runtime_domain_quota --test runtime_elf_reclaim_source --test runtime_memory_reconciliation --test runtime_oom_effect --test runtime_oom_scheduler_executor --test runtime_oom_current_deferred --test runtime_oom_live_ipc_teardown --test runtime_oom_el0_ipc_teardown --test runtime_oom_el0_responder_teardown --test runtime_oom_el0_strict_peers_teardown --test runtime_pressure_authority --test task_id_allocator --test task_lifecycle_source --test task_publication_source --test task_spawn_asid_source -- --test-threads=1
proof: docs/K1-S135-Strict-EL0-IPC-Peers-Teardown-Proof.md
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06