ASELSANMicrokernel
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: 7de2d9d3e3dcfile 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: 10f6e9b59d8afile 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: 77086447b262file sha256: 9726dbf00f84
Focused test komutu
cargo test -p aselsan_microkernel_simulation --test g8k_allocator -- --test-threads=1
proof: 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