CuBit
1.0.0
Cubitos es un sistema operativo de propósito general de 64 bits, de 64 bits, (parcialmente), verificado formalmente, actualmente para la arquitectura X86-64.
CUBIT está escrito en el dialecto Spark de Ada.
¡CUBIT es un trabajo en progreso! Dicho esto, por favor dale un giro. ¡Los contribuyentes bienvenidos!
gprbuild , gnat , etc. en su $PATHPara crear Bootable .ISO, también necesitará:
Dependencias: necesitará el compilador GNAT 2020, y si desea construir el CD en vivo, necesitará las herramientas Xorriso y Grub-Mkrescue , y posiblemente Grub-PC-Bin dependiendo del entorno de emulador/virtualización que esté utilizando. Probablemente se proporcionen en el Administrador de paquetes de su distribución. Esto se puede construir en Linux y en Windows con WSL.
git clone https://github.com/docandrew/CuBit.git
make
Esto construirá CUBIT y creará un archivo .ISO en vivo. El ISO se puede montar y ejecutar en Virtualbox, Bochs o Qemu.
| Tarea | Dominio |
|---|---|
| Crear documentación (en Build/Docs) | make docs |
| Manejar | make prove |
| Construir documentación HTML | make html |
ADA es insensible al caso (lo cual es un poco agradable, honestamente), pero hace que todos los símbolos exportados sean más bajos, por lo que cualquier cosa en .men, que referencia ese símbolo, necesita usar la versión de menor carga, o especificar el nombre externo para el símbolo en un aspecto.
Los tipos enumerados que contienen "agujeros" hacen que GNAT inserta verificaciones de tiempo de ejecución para valores válidos al asignarlos. No pude encontrar un pragma para deshabilitar estos controles. Eventualmente escribiremos funciones del controlador de excepción que pueden realizar los cheques o causar un pánico del núcleo, pero por ahora, llene los agujeros con valores obvios como Bad_1, Bad_2, etc.
Asegúrese de que se ejecuten las pruebas (usando make prove ) antes de enviar solicitudes de extracción. Sea muy cauteloso sobre el anotado de Pragma para deshabilitar las advertencias. gnatprove dará algunas advertencias espurias como statement has no effect o unused assignment que sean claramente incorrectas, pero por favor verifique estas.
Los registros de variantes parecen insertar un poco de Cruft adicional en el registro subyacente, incluso si se usa Pragma Pack. No los use como "superposiciones" además de la memoria existente, por ejemplo, las tablas ACPI. Tendrá problemas de alineación con algunos de los campos y terminará con datos basura. Lo mismo es cierto incluso para los registros no variantes que usan discriminantes.
Max_phys_alloc - Establecer en config.ads, esta es la memoria física máxima que admite Cubit. El único límite aquí es práctico, ya que el asignador de MEM de arranque está configurado para crear mapas de bits para toda esta memoria (128 GIB), lo que ocupa una buena cantidad de espacio. (Podemos considerar simplemente dejar de lado una pequeña sección de montón lineal para uso del núcleo y construir un mejor asignador para que este límite ya no sea un factor).
MAX_PHYS_ADDRESS: la memoria física teórica máxima que nuestro hardware admite (si usamos mapeo lineal). En el caso de X86-64, tenemos direcciones virtuales canónicas de 48 bits, por lo que si queremos que toda la memoria física se asigne en la memoria virtual, nos queda aproximadamente 280TB, que necesitamos dividir para usar en la mitad más alta, por lo que 128tib. Tenga en cuenta que Intel está buscando direccionamiento de 56 bits con una tabla de páginas de cinco niveles, por lo que este número puede cambiar pronto para x86-64.
Max_Phys_Addressable: la dirección de memoria física superior en nuestro sistema que detectamos en tiempo de ejecución. Lineal-Map Memory Áreas hasta este punto (comenzando en 0xffff_8000_0000_0000).
MAX_PHYS_USABLE: la dirección de RAM utilizable superior en nuestro sistema . Puede haber agujeros dentro de esto, por lo que no podemos asignar ciegamente la memoria debajo de este límite, pero se espera que un asignador físico manejemos direcciones hasta este punto.
Algunas de las estructuras utilizadas, como el GDT y las tablas de página, deben configurarse en boot.asm . Estos se denominan Tablas y tablas de página "Bootstrap", respectivamente. También está el asignador de memoria física de "arranque". Más tarde, volvemos a mapear la totalidad de la memoria física en la mitad más alta del núcleo junto con un nuevo GDT en segment.adb . Estos se llaman "Tablas de página del núcleo" y "GDT del kernel".
Las tablas de página de Bootstrap mapea el primer 1 g de memoria, y luego mapee nuevamente en la mitad superior, comenzando en 0xffff_8000_0000_0000. Entonces, el P2V y V2P (físico a virtual, virtual a físico) funcionan mediante una simple adición y sustracción porque puede acceder a la memoria física en, por ejemplo, 0x0000_0000_dead_beef en las direcciones virtuales 0x0000_0000_dead_beef y también 0xffff_8000_dead_beef.
Cuando cambiamos al mapa del núcleo, ya no podemos abordar la memoria utilizando direcciones físicas directas. En su lugar, se debe acceder a una dirección física específica utilizando la dirección lineal mapeada en 0xffff_8000_0000_0000. Lineal-Map toda la memoria física en 0xffff_8000_0000_0000 a 0xffff_8fff_ffff_ffff.
Tenga en cuenta que debido al X86-64 ABI, el núcleo debe estar vinculado en el 2GIB superior de la memoria cuando se usa McModel = kernel. Por lo tanto, nuestras tablas de página también necesitan una asignación para 0xffff_ffff_8xxx_xxxx -> 0x0000_0000_0xxx_xxxxx.
¡Sí! He tratado de hacer que el código sea muy amigable para aquellos que no están familiarizados con Cubitos, ADA o Spark. Por favor, pruébelo en una VM y hágame saber lo que piensa. La retroalimentación negativa y la crítica constructiva también son útiles.
¡Es muy documentado y los contribuyentes son bienvenidos!
Los cubitos pueden ser un buen punto de partida para la investigación académica. Spark tiene una escotilla de escape para realizar pruebas en COQ, por lo que para los contribuyentes más matemáticos que quieren un buen desafío, ¡vea lo que puede probar sobre Cubitos!
Spark usa Why3 Framework y Z3 SMT Solver. Los solucionadores SMT buenos y rápidos son siempre un área de interés, y los cubitos podrían ser una buena manera de compararlos con otros usos del mundo real.
| Elemento de código | Convención |
|---|---|
| Palabras clave ADA (tipo, para, bucle, etc.) | todo minúscula |
| Tipos (Multibootstruct, PagetableEntry, etc.) | Camelcase capitalizado |
| Nombres de paquetes | Camelcase capitalizado |
| Variables, funciones (KMAIN, TOHEXSTRING, etc.) | Camelcase nopitalizado |
| Constantes (lt_gray, kern_base, etc.) | Todas las gorras |
| Nombre de archivo | todos más bajos o serpientes_case |
Nota: Si se interfiere con un componente externo, digamos Multiboot, entonces los nombres de variables deben usar la misma convención que la API de ese componente. Por ejemplo, la estructura de información multibotual tiene campos como MEM_LOWER, etc.
Usaremos esos nombres literalmente aquí para facilitar la referencia de documentación. Esta no es una regla dura y rápida. Si los nombres de la API son excesivamente tritulados, confusos, usan una extraña notación húngara o son tontos, entonces no dude en cambiarlos en el código ADA.
Evite las abreviaturas excesivas. Los términos comunes como "kern" para "kernel", o "mem" para la memoria, están bien si no hay ambigüedad. "VM" para la memoria virtual se puede confundir con la "máquina virtual", así que prefiere "virtmem" o simplemente explicarla por completo. Los acrónimos solo deben usarse si se usan ampliamente o una convención del hardware subyacente, como ACPI,
Convierta las pestañas en cuatro espacios.
Los compromisos deben ser las terminaciones de línea LF.
Evite las cláusulas de "usar" a menos que sea necesario para los operadores y luego, limite su uso a subprogramas específicos cuando sea necesario o use la cláusula de "Uso de tipo". Esto obliga al paquete de un tipo a explicarse explícitamente, por lo que el paquete puede ser fácilmente referenciado y saltado en un editor. Las excepciones a esta regla son:
Use el término "marco" cuando se refiera a la memoria física y a la "página" al discutir la memoria virtual.
Utilice los nombres descriptivos para variables, tipos, etc. No nos faltan espacio en el disco duro para almacenar el código fuente, por lo que usa nombres más largos (dentro de lo razonable) si ayudan a fomentar la comprensión del código.
Intente mantener las líneas de menos de 80 caracteres de ancho en su mayor parte, pero si afecta negativamente la legibilidad para romper una línea, entonces está bien reventar el límite de los 80 en todo. Los comentarios finales de línea pueden pasar más de los 80 si perjudica el flujo del código para ponerlos en su propia línea.
Si el modo Spark está deshabilitado en un cuerpo de subprograma, agregue un comentario por qué. Esto puede ser perfectamente válido, es decir, ASM en línea. Sin embargo, intente reestructurar el código para habilitar el modo Spark, especialmente las especificaciones de subprograma. A veces, esto puede ser un poco doloroso, es decir, cambiando las funciones a los procedimientos con múltiples parámetros "fuera".
Celebra el espacio en blanco. Deje que el código respire. Use dos líneas nuevas después de cada cuerpo de subprograma. Una nueva línea después de un cuerpo de subprograma es apropiado si los subprogramas son variaciones menores entre sí, es decir, argumentos sobrecargados, y se agrupan estrechamente para aclarar su relación.
Use muchos comentarios, en formato GnatDoc. Obviamente, esta es un área donde las opiniones difieren, pero creo que tratar el sistema operativo como una biblioteca con documentación exhaustiva fomenta la corrección y lo hace más amigable para los nuevos contribuyentes. Esto también facilita la documentación de generación automática, en lugar de mantener la documentación por separado. Todos conocemos una buena API cuando vemos una.
"¡Pero el código cambiará y los comentarios estarán desactualizados!"
Entonces ... uh ... ¡solo actualiza los comentarios!
Tomar prestado una página de los manuales del operador de aeronaves:
Nota: denota información que se considera importante para enfatizar
PRECAUCIÓN: denota información que, si no se considera, puede provocar bloqueos del sistema o operación incorrecta.
Advertencia: denota información que, si no se considera, puede dar lugar a la pérdida de datos del usuario o daños al hardware subyacente.
| Término utilizado | Tamaño |
|---|---|
| Picar | 4 bits |
| Byte | 8 bits |
| Palabra | 16 bits |
| DWORD (doble palabra) | 32 bits |
| QWORD (Quad-Word) | 64 bits |
Esto se incluye aquí para evitar la confusión utilizada al describir interfaces o componentes de hardware donde la "palabra" puede significar algo más que 16 bits. Siempre nos referimos a 16 bits en el código CUBIT cuando se usa "palabra" en comentarios, etc.
En términos generales, estableceremos explícitamente la longitud de un tipo de datos utilizando el paquete de interfaces ADA, es decir, unsigned_8, unsigned_32, etc. Los términos anteriores se pueden usar en comentarios en lugar de deletrear "valor de 32 bits", por ejemplo.
Las funciones de Spark no pueden tener efectos secundarios, por lo que muchas veces, se usa un procedimiento, y se requiere un parámetro de salida para el resultado, en lugar de simplemente devolver el resultado. Es un poco doloroso asignar temporales para todos los resultados del procedimiento.
Las definiciones de constantes no se pueden compartir (fácilmente) entre el código ADA y los archivos de ensamblaje, por lo que algunas de ellas están duplicadas. He tratado de obtener todas las constantes utilizadas por los archivos de ensamblaje en Cubit.InC, junto con una nota de dónde podría duplicarse en el código ADA. Asegúrese de que si cambia alguno de estos valores, se cambian en ambos lugares. Si presenta su propia constante que se comparte entre el ensamblaje y el código ADA, ¡asegúrese de que usen el mismo nombre!
CUBIT divide el área de la pila estática en trozos per-CPU, cada uno de los cuales se divide en las pilas primarias y secundarias para esa CPU. La pila primaria crece, la pila secundaria crece. El puntero de la pila primaria está configurado para la CPU principal en el arranque.
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 +-----------------------+
La llamada de pila secundaria SS_INIT se realiza durante cada arranque de la CPU. Los desbordamientos de pila secundarios deben detectarse en tiempo de ejecución, sin embargo, use precaución. Durante las syscalls e interrupciones, la pila del núcleo del proceso puede estar en uso, lo que no tiene una pila secundaria.
X significa terminado- Medios en progreso [ ] 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.
| Tarea | Dominio |
|---|---|
| Crear documentación (en Build/Docs) | make docs |
| Manejar | make prove |
| Construir documentación HTML | make html |
Puede crear una imagen de disco EXT2 y leerla en CUBIT con estos comandos, que se muestra aquí para un 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
Ahora tiene un sistema de archivos vacío en vhd/ al que puede agregar archivos, jugar con permisos, etc. Cuando haya terminado, desmonte la imagen. Tenga en cuenta que la implementación EXT2 de CUBIT actualmente admite solo tamaños de bloque 4K.
umount vhd
Ahora tiene una imagen de disco con la que puede convertir al formato VirtualBox con:
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
Puede agregar el nuevo disco en el controlador de almacenamiento -> IDE en su configuración de VM. Probablemente querrás usar el chipset ICH6. CUBIT utiliza actualmente el método antiguo de PIO para ATA I/O. Si crea una imagen de disco y la agrega al controlador IDE con un chipset diferente, las lecturas probablemente fallarán.
Tenga en cuenta que Cubit solo lee el Superblock EXT2 actualmente, pero el progreso se está haciendo con el soporte básico del sistema de archivos.
Experimente con diferentes cantidades de RAM, número de CPU, etc.
Virtualbox es una buena herramienta para las pruebas, sin embargo, QEMU es bueno cuando necesita usar GDB para rastrear ciertos problemas. Tenga en cuenta que Cubit utiliza algunas características de CPU bastante recientes, por lo que querrá decirle a QEMU que use un chipset y CPU más nuevos. Las opciones -cpu Broadwell -machine q35 -CPU -CPU parecen funcionar bien.
Comando QEMU sin depurador:
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
Consejos de GDB:
Registre la información adicional: rt RECINTERS: rg64 PISTA TRACE: k
Para usar QEMU para depurar:
qemu-system-x86_64 -machine q35 -cpu Broadwell -s -S -m 4G -cdrom pathtocubit_kernel.iso -serial stdio
QEMU comenzará en un estado pausado mientras espera al depurador.
Luego ejecute GDB: gdb cubit_kernel (nota: No ".ISO" Aquí, queremos el archivo de objeto del núcleo en sí, que contiene símbolos de depuración)
Para conectarse a QEMU: target remote localhost:1234 Uso (gdb) c para continuar.
Desde aquí, los comandos normales de GDB funcionan, como break , x , etc.
Tenga en cuenta que Hyper-V no parece arrancar el .iso actualmente. Se recomiendan otras plataformas de virtualización o emulación.
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.
