VeridianOS

Prompt

VeridianOS — Advanced Kernel Code Review & Architecture Benchmark Objetivo Esta avaliação mede capacidade de revisão profunda de código de kernel e desenho de sistemas, com foco em: concorrência SMP; x86_64 e MMU/TLB; lifetime e memory reclamation; Rust unsafe e soundness; interrupts/NMI; lock ordering; capability systems; linearizabilidade; isolamento kernel/user; resistência a over-auditing e correções artificiais. O objetivo não é medir quantidade de comentários nem reconhecimento de padrões conhecidos. Não assumes que existe um defeito apenas porque o código é complexo. Não inventes contratos, garantias de hardware ou invariantes que não estejam fundamentados no enunciado. Quando a conclusão depender de uma propriedade não especificada, distingue: o que pode ser demonstrado; o que é apenas possível; que informação adicional seria necessária para fechar a análise. Regras de análise Para cada tarefa: Reconstrói os invariantes relevantes antes de concluir. Determina se existe uma violação real. Se houver: identifica precisamente a propriedade violada; fornece um interleaving, estado ou execução concreta; explica por que essa execução é permitida; propõe a correção; demonstra que a correção preserva as invariantes. Se não houver problema demonstrável, diz explicitamente que o código/diff deve ser aceite. Não uses afirmações vagas como "há uma race", "falta uma barrier" ou "pode dar UB" sem explicar o mecanismo. Distingue: race lógica; data race; ordering; lifetime bug; deadlock; contention; hardware ordering; Rust Undefined Behavior. volatile não é solução de sincronização. Atomicidade não implica automaticamente ordering suficiente. acquire/release não resolve automaticamente lifetime/reclamation. "x86 é forte" não torna algoritmos lock-free automaticamente corretos. Código Rust que compila não é automaticamente sound. Não alteres a arquitetura apenas para tornar a análise mais fácil. Modelo de execução Assume: x86_64; SMP; múltiplos CPUs; preempção; interrupts; NMIs; page tables por address space; TLBs privados por CPU; IPI; scheduler SMP; userland não confiável; drivers parcialmente em userland; capabilities como mecanismo de autoridade; memória virtual; DMA; Rust unsafe onde indicado. Quando uma propriedade depender de uma garantia concreta de x86_64, explica qual. Não uses "speculative execution" como explicação genérica. Tarefa 1 — TLB Shootdown, Page-Table Lifetime e ACK Contexto Cada mm possui estruturas de page table que podem ser libertadas quando deixam de estar referenciadas pelo address space. void unmap_page(struct mm *mm, uintptr_t va) { struct pt_page *pt = lookup_leaf_page_table(mm, va); clear_pte(mm, va); for_each_cpu(cpu, mm->active_cpus) { if (cpu != current_cpu()) send_ipi(cpu, IPI_TLB_FLUSH, va); } free_pt_page_if_empty(pt); } Handler remoto: void handle_tlb_flush(uintptr_t va) { invlpg((void *)va); atomic_fetch_add_explicit( &tlb_acks[current_cpu()], 1, memory_order_relaxed ); } Os IPI são assíncronos. Enunciado Determina se o protocolo é correto. Analisa: quando deixa de existir uma tradução válida; o que INVLPG garante; o que INVLPG não garante; quando o CPU remoto realizou efetivamente a invalidação; quando pt pode ser libertado; se o ACK é suficiente; se existe execução concreta que permita uso de memória já libertada; que protocolo seria necessário para tornar a libertação segura. Explica precisamente a relação: PTE update → TLB invalidation → remote acknowledgement → page-table reclamation Apresenta uma sequência concreta em pelo menos dois CPUs caso consideres o código incorreto. Tarefa 2 — Rust unsafe: Send/Sync, aliasing e NonNull Contexto Existe um objeto de kernel localizado numa região específica de um CPU: use core::marker::PhantomData; use core::ptr::NonNull; pub struct Slot<T> { ptr: NonNull<T>, owner_cpu: usize, _marker: PhantomData<T>, } unsafe impl<T: Send> Send for Slot<T> {} unsafe impl<T: Send> Sync for Slot<T> {} impl<T> Slot<T> { pub unsafe fn get(&self) -> &T { self.ptr.as_ref() } pub unsafe fn get_mut(&self) -> &mut T { self.ptr.as_ptr().as_mut().unwrap() } } Único contrato informal: ptr aponta para um T válido que pertence logicamente ao CPU indicado por owner_cpu. Não existe lock interno. Enunciado Determina se as implementações de Send e Sync são sound. Analisa: significado de Sync; o que &Slot<T> permite fazer simultaneamente; se T: Send é suficiente; papel de NonNull<T>; garantias de get() e get_mut(); aliasing entre &T e &mut T; efeito de owner_cpu; invariantes adicionais necessários para tornar a abstração sound. Se considerares incorreto, constrói um cenário concreto de UB. Não respondas apenas "não é thread-safe": identifica a regra semântica violada. Formato obrigatório Para cada tarefa: Veredito correto / incorreto / indeterminado devido a contrato em falta Invariantes relevantes Análise Execução/interleaving demonstrativo Correção ou design proposto Porque a correção é suficiente Dependências / pressupostos Não atribuas bugs por associação de palavras.