S162 · SOURCE-BOUND GATE EVIDENCE
G8k: generation-bound ASID allocator ve TCR.AS read-back modeli
Operations --test hedefi → test hedefiyle aynı adlı uygulama/model modülü → kaynak kesiti Bu sayfa yalnız S162 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.
S162Focused kod testiOperations id exactsource SHA exacttest target exact
operation: g8k-asid-generation-tcr-readback-model-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 öğesiL12–L63
simulation/src/g8k_allocator.rs::ONLINE_MASK
pub use crate::tcr_contract::{TcrAsidError, TcrAsidReadback, TCR_ASID_SIZE_BIT};
use production_asid_allocator::{AsidAllocator, AsidError, MAX_ASIDS};
pub const ONLINE_MASK: u8 = 0b1111;
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct GenerationLease {
pub asid: u16,
pub generation: u64,
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct PendingRelease {
pub lease: GenerationLease,
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct ShootdownCompletion {
pub asid: u16,
pub generation: u64,
pub online_mask: u8,
pub ack_mask: u8,
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum SlotState {
Kernel,
Free,
Active,
Retiring,
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum GenerationAllocatorError {
Production(AsidError),
Tcr(TcrAsidError),
KernelReserved,
InvalidAsid,
StaleLease,
ReleaseAlreadyPending,
ShootdownIncomplete,
OnlineMaskInvalid,
OnlineMaskChanged,
GenerationOverflow,
}
pub struct G8kGenerationAllocator {
allocator: AsidAllocator,
generations: [u64; MAX_ASIDS],
states: [SlotState; MAX_ASIDS],
}snippet sha256: 7de2d9d3e3dc…file sha256: 2e3b2bffb3a3…
02 · Doğrulayan test kodu
Operations komutuna bağlı focused test
tam Rust öğesiL103–L127
simulation/tests/g8k_allocator.rs::stale_generation_and_foreign_completion_are_transactional
#[test]
fn stale_generation_and_foreign_completion_are_transactional() {
let mut allocator = G8kGenerationAllocator::new();
let lease = allocator.allocate().unwrap();
let pending = allocator.arm_release(lease).unwrap();
assert_eq!(
allocator.release_after_shootdown(
pending,
ShootdownCompletion {
asid: lease.asid + 1,
..completion(lease)
},
),
Err(GenerationAllocatorError::StaleLease)
);
assert_eq!(allocator.state(lease.asid), Ok("retiring"));
assert_eq!(
allocator.arm_release(GenerationLease {
generation: lease.generation + 1,
..lease
}),
Err(GenerationAllocatorError::StaleLease)
);
}snippet sha256: 10f6e9b59d8a…file sha256: a91a92c20b50…
03 · Kapı kimlik kaydı
Operations sıra, kimlik ve başlık bağı
tam Operations kaydıL23483–L23527
website/src/lib/operations.ts::g8k-asid-generation-tcr-readback-model-partial
{
id: "g8k-asid-generation-tcr-readback-model-partial",
date: "2026-08-24",
sequence: 162,
status: "passed",
umbrella_status: "partial",
title: "G8k: generation-bound ASID allocator ve TCR.AS read-back modeli",
summary:
"S162, S161 shootdown kapısının allocator devamını 11/11 bounded source/model seviyesinde kapattı: production allocator kaynağı doğrudan kullanıldı; ilk kullanıcı lease'i nonzero ASID1/generation1, ASID0 kernel-reserved kaldı. Shootdown completion öncesi release/reuse reddedildi ve ASID retiring durumunda allocation bitmapinde canlı tutuldu. Exact dört-CPU online maskesi ve ACK maskesi olmadan release commit edilmedi; online-mask değişimi, forged ACK maskesi ve invalid mask transactional fail-closed kaldı. Exact completion sonrası aynı ASID generation1→2 olarak yeniden alınabildi; stale/foreign generation, duplicate arm ve replayed release state değiştirmedi. Generation u64::MAX taşmasında başarısız allocate production bitmap tahsisini geri aldı; slot free ve görünmez tahsis yok. Production TCR contract kaynağı TCR_EL1.AS=0 8-bit seçimini ve write/read-back eşleşmesini doğruladı. Production TLBI runtime, scheduler migration, QEMU, fiziksel runtime ve generic SMP açık kaldı.",
evidence: [
"g8k_allocator: 11/11 PASS; production AsidAllocator kaynağı üzerinden generation-bound lease, release ordering ve overflow rollback doğrulandı.",
"TCR_EL1.AS=0 8-bit contract, write/read-back mismatch ve 16-bit selection fail-closed sınırlarıyla doğrulandı.",
"ASID0 reserve, generation1 başlangıcı, retiring allocation canlılığı, exact online-mask completion ve generation1→2 reuse kabulü geçti.",
"Stale/foreign generation, duplicate arm, replayed release, forged ACK maskesi ve online-mask değişimi allocator state'ini değiştirmedi.",
"u64::MAX generation preflight hatasında production bitmap rollback edildi: ASID1 free, generation MAX ve is_allocated=false kaldı.",
"Kalıcı kapsam: `docs/M8.1-RPi5-G8k-S162-ASID-Generation-TCR-Readback-Proof.md`.",
"S162 fiziksel/device operasyonu yapmadı: physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S162=NO.",
],
commands: [
"cargo test -p aselsan_microkernel_simulation --test g8k_allocator -- --test-threads=1",
],
terminalSessions: [
{
id: "s162-g8k-asid-generation-tcr-readback-model",
title: "G8k generation-bound ASID/TCR.AS host model kapısı",
commandLines: [
"cargo test -p aselsan_microkernel_simulation --test g8k_allocator -- --test-threads=1",
],
outputLines: [
"running 11 tests",
"test result: ok. 11 passed; 0 failed",
],
exitCode: 0,
outputMode: "selected",
},
],
terminalSessionsNote:
"S162 bounded source/model allocator ve TCR contract kapısıdır; production TLBI execution, allocator shootdown wiring, scheduler migration, QEMU, fiziksel RPi ve generic SMP runtime sonucu değildir.",
limitations: [
"Production allocator generation state'i scheduler/TLBI runtime yoluna bağlanmadı; model production allocator source'unu doğrudan tüketir.",
"ShootdownCompletion bu dilimde bounded input kaydıdır; S161 completion authority'sine üretim düzeyinde bağlanmış unforgeable receipt değildir.",
"EL0/nonzero-ASID migration, CPU hotplug, long soak, CPU2/CPU3 production arbitration ve generic SMP coordination sonraki kapılardır.",
"QEMU ve fiziksel/device operations kapsam dışıdır; RUNBOOK_EXECUTED_IN_S162=NO.",
],
},snippet sha256: 77086447b262…file sha256: 9726dbf00f84…
Focused test komutu
cargo test -p aselsan_microkernel_simulation --test g8k_allocator -- --test-threads=1proof: docs/M8.1-RPi5-G8k-S162-ASID-Generation-TCR-Readback-Proof.md
Registry schema v5 · generator
website/scripts/generate-code-gates.mjs · Tam SHA-256: 3050638b71a684d8f8f947a8a6faa237a17fa8db5dc0db04fb207b668b462af9