CuBit
1.0.0
Cubitos是一家多处理器，64位，（部分）正式验证的通用操作系统，目前适用于X86-64体系结构。
Cubit用ADA的火花方言写。
Cubit是一个正在进行的工作！话虽如此，请给它一个旋转。贡献者欢迎！
$PATH与gprbuild ， gnat等要创建可启动.iso，您还需要：
依赖项：您需要GNAT 2020编译器，如果要构建Live-CD，则需要Xorriso和Grub-Mkrescue工具，并且可能会根据所使用的模拟器/虚拟化环境而可能是GRUB-PC-bin 。这些可能是在您的发行版本管理器中提供的。可以使用WSL在Linux和Windows上构建。
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，etc。
在提交拉请请求之前，请确保运行证明（使用make prove ）。对pragma批准对禁用警告非常谨慎。 gnatprove会发出一些虚假的警告，例如statement has no effect或未unused assignment ，这显然是不正确的，但请仔细检查这些。
即使使用Pragma Pack，变体记录似乎在基础记录中插入了一些额外的巡回赛。请勿将它们用作现有内存之上的“叠加”，例如ACPI表。您将在某些字段中遇到一致问题，最终得到垃圾数据。即使对于使用判别因子的非变化记录，也是如此。
MAX_PHYS_ALLOC-在Config.Ads中设置，这是Cubit支持的最大物理内存。这里只有限制是实用的，因为设置了启动MEM分配器来为所有这些内存创建位图（128 GIB），从而占用了相当多的空间。 （我们可能会考虑仅保留一个小的线性映射堆部分以供内核使用并构建更好的分配器，因此此限制不再是一个因素。）
MAX_PHYS_ADDRESS-硬件支持的最大理论物理内存（如果使用线性映射）。对于X86-64，我们具有规范的48位虚拟地址，因此，如果我们希望将所有物理内存映射在虚拟内存中，我们将剩下约280TB，我们需要将其分开以在高级中使用，因此128Tib。请注意，英特尔正在使用5级页面表的56位寻址，因此对于X86-64，此数字可能很快就会更改。
max_phys_addressable-我们在运行时检测到的系统上的顶部物理内存地址。我们直到这一点线性映射内存区域（从0xffff_8000_0000_0000开始）。
MAX_PHYS_USABLE-系统上的顶级可用RAM地址。内部可能有孔，因此我们不能从此限制之下盲目分配内存，但是希望到达这一点的物理分配者可以处理地址。
在切换到长模式之前，必须在boot.asm中设置一些使用的结构，例如GDT和页面表。这些分别称为“ Bootstrap” GDT和页面表。还有“引导”物理内存分配器。稍后，我们将整个物理内存重新映射到内核的高度，并在segment.adb中的新GDT中将其映射到更高的内存中。这些称为“内核页面表”和“内核GDT”。
Bootstrap Page表Identity映射第一个1G内存的记忆，然后再次将其映射到更高的半级内，从0xffff_8000_0000_0000开始。因此，P2V和V2P（物理到虚拟的，虚拟到物理）可以通过简单的加法和减法来工作，因为您可以在例如0x0000_0000_dead_beef上访问物理内存，在虚拟地址0x000000_0000_dead_dead_beef和0x0000_0000_dead_beef和0xfffffffffffffffffffffffffff_8000_dead_dead_dead_dead_dead_dead_beef。
当我们切换到内核图时，我们无法再使用直接物理地址来解决内存。相反，必须使用0xffff_8000_0000_0000的线性映射地址访问特定的物理地址。我们在0xffff_8000_0000_0000至0xffff_8fff_fff_ffff_ffff中线性映射所有物理内存。
请注意，由于X86-64 ABI，使用McModel =内核时，必须将内核链接在内存的前2GIB中。因此，我们的页面表还需要0xfffff_ffff_8xxx_xxxx的映射 - > 0x0000_0000_0000_0xxx_xxxx。
是的！我试图使代码对那些不熟悉Cubitos，Ada或Spark的人非常友好。请在VM上尝试一下，让我知道您的想法。负面的反馈和建设性批评也很有用。
它是有据可查的，欢迎贡献者！
Cubitos可能是学术研究的好起点。 Spark有一个逃生的舱口，可以在COQ中执行证明，因此对于想要一个好的挑战的更具数学意识的贡献者，请参阅您对Cubitos的证明！
Spark使用Why3 Framework和Z3 SMT求解器。良好，快速的SMT求解器始终是一个有趣的领域，Cubitos可能是将它们用于其他现实世界使用的好方法。
| 代码元素 | 习俗 |
|---|---|
| ADA关键字（类型，用于，循环等） | 所有小写 |
| 类型（MultibootStruct，PagetableEntry等） | 大写的骆驼 |
| 软件包名称 | 大写的骆驼 |
| 变量，函数（kmain，tohexstring等） | 未资本化的骆驼 |
| 常数（lt_gray，kern_base等） | 所有帽子 |
| 文件名 | 所有较低或蛇case |
注意：如果与外部组件（例如Multiboot）接口，则可变名称应使用与该组件的API相同的约定。例如，Multiboot信息结构具有MEM_LOWER等字段。
我们将在此处逐字使用这些名称，以易于文档参考。这不是一个艰难的规则。如果API名称过于混乱，使用奇怪的匈牙利符号或以其他方式愚蠢，请随时在ADA代码中重命名它们。
避免过度缩写。如果没有歧义，诸如“ kernel”或“ mem”的“ kern”或“ mem”的常见术语是可以的。对于虚拟内存，“ VM”可以与“虚拟机”混淆，因此更喜欢“ virtmem”，也可以完全拼出。首字母缩略词仅在广泛使用或诸如ACPI之类的基础硬件的约定时才使用
请将选项卡转换为四个空间。
提交应该是LF线路的结尾。
除非运算符另有必要，否则请避免使用“使用”条款，然后将其用途限制为需要的特定子程序，或使用“使用类型”子句。这迫使要明确拼写的类型包装，因此可以轻松地引用该包装并在编辑器中跳到。该规则的例外是：
在讨论虚拟内存时，请在参考物理内存时使用术语“帧”和“页面”。
请使用变量，类型等的描述性名称。我们不缺少硬盘驱动器空间来存储源代码，因此，如果它们有助于促进对代码的理解，请使用更长的名称（在理性之内）。
尝试在大部分时间内保持不到80个字符宽的线条，但是如果它对破坏线路的可读性产生负面影响，那么可以破坏80宽的限制。线条评论的结束可能会超过80，如果它损害了代码的流程将它们置于自己的行上。
如果在子程序主体上禁用了火花模式，请添加评论原因。这可能是完全有效的，即内联ASM。但是，尝试重组代码以启用SPARK模式，尤其是子程序规范。有时，这可能有些痛苦，即将功能更改为具有多个“ OUT”参数的过程。
庆祝空格。让代码呼吸。在每个子程序主体后使用两个新线。如果子程序是彼此之间的较小变化，即超载的参数，并且将它们紧密组合在一起以澄清其关系，则在子程序主体之后的一个新线是合适的。
使用大量评论，以GNATDOC格式使用。显然，这是一个意见不同的领域，但我相信将OS作为图书馆作为图书馆进行详尽的文档鼓励了正确性，并使其与新贡献者更加友好。这也使自动生成文档的自动化而不是单独维护文档变得更加容易。当我们看到一个时，我们都知道一个很好的API。
“但是代码将更改，评论将过时！”
所以...呃...只需更新评论！
从飞机运营商手册中借入页面：
注意 - 表示被认为很重要的信息
注意 - 表示信息，如果不考虑，可能会导致系统崩溃或操作不正确。
警告 - 表示信息，如果不考虑，可能会导致用户数据丢失或损坏基础硬件。
| 使用的术语 | 尺寸 |
|---|---|
| 蚕食 | 4位 |
| 字节 | 8位 |
| 单词 | 16位 |
| dword（双字） | 32位 |
| QWORD（Quad-Word） | 64位 |
此处包括在内，以避免描述“词”可能意味着16位的界面或硬件组件时使用的混乱。在注释中使用“ word”时，我们总是指16位。
一般而言，我们将使用ADA接口软件包，即UNSIGNED_8，UNSIGNED_32等明确说明数据类型的长度。上面的术语可以在评论中使用，而不是拼写“ 32位值”。
火花功能不允许具有任何副作用，因此使用了一个过程，而是需要一个过程，并且需要一个结果参数，而不仅仅是返回结果。为所有过程结果分配临时性有点痛苦。
常数的定义不能（容易）在ADA代码和汇编文件之间共享，因此其中一些是重复的。我试图在cubit.inc中获取汇编文件使用的所有常数，以及在ADA代码中可以重复的何处。请确保，如果您更改这些值的任何一个，则它们在两个地方都会更改。如果您引入了自己的常数，该常数在汇编和ADA代码之间共享 - 请确保它们使用相同的名称！
CUBIT将静态堆栈区域分为每个CPU块，每个块块分为该CPU的主要和次要堆栈。主要堆栈成长，次要堆栈成长。主堆栈指针设置为boot.asm中的主CPU，并在boot_ap.asm启动时为每个附加CPU设置。
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调用是在每个CPU启动过程中进行的。应在运行时检测到次要堆栈溢出，但是请谨慎。在SYSCALL和中断期间，可能正在使用该过程的内核堆栈，该堆栈没有次要堆栈。
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读取它，此处显示了一个128MB磁盘：
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
现在，您拥有一个磁盘映像，可以使用以下方式将其转换为虚拟盒格式
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
您可以在VM设置中添加存储 - > IDE控制器的新磁盘。您可能需要使用ICH6芯片组。 Cubit目前使用古代PIO方法进行ATA I/O。如果您创建磁盘映像并使用不同的芯片组将其添加到IDE控制器中，则读取可能会失败。
请注意，Cubit当前只是读取Ext2 SuperBlock，但是基本文件系统支持正在取得进展。
请尝试使用不同量的RAM，CPU数量等。
VirtualBox是测试的好工具，但是，当您需要使用GDB来跟踪某些问题时，QEMU很好。请注意，CUBIT利用了一些相当最近的CPU功能，因此您需要告诉Qemu使用较新的芯片组和CPU。 -machine q35和-cpu Broadwell选项似乎效果很好。
QEMU命令w/o调试器：
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
GDB提示：
注册添加'l信息： rt寄存器： rg64堆栈跟踪： 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.
