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 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.
