CuBit
1.0.0
Cubitos-это многопроцессорная, 64-битная, (частично), формально проверенная операционной системой общего назначения, в настоящее время для архитектуры X86-64.
Кубит написан на диалекте Spark of ADA.
Cubit-это очень работающая работа! Сказав это, пожалуйста, сделайте это. Участники приветствуются!
gprbuild , gnat и т. Д. В вашем $PATHЧтобы создать загрузочный .ис, вам также понадобится:
Зависимости: вам понадобится компилятор GNAT 2020, и если вы хотите построить Live-CD, вам понадобятся инструменты Xorriso и Grub-Mkrescue , и, возможно, Grub-PC-бин в зависимости от того, какую среду эмулятора/виртуализации вы используете. Они, вероятно, предоставляются в менеджере пакетов вашего дистрибуции. Это может быть встроено в Linux и в Windows с помощью WSL.
git clone https://github.com/docandrew/CuBit.git
make
Это построит Cubit и создаст файл Live-CD .ISO. ISO может быть установлен и запускаться в VirtualBox, Bochs или Qemu.
| Задача | Командование |
|---|---|
| Создать документацию (в сборке/документах) | make docs |
| Пробежать пост | make prove |
| Создайте HTML -документацию | make html |
ADA нечувствителен к регисту (что, честно говоря, довольно приятно), но это делает все экспортируемые символы более низкими, поэтому все в файлах .asm, которые ссылаются на то, что символ должен использовать нижнюю версию, или указать External_name для символа в аспекте.
Перечисленные типы, содержащие «отверстия», приводят к тому, что GNAT вставьте проверки времени выполнения для допустимых значений при их назначении. Я не мог найти прагму, чтобы отключить эти чеки. В конце концов мы напишем функции обработчика исключений, которые могут либо выполнить чеки, либо вызвать панику ядра, но на данный момент заполнить отверстия очевидными значениями, такими как BAD_1, BAD_2 и т. Д.
Пожалуйста, убедитесь, что доказательства запускаются (используя make prove ), прежде чем отправлять запросы на привлечение. Будьте очень осторожны с аннотацией прагмы, чтобы отключить предупреждения. gnatprove даст некоторые ложные предупреждения, подобные statement has no effect или unused assignment , которые явно неверны, но, пожалуйста, дважды проверьте их.
Варианты записей, по -видимому, вставляют дополнительные круты в базовую запись, даже если используется Pragma Pack. Не используйте их как «наложения» поверх существующей памяти, например, таблицы ACPI. У вас будут проблемы с выравниванием с некоторыми областями и получите нежелательные данные. То же самое верно даже для неводных записей, в которых используются дискриминанты.
Max_phys_alloc - установлен в config.ads, это максимальная физическая память, которую поддерживает Cubit. Здесь только ограничение является практичным, так как Allocator Boot MEM настроен на создание растровых карт для всей этой памяти (128 GIB), которое занимает достаточное количество места. (Мы можем рассмотреть вопрос о том, чтобы просто отложить небольшой линейный раздел кучи для использования ядра и создать лучший выделений, чтобы этот предел больше не является фактором.)
Max_phys_address - максимальная теоретическая физическая память, которую поддерживает наше оборудование (если мы используем линейное отображение). В случае X86-64 у нас есть канонические 48-битные виртуальные адреса, поэтому, если мы хотим, чтобы вся физическая память была нанесена на карту в виртуальной памяти, у нас осталось около 280 ТБ, которые нам нужно разделить, чтобы использовать в более высокой половине, так что 128TIB. Обратите внимание, что Intel рассчитывает на 56-битную адресацию с пятиуровневой таблицей страниц, поэтому этот номер может вскоре измениться для X86-64.
Max_phys_addressable - верхний адрес физической памяти в нашей системе , который мы обнаруживаем во время выполнения. Мы до этой точки до этой точки (начиная с 0xffff_8000_0000_0000).
Max_phys_usable - верхний адрес использования ОЗУ в нашей системе . Внутри этого могут быть отверстия, поэтому мы не можем слепо выделить память из -под этого предела, но ожидается, что физический распределитель будет обрабатывать адреса до этого момента.
Некоторые из используемых структур, таких как таблицы GDT и Page, должны быть настроены в boot.asm прежде чем переходить в длинный режим. Они называются таблицами GDT и страниц «Bootstrap» соответственно. Есть также распределитель физической памяти «загрузки». Позже мы переоцениваем целую физическую память в более высокую половину ядра вместе с новым GDT в segment.adb . ADB. Они называются «таблицами страниц ядра» и «GDT ядра».
Начала таблицы страниц начальной загрузки первой 1G памяти, а затем отобразите ее снова в более высокую половину, начиная с 0xffff_8000_0000_0000. Таким образом, работа P2V и V2P (физическая и виртуальная, виртуально-физическая) работая с помощью простого сложения и вычитания, поскольку вы можете получить доступ к физической памяти, например, 0x0000_0000_dead_beef на виртуальных адресах 0x0000_0000_dead_beef, а также 0xffff_8000_dead_beef.
Когда мы переключаемся на карту ядра, мы больше не можем обращаться к памяти, используя прямые физические адреса. Вместо этого должен быть доступ к конкретному физическому адресу с использованием линейного отображения адреса по адресу 0xffff_8000_0000_0000. Мы линейной картой всей физической памяти в 0xffff_8000_0000_0000 до 0xffff_8fff_ffff_ffff.
Обратите внимание, что из-за x86-64 ABI ядро должно быть связано в верхних 2gib памяти при использовании McModel = ядро. Поэтому наши таблицы страниц также нуждаются в сопоставлении для 0xffff_ffff_8xxx_xxxx -> 0x0000_0000_0xxx_xxxx.
Да! Я пытался сделать код очень дружелюбным с теми, кто не знаком с Cubitos, Ada или Spark. Пожалуйста, попробуйте это на виртуальной машине и дайте мне знать, что вы думаете. Негативная обратная связь и конструктивная критика тоже полезны.
Это сильно документировано, и участники приветствуются!
Кубито может быть хорошей отправной точкой для академических исследований. У Spark есть люк Escape для выполнения доказательств в COQ, поэтому для более математически ориентированных участников, которые хотят хорошего вызова, посмотрите, что вы можете доказать о Cubitos!
Spark использует Framework Why3 и Z3 SMT Solver. Хорошие, быстрые решатели SMT всегда представляют интерес, и Cubitos может быть хорошим способом сравнить их для других реальных видов использования.
| Кодовый элемент | Соглашение |
|---|---|
| Ключевые слова ADA (тип, для петли и т. Д.) | все строчные |
| Типы (MultiBootStruct, PageTableEntry и т. Д.) | Капитализированная верблюда |
| Имена пакетов | Капитализированная верблюда |
| Переменные, функции (Kmain, ToHexstring и т. Д.) | необразованная верблюда |
| Константы (lt_gray, kern_base и т. Д.) | Все кепки |
| Имена файлов | все нижняя или змея |
Примечание. Если взаимодействие с внешним компонентом, скажем, Multiboot, то имена переменных должны использовать то же соглашение, что и API этого компонента. Например, Multiboot Info Instruct имеет поля, такие как mem_lower и т. Д.
Мы будем использовать эти имена Vorbatim здесь для облегчения ссылки на документацию. Это не жесткое правило. Если имена API чрезмерно, сбивают с толку, используйте странную венгерскую нотацию или иначе глупы, не стесняйтесь переименовать их в коде ADA.
Избегайте чрезмерно термовых сокращений. Общие термины, такие как «Керн» для «ядра», или «мем» для памяти, в порядке, если нет двусмысленности. «VM» для виртуальной памяти можно путать с «виртуальной машиной», поэтому предпочитайте «virtmem» или просто полностью написать. Аббревиатуры следует использовать только в том случае, если они широко используются или согласно базовому аппаратному обеспечению, например, ACPI,
Пожалуйста, преобразуйте вкладки в четыре пространства.
Коммитами должны быть линейные окончания LF.
Избегайте «Использовать» предложения, если иное не необходимо для операторов, а затем ограничивайте их использование определенными подпрограммами, где это необходимо, или используйте предложение «Использование типа». Это заставляет пакет типа быть явно изложенным, и поэтому на пакет можно легко ссылаться и поднять в редактор. Исключения из этого правила:
Используйте термин «кадр» при обращении к физической памяти и «странице» при обсуждении виртуальной памяти.
Пожалуйста, используйте описательные имена для переменных, типов и т. Д. Нас не хватает в пространстве жесткого диска для хранения исходного кода, поэтому используйте более длинные имена (в пределах разума), если они помогают способствовать пониманию кода.
Постарайтесь сохранить линии меньше 80 Chars шириной по большей части, но если это негативно влияет на читабельность, чтобы разорвать линию, то можно сломать предел 80. Конец линейных комментариев может пройти за 80, если наносит ущерб потоку кода, чтобы поставить их на свою линию.
Если режим Spark отключен в корпусе подпрограммы, добавьте комментарий, почему. Это может быть совершенно верно, т.е. встроенный ASM. Тем не менее, попробуйте реструктурировать код, чтобы включить режим Spark - особенно спецификации подпрограммы. Иногда это может быть немного болезненным, т.е. изменяет функции на процедуры с множественными параметрами «Out».
Праздновать пробел. Пусть код дышит. Используйте две новички после каждого тела подпрограммы. Одна новая линия после того, как тело подпрограммы подходит, если подпрограммы являются незначительными вариациями друг друга, т.е. перегруженными аргументами, и они тесно сгруппированы вместе для прояснения своих отношений.
Используйте много комментариев, в формате Gnatdoc. Это, очевидно, та область, где мнения различаются, но я считаю, что обращение с ОС как к библиотеке с тщательной документацией поощряет правильность и делает ее дружелюбным для новых участников. Это также облегчает автоматическую документацию, а не поддерживать документацию отдельно. Мы все знаем хороший API, когда видим его.
«Но код изменится, и комментарии будут устаревшими!»
Так что ... э -э ... просто обновите комментарии!
Заимствование страницы из руководств по операторам самолетов:
Примечание - обозначает информацию, которая считается важной, чтобы подчеркнуть
Внимание - обозначает информацию, которая, если не рассматриваться, может привести к сбою системы или неправильной работе.
Предупреждение - обозначает информацию, которая, если не рассматриваться, может привести к потере пользовательских данных или повреждению базового оборудования.
| Термин используется | Размер |
|---|---|
| Захмель | 4 бита |
| Байт | 8 битов |
| Слово | 16 бит |
| Dword (двойное слово) | 32 бита |
| QWORD (четырехвол) | 64 бита |
Это включено здесь, чтобы избежать путаницы, используемой при описании интерфейсов или аппаратных компонентов, где «слово» может означать нечто иное, чем 16 бит. Мы всегда имеем в виду 16-битные в коде кубита при использовании «Слово» в комментариях и т. Д.
Вообще говоря, мы явно указам длину типа данных, используя пакет интерфейсов ADA, то есть unsigned_8, unsigned_32 и т. Д. Приведенные выше термины могут использоваться в комментариях, а не на написании «32-разрядного значения», например.
Функции Spark не разрешаются иметь какие-либо побочные эффекты, так много раз, вместо этого используется процедура, и требуется параметр OUT для результата, а не просто возврат результата. Немного больно назначать временные результаты для всех результатов процедуры.
Определения констант не могут быть (легко) делиться между кодом ADA и файлами сборки, поэтому некоторые из них дублируются. Я пытался получить все константы, используемые файлами сборки в Cubit.inc, а также примечание о том, где это может быть дублировано в коде ADA. Пожалуйста, убедитесь, что если вы измените какое -либо из этих значений, они изменяются в обоих местах. Если вы представляете свою собственную константу, которая разделена между сборкой и кодом ADA - убедитесь, что они используют одно и то же имя!
Cubit делит область статического стека на куски для CPU, каждый из которых разделен на первичные и вторичные стеки для этого процессора. Основной стек растет, вторичный стек растет. Основной указатель стека установлен для основного процессора в boot.asm и устанавливается для каждого дополнительного процессора, когда они загружаются в 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 +-----------------------+
Вторичный стек SS_INIT вызов выполняется во время каждой загрузки процессора. Вторичные переполнения стека должны быть обнаружены во время выполнения, однако используйте осторожность. Во время SYSCALLS и прерываний может использоваться стек ядра процесса, который не имеет вторичного стека.
X означает закончен- означает в процессе [ ] 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.
| Задача | Командование |
|---|---|
| Создать документацию (в сборке/документах) | make docs |
| Пробежать пост | make prove |
| Создайте HTML -документацию | make html |
Вы можете создать изображение диска EXT2 и прочитать его в Cubit с этими командами, показанные здесь для диска 128 МБ:
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
Теперь у вас есть пустая файловая система в vhd/ , в которую вы можете добавить файлы, возиться с разрешениями и т. Д. Когда вы закончите, отсоедините изображение. Обратите внимание, что реализация Cubit Ext2 в настоящее время поддерживает только 4K -размеры блоков.
umount vhd
Теперь у вас есть изображение диска, которое вы можете преобразовать в формат VirtualBox с:
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
Вы можете добавить новый диск под хранилищем -> контроллер IDE в настройки виртуальной машины. Вы, вероятно, захотите использовать чипсет ICH6. В настоящее время Cubit использует древний метод PIO для ввода -вывода ATA. Если вы создаете изображение диска и добавите его в контроллер IDE с другим чипсетом, чтения, вероятно, потерпит неудачу.
Обратите внимание, что Cubit только что читает Superblock Ext2 в настоящее время, но прогресс достигается с помощью базовой поддержки файловой системы.
Пожалуйста, экспериментируйте с различными объемами оперативной памяти, количеством процессоров и т. Д.
VirtualBox - хороший инструмент для тестирования, однако QEMU хорош, когда вам нужно использовать GDB для отслеживания определенных проблем. Обратите внимание, что Cubit использует некоторые довольно недавние функции процессора, поэтому вы захотите сказать Qemu использовать новый чипсет и процессор. Варианты -machine q35 и -cpu Broadwell похоже, работают хорошо.
Команда QEMU без отладчика:
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
Советы GDB:
Зарегистрируйтесь добавить информацию: rt Registers: rg64 Stack Trace: k
Использовать Qemu для отладки:
qemu-system-x86_64 -machine q35 -cpu Broadwell -s -S -m 4G -cdrom pathtocubit_kernel.iso -serial stdio
Qemu начнет в приостановленном состоянии, пока он ждет отладчика.
Затем запустите GDB: gdb cubit_kernel (Примечание: нет ".iso" Здесь мы хотим, чтобы сам файл объекта ядра, который содержит символы отладки)
Для подключения к QEMU: target remote localhost:1234 Использование (gdb) c для продолжения.
Отсюда работают обычные команды GDB, например, break , x и т. Д.
Обратите внимание, что Hyper-V, по-видимому, не загружается в настоящее время .ISO. Рекомендуются другие платформы виртуализации или эмуляции.
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.
