CuBit
1.0.0
Cubitos adalah multi-prosesor, 64-bit, (sebagian) yang diverifikasi secara formal, sistem operasi tujuan umum, saat ini untuk arsitektur X86-64.
Cubit ditulis dalam dialek percikan ADA.
Cubit sangat maju dalam proses! Setelah mengatakan itu, tolong berikan putaran. Kontributor selamat datang!
gprbuild , gnat , dll. Di $PATH AndaUntuk membuat bootable .iso, Anda juga akan membutuhkan:
Ketergantungan: Anda akan memerlukan kompiler GNAT 2020, dan jika Anda ingin membangun Live-CD, Anda akan memerlukan alat Xorriso dan Grub-Mkrescue , dan mungkin grub-pc-bin tergantung pada lingkungan emulator/virtualisasi yang Anda gunakan. Ini mungkin disediakan di manajer paket distro Anda. Ini dapat dibangun di Linux dan di Windows menggunakan WSL.
git clone https://github.com/docandrew/CuBit.git
make
Ini akan membangun hubit dan membuat file .iso live-cd. ISO dapat dipasang dan dijalankan di VirtualBox, Bochs, atau Qemu.
| Tugas | Memerintah |
|---|---|
| Buat dokumentasi (di build/docs) | make docs |
| Jalankan provers | make prove |
| Bangun dokumentasi HTML | make html |
ADA tidak peka case (yang agak bagus, jujur), tetapi membuat semua simbol yang diekspor lebih rendah, jadi apa pun dalam file .asm yang merujuk simbol itu perlu menggunakan versi yang lebih rendah, atau menentukan eksternal_name untuk simbol dalam suatu aspek.
Tipe yang disebutkan yang berisi "lubang" menyebabkan nyamuk untuk memasukkan pemeriksaan run-time untuk nilai yang valid saat menetapkannya. Saya tidak dapat menemukan pragma untuk menonaktifkan cek ini. Akhirnya kita akan menulis fungsi penangan pengecualian yang dapat melakukan cek atau menyebabkan kepanikan kernel, tetapi untuk saat ini, mengisi lubang dengan nilai -nilai yang jelas seperti bad_1, bad_2, dll.
Harap pastikan bukti dijalankan (menggunakan make prove ) sebelum mengirimkan permintaan tarik. Bersikaplah sangat berhati -hati tentang anotasi pragma untuk menonaktifkan peringatan. gnatprove akan memberikan beberapa peringatan palsu seperti statement has no effect atau unused assignment yang jelas-jelas salah, tapi tolong periksa ulang ini.
Catatan varian tampaknya memasukkan beberapa cruft tambahan dalam catatan yang mendasarinya, bahkan jika paket pragma digunakan. Jangan gunakan ini sebagai "overlay" di atas memori yang ada, misalnya tabel ACPI. Anda akan memiliki masalah penyelarasan dengan beberapa bidang dan berakhir dengan data sampah. Hal yang sama berlaku bahkan untuk catatan non-varian yang menggunakan diskriminan.
MAX_PHYS_ALLOC - Set di config.ads, ini adalah memori fisik maks yang didukung Cubit. Hanya ada batasan di sini yang praktis, karena pengalokasi boot memsib untuk membuat bitmap untuk semua memori ini (128 Gib), yang memakan cukup banyak ruang. (Kami dapat mempertimbangkan hanya menyisihkan bagian tumpukan kecil yang dipetakan linier untuk penggunaan kernel dan membangun alokasi yang lebih baik sehingga batas ini bukan faktor lagi.)
MAX_PHYS_ADDRESS - Memori fisik teoritis maksimum yang didukung perangkat keras kami (jika kami menggunakan pemetaan linier). Dalam kasus x86-64, kami memiliki alamat virtual 48-bit kanonik, jadi jika kami ingin semua memori fisik dipetakan dalam memori virtual, kami dibiarkan dengan sekitar 280TB, yang perlu kami belah untuk digunakan di bagian yang lebih tinggi, jadi 128TIB. Perhatikan bahwa Intel melihat pengalamatan 56-bit dengan tabel halaman lima tingkat, sehingga nomor ini dapat segera berubah untuk x86-64.
MAX_PHYS_Addressable - Alamat memori fisik teratas pada sistem kami yang kami deteksi saat runtime. Area memori peta linier hingga titik ini (mulai dari 0xffff_8000_0000_0000).
MAX_PHYS_USABLE - Alamat RAM yang dapat digunakan atas pada sistem kami . Mungkin ada lubang di dalamnya, jadi kita tidak dapat secara membabi buta mengalokasikan memori dari bawah batas ini, tetapi pengalokasi fisik akan diharapkan untuk menangani alamat hingga titik ini.
Beberapa struktur yang digunakan, seperti tabel GDT dan halaman, harus diatur dalam boot.asm sebelum beralih ke mode panjang. Ini disebut sebagai tabel "bootstrap" dan tabel halaman. Ada juga pengalokasi memori fisik "boot". Kemudian, kami memetakan kembali keseluruhan memori fisik ke dalam setengah lebih tinggi kernel bersama dengan GDT baru di segment.adb . Ini disebut "tabel halaman kernel" dan "kernel gdt."
Halaman Bootstrap Tabel Identity-Map memori 1G pertama, dan kemudian memetakannya lagi menjadi setengah lebih tinggi, mulai dari 0xffff_8000_0000_0000. Jadi P2V dan V2P (fisik-ke-virtual, virtual-ke-fisik) bekerja dengan penambahan dan pengurangan sederhana karena Anda dapat mengakses memori fisik pada, misalnya, 0x0000_0000_dead_beef di alamat virtual 0x0000_0000_dead_beef dan juga 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF_8000_DEAD_BEEF.
Saat kami beralih ke peta kernel, kami tidak dapat lagi membahas memori menggunakan alamat fisik langsung. Sebaliknya, alamat fisik tertentu harus diakses menggunakan alamat yang dipetakan linier di 0xFFFF_8000_0000_0000. Kami linear-peta semua memori fisik di 0xffff_8000_0000_0000 ke 0xffff_8fff_ffff_ffff.
Perhatikan bahwa karena X86-64 ABI, kernel harus dihubungkan di 2Gib memori atas saat menggunakan McModel = kernel. Oleh karena itu, tabel halaman kami juga memerlukan pemetaan untuk 0xffff_ffff_8xxx_xxxx -> 0x0000_0000_0xxx_xxxx.
Ya! Saya sudah mencoba membuat kode sangat ramah kepada mereka yang tidak terbiasa dengan Cubitos, Ada atau Spark. Tolong coba di VM dan beri tahu saya pendapat Anda. Umpan balik negatif dan kritik konstruktif juga berguna.
Ini sangat didokumentasikan, dan kontributor dipersilakan!
Cubitos mungkin menjadi titik awal yang baik untuk penelitian akademik. Spark memiliki penetasan pelarian untuk melakukan bukti di COQ, jadi untuk kontributor yang lebih berpikiran matematis yang menginginkan tantangan yang baik, lihat apa yang dapat Anda buktikan tentang Cubitos!
Spark menggunakan kerangka kerja Why3 dan Z3 SMT Solver. Pemecah SMT yang baik dan cepat selalu merupakan bidang yang menarik, dan Cubitos mungkin merupakan cara yang baik untuk membandingkan mereka untuk penggunaan dunia nyata lainnya.
| Elemen kode | Konvensi |
|---|---|
| Kata kunci ADA (ketik, untuk, loop, dll.) | semua huruf kecil |
| Jenis (MultibootStruct, Pagetableentry, dll.) | Camelcase yang dikapitalisasi |
| Nama paket | Camelcase yang dikapitalisasi |
| Variabel, fungsi (kmain, tohexstring, dll.) | Camelcase yang tidak dikapitalisasi |
| Konstanta (lt_gray, kern_base, dll.) | Semua topi |
| Nama file | semua lebih rendah atau snake_case |
Catatan: Jika berinteraksi dengan komponen eksternal, katakanlah multiboot, maka nama variabel harus menggunakan konvensi yang sama dengan API komponen itu. Misalnya, struct info multiboot memiliki bidang seperti mem_lower, dll.
Kami akan menggunakan nama -nama itu kata demi kata di sini untuk kemudahan referensi dokumentasi. Ini bukan aturan yang keras dan cepat. Jika nama API terlalu banyak, membingungkan, gunakan notasi Hongaria yang aneh, atau sebaliknya, maka jangan ragu untuk mengganti nama mereka dalam kode ADA.
Hindari singkatan yang berlebihan. Istilah umum seperti "kern" untuk "kernel", atau "mem" untuk memori, baik -baik saja jika tidak ada ambiguitas. "VM" untuk memori virtual dapat dikacaukan dengan "mesin virtual", jadi lebih suka "virtmem" atau hanya mengejanya sepenuhnya. Akronim hanya boleh digunakan jika banyak digunakan atau konvensi perangkat keras yang mendasarinya, seperti ACPI,
Harap konversi tab ke empat spasi.
Komitmen harus merupakan akhir garis.
Hindari klausa "gunakan" kecuali jika tidak perlu untuk operator, dan kemudian, batasi penggunaannya pada subprogram tertentu jika diperlukan atau gunakan klausa "Gunakan tipe". Ini memaksa paket jenis yang akan dijabarkan secara eksplisit, sehingga paket dapat dengan mudah dirujuk dan dilompat ke editor. Pengecualian untuk aturan ini adalah:
Gunakan istilah "bingkai" saat mengacu pada memori fisik, dan "halaman" saat membahas memori virtual.
Silakan gunakan nama deskriptif untuk variabel, jenis, dll. Kami tidak kekurangan ruang hard drive untuk menyimpan kode sumber, jadi gunakan nama yang lebih lama (dengan alasan) jika mereka membantu menumbuhkan pemahaman kode.
Cobalah untuk menjaga garis kurang dari 80 chars untuk sebagian besar, tetapi jika secara negatif mempengaruhi keterbacaan untuk memecahkan garis, maka tidak apa-apa untuk menghancurkan batas 80-lebar. Komentar akhir baris dapat melewati 80 jika itu menyakitkan aliran kode untuk menempatkannya di jalur mereka sendiri.
Jika mode Spark dinonaktifkan pada badan subprogram, silakan tambahkan komentar mengapa. Ini mungkin sangat valid, yaitu ASM inline. Namun, cobalah dan performing ulang kode untuk mengaktifkan mode Spark - terutama spesifikasi subprogram. Terkadang ini bisa sedikit menyakitkan, yaitu mengubah fungsi menjadi prosedur dengan beberapa param "keluar".
Rayakan Whitespace. Biarkan kode bernafas. Gunakan dua garis baru setelah setiap badan subprogram. Satu garis baru setelah badan subprogram sesuai jika subprogram adalah variasi kecil satu sama lain, yaitu argumen yang kelebihan beban, dan mereka dikelompokkan bersama untuk mengklarifikasi hubungan mereka.
Gunakan banyak komentar, dalam format gnatdoc. Ini jelas merupakan area di mana pendapat berbeda, tetapi saya percaya bahwa memperlakukan OS seperti perpustakaan dengan dokumentasi menyeluruh mendorong kebenaran dan membuatnya lebih ramah kepada kontributor baru. Ini juga membuatnya lebih mudah untuk menghasilkan dokumentasi secara otomatis, daripada memelihara dokumentasi secara terpisah. Kita semua tahu API yang bagus saat kita melihatnya.
"Tapi kode akan berubah dan komentarnya akan ketinggalan zaman!"
Jadi ... eh ... Perbarui komentar saja!
Meminjam halaman dari manual operator pesawat:
Catatan - menunjukkan informasi yang dianggap penting untuk ditekankan
PERHATIAN - Menunjukkan informasi yang, jika tidak dipertimbangkan, dapat mengakibatkan kerusakan sistem atau operasi yang salah.
PERINGATAN - Menunjukkan informasi yang, jika tidak dipertimbangkan, dapat mengakibatkan hilangnya data pengguna atau kerusakan pada perangkat keras yang mendasarinya.
| Istilah yang digunakan | Ukuran |
|---|---|
| Menggigit | 4 bit |
| Byte | 8 bit |
| Kata | 16 bit |
| DWORD (kata ganda) | 32 bit |
| Qword (Quad-Word) | 64 bit |
Ini termasuk di sini untuk menghindari kebingungan yang digunakan saat menggambarkan antarmuka atau komponen perangkat keras di mana "kata" dapat berarti sesuatu selain 16 bit. Kami selalu berarti 16-bit dalam kode hubit saat menggunakan "kata" dalam komentar, dll.
Secara umum, kami akan secara eksplisit menyatakan panjang tipe data menggunakan paket antarmuka ADA, yaitu unsigned_8, unsigned_32, dll. Istilah di atas dapat digunakan dalam komentar daripada mengeja "nilai 32-bit", misalnya.
Fungsi percikan tidak diperbolehkan memiliki efek samping, berkali-kali, prosedur digunakan sebagai gantinya, dan parameter keluar untuk hasilnya diperlukan, daripada hanya mengembalikan hasilnya. Agak menyakitkan untuk menetapkan temporari untuk semua hasil prosedur.
Definisi konstanta tidak dapat (dengan mudah) dibagikan antara kode ADA dan file perakitan, sehingga beberapa di antaranya digandakan. Saya sudah mencoba untuk mendapatkan semua konstanta yang digunakan oleh file perakitan di Cubit.inc, bersama dengan catatan di mana itu mungkin digandakan dalam kode ADA. Pastikan bahwa jika Anda mengubah nilai -nilai ini, mereka diubah di kedua tempat. Jika Anda memperkenalkan konstanta Anda sendiri yang dibagikan antara perakitan dan kode ADA - pastikan mereka menggunakan nama yang sama!
Cubit membagi area tumpukan statis menjadi potongan per-CPU, yang masing-masing dibagi menjadi tumpukan primer dan sekunder untuk CPU itu. Tumpukan utama tumbuh, tumpukan sekunder tumbuh. Pointer tumpukan utama diatur untuk CPU utama dalam boot.asm, dan diatur untuk setiap CPU tambahan saat mereka boot di 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 +-----------------------+
Panggilan tumpukan sekunder SS_INIT dilakukan selama setiap boot-up CPU. Luapan tumpukan sekunder harus terdeteksi saat runtime, namun berhati -hati. Selama syscalls dan interupsi, proses 'stack kernel mungkin digunakan, yang tidak memiliki tumpukan sekunder.
X berarti selesai- Berarti sedang berlangsung [ ] 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.
| Tugas | Memerintah |
|---|---|
| Buat dokumentasi (di build/docs) | make docs |
| Jalankan provers | make prove |
| Bangun dokumentasi HTML | make html |
Anda dapat membuat gambar disk EXT2 dan membacanya di Cubit dengan perintah -perintah ini, ditampilkan di sini untuk disk 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
Sekarang Anda memiliki sistem file kosong di vhd/ bahwa Anda dapat menambahkan file, mengacaukan dengan izin, dll. Ketika Anda selesai, membuka gambar gambar. Perhatikan bahwa implementasi Ext2 Cubit saat ini hanya mendukung ukuran blok 4K.
umount vhd
Sekarang Anda memiliki gambar disk yang dapat Anda konversi ke format VirtualBox dengan:
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
Anda dapat menambahkan disk baru di bawah penyimpanan -> Pengontrol IDE di pengaturan VM Anda. Anda mungkin ingin menggunakan chipset ICH6. Cubit saat ini menggunakan metode pio kuno untuk ATA I/O. Jika Anda membuat gambar disk dan menambahkannya ke pengontrol IDE dengan chipset yang berbeda, bacaan mungkin akan gagal.
Perhatikan bahwa Cubit baru saja membaca Ext2 Superblock saat ini, tetapi kemajuan sedang dibuat dengan dukungan sistem file dasar.
Harap bereksperimen dengan jumlah RAM yang berbeda, jumlah CPU, dll.
VirtualBox adalah alat yang baik untuk pengujian, namun QEMU bagus ketika Anda perlu menggunakan GDB untuk melacak masalah tertentu. Perhatikan bahwa Cubit memanfaatkan beberapa fitur CPU yang cukup baru, jadi Anda ingin memberi tahu QEMU untuk menggunakan chipset dan CPU yang lebih baru. Opsi -machine q35 dan -cpu Broadwell tampaknya bekerja dengan baik.
Perintah QEMU dengan debugger:
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
Tips GDB:
Daftar Add'l Info: rt Register: rg64 Stack Trace: k
Untuk menggunakan QEMU untuk men -debug:
qemu-system-x86_64 -machine q35 -cpu Broadwell -s -S -m 4G -cdrom pathtocubit_kernel.iso -serial stdio
Qemu akan mulai dalam keadaan yang dijeda saat menunggu debugger.
Kemudian Jalankan GDB: gdb cubit_kernel (Catatan: Tidak ".iso" di sini, kami ingin file objek kernel itu sendiri, yang berisi simbol debugging)
Untuk terhubung ke QEMU: target remote localhost:1234 Use (gdb) c untuk melanjutkan.
Dari sini, perintah GDB normal berfungsi, seperti break , x , dll.
Perhatikan bahwa Hyper-V tampaknya tidak mem-boot .iso saat ini. Platform virtualisasi atau emulasi lainnya direkomendasikan.
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.
