ASELSANMicrokernel
S317 · SOURCE-BOUND GATE EVIDENCE

G8l: QEMU S142 replacement exact-ACK writer-authority audit

Operations --test hedefi → test hedefiyle aynı adlı uygulama/model modülü → kaynak kesiti Bu sayfa yalnız S317 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S317Focused kod testiOperations id exactsource SHA exacttest target exact

operation: g8l-s317-qemu-s142-replacement-exact-ack-writer-authority-audit-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 öğesiL30–L103
kernel/src/g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s317_qemu_s142_replacement_exact_ack_writer_authority_audit.rs::S317_MAIN_REMAINING_UNAUDITED_WRITER_SITES

pub const S317_WRITER_BOUNDARY_SITES: usize = 1;
pub const S317_WRITER_AUTHORITY_SITES: usize = 0;
pub const S317_MAIN_EXPLICIT_WRITER_SITES: usize = 17;
pub const S317_MAIN_PREVIOUSLY_AUDITED_WRITER_SITES: usize = 7;
pub const S317_MAIN_REMAINING_UNAUDITED_WRITER_SITES: usize = 9;
pub const S317_S142_EXPLICIT_WRITER_SITES: usize = 2;
pub const S317_S142_REMAINING_UNAUDITED_WRITER_SITES: usize = 1;
pub const S317_DIRECT_SCHEDULER_ACCESS_SITES: usize = S316_DIRECT_SCHEDULER_ACCESS_SITES;
pub const S317_IMMUTABLE_READ_SITES: usize = S316_IMMUTABLE_READ_SITES;
pub const S317_WHOLE_SCHEDULER_GUARDED_SITES: usize = S316_WHOLE_SCHEDULER_GUARDED_SITES;
pub const S317_WHOLE_SCHEDULER_UNROUTED_SITES: usize = S316_WHOLE_SCHEDULER_UNROUTED_SITES;
pub const S317_OPEN_WRITER_SITES: usize = S316_OPEN_WRITER_SITES;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS317SchedulerWriterAuthorityAuditOutcome {
    Idle,
    AwaitingWriterAuthority {
        request_id: u64,
        guarded_sites: usize,
        writer_sites: usize,
    },
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum G8lS317SchedulerWriterAuthorityAuditError {
    S316(G8lS316SchedulerWriterAuthorityAuditError),
    S245(G8lS245ExclusionAdmissionRequestError),
    PriorCoverageDrift {
        guarded_sites: usize,
        unrouted_sites: usize,
    },
}

/// Revalidate the prior fail-closed authority boundary without taking
/// admission or constructing a production exclusive wrapper.
pub fn preflight_s317_scheduler_writer_authority(
    caller_cpu: usize,
    request: Option<G8lS245WholeSchedulerExclusionAdmissionRequestView>,
) -> Result<G8lS317SchedulerWriterAuthorityAuditOutcome, G8lS317SchedulerWriterAuthorityAuditError>
{
    match preflight_s316_scheduler_writer_authority(caller_cpu, request)
        .map_err(G8lS317SchedulerWriterAuthorityAuditError::S316)?
    {
        G8lS316SchedulerWriterAuthorityAuditOutcome::Idle => {
            Ok(G8lS317SchedulerWriterAuthorityAuditOutcome::Idle)
        }
        G8lS316SchedulerWriterAuthorityAuditOutcome::AwaitingWriterAuthority {
            request_id,
            guarded_sites,
            writer_sites,
        } if guarded_sites == S317_WHOLE_SCHEDULER_GUARDED_SITES
            && writer_sites == S317_OPEN_WRITER_SITES =>
        {
            Ok(
                G8lS317SchedulerWriterAuthorityAuditOutcome::AwaitingWriterAuthority {
                    request_id,
                    guarded_sites,
                    writer_sites,
                },
            )
        }
        G8lS316SchedulerWriterAuthorityAuditOutcome::AwaitingWriterAuthority {
            guarded_sites,
            writer_sites: _,
            ..
        } => Err(
            G8lS317SchedulerWriterAuthorityAuditError::PriorCoverageDrift {
                guarded_sites,
                unrouted_sites: S317_DIRECT_SCHEDULER_ACCESS_SITES - guarded_sites,
            },
        ),
    }
}
snippet sha256: 197268982c16file sha256: 14e96c81148e
02 · Doğrulayan test kodu

Operations komutuna bağlı focused test

tam Rust öğesiL292–L331
simulation/tests/g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s317_qemu_s142_replacement_exact_ack_writer_authority_audit.rs::s317_helper_revalidates_kernel_caller_send_and_linked_reply_under_transaction

#[test]
fn s317_helper_revalidates_kernel_caller_send_and_linked_reply_under_transaction() {
    let source = include_str!("../../kernel/src/task/scheduler.rs");
    let helper = kernel_call_and_wait_boundary(source);
    for required in [
        "IrqGuard::new()",
        "IPC_TRANSACTION_LOCK.lock()",
        "IPC_CALL_DEADLINES.lock()",
        ".filter(|task| !task.is_user)",
        ".filter(|task_id| *task_id != 0)",
        "current_endpoint_authority_is_live(",
        "CapabilityRights::ENDPOINT_SEND",
        "ENDPOINT_REGISTRY.lock()",
        "endpoint.id == target_endpoint && !endpoint.is_reply_cap",
        "endpoint.id == reply_cap_id",
        "endpoint.is_reply_cap",
        "endpoint.owner == caller_task",
        "endpoint.reply_target == Some(target_endpoint)",
        "if !reply_is_linked",
    ] {
        assert!(
            helper.contains(required),
            "missing S317 helper authority token: {required}"
        );
    }
    let irq = helper.find("IrqGuard::new()").unwrap();
    let transaction = helper.find("IPC_TRANSACTION_LOCK.lock()").unwrap();
    let caller = helper.find("let caller_task").unwrap();
    let send = helper.find("current_endpoint_authority_is_live(").unwrap();
    let endpoints = helper.find("ENDPOINT_REGISTRY.lock()").unwrap();
    let reply = helper.find("let reply_is_linked").unwrap();
    assert!(
        irq < transaction
            && transaction < caller
            && caller < send
            && send < endpoints
            && endpoints < reply
    );
}
snippet sha256: 15b828e1cd38file sha256: d3dd8a74652a
03 · Kapı kimlik kaydı

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

tam Operations kaydıL15245–L15309
website/src/lib/operations.ts::g8l-s317-qemu-s142-replacement-exact-ack-writer-authority-audit-partial
  {
    id: "g8l-s317-qemu-s142-replacement-exact-ack-writer-authority-audit-partial",
    date: "2026-08-27",
    sequence: 317,
    status: "passed",
    umbrella_status: "partial",
    title: "G8l: QEMU S142 replacement exact-ACK writer-authority audit",
    summary:
      "S317 focused 15/15 PASS ile main.rs kaynak sırasındaki bir sonraki explicit mutable scheduler sınırını doğrular: run_qemu_s142_lower_el_fault_recovery içindeki iki ipc_kernel_call_and_wait writer'ından daha sonraki replacement-supervisor exact-ACK çağrısı. İlk faulting-supervisor CALL'i ordinary fatal lifecycle sonrasında InvalidCapability döner, cancelled reply retired olur, broker lease otomatik requeue edilir, old lease StaleLease olur ve faulting supervisor writer'dan önce reclaim edilir. Nonzero controller, controller-owned normal Endpoint SEND authority, fresh strict EL0 replacement RECV grant, newer task-bound session ve retry lease, immutable retry message ve linked one-shot reply writer'dan önce doğrulanır. Helper aynı IRQ/IPC transaction altında non-user caller SEND authority'sini, normal endpoint'i, linked reply'ı, optional receiver authority/deadline'ını ve park kapasitesini yeniden doğrular; CALL publication/park ve optional delivery tek transaction içindedir. Continuation aynı caller'ı resume eder, exact replacement ACK'i yeniden kurar; broker exact acknowledge ve replacement session close bundan sonra yapılır. Writer authority yalnız model gate'inin exclusive lease'iyle mümkündür; reader lease'i writer'ı açmaz. main.rs 17 explicit writer / 7 previously audited / 9 remaining unaudited; S142 işlevi 2 / 1; production inventory 113 direct / 44 immutable guarded / 69 open writer olarak değişmez ve production exclusive wrapper, provider authority, whole-scheduler exclusion veya scheduler mutation üretilmez.",
    evidence: [
      "S317 focused kaynak/model kapısı iki bağımsız koşuda 15/15 PASS verdi: 130 B / SHA-256 0447f2fe9dc6fdf30815a6962cf23d978425e51bef2acde1efb27e5da13a78b3.",
      "main.rs içindeki 17 explicit addr_of_mut!(crate::task::scheduler::SCHEDULER) sitesinin positions[9], kaynakta alttan sekizinci sınırı audit edilir. run_qemu_s142_lower_el_fault_recovery iki explicit alias taşır; daha önceki cancelled CALL açık kalırken main.rs genelinde 9 alias ayrıca açıktır.",
      "İlk S142 CALL'i faulting supervisor'ın ordinary fatal lifecycle teardown'ı sonrasında InvalidCapability verir; cancelled reply registry'den kalkar, broker pending=1/in_flight=0 ile lease'i otomatik requeue eder, old lease StaleLease olur ve faulting supervisor exact reclaim ile RuntimePmm baseline'a döner.",
      "Nonzero controller kimliği ve controller-owned normal Endpoint ENDPOINT_SEND authority korunur; fresh strict EL0 replacement'a exact ENDPOINT_RECV grant verilir. Replacement session fault session'dan, retry lease old lease'ten yenidir ve retry event old event ile exact eşittir.",
      "Recovery publication IrqGuard writer'dan önce bırakılır; immutable retry IpcMessage ve controller-owned linked one-shot reply-cap writer'dan önce kurulur.",
      "ipc_kernel_call_and_wait exact endpoint id/generation, reply id ve immutable retry_message'i alır; S142 yalnız exact ACK label, replacement-task badge ve retry_message.data eşleşmesini kabul eder.",
      "Helper IrqGuard ve IPC_TRANSACTION_LOCK altında nonzero non-user caller, canlı ENDPOINT_SEND authority, normal target endpoint ve caller-owned linked reply-cap'i yeniden doğrular. Optional receiver varsa exact ENDPOINT_RECV generation/owner ve receive deadline da doğrulanır; ready/blocked kapasite preflight'ı mutation'dan önce gelir.",
      "CALL publish/finish-park, caller BlockedOnIpc publication ve optional receiver delivery/deadline retirement/Ready enqueue tek transaction içindedir. Transaction bırakıldıktan sonra aynı kernel caller resume edilir ve saved GPR'lerden exact reply yeniden kurulur.",
      "Exact replacement ACK sonrasında controller retry lease'i bir kez acknowledge eder ve replacement session'ı bir kez kapatır; final broker queued/pending/in_flight=0, acknowledged=2, sessions=4, crashes=2, recovered_inflight=2; endpoint/reply absence ve RuntimePmm baseline korunur.",
      "Model gate reader membership exclusive writer authority'yi ExclusiveBusy ile bloklar; reader bırakıldıktan sonra non-zero token'lı exclusive lease alınır. Wrong CPU InvalidCpu ile fail-closed kalır. Bu host/model evidence'tır.",
      "S316 authority preflight yeniden doğrulanır; pending S245 request korunur ve sonuç AwaitingWriterAuthority { guarded_sites: 44, writer_sites: 69 } olarak döner.",
      "Dört AArch64 profil derlemesi iki koşuda byte-equal exit 0 verdi: QEMU 110646 B / ae504556, RPi4 149371 B / 01c4d2f4, RPi5 461261 B / 62559d64 ve RPi5+SMP 461203 B / ec4f1475. Warning header'ları sırasıyla 291, 389, 985 ve 985'tir; zero-warning iddiası değildir.",
      "Birleşik board-rpi5,board-qemu özellikleri iki koşuda beklenen exit 101, 18590 B / 5cfa5ab4, 17 error ve 22 warning header ile fail-closed kaldı.",
      "S238–S317 dependency matrisi iki koşuda 81 grup / 1139/1139 PASS; ham loglar 10452 B / 8dd2a75b ve 358cb73b, süre-normalize özetler byte-equal 10614 B / 1dbec961036a1cbe525dc0766de7691de01ebb355bd76ebf9072d4cedaa1191c. Bu production writer-authority invocation kanıtı değildir.",
      "Ortak make verify-qemu iki koşuda PASS verdi: 116222 B / a7d17718 ve 116139 B / 2f5018fd; guest logları 2135784 B / 37255c6d ve 2149920 B / 4430ab61. W^X 31/31, S271 GRAPH_ABSENT=YES, RuntimePmm baseline, EL0 x4096, IPC 20/20, koşu başına tek FATAL_TASK_EXIT, SEC5 ve 13 KERNEL_FAULTS=0 marker'ı korunur. Bu ortak smoke S317 production writer-authority invocation kanıtı değildir.",
      "Exact yedi tarihsel G8h assertion adıyla dışlandığında workspace iki koşuda 279 sonuç grubu / 2946 PASS / 7 filtered verdi: ham loglar 63769 B / 1753dc2d ve 42cc1d53, sonuç özetleri 26388 B / 3c986b19 ve 2d17a4f1, süre-normalize 26944 B özet byte-equal / SHA-256 fa14ff998bc2b88ecd5e81b1f0015f294501c9457ac84aa7d30f64fa8c3bb8b1. Filtresiz koşu exit 101, 58991 B / 30596f52 ile frozen S96 exceptions.S identity kapısında RED kaldı; full-workspace GREEN iddia edilmez.",
      "S317 production exclusive wrapper, provider authority, whole-scheduler exclusion, QEMU fixture mutation veya scheduler mutation iddiası eklemez; physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S317=NO.",
    ],
    commands: [
      "cargo test --quiet -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s317_qemu_s142_replacement_exact_ack_writer_authority_audit -- --test-threads=1",
      "cargo check --quiet -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-qemu",
      "cargo check --quiet -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi4",
      "cargo check --quiet -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi5",
      "cargo check --quiet -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi5,smp",
      "cargo check --quiet -p aselsan_kernel --target aarch64-unknown-none --no-default-features --features board-rpi5,board-qemu",
      "make verify-qemu",
    ],
    terminalSessions: [
      {
        id: "g8l-s317-qemu-s142-replacement-exact-ack-writer-authority-audit",
        title:
          "G8l S317 QEMU S142 replacement exact-ACK writer-authority audit",
        commandLines: [
          "cargo test --quiet -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s317_qemu_s142_replacement_exact_ack_writer_authority_audit -- --test-threads=1",
        ],
        outputLines: [
          "test result: ok; S317 focused 1 group / 15 passed; 0 failed",
          "repeat-stable quiet output: 130 B / 0447f2fe9dc6fdf30815a6962cf23d978425e51bef2acde1efb27e5da13a78b3",
          "QEMU S142 replacement exact-ACK writer authority remains model-only: faulted CALL retirement/requeue/reclaim and fresh replacement session/lease precede exact retry forwarding; S142 retains 1 unaudited alias, main.rs retains 9 unaudited aliases and all 69 production writer sites remain open",
          "dependency: S238–S317 · 81 groups · 1139/1139 PASS; workspace: 279 groups · 2946 PASS · 7 historical filtered",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    terminalSessionsNote:
      "S317 kaynak/model fail-closed authority boundary'sidir; production writer guard/migration, QEMU fixture mutation ve fiziksel/device execution claim edilmez.",
    limitations: [
      "S317 run_qemu_s142_lower_el_fault_recovery içindeki daha sonraki replacement exact-ACK ipc_kernel_call_and_wait mutable scheduler aliasını audit eder; S142 işlevinde önceki cancelled CALL, main.rs genelinde 9 ve toplam 69 production writer site authority wrapper dışında açık kalır.",
      "Exclusive lease yalnız host/model gate'inde test edilir; production exclusive wrapper, provider authority ve whole-scheduler exclusion açık kalır.",
      "S238–S317 dependency matrisi exact 81 grup / 1139/1139 PASS'tir; bu production writer authority invocation kanıtı değildir.",
      "Filtresiz workspace frozen S96 identity kapısında RED'dir; workspace umbrella GREEN iddia edilmez.",
      "Supported-profile writer-authority runtime invocation, Generic SMP ve fiziksel RPi kabulü açık kalır; S317 physical/device operations=0 ve RUNBOOK_EXECUTED_IN_S317=NO.",
    ],
  },
snippet sha256: 17101f395da4file sha256: 9726dbf00f84
Focused test komutu
cargo test --quiet -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s317_qemu_s142_replacement_exact_ack_writer_authority_audit -- --test-threads=1
proof: docs/M8.1-RPi5-G8l-S317-QEMU-S142-Replacement-Exact-Ack-Writer-Authority-Audit-Proof.md
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06