CuBit
1.0.0
キュービトスは、現在X86-64アーキテクチャ向けのマルチプロセッサ、64ビット、（部分的に）正式に検証された汎用オペレーティングシステムです。
キュービットは、ADAの火花方言で書かれています。
キュービットは非常に進行中の作業です！そうは言っても、スピンしてください。貢献者を歓迎します！
gprbuild 、 gnat $PATHのGNAT CE 2020bootable .isoを作成するには、次のことも必要です。
依存関係：GNAT 2020コンパイラが必要です。ライブCDを構築する場合は、使用しているエミュレータ/仮想化環境に応じて、 XorrisoおよびGrub-Mkrescueツール、場合によってはGrub-PC-Binが必要です。これらはおそらく、ディストリビューションのパッケージマネージャーに提供されます。これは、WSLを使用してLinuxとWindowsで構築できます。
git clone https://github.com/docandrew/CuBit.git
make
これにより、キュービットが構築され、ライブCD .ISOファイルが作成されます。 ISOは、VirtualBox、Bochs、またはQemuでマウントして実行できます。
| タスク | 指示 |
|---|---|
| ドキュメントを作成する（ビルド/ドキュメントで） | make docs |
| プロバーを実行します | make prove |
| HTMLドキュメントを作成します | make html |
ADAはケース非感受性（これは一種の素晴らしく、正直です）ですが、エクスポートされたすべてのシンボルを低いケースにします。
「穴」を含む列挙されたタイプにより、GNATはこれらを割り当てるときに有効な値のランタイムチェックを挿入します。これらのチェックを無効にするためのプラグマが見つかりませんでした。最終的には、チェックを実行するか、カーネルパニックを引き起こす可能性のある例外ハンドラー関数を書き込みますが、今のところ、穴をbad_1、bad_2などの明白な値で埋めます。
プルリクエストを送信する前に、証明が実行されていることを確認してください（ make proveを使用して）。 Pragma Annotateに警告を無効にすることに非常に注意してください。 gnatprove 、明確に間違ってstatement has no effectやunused assignmentのような偽りの警告を与えますが、これらを再確認してください。
バリアントレコードは、たとえプラグマパックを使用していても、基礎となる記録に余分な口頭を挿入するようです。これらを既存のメモリ、たとえばACPIテーブルの上に「オーバーレイ」として使用しないでください。いくつかのフィールドに合わせて問題が発生し、ジャンクデータが表示されます。同じことは、判別剤を使用する非バリアントレコードでも当てはまります。
max_phys_alloc -config.adsに設定すると、これはキュービットがサポートする最大物理メモリです。 Boot Mem Allocatorがセットアップされ、このメモリ（128 GIB）のすべてのビットマップが作成され、かなりのスペースを占めるために、ここには実用的な制限のみが実用的です。 （カーネルの使用のために小さな線形マッピングヒープセクションを脇に置き、より良いアロケーターを構築することを検討する場合があります。これにより、この制限はもう要因ではありません。）
max_phys_address-ハードウェアがサポートする最大理論的物理メモリ（線形マッピングを使用する場合）。 x86-64の場合、標準的な48ビットの仮想アドレスがあるため、すべての物理メモリを仮想メモリにマッピングしたい場合は、約280TBのままになります。 Intelは5レベルのページテーブルを使用して56ビットアドレス指定を検討しているため、X86-64でこの数値がすぐに変更される可能性があることに注意してください。
MAX_PHYS_ADDRESSABLE-実行時に検出されたシステム上のトップの物理メモリアドレス。この時点までのメモリ領域を線形マップします（0xffff_8000_0000_0000から）。
MAX_PHYS_USABLE-システム上の最上位の使用可能なRAMアドレス。この中に穴がある可能性があるため、この制限の下からメモリを盲目的に割り当てることはできませんが、物理的なアロケーターはこの時点までのアドレスを処理することが期待されます。
GDTやページテーブルなどの使用される構造の一部は、ロングモードに切り替える前に、 boot.asmでセットアップする必要があります。これらは、それぞれ「ブートストラップ」GDTおよびページテーブルと呼ばれます。 「ブート」物理メモリアロケーターもあります。その後、物理メモリの全体をカーネルの上位半分に再マップし、 segment.adbの新しいGDTに加えます。これらは、「カーネルページテーブル」と「カーネルGDT」と呼ばれます。
ブートストラップページは、メモリの最初の1gをIDマップし、0xffff_8000_0000_0000から始まる上位ハーフに再度マップします。したがって、P2VおよびV2P（物理的、仮想、および物理的）は、たとえば0x0000_0000_Dead_Beefで物理メモリにアクセスできるため、0x0000_Dead_Beefにアクセスできるため、P2VおよびV2P（物理的、仮想、物理的）は、0x0000_Dead_Beefにアクセスできます。
カーネルマップに切り替えると、直接的な物理アドレスを使用してメモリに対処できなくなります。代わりに、0xfffff_8000_0000_0000の線形マップアドレスを使用して、特定の物理アドレスにアクセスする必要があります。 0xffff_8000_0000_0000から0xffff_8fff_ffffffffのすべての物理メモリを線形マップします。
X86-64 ABIのため、McModel =カーネルを使用する場合、メモリの上位2GIBにカーネルをリンクする必要があることに注意してください。したがって、ページテーブルには0xffff_ffff_8xxx_xxxx-> 0x0000_00_0xxx_xxxxのマッピングも必要です。
はい！私は、キュビトス、ADA、またはSparkに不慣れな人たちに非常に友好的なコードを作ろうとしました。 VMで試してみてください。ご意見をお聞かせください。否定的なフィードバックと建設的な批判も有用です。
それは非常に文書化されており、貢献者は大歓迎です！
キュービトスは、学術研究の良い出発点かもしれません。 SparkにはCoQで証明を行うためのエスケープハッチがあります。そのため、良い挑戦を望んでいる数学的に志向の貢献者のために、Cubitosについて証明できることをご覧ください！
Sparkは、WHY3フレームワークとZ3 SMTソルバーを使用します。優れた高速SMTソルバーは常に関心のある領域であり、キュービトスは他の現実の使用のためにそれらをベンチマークする良い方法かもしれません。
| コード要素 | 大会 |
|---|---|
| ADAキーワード（タイプ、for、ループなど） | すべて小文字 |
| タイプ（MultiBootStruct、PagetableEntryなど） | 大文字のカメルケース |
| パッケージ名 | 大文字のカメルケース |
| 変数、関数（kmain、tohexstringなど） | 資本化されていないキャメルケース |
| 定数（LT_Gray、Kern_Baseなど） | すべてのキャップ |
| ファイル名 | すべて低いまたはsnake_case |
注：外部コンポーネント（たとえばMultiBoot）にインターフェースする場合、変数名はそのコンポーネントのAPIと同じ慣習を使用する必要があります。たとえば、MultiBoot Info StructにはMEM_LOWERなどのフィールドがあります。
ドキュメントリファレンスを容易にするために、これらの名前の名前をこちらを使用します。これは難しいルールではありません。 API名が過度に、混乱を招く、奇妙なハンガリーの表記法を使用している場合、またはそれ以外の場合は愚かな馬鹿げている場合は、ADAコードで自由に変更してください。
過度に略語を避けてください。 「カーネル」の「カーン」やメモリの「メム」などの一般的な用語は、あいまいさがない場合は大丈夫です。仮想メモリの「VM」は「仮想マシン」と混同される可能性があるため、「Virtmem」を好むか、完全に綴るだけです。頭字語は、それらが広く使用されている場合、またはACPIのような基礎となるハードウェアの慣習でのみ使用する必要があります。
タブを4つのスペースに変換してください。
コミットはLFラインエンディングである必要があります。
オペレーターに必要な場合を除き、「使用」条項を避け、その後、必要な場合に使用を特定のサブプログラムに制限するか、「使用タイプ」節を使用します。これにより、タイプのパッケージが明示的に綴られるように強制されるため、パッケージを簡単に参照して編集者にジャンプできます。このルールの例外は次のとおりです。
物理メモリを参照するときは「フレーム」という用語を使用し、仮想メモリについて議論するときは「ページ」を使用します。
変数、タイプなどに記述名を使用してください。ソースコードを保存するためのハードドライブスペースが不足していないため、コードの理解を促進するのに役立つ場合は、より長い名前を使用してください。
ほとんどの場合、幅80枚未満の炭火を保つようにしてください。ただし、読みやすさに悪影響を及ぼしてラインを破る場合は、80回の制限を破ることは問題ありません。コードの流れを傷つけて自分のラインに置くと、行のコメントが80を超える可能性があります。
サブプログラム本文でSparkモードが無効になっている場合は、理由を追加してください。これは完全に有効かもしれません。つまり、インラインASM。ただし、スパークモード、特にサブプログラムの仕様を有効にするために、コードを再構築して再構築してください。これは少し苦痛になる場合があります。つまり、複数の「out」パラメーションを持つ手順に関数を変更することがあります。
Whitespaceを祝います。コードを呼吸させてください。各サブプログラム本体の後に2つのニューラインを使用します。サブプログラムの後の1つの新しいラインは、サブプログラムが互いにマイナーなバリエーションである場合、つまりオーバーロードされた引数で適切であり、関係を明確にするために密接にグループ化されています。
Gnatdoc形式で多くのコメントを使用してください。これは明らかに意見が異なる分野ですが、徹底的な文書を備えたライブラリのようにOSを扱うことは正確性を促進し、新しい貢献者に友好的になると思います。また、ドキュメントを個別に維持するのではなく、ドキュメントを自動生成しやすくなります。私たちは皆、私たちがそれを見るとき、良いAPIを知っています。
「しかし、コードは変更され、コメントは古くなります！」
だから...ええと...コメントを更新してください！
航空機のオペレーターマニュアルからページを借りる：
注 - 強調することが重要であると考えられる情報を示します
注意 - 考慮されない場合、システムがクラッシュしたり、操作が誤っている可能性があるという情報を示します。
警告 - 考慮されない場合、ユーザーデータの損失または基礎となるハードウェアの損傷が発生する可能性があるという情報を示します。
| 使用された用語 | サイズ |
|---|---|
| ニブル | 4ビット |
| バイト | 8ビット |
| 言葉 | 16ビット |
| DWORD（ダブルワード） | 32ビット |
| qword（quad-word） | 64ビット |
これは、「単語」が16ビット以外のものを意味する可能性のあるインターフェイスまたはハードウェアコンポーネントを説明するときに使用される混乱を避けるためにここに含まれています。コメントなどで「単語」を使用する場合、キュービットコードの16ビットを常に意味します。
一般的に言えば、ADAインターフェイスパッケージ、つまりunsigned_8、unsigned_32などを使用してデータ型の長さを明示的に述べます。たとえば、上記の用語は、「32ビット値」を綴るのではなく、コメントで使用できます。
Spark関数には副作用がないため、代わりに手順が使用され、結果を返すのではなく、結果のパラメーターが必要です。すべての手順の結果に一時的な割り当てを割り当てるのは少し苦痛です。
定数の定義は、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ブートアップ中に行われます。セカンダリスタックオーバーフローは実行時に検出する必要がありますが、注意してください。 syscalls and indurters中に、プロセスのカーネルスタックが使用されている場合があり、セカンダリスタックはありません。
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ディスクイメージを作成して、これらのコマンドを使用してキュービットで読むことができます。ここには、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
これで、次のようなvirtualbox形式に変換できるディスクイメージがあります。
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
VM設定で、> IDEコントローラーの下に新しいディスクを追加できます。おそらくICH6チップセットを使用したいと思うでしょう。 Cubitは現在、ATA I/Oに古代のPIO法を使用しています。ディスクイメージを作成し、異なるチップセットで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のヒント：
登録add'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を実行します（注：no ".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.
