Theseus
Theseus is a modern OS written from scratch in Rust that explores 𝐢𝐧𝐭𝐫𝐚𝐥𝐢𝐧𝐠𝐮𝐚𝐥 𝐝𝐞𝐬𝐢𝐠𝐧: closing the semantic gap between compiler and hardware by maximally leveraging the power of language safety and affine types. Theseus aims to shift OS responsibilities like resource management into the compiler.
Top Related Projects
Mirror of https://gitlab.redox-os.org/redox-os/redox
A secure embedded operating system for microcontrollers
Rust version of THU uCore OS. Linux compatible.
A new operating system kernel with Linux binary compatibility written in Rust.
The seL4 microkernel
Quick Overview
Theseus is an experimental operating system written in Rust, focusing on intralingual design and runtime flexibility. It aims to explore new OS structure paradigms, emphasizing type safety, fault isolation, and dynamic runtime adaptation without sacrificing performance.
Pros
- Built entirely in Rust, leveraging its safety and performance features
- Innovative intralingual design, allowing for better integration between kernel and userspace
- Supports runtime flexibility and adaptability
- Strong focus on type safety and fault isolation
Cons
- Experimental nature means it's not suitable for production use
- Limited hardware support compared to mainstream operating systems
- Steep learning curve due to its unique design and implementation
- Smaller community and ecosystem compared to established operating systems
Getting Started
To get started with Theseus OS:
-
Clone the repository:
git clone https://github.com/theseus-os/Theseus.git cd Theseus
-
Install dependencies (assuming you're on a Unix-like system):
./scripts/install_deps.sh
-
Build Theseus:
make
-
Run Theseus in QEMU:
make run
Note: Theseus OS is a research project and not intended for daily use. These instructions are for developers interested in exploring or contributing to the project.
Competitor Comparisons
Mirror of https://gitlab.redox-os.org/redox-os/redox
Pros of Redox
- More mature and feature-complete operating system
- Larger community and ecosystem of applications
- Supports a wider range of hardware architectures
Cons of Redox
- Less focus on memory safety at the kernel level
- More complex system architecture
- Slower boot times due to traditional OS design
Code Comparison
Redox (Rust):
#[no_mangle]
pub extern fn rust_main() -> ! {
// Initialize system
init::init();
// Drop to userspace
userspace::userspace_init();
}
Theseus (Rust):
#[no_mangle]
pub extern "C" fn kernel_init() -> ! {
// Initialize kernel subsystems
kernel::init();
// Start scheduler
scheduler::start();
}
Both projects use Rust for system-level programming, but Theseus focuses on a single address space OS design, while Redox follows a more traditional microkernel architecture. Theseus emphasizes type-safe and memory-safe abstractions throughout the entire system, whereas Redox prioritizes POSIX compatibility and a Unix-like design. The code snippets show the entry points for both operating systems, highlighting their different approaches to system initialization and execution flow.
A secure embedded operating system for microcontrollers
Pros of Tock
- Written in Rust, providing memory safety and concurrency benefits
- Designed specifically for embedded systems and IoT devices
- Supports multiple architectures including ARM Cortex-M and RISC-V
Cons of Tock
- Less flexible than Theseus for general-purpose computing
- May have a steeper learning curve for developers not familiar with embedded systems
- Limited to specific hardware platforms compared to Theseus' broader compatibility
Code Comparison
Tock (kernel initialization):
pub unsafe fn initialize() {
// Enable all interrupts
cortexm::interrupt::enable_all();
// Initialize and enable systick counter
cortexm::systick::SysTick::initialize();
}
Theseus (kernel initialization):
pub fn initialize() -> Result<(), &'static str> {
interrupts::init()?;
memory::init()?;
scheduler::init()?;
Ok(())
}
Both operating systems use Rust for kernel development, emphasizing safety and performance. Tock focuses on embedded systems with specific hardware initializations, while Theseus takes a more general approach to system initialization, reflecting its broader compatibility goals.
Rust version of THU uCore OS. Linux compatible.
Pros of rCore
- Written in Rust, providing memory safety and concurrency benefits
- Supports multiple architectures (x86_64, RISC-V, aarch64)
- More mature project with a larger community and documentation
Cons of rCore
- Less focus on language-based isolation compared to Theseus
- May have higher memory overhead due to traditional OS design
- Potentially slower inter-process communication
Code Comparison
rCore (syscall implementation):
pub fn sys_write(fd: usize, buf: *const u8, len: usize) -> isize {
let task = current_task().unwrap();
let token = current_user_token();
let mut buffer = Vec::new();
for i in 0..len {
let byte_ref = translated_byte(token, (buf as usize + i) as *const u8);
buffer.push(*byte_ref);
}
task.acquire_inner_lock().write(fd, buffer.as_slice())
}
Theseus (syscall implementation):
pub fn syscall_write(fd: usize, buf: *const u8, count: usize) -> Result<usize, SyscallError> {
let current_task = scheduler::get_my_current_task()?;
let bytes = current_task.copy_from_userspace(buf, count)?;
let file = current_task.get_file(fd)?;
file.write(&bytes)
}
Both examples show syscall implementations, but Theseus demonstrates a more streamlined approach with stronger type safety and error handling.
A new operating system kernel with Linux binary compatibility written in Rust.
Pros of Kerla
- Written in Rust, providing memory safety and concurrency benefits
- Supports userspace applications and has a basic shell
- Implements virtual memory and process management
Cons of Kerla
- Less mature and feature-rich compared to Theseus
- Limited documentation and community support
- Narrower focus on basic OS functionality
Code Comparison
Kerla (memory allocation):
pub fn alloc_pages(order: usize) -> Option<PhysAddr> {
ALLOCATOR.lock().alloc_pages(order)
}
Theseus (memory allocation):
pub fn allocate_pages(num_pages: usize) -> Result<PhysicalAddress, &'static str> {
FRAME_ALLOCATOR.lock().allocate_pages(num_pages)
}
Both projects use Rust for memory management, but Theseus offers a more comprehensive and modular approach to OS development. Kerla focuses on basic OS functionality, while Theseus explores novel OS design concepts like single-address-space and language-based isolation.
Theseus provides more extensive documentation and research papers, making it easier for developers to understand and contribute. Kerla, being a smaller project, may be more approachable for beginners but lacks the depth and breadth of features found in Theseus.
Overall, Theseus offers a more ambitious and well-documented approach to OS development, while Kerla provides a simpler, more focused implementation of basic OS concepts in Rust.
The seL4 microkernel
Pros of seL4
- Formally verified microkernel, providing high security and reliability
- Extensive documentation and research backing its design and implementation
- Supports multiple architectures (x86, ARM, RISC-V)
Cons of seL4
- Steeper learning curve due to its formal verification approach
- Less flexible for rapid prototyping and experimentation
- Requires more resources for development and maintenance
Code Comparison
seL4:
static inline void *
PURE CONST cap_get_capPtr(cap_t cap)
{
return (void *)(cap.words[0] & MASK(WORD_SIZE - 1));
}
Theseus:
pub fn create_task(
task_type: TaskType,
name: String,
function: extern "C" fn() -> !,
) -> Result<TaskRef, &'static str> {
// Implementation details...
}
Key Differences
- seL4 is written in C, while Theseus is implemented in Rust
- seL4 focuses on formal verification, whereas Theseus emphasizes language-based safety
- Theseus aims for runtime flexibility and modularity, while seL4 prioritizes security guarantees
Use Cases
- seL4: High-security systems, critical infrastructure, verified software stacks
- Theseus: Research, experimental OS designs, exploring language-based safety in systems
Convert designs to code with AI
Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.
Try Visual CopilotREADME
Theseus OS
Theseus is a new OS written from scratch in Rust to experiment with novel OS structure, better state management, and how to leverage intralingual design principles to shift OS responsibilities like resource management into the compiler.
For more info, check out Theseus's documentation or our published academic papers, which describe Theseus's design and implementation.
Theseus is under active development, and although it is not yet mature, we envision that Theseus will be useful in high-end embedded systems or edge datacenter environments. We are continually working to improve the OS, including its fault recovery abilities for higher system availability without redundancy, as well as easier and more arbitrary live evolution and runtime flexibility.
Quick start
On Linux (Debian-like distros), do the following:
- Obtain the Theseus repository (with all submodules):
git clone --recurse-submodules --depth 1 https://github.com/theseus-os/Theseus.git
- Install Rust:
curl https://sh.rustup.rs -sSf | sh
- Install dependencies:
sudo apt-get install make gcc nasm pkg-config grub-pc-bin mtools xorriso qemu qemu-kvm wget
- Build and run (in QEMU):
To exit QEMU, press Ctrl + A, then X.cd Theseus make run
See below for more detailed instructions.
Building and Running Theseus
Note: when you first check out the project, be sure to get all the submodule repositories too:
git submodule update --init --recursive
Currently, we support building Theseus on the following platforms:
- Linux, 64-bit Debian-based distributions like Ubuntu, tested on Ubuntu 16.04, 18.04, 20.04.
- Arch Linux and Fedora have also been reported to work correctly.
- Windows, using the Windows Subsystem for Linux (WSL), tested on the Ubuntu version of WSL and WSL2.
- MacOS, tested on versions High Sierra (v10.13), Catalina (v10.15), and Ventura (v13.5).
- Docker, atop any host OS that can run a Docker container.
Setting up the build environment
First, install Rust by following the setup instructions here. On Linux, just run:
curl https://sh.rustup.rs -sSf | sh
Building on Linux or WSL (Windows Subsystem for Linux)
Install the following dependencies using your package manager:
sudo apt-get install make gcc nasm pkg-config grub-pc-bin mtools xorriso qemu qemu-kvm wget
- Or:
# Arch Linux sudo pacman -S make gcc nasm pkg-config grub mtools xorriso qemu wget # Fedora sudo dnf install make gcc nasm pkg-config grub2 mtools xorriso qemu wget
If you're on WSL, also do the following steps:
-
Install an X Server for Windows; we suggest using Xming or VcXsvr.
- You'll likely need to invoke those X servers with the
-ac
argument (or use the GUI to disable access control).
- You'll likely need to invoke those X servers with the
-
Setup an X display as follows:
- on original WSL (version 1), run:
export DISPLAY=:0
- on WSL2 (version 2), run:
export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2}'):0
You'll need to do this each time you open up a new WSL terminal, so it's best to add it to the end of your
.bashrc
or.profile
file in your$HOME
directory. - on original WSL (version 1), run:
-
If you get an error like
Could not initialize SDL (No available video device) ...
or any type of GTK or video device error, then make sure that your X Server is running and that you have set theDISPLAY
environment variable above. -
NOTE: WSL and WSL2 do not currently support using KVM.
Building on MacOS
- Install HomeBrew, then run the MacOS build setup script:
If things go wrong, remove the following build directories and try to run the script again.sh ./scripts/mac_os_build_setup.sh
rm -rf /tmp/theseus_tools_src
- NOTE: on MacOS, you need to run
gmake
instead ofmake
for build commands (or you can simply create a shell alias).- This is because HomeBrew installs its binaries in a way that doesn't conflict with built-in versions of system utilities.
- (This is typically not necessary): if you're building Theseus on older Apple Silicon (M1 chips), you may need to use
bash
with x86 emulation:
and possibly adjust your systemarch -x86_64 bash # or another shell of your choice
PATH
if both x86 and ARM homebrew binaries are installed:export PATH=/usr/local/Homebrew/bin:$PATH
Building using Docker
Note: building and running Theseus within a Docker container may be slower than on a native host OS.
- Ensure docker scripts are executable:
chmod +x docker/*.sh
- (Skip if docker is already installed.) Install Docker Engine. We provide a convenience script for this on Ubuntu:
./docker/install_docker_ubuntu.sh
- After docker installs, enable your user account to run docker without root privileges:
sudo groupadd docker; sudo usermod -aG docker $USER
Then, log out and log back in (or restart your computer) for the user/group changes to take effect.
- After docker installs, enable your user account to run docker without root privileges:
- Build the docker image:
This does not build Theseus, but rather only creates a docker image that contains all the necessary dependencies to build and run Theseus../docker/build_docker.sh
- Run the new docker image locally as a container:
Now you can run./docker/run_docker.sh
make run
or other Theseus-specific build/run commands from within the docker container's shell.
Notes on Docker usage:
- The docker-based workflow should only require you to re-run the
run_docker.sh
script multiple times when re-building or running Theseus after modifying its code. You shouldn't need to re-runbuild_docker.sh
multiple times, though it won't hurt. - KVM doesn't currently work in docker. To run Theseus in QEMU using KVM, you can build Theseus within docker, exit the container (via Ctrl + D
), and then run
make orun host=yes` on your host machine.
Building and Running
Build the default Theseus OS image and run it in QEMU:
make run
Or, build a full Theseus OS image with all features and crates enabled:
make full ## or `make all`
Run make help
to see other make targets and the various command-line options.
Using the Limine bootloader instead of GRUB
To use Limine instead of GRUB, clone pre-built limine and pass bootloader=limine
to make:
git clone https://github.com/limine-bootloader/limine.git limine-prebuilt
git -C limine-prebuilt reset --hard 3f6a330
make run bootloader=limine
Feel free to try newer versions, however they may not work.
Targeting ARMv8 (aarch64)
Support for Theseus on aarch64 is an ongoing effort, but most of the core subsystems are complete.
To build and run Theseus on aarch64, first install the required dependencies:
- On Debian-like Linux (Ubuntu, etc):
sudo apt-get install qemu-system-arm gcc-aarch64-linux-gnu
- On Arch Linux:
sudo pacman -S aarch64-linux-gnu-gcc qemu-system-aarch64
- On macOS, the
mac_os_build_setup
script should have already installed this for you, but if not:brew install aarch64-elf-gcc aarch64-elf-binutils
Then, build Theseus and run it in QEMU:
make ARCH=aarch64 run
Doing a "full" build of all Theseus crates isn't yet supported on aarch64, as our aarch64 support in Theseus doesn't yet cover all crates in the entire repo.
Using QEMU
QEMU allows us to run Theseus quickly and easily in its own virtual machine.
To release your keyboard and mouse focus from the QEMU window, press Ctrl + Alt + G, or Ctrl + Alt on some systems, or just Cmd + Tab out to another app on macOS.
To exit QEMU, in the terminal window that you originally ran make run
, press Ctrl + A then X, or you can also click the GUI â§
button on the title bar if running QEMU in graphical mode.
To investigate the hardware/machine state of the running QEMU VM, you can switch to the QEMU console by pressing Ctrl + Alt + 2.
Switch back to the main window with Ctrl + Alt + 1.
On Mac, manually select VGA
or compact_monitor0
under View
from the QEMU menu bar.
To access/expose a PCI device in QEMU using PCI passthrough via VFIO, see these instructions.
Linux does not support the ICMP protocol (for ping
) for guest OSes in QEMU by default, so to allow ping
to work on Theseus, you may need to run the following in your Linux host machine:
sudo sh -c "echo \"0 2147483647\" > /proc/sys/net/ipv4/ping_group_range"
KVM Support
While not strictly required, KVM will speed up the execution of QEMU. To install KVM, run the following command:
sudo apt-get install kvm
To enable KVM support, add host=yes
to your make command, e.g.,
make run host=yes
Note that KVM acceleration is only supported on native Linux hosts.
Documentation
Theseus includes two forms of documentation:
- The source-level documentation, generated from code and inline comments (via rustdoc).
- Intended for Theseus developers and contributors, or those who want low-level details.
- The book-style documentation, written in Markdown.
- Useful for high-level descriptions of design concepts and key components.
To build the documentation yourself, set up your local build environment and then run the following:
make view-doc ## for the source-level docs
make view-book ## for the Theseus book
Other
Booting on Real Hardware
We have tested Theseus on a variety of real machines, including Intel NUC devices, various Thinkpad laptops, and Supermicro servers. Currently, we have only tested booting Theseus via USB or PXE using a traditional BIOS bootloader rather than UEFI, but UEFI is fully supported so it should work.
To boot over USB, simply run make usb drive=sdc
, in which sdc
is the device node for the USB disk itself (not a partition like sdc2) to which you want to write the OS image.
On WSL or other host environments where /dev
device nodes don't exist, you can simply run make iso
and burn the .iso
file in the build/
directory to a USB, e.g., using Rufus on Windows.
To boot Theseus over PXE (network boot), see this set of separate instructions.
Debugging Theseus on QEMU
GDB has built-in support for QEMU, but it doesn't play nicely with OSes that run in 64-bit long mode. In order to get it working properly with our OS in Rust, we need to patch it and build it locally. The hard part has already been done for us (details here), so we can just quickly set it up with the following commands.
-
Install the following packages:
sudo apt-get install texinfo flex bison python-dev ncurses-dev
-
From the base Theseus directory, run this script to download and build GDB from an existing patched repo:
curl -sf https://raw.githubusercontent.com/phil-opp/binutils-gdb/rust-os/build-rust-os-gdb.sh | sh
After that, you should have a
rust-os-gdb
directory that contains thegdb
executables and scripts. -
Run Theseus in QEMU using
make run
(ormake run_pause
to pause QEMU until we attach GDB). -
In another terminal window, run the following to start GDB and attach it to the running QEMU instance:
make gdb
QEMU will be paused until we move the debugger forward, with standard GDB commands like
n
to step through the next instruction orc
to continue execution. Any standard GDB commands will now work.
Connecting GDB to aarch64 Theseus on QEMU
We don't yet have a patched version of GDB for aarch64 targets, but we can use the existing gdb-multiarch
package to
-
Install the required package:
sudo apt-get install gdb-multiarch
-
Build Theseus for aarch64 and run it in QEMU:
make ARCH=aarch64 run ## or use `run_pause`
-
In another terminal window, run the following to start GDB and attach it to the running QEMU instance:
gdb-multiarch -ex "target remote :1234"
-
Within GDB, symbols aren't yet supported, but you can view assembly code with
layout asm
and set breakpoints on virtual addresses.
IDE Setup
Our personal preference is to use VS Code, which has excellent cross-platform support for Rust. Other options are available here.
For VS Code, recommended plugins are:
- rust-analyzer, by matklad
- Better TOML, by bungcip
- x86 and x86_64 Assembly, by 13xforever
Acknowledgements
We would like to express our thanks to the OS Dev wiki and its community and to Philipp Oppermann's blog_os for serving as excellent starting points for Theseus. The early days of Theseus's development progress are indebted to these resources.
License
Theseus's source code is licensed under the MIT License. See the LICENSE-MIT file for more.
Contributing
We adhere to similar development and code style guidelines as the core Rust language project. See more here.
PRs and issues are welcome from anyone; because Theseus is an experimental OS, certain features may be deprioritized or excluded from the main branch. Don't hesitate to ask or mention something though! :smile:
Top Related Projects
Mirror of https://gitlab.redox-os.org/redox-os/redox
A secure embedded operating system for microcontrollers
Rust version of THU uCore OS. Linux compatible.
A new operating system kernel with Linux binary compatibility written in Rust.
The seL4 microkernel
Convert designs to code with AI
Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.
Try Visual Copilot