ASELSANMicrokernel
S46 · SOURCE-BOUND GATE EVIDENCE

RPi5 G8b CPU1 PPI27 one-shot paketi hazırlandı; fiziksel BOOT8B bekliyor

Operations komutu/kapı ailesi → gerçek repository yürütme sözleşmesi Bu sayfa yalnız S46 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S46Komut / fiziksel sözleşmeOperations id exactsource SHA exact

operation: rpi5-g8b-cpu1-ppi27-package-staged

script/Makefile/config · Operations · 2 exact excerpt

sequence-bound=true · implementation-bound=false
01 · Yürütme sözleşmesi

Gerçek script / Makefile / config kaynağı

tam dosyaL1–L150
scripts/verify-rpi5-g8b-layout.sh::verify-rpi5-g8b-layout.sh
#!/bin/sh
set -eu

if [ "$#" -ne 2 ]; then
    echo "usage: $0 <llvm-objdump> <rpi5-kernel-elf>" >&2
    exit 2
fi

objdump=$1
kernel=$2
for input in "$objdump" "$kernel"; do
    if [ ! -f "$input" ] || [ ! -r "$input" ]; then
        echo "HATA: G8b gate okuyamıyor: $input" >&2
        exit 1
    fi
done

disassembly=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g8b-dis.XXXXXX")
secondary=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g8b-secondary.XXXXXX")
irq=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g8b-irq.XXXXXX")
one_shot=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g8b-oneshot.XXXXXX")
secondary_gic=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g8b-gic.XXXXXX")
generic_irq=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g8b-generic-irq.XXXXXX")
trampoline=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g8b-trampoline.XXXXXX")
trap 'rm -f "$disassembly" "$secondary" "$irq" "$one_shot" "$secondary_gic" "$generic_irq" "$trampoline"' EXIT HUP INT TERM

"$objdump" -d --no-show-raw-insn "$kernel" > "$disassembly"

extract_symbol() {
    symbol=$1
    output=$2
    awk -v header="<$symbol>:" '
        index($0, header) { capture = 1 }
        capture && /^[[:space:]]*$/ { exit }
        capture { print }
    ' "$disassembly" > "$output"
    if [ ! -s "$output" ]; then
        echo "HATA: G8b makine-kodu sembolü bulunamadı: $symbol" >&2
        exit 1
    fi
}

extract_symbol rpi5_g8b_secondary_run "$secondary"
extract_symbol rpi5_g8b_try_handle_secondary_irq "$irq"
extract_symbol rpi5_g8b_init_per_cpu_oneshot "$one_shot"
extract_symbol rpi5_g8b_init_secondary_timer_ppi "$secondary_gic"
extract_symbol rust_irq_handler "$generic_irq"
extract_symbol rpi5_g8_secondary_entry "$trampoline"

for contract in \
    'msr[[:space:]]+CNTHCTL_EL2' \
    'msr[[:space:]]+CNTVOFF_EL2, xzr' \
    'msr[[:space:]]+CPACR_EL1, xzr'; do
    if ! grep -Eq "$contract" "$trampoline"; then
        echo "HATA: G8b CPU1 timer/FP EL2 trampoline sözleşmesi eksik: $contract" >&2
        exit 1
    fi
done

for contract in \
    'mrs[[:space:]]+x[0-9]+, MPIDR_EL1' \
    'bl[[:space:]]+.*<rpi5_g8b_init_secondary_timer_ppi>' \
    'bl[[:space:]]+.*<rpi5_g8b_init_per_cpu_oneshot>' \
    'msr[[:space:]]+DAIFClr, #0x2' \
    'msr[[:space:]]+DAIFSet, #0x2' \
    '[[:space:]]wfi([[:space:]]|$)' \
    '[[:space:]]wfe([[:space:]]|$)' \
    '[[:space:]]sev([[:space:]]|$)'; do
    if ! grep -Eq "$contract" "$secondary"; then
        echo "HATA: G8b CPU1 one-shot sözleşmesi eksik: $contract" >&2
        exit 1
    fi
done
if grep -Eq 'bl[[:space:]]+.*<(.*kprint|.*scheduler|.*rpi5_g7d)' "$secondary"; then
    echo "HATA: G8b CPU1 gövdesi UART/scheduler/G7d çağrısı içeriyor" >&2
    exit 1
fi

for contract in \
    'mrs[[:space:]]+x[0-9]+, CNTFRQ_EL0' \
    'mrs[[:space:]]+x[0-9]+, CNTVCT_EL0' \
    'msr[[:space:]]+CNTV_CTL_EL0' \
    'msr[[:space:]]+CNTV_CVAL_EL0' \
    '[[:space:]]isb([[:space:]]|$)'; do
    if ! grep -Eq "$contract" "$one_shot"; then
        echo "HATA: G8b one-shot timer makine-kodu eksik: $contract" >&2
        exit 1
    fi
done
if grep -Eq 'PERIOD_TICKS|NEXT_CVAL|FREQ_HZ|exceptions5TICKS' "$one_shot"; then
    echo "HATA: G8b CPU1 one-shot yolu CPU0 periyodik timer durumuna dokunuyor" >&2
    exit 1
fi

for contract in \
    '[[:space:]]str[[:space:]]+w[0-9]+' \
    '[[:space:]]ldr[[:space:]]+w[0-9]+' \
    '[[:space:]]dsb[[:space:]]+sy' \
    '[[:space:]]isb([[:space:]]|$)'; do
    if ! grep -Eq "$contract" "$secondary_gic"; then
        echo "HATA: G8b banked GIC read/write kapısı eksik: $contract" >&2
        exit 1
    fi
done

for contract in \
    'mrs[[:space:]]+x[0-9]+, MPIDR_EL1' \
    'msr[[:space:]]+CNTV_CTL_EL0' \
    'mrs[[:space:]]+x[0-9]+, CNTV_CTL_EL0' \
    'mrs[[:space:]]+x[0-9]+, CNTVCT_EL0' \
    'orr[[:space:]]+x[0-9]+, x[0-9]+, #0x80' \
    'cmp[[:space:]]+w2, #0x1b' \
    '[[:space:]]sev([[:space:]]|$)'; do
    if ! grep -Eq "$contract" "$irq"; then
        echo "HATA: G8b CPU1 IRQ/EOI/masked-return kapısı eksik: $contract" >&2
        exit 1
    fi
done
if grep -Eq 'exceptions5TICKS|bl[[:space:]]+.*<(.*kprint|.*scheduler|.*rpi5_g7d)' "$irq"; then
    echo "HATA: G8b CPU1 IRQ yolu global tick/UART/scheduler durumuna dokunuyor" >&2
    exit 1
fi

for cpu1_body in "$secondary" "$irq" "$one_shot" "$secondary_gic"; do
    if grep -Eq '(^|[[:space:],\[])(([qv][0-9]+)|([sd][0-9]+))([[:space:],\]]|$)' "$cpu1_body"; then
        echo "HATA: G8b FP=TRAP CPU1 makine-kodu FP/SIMD talimatı içeriyor" >&2
        exit 1
    fi
done

hook_line=$(grep -n 'bl[[:space:]]\+.*<rpi5_g8b_try_handle_secondary_irq>' "$generic_irq" | head -n 1 | cut -d: -f1)
tick_line=$(grep -n 'exceptions5TICKS' "$generic_irq" | head -n 1 | cut -d: -f1)
if [ -z "$hook_line" ] || [ -z "$tick_line" ] || [ "$hook_line" -ge "$tick_line" ]; then
    echo "HATA: G8b CPU1 kesmesi genel CPU0 TICKS yolundan önce ayrılmıyor" >&2
    exit 1
fi

for marker in \
    'ASELSAN/G8B0 CPU=0 TARGET=CPU1 MPIDR=0x' \
    'ASELSAN/G8B1 CPU=1 MPIDR=0x' \
    'ASELSAN/BOOT8B GIC=OK TIMER=OK CPU1_IRQ=1' \
    'ASELSAN/G8BERR CODE='; do
    if ! strings "$kernel" | grep -Fq "$marker"; then
        echo "HATA: G8b marker ELF içinde yok: $marker" >&2
        exit 1
    fi
done

echo "PASS: G8b CPU1 banked GICv2 PPI27 one-shot, early IRQ intercept, local timer disable/EOI and IRQ-masked EL1h return verified"
snippet sha256: 7e3082a309a1file sha256: 7e3082a309a1
02 · Kapı kimlik kaydı

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

tam Operations kaydıL32996–L33099
website/src/lib/operations.ts::rpi5-g8b-cpu1-ppi27-package-staged
  {
    id: "rpi5-g8b-cpu1-ppi27-package-staged",
    date: "2026-08-20",
    sequence: 46,
    status: "partial",
    title:
      "RPi5 G8b CPU1 PPI27 one-shot paketi hazırlandı; fiziksel BOOT8B bekliyor",
    summary:
      "Fiziksel G8a/BOOT8 sınırı korunarak CPU1'in yalnız banked GICv2 CPU interface ve virtual timer PPI27 katılımını açan dar G8b dilimi hazırlandı. CPU1 beş CPU0 tick gecikmeli tek one-shot IRQ alıyor; handler local timer'ı kapatıp raw EOI veriyor, exactly-once teslimi yayımlıyor ve CPU1'i IRQ maskeli EL1h WFE parkına döndürüyor. Scheduler, migration, IPI, TLB shootdown ve CPU2/3 kapalı kalıyor. G8b hedef testleri 14/14, workspace 116/116, QEMU smoke, üç-board build, RPi5 disassembly/izolasyon kapısı ve paket manifesti geçti. 246960 baytlık dc241315…fb44a8a imaj yalnız build/rpi5 içinde staged durumdadır; microSD'ye yazılmadı ve fiziksel G8B0/G8B1/BOOT8B UART10 kanıtı yoktur.",
    evidence: [
      "G8a BOOT8 ön koşulundan sonra ayrı release mailbox kullanılır; CPU1'in tarihsel IRQ-masked WFE sınırı G8b başlamadan değiştirilmez.",
      "CPU1 yalnız banked GICv2 CPU interface/PPI27 durumunu kurar; GIC distributor yeniden başlatılmaz ve CPU0'ın PPI/periyodik timer durumu değiştirilmez.",
      "CPU1 virtual timer tam 5 CPU0 tick eşdeğerinde one-shot kurulur. G8b IRQ intercept'i global timer::ack_and_rearm, TICKS ve G7d yollarından önce çalışır.",
      "Handler local timer'ı kapatır, raw acknowledge değerini EOI eder, delivery sayısını exactly-once 1 yapar ve trap frame'i IRQ maskeli EL1h dönüşüne hazırlar.",
      "G8b hedef testleri 8 kaynak/izolasyon + 6 strict UART/adversarial olmak üzere 14/14 PASS verdi.",
      "make verify-core exit 0 verdi: cargo test --workspace 116/116, QEMU runtime hello ELF + IPC ELF + scheduler SEC 5, QEMU/RPi4/RPi5 build'leri ve önceki G7c/G7d/G8a kapıları PASS.",
      "scripts/verify-rpi5-g8b-layout.sh CPU1 EL2 virtual timer erişimini, banked PPI27 init'i, local CNTV one-shot/disable, erken IRQ intercept, raw EOI ve IRQ maskeli EL1h dönüşünü makine kodunda PASS verdi.",
      "G8b kabul marker'ları QEMU ve RPi4 ELF'lerinde 0, yalnız board-rpi5 ELF'inde 4 bulundu; UART/scheduler/FP-SIMD CPU1 izolasyon taramaları geçti.",
      "build/rpi5 manifesti 3/3 OK verdi. İmaj 246960 bayt ve SHA-256 dc241315fa24992ab025da79c72cc14cebf28d7e420e859a8f756d7e5fb44a8a'dır.",
      "DTB 78703 bayt / 40a2fbe9…ca00, config 501 bayt / 1248275c…d76b ve SHA256SUMS 248 bayt / 072428ab…7632 olarak donduruldu.",
      "Artefaktsız geçici repo kopyasındaki baştan üretim ana build ile aynı dc241315…fb44a8a imaj hashini verdi.",
      "Staged kabul, fiziksel sınır ve sıradaki güvenli kart işlemi docs/M8.1-RPi5-G8b-CPU1-PPI27-Staged-Proof.md içinde donduruldu.",
    ],
    commands: [
      "make verify-rpi5-g8b-host",
      "make verify-core",
      "scripts/verify-rpi5-g8b-layout.sh <llvm-objdump> target/rpi5/aarch64-unknown-none/debug/aselsan_kernel",
      "cd build/rpi5 && shasum -a 256 -c SHA256SUMS",
      "artifact-free temporary checkout: make verify-core + SHA-256 compare",
    ],
    terminalSessionsNote:
      "Bu oturumlar dondurulmuş G8b kaynağı üzerinde gerçekten çalıştırılan host/build/makine-kodu/paket komutlarının seçili sonuçlarıdır. G8b UART satırları sentetik strict-validator fixture'ıdır; fiziksel UART10 çıktısı değildir.",
    terminalSessions: [
      {
        id: "g8b-targeted-tests",
        title: "G8b kaynak, izolasyon ve strict UART sözleşmesi",
        commandLines: ["make verify-rpi5-g8b-host"],
        outputLines: [
          "rpi5_g8b_source: 8 passed; 0 failed",
          "rpi5_g8b_uart: 6 passed; 0 failed",
          "G8b targeted total: 14/14 PASS",
          "synthetic validator: G8b PASS: intid=27 deliveries=1 irq_tick=705 timer_counts=2700100 timer_delta=100",
        ],
        exitCode: 0,
        outputMode: "selected",
        outputNote:
          "Validator özeti sentetik fixture'a aittir; fiziksel kart ölçümü değildir.",
      },
      {
        id: "g8b-full-matrix",
        title: "Workspace, QEMU ve üç-board geriye dönük matris",
        commandLines: ["make verify-core"],
        outputLines: [
          "cargo test --workspace: 116 passed; 0 failed",
          "QEMU smoke PASS: hello ELF + IPC ELF + scheduler SEC 5; fault marker yok",
          "QEMU kernel build: PASS",
          "Raspberry Pi 4 kernel build: PASS",
          "Raspberry Pi 5 image/package build: PASS",
          "G8b marker isolation: qemu=0 rpi4=0 rpi5=4",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "g8b-machine-code",
        title: "RPi5 G8b makine-kodu ve privilege izolasyonu",
        commandLines: [
          "scripts/verify-rpi5-g8b-layout.sh <llvm-objdump> target/rpi5/aarch64-unknown-none/debug/aselsan_kernel",
        ],
        outputLines: [
          "PASS: G8b CPU1 banked GICv2 PPI27 one-shot, early IRQ intercept, local timer disable/EOI and IRQ-masked EL1h return verified",
          "CPU1 UART/scheduler/FP-SIMD path: absent",
          "GIC distributor reset from secondary path: absent",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
      {
        id: "g8b-package-reproducibility",
        title: "RPi5 staged paket, manifest ve temiz üretim",
        commandLines: [
          "cd build/rpi5 && shasum -a 256 -c SHA256SUMS",
          "shasum -a 256 build/rpi5/aselsanos-rpi5.img",
          "artifact-free temporary checkout: make verify-core + shasum -a 256 image",
        ],
        outputLines: [
          "aselsanos-rpi5.img: OK",
          "bcm2712-rpi-5-b.dtb: OK",
          "config.txt: OK",
          "image bytes=246960",
          "image sha256=dc241315fa24992ab025da79c72cc14cebf28d7e420e859a8f756d7e5fb44a8a",
          "clean-copy image sha256=dc241315fa24992ab025da79c72cc14cebf28d7e420e859a8f756d7e5fb44a8a",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
    ],
    limitations: [
      "Bu kayıt STAGED host/build/paket kanıtıdır; microSD'ye yazılmadı, Raspberry Pi 5 açılmadı ve fiziksel G8B0/G8B1/BOOT8B gözlenmedi.",
      "Sentetik fixture ve validator PASS'i fiziksel UART10 kanıtı değildir.",
      "G8b yalnız CPU1 banked GICv2 PPI27 ve tek one-shot IRQ smoke'udur; genel SMP scheduler PASS'i değildir.",
      "Scheduler runqueue, task migration, reschedule IPI, TLB shootdown, CPU2/CPU3, hotplug ve EL0-on-CPU1 kapsam dışıdır.",
    ],
  },
snippet sha256: e6dfa5c9f01cfile sha256: 9726dbf00f84
Kayıtlı yürütme/kanıt komutu
make verify-rpi5-g8b-host
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 3050638b71a684d8f8f947a8a6faa237a17fa8db5dc0db04fb207b668b462af9