CuBit
1.0.0
Cubitos est un système d'exploitation à usage général multipro-processeur, 64 bits et partiellement), actuellement pour l'architecture x86-64.
La cubit est écrite dans le dialecte Spark d'Ada.
Cubit est vraiment un travail en cours! Cela dit, veuillez lui faire un tour. Les contributeurs sont les bienvenus!
gprbuild , gnat , etc. dans votre $PATHPour créer un boobleable .iso, vous aurez également besoin:
Dépendances: vous aurez besoin du compilateur GNAT 2020, et si vous souhaitez construire le live-cd, vous aurez besoin des outils Xorriso et Grub-Mkrescue , et peut-être Grub-PC-Bin en fonction de l'émulateur / environnement de virtualisation que vous utilisez. Ceux-ci sont probablement fournis dans le gestionnaire de packages de votre distribution. Cela peut être construit en Linux et sous Windows à l'aide de WSL.
git clone https://github.com/docandrew/CuBit.git
make
Cela construira Cubit et créera un fichier .iso en direct. L'ISO peut être monté et exécuté dans VirtualBox, Bochs ou Qemu.
| Tâche | Commande |
|---|---|
| Créer une documentation (dans Build / Docs) | make docs |
| Exécuter des proverses | make prove |
| Construire une documentation HTML | make html |
L'ADA est insensible à la casse (ce qui est plutôt agréable, honnêtement), mais il rend tous les symboles exportés dans un cas inférieur, donc tout dans les fichiers .asm qui fait référence à ce symbole pour utiliser la version basée inférieure, ou spécifiez le nom externe_name pour le symbole dans un aspect.
Les types énumérés contenant des "trous" font que le GNAT insérer les vérifications d'exécution des valeurs valides lors de ces attributions. Je n'ai pas trouvé de pragma pour désactiver ces chèques. Finalement, nous rédigerons des fonctions de gestionnaire d'exceptions qui peuvent soit effectuer les contrôles, soit provoquer une panique du noyau, mais pour l'instant, remplissez les trous de valeurs évidentes comme Bad_1, Bad_2, etc.
Veuillez vous assurer que les épreuves sont exécutées (en utilisant make prove ) avant de soumettre des demandes de traction. Soyez très prudent à propos de Pragma annoter pour désactiver les avertissements. gnatprove donnera des avertissements parasites comme statement has no effect ou unused assignment qui sont clairement incorrectes, mais veuillez les revérifier.
Les enregistrements variants semblent insérer une crupt supplémentaire dans l'enregistrement sous-jacent, même si le pack Pragma est utilisé. Ne les utilisez pas comme des «superpositions» en plus de la mémoire existante, par exemple les tables ACPI. Vous aurez des problèmes d'alignement avec certains champs et vous vous retrouverez avec des données indésirables. Il en va de même même pour les enregistrements non variés qui utilisent des discriminants.
MAX_PHYS_ALLOC - Défini dans config.ads, c'est la mémoire physique maximale prise en charge. Il n'y a que la limite ici est pratique, car l'allocateur Boot MEM est configuré pour créer des bitmaps pour toute cette mémoire (128 GIB), qui occupe une bonne quantité d'espace. (Nous pouvons envisager simplement de mettre de côté une petite section de tas de mappage linéaire pour une utilisation du noyau et de construire un meilleur allocateur afin que cette limite ne soit plus un facteur.)
MAX_PHYS_ADdress - La mémoire physique théorique maximale que notre matériel prend en charge (si nous utilisons le mappage linéaire). Dans le cas de x86-64, nous avons des adresses virtuelles canoniques 48 bits, donc si nous voulons que toute la mémoire physique soit cartographiée en mémoire virtuelle, nous nous retrouvons avec environ 280 To, que nous devons nous diviser pour utiliser dans la moitié supérieure, donc 128tib. Notez qu'Intel examine l'adressage 56 bits avec un tableau de page à cinq niveaux, donc ce numéro peut changer bientôt pour x86-64.
MAX_PHYS_ADDRESSABLE - L'adresse de mémoire physique supérieure de notre système que nous détectons à l'exécution. Nous avons des zones de mémoire linéaire jusqu'à ce point (à partir de 0xffff_8000_0000_0000).
MAX_PHYS_USABLE - L'adresse RAM utilisable supérieure de notre système . Il peut y avoir des trous à l'intérieur, nous ne pouvons donc pas allouer aveuglément la mémoire sous cette limite, mais un allocateur physique devrait gérer les adresses jusqu'à ce point.
Certaines des structures utilisées, comme les tables GDT et Page, doivent être configurées dans boot.asm avant de passer en mode long. Ceux-ci sont appelés les tables GDT et pages "bootstrap" respectivement. Il y a aussi l'allocateur de mémoire physique "démarrage". Plus tard, nous refaisons l'intégralité de la mémoire physique dans la moitié supérieure du noyau avec un nouveau GDT dans segment.adb . Ceux-ci sont appelés les "tables de page du noyau" et "Kernel GDT".
La page bootstrap tables à l'identité MAP le premier 1 g de mémoire, puis la mappez à nouveau dans la moitié supérieure, à partir de 0xffff_8000_0000_0000. Ainsi, les P2V et V2P (physiques à virtuel, virtuels à physique) fonctionnent par addition et soustraction simples car vous pouvez accéder à la mémoire physique à, par exemple, 0x0000_0000_DEAD_BEEF aux adresses virtuelles 0x0000_0000_DEAD_BEEF et également 0xFFFF_8000_DEAD_BEEF.
Lorsque nous passons à la carte du noyau, nous ne pouvons plus aborder la mémoire à l'aide d'adresses physiques directes. Au lieu de cela, une adresse physique spécifique doit être accessible à l'aide de l'adresse de mappé linéaire à 0xffff_8000_0000_0000. Nous mapons linéaire toute la mémoire physique dans 0xffff_8000_0000_0000 à 0xffff_8fff_ffff_ffff.
Notez qu'en raison de l'ABI x86-64, le noyau doit être lié dans le 2gib supérieur de la mémoire lors de l'utilisation du noyau McModel =. Par conséquent, nos tables de page ont également besoin d'un mappage pour 0xffff_ffff_8xxx_xxxx -> 0x0000_0000_0xxx_xxxx.
Oui! J'ai essayé de rendre le code très sympathique à ceux qui ne connaissent pas les cubitos, Ada ou Spark. Veuillez l'essayer sur une machine virtuelle et faites-moi savoir ce que vous en pensez. La rétroaction négative et les critiques constructives sont également utiles.
C'est fortement documenté et les contributeurs sont les bienvenus!
Les cubitos peuvent être un bon point de départ pour la recherche universitaire. Spark a une trappe d'évacuation pour effectuer des preuves en COQ, donc pour les contributeurs plus mathématiquement à l'esprit qui veulent un bon défi, voyez ce que vous pouvez prouver sur Cubitos!
Spark utilise le framework Why3 et le solveur SMT Z3. Les bons solveurs SMT rapides sont toujours un domaine d'intérêt, et Cubitos pourrait être un bon moyen de les comparer pour d'autres utilisations du monde réel.
| Élément de code | Convention |
|---|---|
| Mots-clés ADA (type, pour, boucle, etc.) | Tous les minuscules |
| Types (Multibootstruct, PagetableEntry, etc.) | Camelcasse capitalisée |
| Noms de packages | Camelcasse capitalisée |
| Variables, fonctions (kmain, thexstring, etc.) | camelcase non capitalisé |
| Constantes (LT_GRAY, KERN_BASE, etc.) | Tous les capuchons |
| Noms de fichiers | Tout inférieur ou serpent_case |
Remarque: Si l'interfaçage vers un composant externe, par exemple, les noms de variables doivent utiliser la même convention que l'API de ce composant. Par exemple, la structure d'informations Multiboot a des champs comme mem_lower, etc.
Nous utiliserons ces noms motorisés ici pour faciliter la référence de la documentation. Ce n'est pas une règle difficile et rapide. Si les noms d'API sont trop torres, déroutants, utilisez une étrange notation hongroise, ou sont autrement stupides, alors n'hésitez pas à les renommer dans le code ADA.
Évitez les abréviations trop terrestres. Les termes communs comme "kern" pour "noyau" ou "mem" pour la mémoire sont OK s'il n'y a pas d'ambiguïté. "VM" pour la mémoire virtuelle peut être confondue avec "Machine virtuelle", donc préfèrent "VirtMem" ou tout simplement épeler complètement. Les acronymes ne doivent être utilisés que s'ils sont largement utilisés ou une convention du matériel sous-jacent, comme ACPI,
Veuillez convertir les onglets en quatre espaces.
Les commits doivent être des fins de ligne LF.
Évitez les clauses "Utiliser", sauf indication contraire des opérateurs, puis limitez leur utilisation à des sous-programmes spécifiques si nécessaire ou utilisez la clause "Utiliser le type". Cela oblige le package d'un type à énoncer explicitement, et donc le package peut être facilement référencé et sauté dans un éditeur. Les exceptions à cette règle sont:
Utilisez le terme "cadre" lorsque vous faites référence à la mémoire physique et "page" lors de la discussion de la mémoire virtuelle.
Veuillez utiliser des noms descriptifs pour les variables, les types, etc. Nous ne manquons pas d'espace de disque dur pour stocker le code source, alors utilisez des noms plus longs (dans des limites raisonnables) s'ils aident à favoriser la compréhension du code.
Essayez de garder les lignes de moins de 80 caractères pour la plupart, mais si elle affecte négativement la lisibilité à briser une ligne, il est normal de rompre la limite de 80 de largeur. Les commentaires de fin de ligne peuvent dépasser 80 si cela nuit au flux du code pour les mettre sur leur propre ligne.
Si le mode Spark est désactivé sur un corps de sous-programme, veuillez ajouter un commentaire pourquoi. Cela peut être parfaitement valable, c'est-à-dire en ligne ASM. Cependant, essayez de restructurer le code pour activer le mode Spark - en particulier les spécifications de sous-programmes. Parfois, cela peut être un peu douloureux, c'est-à-dire en changeant les fonctions en procédures avec plusieurs paramètres "Out".
Célébrez Whitespace. Laissez le code respirer. Utilisez deux nouvelles lignes après chaque corps de sous-programme. Une nouvelle ligne après un corps de sous-programme est appropriée si les sous-programmes sont des variations mineures les unes des autres, c'est-à-dire des arguments surchargés, et ils sont étroitement regroupés pour clarifier leur relation.
Utilisez beaucoup de commentaires, au format Gnatdoc. C'est évidemment un domaine où les opinions diffèrent, mais je crois que le traitement du système d'exploitation comme une bibliothèque avec une documentation approfondie encourage l'exactitude et le rend plus convivial avec de nouveaux contributeurs. Cela facilite également la documentation automatique, plutôt que de maintenir la documentation séparément. Nous connaissons tous une bonne API quand nous en voyons une.
"Mais le code changera et les commentaires seront obsolètes!"
Alors ... euh ... il suffit de mettre à jour les commentaires!
Emprunt une page aux manuels des opérateurs d'avion:
Remarque - indique des informations considérées comme importantes pour souligner
ATTENTION - indique des informations qui, si elles ne sont pas prises en compte, peuvent entraîner des accidents du système ou un fonctionnement incorrect.
AVERTISSEMENT - indique des informations qui, si elles ne sont pas prises en compte, peuvent entraîner une perte de données utilisateur ou des dommages au matériel sous-jacent.
| Terme utilisé | Taille |
|---|---|
| Grignoter | 4 bits |
| Octet | 8 bits |
| Mot | 16 bits |
| DWORD (double mot) | 32 bits |
| Qword (quad-mot) | 64 bits |
Ceci est inclus ici pour éviter la confusion utilisée lors de la description des interfaces ou des composants matériels où le "mot" peut signifier autre chose que 16 bits. Nous voulons toujours dire 16 bits dans le code coudé lorsque vous utilisez "Word" dans les commentaires, etc.
D'une manière générale, nous énoncerons explicitement la durée d'un type de données à l'aide du package Interfaces ADA, c'est-à-dire unsigned_8, unsigned_32, etc. Les termes ci-dessus peuvent être utilisés dans les commentaires plutôt que de dépeindre la "valeur 32 bits", par exemple.
Les fonctions Spark ne sont pas autorisées à avoir des effets secondaires, donc de nombreuses fois, une procédure est utilisée à la place, et un paramètre OUT pour le résultat est requis, plutôt que de retourner le résultat. Il est un peu douloureux d'attribuer des temporaires à tous les résultats de la procédure.
Les définitions des constantes ne peuvent pas être (facilement) partagées entre le code ADA et les fichiers d'assembly, donc certains d'entre eux sont dupliqués. J'ai essayé d'obtenir toutes les constantes utilisées par les fichiers d'assembly dans cubit.inc, ainsi qu'une note de l'endroit où il pourrait être dupliqué dans le code ADA. Veuillez vous assurer que si vous modifiez l'une de ces valeurs, ils sont modifiés aux deux endroits. Si vous présentez votre propre constante qui est partagée entre l'assemblage et le code ADA - assurez-vous qu'ils utilisent le même nom!
Cabit divise la zone de pile statique en morceaux par CPU, chacun étant divisé en piles primaires et secondaires pour ce processeur. La pile primaire se développe, la pile secondaire grandit. Le pointeur de pile primaire est défini pour le CPU principal dans boot.asm et défini pour chaque CPU supplémentaire lorsqu'ils démarrent dans 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 +-----------------------+
L'appel SS_INIT SECHELARY est effectué lors de chaque démarrage du processeur. Les débordements de pile secondaire doivent être détectés au moment de l'exécution, mais utilisez la prudence. Pendant les systèmes et les interruptions, la pile de noyau du processus peut être utilisée, qui n'a pas de pile secondaire.
X signifie fini- signifie en cours [ ] 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.
| Tâche | Commande |
|---|---|
| Créer une documentation (dans Build / Docs) | make docs |
| Exécuter des proverses | make prove |
| Construire une documentation HTML | make html |
Vous pouvez créer une image de disque ext2 et la lire en cubit avec ces commandes, illustrée ici pour un disque de 128 Mo:
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
Vous avez maintenant un système de fichiers vide dans vhd/ auquel vous pouvez ajouter des fichiers, gâcher avec les autorisations, etc. Notez que l'implémentation EXT2 de Cubit ne prend actuellement en charge que les tailles de blocs 4K.
umount vhd
Vous avez maintenant une image disque que vous pouvez convertir au format VirtualBox avec:
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
Vous pouvez ajouter le nouveau disque sous stockage -> contrôleur IDE dans vos paramètres VM. Vous voudrez probablement utiliser le chipset ICH6. Cubit utilise actuellement l'ancienne méthode PIO pour les E / S ATA. Si vous créez une image disque et l'ajoutez au contrôleur IDE avec un chipset différent, les lectures échoueront probablement.
Notez que Cubit lit juste l'EXT2 Superblock actuellement, mais les progrès sont en cours avec la prise en charge du système de fichiers de base.
Veuillez expérimenter différentes quantités de RAM, nombre de processeurs, etc.
VirtualBox est un bon outil pour les tests, mais QEMU est agréable lorsque vous devez utiliser GDB pour retrouver certains problèmes. Notez que Cubit utilise certaines fonctionnalités CPU assez récentes, vous voudrez donc dire à Qemu d'utiliser un chipset et un CPU plus récent. Les options -machine q35 et -cpu Broadwell semblent bien fonctionner.
Commande Qemu sans débogueur:
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
Conseils GDB:
Enregistrer les informations sur Add'l: rt Registres: rg64 Trace de pile: k
Pour utiliser Qemu pour déboguer:
qemu-system-x86_64 -machine q35 -cpu Broadwell -s -S -m 4G -cdrom pathtocubit_kernel.iso -serial stdio
Qemu commencera dans un État en pause pendant qu'il attend le débogueur.
Puis exécutez gdb: gdb cubit_kernel (note: non ".iso" ici, nous voulons le fichier d'objet du noyau lui-même, qui contient des symboles de débogage)
Pour se connecter à QEMU: target remote localhost:1234 Utiliser (gdb) c pour continuer.
De là, les commandes GDB normales fonctionnent, comme break , x , etc.
Notez que Hyper-V ne semble pas démarrer le .iso actuellement. D'autres plates-formes de virtualisation ou d'émulation sont recommandées.
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.
