Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Asterinas OSTD

Confucious remarked, “I could follow whatever my heart desired without transgressing the law.”

子曰: “从心所欲,不逾矩。”

有了 Asterinas OSTD(作業系統標準函式庫),你無需學習那些不安全的 Rust 程式設計黑魔法,也不必冒著自討苦吃的風險。無論你想做什麼,都能放心去實現。即使今天是你的 Rust 程式設計初體驗,也能確信你的內核絕不會因未定義行為而當機或被入侵。

API

Asterinas OSTD stands as a powerful and solid foundation for safe kernel development, providing high-level safe Rust APIs that are

  1. 對於作業系統開發至關重要,並且
  2. 依賴於使用不安全 Rust。

Most of these APIs fall into the following categories:

  • 記憶體分配(例如:分配與存取物理記憶體分頁)
  • 任務管理(例如:在內核任務之間的上下文切換)
  • 使用者空間(例如:操縱與進入使用者空間)
  • 中斷處理(例如:註冊中斷處理器)
  • 計時器管理(例如:註冊計時器處理器)
  • Driver support (e.g., performing DMA and MMIO)
  • 開機支援(例如:從開機載入程式獲取資訊)
  • 同步(例如:鎖定與休眠)

To explore how these APIs come into play, see the example of a 100-line kernel in safe Rust.

OSTD API 已獲得完整文件記載。您可以透過訪問 docs.rs 來存取完整的 API 文件。

滿足四個要求

In designing and implementing OSTD, we have risen to meet the challenge of fulfilling the aforementioned four criteria as demanded by the framekernel architecture.

Expressiveness is evident through Asterinas Kernel itself, where all system calls, file systems, network protocols, and device drivers (e.g., Virtio drivers) have been implemented in safe Rust by leveraging OSTD.

Adopting a minimalist philosophy, OSTD has a small codebase. At its core lies the ostd crate, currently encompassing about 10K lines of code - a figure that is even smaller than those of many microkernels. As OSTD evolves, its codebase will expand, albeit at a relatively slow rate in comparison to the OS services layered atop it.

The OSTD’s efficiency is measurable through the performance metrics of its APIs and the system calls of Asterinas Kernel. No intrinsic limitations have been identified within Rust or the framekernel architecture that could hinder kernel performance.

健全性,與其他三項要求不同,並不容易量化或證明。雖然形式驗證被視為黃金標準,但它需要相當多的資源和時間,且並非當前的首要任務。作為一種更務實的方法,我們將在健全性分析中解釋為何高層設計是健全的,並依賴社區的眾多眼睛來捕捉實作中任何潛在的缺陷。