CuBit
1.0.0
O Cubitos é um multiprocessador, de 64 bits, (parcialmente) do sistema operacional de uso geral formalmente, atualmente para a arquitetura x86-64.
O cúbito está escrito no dialeto de faísca de Ada.
O Cubit é muito um trabalho em andamento! Dito isto, por favor, dê uma volta. Contribuidores são bem -vindos!
gprbuild , gnat , etc. No seu $PATHPara criar .ISO inicializável, você também precisará:
Dependências: você precisará do compilador GNAT 2020 e, se deseja criar o CD ao vivo, precisará das ferramentas Xorriso e Grub-Mkrescue e, possivelmente , Grub-PC-Bin, dependendo do ambiente de emulador/virtualização que você está usando. Provavelmente, eles são fornecidos no gerenciador de pacotes da sua distro. Isso pode ser construído no Linux e no Windows usando WSL.
git clone https://github.com/docandrew/CuBit.git
make
Isso construirá o cúbito e criará um arquivo .ISO de CD ao vivo. O ISO pode ser montado e executado no VirtualBox, Bochs ou Qemu.
| Tarefa | Comando |
|---|---|
| Crie documentação (em Build/Docs) | make docs |
| Correr proversores | make prove |
| Crie documentação HTML | make html |
A ADA é insensível a minúsculas (o que é meio legal, honestamente), mas torna todos os símbolos exportados inferiores, portanto, qualquer coisa em arquivos .ASM que referenciam que o símbolo precisa usar a versão de baixa qualidade ou especificar o nome externo_name para o símbolo em um aspecto.
Os tipos enumerados que contêm "orifícios" fazem com que o mosquito insira verificações em tempo de execução para valores válidos ao atribuí-los. Não consegui encontrar um Pragma para desativar essas verificações. Eventualmente, escreveremos funções de manipulador de exceção que podem executar os cheques ou causar um pânico no kernel, mas, por enquanto, preenchem os orifícios com valores óbvios como Bad_1, Bad_2, etc.
Certifique -se de que as provas sejam executadas (usando make prove ) antes de enviar solicitações de tração. Seja muito cauteloso com a anotação de Pragma para desativar os avisos. gnatprove fornecerá alguns avisos espúrios como statement has no effect ou unused assignment que sejam claramente incorretas, mas verifique novamente.
Os registros variantes parecem inserir algum cruzamento extra no registro subjacente, mesmo que o Pragma Pack seja usado. Não use -os como "sobreposições" sobre a memória existente, por exemplo, as tabelas ACPI. Você terá problemas de alinhamento com alguns dos campos e acabará com dados de junk. O mesmo acontece mesmo para registros não variantes que usam discriminantes.
Max_phys_alloc - definido em config.ads, esta é a memória física máxima suportada por cúbito. Lá apenas o limite aqui é prático, pois o alocador de botas de inicialização está configurado para criar bitmaps para toda essa memória (128 GIB), que ocupa uma quantidade razoável de espaço. (Podemos considerar apenas reservar uma pequena seção de heap linear para uso do kernel e construir um melhor alocador para que esse limite não seja mais um fator.)
Max_phys_address - a memória física teórica máxima suportada pelo nosso hardware (se usarmos o mapeamento linear). No caso de x86-64, temos endereços virtuais canônicos de 48 bits; portanto, se queremos que toda a memória física seja mapeada na memória virtual, ficamos com cerca de 280 TB, que precisamos dividir na metade superior, então 128tib. Observe que a Intel está analisando o endereçamento de 56 bits com uma tabela de páginas de cinco níveis, para que esse número possa mudar em breve para x86-64.
Max_phys_addressable - o melhor endereço de memória física em nosso sistema que detectamos em tempo de execução. Áreas de memória de mapa linear até este ponto (começando em 0xffff_8000_0000_0000).
Max_phys_usable - o melhor endereço de RAM utilizável em nosso sistema . Pode haver orifícios dentro disso, por isso não podemos alocar cegamente a memória por baixo desse limite, mas seria esperado que um alocador físico lide com endereços até este ponto.
Algumas das estruturas utilizadas, como as tabelas GDT e Page, precisam ser configuradas no boot.asm antes de alternar para o modo longo. Estes são chamados de tabelas GDT e página "Bootstrap", respectivamente. Há também o alocador de memória física "Boot". Posteriormente, aumentamos novamente a totalidade da memória física na metade superior do kernel, juntamente com um novo GDT no segment.adb . Estes são chamados de "Tabelas da página do kernel" e "Kernel GDT".
O MAP de identidade da página de bootstrap é o primeiro 1g de memória e depois mapeá-lo novamente na metade superior, começando em 0xffff_8000_0000_0000. Portanto, o P2V e o V2P (físico-virtual, virtual-físico) funcionam por adição e subtração simples, porque você pode acessar a memória física em, por exemplo, 0x0000_0000_Dead_Beef nos endereços virtuais 0x0000_00_Dead_Beef e também 0xffff_8000_Dead_Beadef.
Quando mudamos para o mapa do kernel, não podemos mais abordar a memória usando endereços físicos diretos. Em vez disso, um endereço físico específico deve ser acessado usando o endereço mapeado linear em 0xffff_8000_0000_0000. Nós map linear toda a memória física em 0xffff_8000_0000_0000 a 0xffff_8fff_ffff_ffff.
Observe que, devido ao X86-64 ABI, o kernel deve estar ligado no 2GIB superior da memória ao usar mcmodel = kernel. Portanto, nossas tabelas de página também precisam de um mapeamento para 0xffff_ffff_8xxx_xxxx -> 0x0000_0000_0xxx_xxxx.
Sim! Tentei tornar o código muito amigável com os que não estão familiarizados com Cubitos, Ada ou Spark. Por favor, experimente em uma VM e deixe -me saber o que você pensa. Feedback negativo e críticas construtivas também são úteis.
É fortemente documentado e os colaboradores são bem-vindos!
Os Cubitos podem ser um bom ponto de partida para a pesquisa acadêmica. O Spark tem uma escotilha de fuga para realizar provas no Coq, portanto, para os colaboradores mais matemáticos que desejam um bom desafio, veja o que você pode provar sobre os Cubitos!
O Spark usa a estrutura do WHY3 e o solucionador do Z3 SMT. Os solucionadores SMT bons e rápidos são sempre uma área de interesse, e os Cubitos podem ser uma boa maneira de compará-los a outros usos do mundo real.
| Elemento de código | Convenção |
|---|---|
| Palavras -chave ADA (tipo, para, loop, etc.) | Todas as minúsculas |
| Tipos (MultiBootStruct, PagetableEntry, etc.) | Camelcase capitalizado |
| Nomes de pacotes | Camelcase capitalizado |
| Variáveis, funções (Kmain, Tohexstring, etc.) | Camelcase não -capitalizado |
| Constantes (lt_gray, kern_base, etc.) | Todas as tampas |
| Nomes de arquivos | tudo mais baixo ou cobra_case |
Nota: Se a interface com um componente externo, digamos MultiBoot, os nomes de variáveis deverão usar a mesma convenção que a API desse componente. Por exemplo, a estrutura de informações multiboot tem campos como mem_lower, etc.
Usaremos esses nomes literalmente aqui para facilitar a referência de documentação. Esta não é uma regra dura e rápida. Se os nomes da API forem excessivamente, confusos, usem uma notação húngara estranha ou forem de outra forma, fique à vontade para renomeá-los no código da ADA.
Evite abreviações excessivamente de terra. Termos comuns como "Kern" para "kernel" ou "Mem" para memória, estão bem se não houver ambiguidade. "VM" para memória virtual pode ser confundida com "Máquina Virtual", então prefira "VirtMem" ou apenas soletrá -la completamente. Os acrônimos só devem ser usados se forem amplamente utilizados ou uma convenção do hardware subjacente, como o ACPI,
Converta as guias em quatro espaços.
Os compromissos devem ser finais da linha LF.
Evite cláusulas de "uso", a menos que sejam necessárias de outra forma para os operadores e, em seguida, limite seu uso a subprogramas específicos quando necessário ou use a cláusula "Tipo de uso". Isso força o pacote de um tipo a ser explicitamente soletrado e, portanto, o pacote pode ser facilmente referenciado e saltado em um editor. Exceções a esta regra são:
Use o termo "quadro" ao se referir à memória física e "página" ao discutir a memória virtual.
Por favor, use nomes descritivos para variáveis, tipos, etc. Não temos espaço no disco rígido para armazenar o código -fonte; portanto, use nomes mais longos (dentro do motivo) se eles ajudarem a promover a compreensão do código.
Tente manter as linhas com menos de 80 chars de largura em sua maior parte, mas se isso afetar negativamente a legibilidade para quebrar uma linha, não há problema em prender o limite de 80 largura. Os comentários de fim de linha podem passar 80 se prejudicar o fluxo do código para colocá -los em sua própria linha.
Se o modo Spark estiver desativado em um corpo do subprograma, adicione um comentário por quê. Isso pode ser perfeitamente válido, ou seja, embutido ASM. No entanto, tente e reestruturar o código para ativar o modo Spark - especialmente as especificações do subprograma. Às vezes, isso pode ser um pouco doloroso, ou seja, mudando funções para procedimentos com vários parâmetros "Out".
Celebre o espaço em branco. Deixe o código respirar. Use duas novas linhas após cada corpo do subprograma. Uma nova linha após um corpo do subprograma é apropriada se os subprogramas forem pequenas variações entre si, ou seja, argumentos sobrecarregados e estiverem agrupados de perto para esclarecer seu relacionamento.
Use muitos comentários, no formato GnatDoc. Obviamente, essa é uma área em que as opiniões diferem, mas acredito que tratar o sistema operacional como uma biblioteca com documentação completa incentiva a correção e a torna mais amigável a novos colaboradores. Isso também facilita a documentação automaticamente-generativa, em vez de manter a documentação separadamente. Todos conhecemos uma boa API quando vemos uma.
"Mas o código mudará e os comentários ficarão desatualizados!"
Então ... uh ... apenas atualize os comentários!
Emprestando uma página dos manuais do operador de aeronaves:
Nota - denota informações consideradas importantes para enfatizar
CUIDADO - denota informações que, se não consideradas, podem resultar em falhas no sistema ou operação incorreta.
Aviso - denota informações que, se não consideradas, podem resultar em perda de dados do usuário ou danos ao hardware subjacente.
| Termo usado | Tamanho |
|---|---|
| Mordidela | 4 bits |
| Byte | 8 bits |
| Palavra | 16 bits |
| DWORD (palavra dupla) | 32 bits |
| QWORD (Quad-Word) | 64 bits |
Isso está incluído aqui para evitar a confusão usada ao descrever interfaces ou componentes de hardware em que "Word" pode significar algo diferente de 16 bits. Sempre queremos dizer de 16 bits no código de cúbitos ao usar "Word" em comentários, etc.
De um modo geral, indicaremos explicitamente a duração de um tipo de dados usando o pacote ADA Interfaces, ou seja, UNSIGNED_8, UNSIGNED_32, etc. Os termos acima podem ser usados nos comentários, em vez de ortografia "valor de 32 bits", por exemplo.
As funções Spark não podem ter efeitos colaterais, muitas vezes, um procedimento é usado, e é necessário um parâmetro out para o resultado, em vez de apenas retornar o resultado. É um pouco doloroso atribuir temporários para todos os resultados do procedimento.
As definições de constantes não podem ser (facilmente) compartilhadas entre o código da ADA e os arquivos de montagem, portanto, alguns deles são duplicados. Eu tentei usar todas as constantes usadas pelos arquivos de montagem em cubit.inc, juntamente com uma nota de onde pode ser duplicado no código da ADA. Certifique -se de que, se você alterar algum desses valores, eles sejam alterados nos dois lugares. Se você apresentar sua própria constante que é compartilhada entre a Assembly e o Código ADA - verifique se eles usam o mesmo nome!
O Cubit divide a área de pilha estática em pedaços por CPU, cada um dos quais é dividido nas pilhas primárias e secundárias para essa CPU. A pilha primária cresce, a pilha secundária cresce. O ponteiro da pilha primária é definido para a CPU principal no boot.asm e configurado para cada CPU adicional quando inicializa em boot_ap.asm.
STACK_TOP +-----------------------+
| |
| CPU 0 Primary Stack |
| |
+-----------------------+
| CPU 0 Secondary Stack |
+-----------------------+
| |
| CPU 1 Primary Stack |
| |
+-----------------------+
| CPU 1 Secondary Stack |
+-----------------------+
| . |
| . |
| . |
+-----------------------+
| |
| CPU N Primary Stack |
| |
+-----------------------+
| CPU N Secondary Stack |
STACK_BOTTOM +-----------------------+
A chamada secundária da pilha SS_init é feita durante cada inicialização da CPU. Os transbordamentos secundários da pilha devem ser detectados em tempo de execução, no entanto, tenha cuidado. Durante os syscalls e interrupções, a pilha do kernel do processo pode estar em uso, que não possui uma pilha secundária.
X significa acabamento- significa em andamento [ ] There are a lot of potential circular dependencies for just "proof stuff",
i.e. preconditions where we don't want to call a blockingSleep until
interrupts are enabled -> don't want to enable interrupts until the
interrupt vector is loaded -> interrupt vector will update the value that
blockingSleep depends on. It might make sense to keep a big "state"
.ads file with nothing but Ghost variables used in SPARK proofs. It would
not have any dependencies itself, but could be included by everything else
to update their states. Downside is that it might grow huge and unwieldy,
and sorta breaks encapsulation. Might make proofs take a long time too.
[X] Put the stack at a more sensible location
[X] Per-CPU Stacks
[X] Secondary Stacks
[X] Print out full register dump with exceptions
[-] Make type-safe more of the address/number conversions I'm doing.
[-] Error-handling. Need to formalize the mechanism, could get very messy with MP.
[X] Exceptions (Last chance handler)
[ ] Broadcast panic to other CPUs
[ ] Figure out a keyboard scancode -> key array scheme with a future eye towards
internationalization. Maybe just use SDL's keyboard handling scheme and let them sort it out.
[X] Physical memory allocator
[X] Boot-mem allocator using bitmaps
[X] Boot phys memory allocator
[X] Keep track of free space as we allocate/free
[X] Buddy allocator
[X] Virtual memory mapper
[X] Mark 0 page as not present
[X] Re-map kernel pages with appropriate NXE bits, etc. depending on region.
[-] Virtual memory allocator
[-] Demand paging.
[-] Processes / Threads
[ ] Kernel Tasks
[X] Usermode
[-] Scheduler
[ ] Implement killing processes.
[ ] Suspend
[ ] Sleep / Wakeup
[-] ACPI tables
[X] Find RSDT/XSDT
[X] Sane code for parsing these.
[-] APIC
[ ] HPET
[ ] MCFG - PCI express
[ ] SSDT?
[-] I/O APIC
[-] Multiprocessing
[ ] MP Tables (necessary?)
[-] LAPIC
[ ] X2APIC
[ ] Hardware
[X] MSRs
[-] Full CPUID detection
[-] Disk drivers
[ ] MBR/GPT Partition Table
[-] PCI bus
[-] Hard Drives
[-] ATA
[-] AHCI
[ ] PCI express
[ ] Enhanced Configuration Access Mechanism (ECAM) via MCFG tables
[ ] NVMe
[ ] Sound
[ ] Video Drivers
[-] VESA Modes
[-] Filesystem / VFS Layer
[ ] Develop FS-agnostic set of VFS hooks to syscalls
[ ] Develop Drive-agnostic set of VFS hooks to hardware
[-] Ext2
[ ] Networking
[ ] Interface driver
[ ] TCP/IP Stack - RecordFlux should help here.
[ ] Security
[ ] ASLR / KASLR
[ ] Disable certain branch speculation behavior (see x86.MSR)
[ ] if processor supports IBRS in ARCH_CAPABILITIES
[-] KPTI
[ ] Disable KPTI if ARCH_CAPABILITIES MSR indicates not susceptible to RDCL
[ ] Sensible Kernel-Mode-Setting / Framebuffer / Compositor arrangement
[ ] Wow Factor / Eye Candy
[ ] Sweet GRUB splash screen w/ logo
[-] Syscalls
[X] SYSCALL/SYSRET working
[ ] Microkernel Concepts?
[ ] User-mode drivers?
[ ] IPC?
[-] More formal proofs of kernel correctness
[ ] Preventing race conditions - may not be feasible outside of
Ravenscar profile, which doesn't really apply to us.
[-] Implement more of the Ada standard library, especially for Tasks.
[-] Init model - should this look like UNIX? Something else?
[ ] Security Model
[-] Codify it
[ ] Prove it
[ ] Implement it
[-] IMGUI framework
[-] Make all package names Uppercase
[-] Rename all setupXYZ to just setup, since package name is already there.
[X] New Makefile
[-] Use gnatdoc format in comments
[ ] Edit gnatdoc format so NOTE, CAUTION, WARNING shows up as different
colors.
[ ] Edit gnatdoc format to ignore the leading and trailing horizontal rules
[-] Work out a CI/CD pipeline
[ ] Proof Step
[ ] Unit Testing
[X] Build
[ ] Integration/Functional Testing
[X] Generate Documentation
[-] Build installers, isos, etc.
[ ] Write unit tests
[ ] Fuzzing
[ ] Integration tests that run in the OS.
| Tarefa | Comando |
|---|---|
| Crie documentação (em Build/Docs) | make docs |
| Correr proversores | make prove |
| Crie documentação HTML | make html |
Você pode criar uma imagem de disco Ext2 e lê -la em cúbito com esses comandos, mostrados aqui para um disco de 128 MB:
dd if=/dev/zero of=vhd.img bs=1M count=128
mkfs -t ext2 -b 4096 vhd.img
mkdir vhd
mount -t auto -o loop vhd.img vhd
Agora você tem um sistema de arquivos vazio no vhd/ para o qual você pode adicionar arquivos, mexer com permissões, etc. Quando terminar, desmonte a imagem. Observe que a implementação do Cubit Ext2 atualmente suporta apenas tamanhos de bloco 4K.
umount vhd
Agora você tem uma imagem de disco que pode converter para o formato VirtualBox com:
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
Você pode adicionar o novo disco em armazenamento -> IDE Controller nas configurações da VM. Você provavelmente vai querer usar o chipset ICH6. Atualmente, o Cubit usa o método PIO antigo para E/S ATA. Se você criar uma imagem de disco e adicioná -la ao controlador IDE com um chipset diferente, as leituras provavelmente falharão.
Observe que o Cubit acabou de ler o Ext2 Soberblock atualmente, mas o progresso está sendo feito com o suporte básico do sistema de arquivos.
Por favor, experimente diferentes quantidades de RAM, número de CPUs, etc.
O VirtualBox é uma boa ferramenta para testar, no entanto, o Qemu é bom quando você precisa usar o GDB para rastrear certos problemas. Observe que a Cubit utiliza alguns recursos de CPU razoavelmente recentes; portanto, você deve dizer a Qemu para usar um chipset e CPU mais recentes. As opções -machine q35 e -cpu Broadwell parecem funcionar bem.
Comando qemu sem depurador:
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
Dicas do GDB:
Registre add'l Info: rt Registros: rg64 Stack Trace: k
Para usar o qemu para depurar:
qemu-system-x86_64 -machine q35 -cpu Broadwell -s -S -m 4G -cdrom pathtocubit_kernel.iso -serial stdio
Qemu começará em um estado pausado enquanto aguarda o depurador.
Em seguida, execute o GDB: gdb cubit_kernel (NOTA: NO ".ISO" Aqui, queremos o próprio arquivo de objeto do kernel, que contém símbolos de depuração)
Para conectar -se ao QEMU: target remote localhost:1234 Uso (gdb) c para continuar.
A partir daqui, os comandos normais do GDB funcionam, como break , x , etc.
Observe que o Hyper-V não parece inicializar o .iso atualmente. Outras plataformas de virtualização ou emulação são recomendadas.
git clone https://github.com/Componolit/RecordFlux
install >= Python 3.6
install pip
install virtualenv if Python 3 not the default
source bin/activate
python setup.py build
python setup.py install
Now the rflx script at bin/rflx should work.
