Skip to content

Commit

Permalink
Renaming everything to Microkit
Browse files Browse the repository at this point in the history
Another thing that had to be lumped up in this commit was
updating to the latest rust-seL4 which also renames to
Microkit.
  • Loading branch information
Ivan-Velickovic committed Sep 23, 2023
1 parent d7d35c0 commit 0d83b51
Show file tree
Hide file tree
Showing 41 changed files with 579 additions and 486 deletions.
52 changes: 26 additions & 26 deletions .github/workflows/ci.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@ on:

jobs:
build_manual:
name: Build VMM manual
name: Build manual
runs-on: ubuntu-20.04
steps:
- name: Checkout seL4CP VMM repository
- name: Checkout VMM repository
uses: actions/checkout@v3
- name: Install pandoc/latex via apt
run: sudo apt update && sudo apt install -y pandoc texlive-latex-base texlive-fonts-recommended texlive-formats-extra
Expand All @@ -27,13 +27,13 @@ jobs:
name: Build and run VMM examples (Linux x86-64)
runs-on: ubuntu-20.04
steps:
- name: Checkout seL4CP VMM repository
- name: Checkout VMM repository
uses: actions/checkout@v3
- name: Download seL4CP SDK
run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
- name: Download Microkit SDK
run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
shell: bash
- name: Extract seL4CP SDK
run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
- name: Extract Microkit SDK
run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
- name: Install VMM dependencies (via apt)
# 'expect' is only a dependency for CI testing
run: sudo apt update && sudo apt install -y make clang lld llvm qemu-system-arm device-tree-compiler expect
Expand All @@ -45,7 +45,7 @@ jobs:
- name: Install Rust
run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
- name: Build and run VMM examples
run: ./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6
run: ./ci/examples.sh ${PWD}/microkit-sdk-1.2.6
shell: bash
- name: Upload built system images
uses: actions/upload-artifact@v3
Expand All @@ -56,13 +56,13 @@ jobs:
name: Build and run VMM examples (macOS x86-64)
runs-on: macos-12
steps:
- name: Checkout seL4CP VMM repository
- name: Checkout VMM repository
uses: actions/checkout@v3
- name: Download seL4CP SDK
run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
- name: Download Microkit SDK
run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
shell: bash
- name: Extract seL4CP SDK
run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
- name: Extract Microkit SDK
run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
- name: Install VMM dependencies (via Homebrew)
# 'expect' is only a dependency for CI testing
run: |
Expand All @@ -76,7 +76,7 @@ jobs:
- name: Install Rust
run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
- name: Build and run VMM examples
run: ./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6
run: ./ci/examples.sh ${PWD}/microkit-sdk-1.2.6
shell: bash
- name: Upload built system images
uses: actions/upload-artifact@v3
Expand All @@ -86,19 +86,19 @@ jobs:
name: Build and run VMM examples (Linux x86-64 via Nix)
runs-on: ubuntu-20.04
steps:
- name: Checkout seL4CP VMM repository
- name: Checkout VMM repository
uses: actions/checkout@v3
- name: Download seL4CP SDK
run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
- name: Download Microkit SDK
run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
shell: bash
- name: Extract seL4CP SDK
run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
- name: Extract Microkit SDK
run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
- name: Install Nix
uses: cachix/install-nix-action@v22
with:
nix_path: nixpkgs=channel:nixos-unstable
- name: Build and run VMM examples
run: nix-shell --pure --run "./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6"
run: nix-shell --pure --run "./ci/examples.sh ${PWD}/microkit-sdk-1.2.6"
- name: Upload built system images
uses: actions/upload-artifact@v3
with:
Expand All @@ -107,21 +107,21 @@ jobs:
name: Build and run VMM examples (macOS x86-64 via Nix)
runs-on: macos-12
steps:
- name: Checkout seL4CP VMM repository
- name: Checkout VMM repository
uses: actions/checkout@v3
- name: Download seL4CP SDK
run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
- name: Download Microkit SDK
run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
shell: bash
- name: Extract seL4CP SDK
run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
- name: Extract Microkit SDK
run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
- name: Install Nix
uses: cachix/install-nix-action@v22
with:
nix_path: nixpkgs=channel:nixos-unstable
- name: Update Nix channel
run: nix-channel --update
- name: Build and run VMM examples
run: nix-shell --pure --run "./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6"
run: nix-shell --pure --run "./ci/examples.sh ${PWD}/microkit-sdk-1.2.6"
- name: Upload built system images
uses: actions/upload-artifact@v3
with:
Expand Down
18 changes: 9 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# VMM on the seL4 Core Platform
# libvmm

This is a Virtual Machine Monitor (VMM) built on the seL4 Core Platform (seL4CP).
This is a Virtual Machine Monitor (VMM) built on the [seL4 Microkit](https://github.com/seL4/microkit).
The purpose of the VMM is to make it easy to run virtual machines on top of the seL4 microkernel.

It is (at least initially) a port of the already existing
Expand Down Expand Up @@ -51,10 +51,10 @@ Using [Nix](https://nixos.org/):
nix-shell --pure
```

Finally, you will need an experimental seL4 Core Platform SDK.
Finally, you will need an experimental Microkit SDK.

* Currently virtualisation support and other patches that the VMM requires are
not part of mainline seL4 Core Platform. See below for instructions on
not part of mainline Microkit. See below for instructions on
acquiring the SDK.
* Upstreaming the required changes is in-progress.

Expand Down Expand Up @@ -96,24 +96,24 @@ tar xf sel4cp-sdk-dev-bf06734-macos-aarch64.tar.gz

##### Option 2 - Building the SDK

You will need a development version of the seL4CP SDK source code. You can acquire it with the following command:
You will need a development version of the Microkit SDK source code. You can acquire it with the following command:
```sh
git clone https://github.com/Ivan-Velickovic/sel4cp.git --branch dev
git clone https://github.com/Ivan-Velickovic/microkit.git --branch dev
```

From here, you can follow the instructions
[here](https://github.com/Ivan-Velickovic/sel4cp/tree/dev) to build the SDK.
[here](https://github.com/Ivan-Velickovic/microkit/tree/dev) to build the SDK.

If you have built the SDK then the path to the SDK should look something like
this: `sel4cp/release/sel4cp-sdk-1.2.6`.
this: `microkit/release/microkit-sdk-1.2.6`.

## Building the example system

Finally, we can simulate a basic system with a single Linux guest with the
following command. We want to run the `simple` example system in a `debug`
configuration for the QEMU ARM virt system.
```sh
make BOARD=qemu_arm_virt SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6 qemu
make BOARD=qemu_arm_virt MICROKIT_SDK=/path/to/sdk qemu
```

You should see Linux booting and be greeted with the buildroot prompt:
Expand Down
6 changes: 3 additions & 3 deletions ci/acquire_sdk.sh
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ fi
SDK_PATH=$1
GITHUB_TOKEN=$2
SDK_TARGET=$3
SEL4CP_REPO="Ivan-Velickovic/sel4cp"
MICROKIT_REPO="Ivan-Velickovic/microkit"
# zip is the only available option
ARCHIVE_FORMAT="zip"

Expand All @@ -40,7 +40,7 @@ ARTIFACT_ID=`curl \
-H "Accept: application/vnd.github+json" \
-H "Authorization: Bearer ${GITHUB_TOKEN}"\
-H "X-GitHub-Api-Version: 2022-11-28" \
https://api.github.com/repos/$SEL4CP_REPO/actions/artifacts | jq ".artifacts[$ARTIFACT_INDEX].id"`
https://api.github.com/repos/$MICROKIT_REPO/actions/artifacts | jq ".artifacts[$ARTIFACT_INDEX].id"`

echo "Downloading SDK with artifact ID: ${ARTIFACT_ID}"
curl \
Expand All @@ -49,4 +49,4 @@ curl \
-o $SDK_PATH \
-H "Accept: application/vnd.github+json" \
-H "X-GitHub-Api-Version: 2022-11-28" \
https://api.github.com/repos/$SEL4CP_REPO/actions/artifacts/$ARTIFACT_ID/$ARCHIVE_FORMAT
https://api.github.com/repos/$MICROKIT_REPO/actions/artifacts/$ARTIFACT_ID/$ARCHIVE_FORMAT
6 changes: 3 additions & 3 deletions ci/examples.sh
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ build_simple_make() {
BUILD_DIR=${BUILD_DIR} \
CONFIG=${CONFIG} \
BOARD=${BOARD} \
SEL4CP_SDK=${SDK_PATH}
MICROKIT_SDK=${SDK_PATH}
}

build_simple_zig() {
Expand All @@ -43,7 +43,7 @@ build_rust() {
make -C examples/rust -B \
BUILD_DIR=${BUILD_DIR} \
CONFIG=${CONFIG} \
SEL4CP_SDK=${SDK_PATH}
MICROKIT_SDK=${SDK_PATH}
}

simulate_rust() {
Expand Down Expand Up @@ -88,7 +88,7 @@ build_simple_make "odroidc4" "release"

build_rust "debug"
simulate_rust "debug"
# @ivanv: TODO get Rust in with release version of seL4CP working
# @ivanv: TODO get Rust in with release version of Microkit working
# build_rust "release"
# simulate_rust "release"

Expand Down
8 changes: 4 additions & 4 deletions docs/MANUAL.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
# seL4CP VMM manual
# libvmm manual

This document aims to describe the VMM and how to use it. If you feel there is
something missing from this document or the VMM itself, feel free to let us
know by [opening an issue on the GitHub repository](https://github.com/au-ts/sel4cp_vmm).
know by [opening an issue on the GitHub repository](https://github.com/au-ts/libvmm).

## Supported platforms

Expand Down Expand Up @@ -109,7 +109,7 @@ driver in the VMM. Like the UART, the address of the GIC is platform specific.
An example Make command looks something like this:
```sh
make BUILD_DIR=build \
SEL4CP_SDK=/path/to/sdk \
MICROKIT_SDK=/path/to/sdk \
CONFIG=debug \
BOARD=qemu_arm_virt \
SYSTEM=simple.system \
Expand All @@ -121,7 +121,7 @@ make BUILD_DIR=build \
Before you can port the VMM to your desired platform you must have the following:

* A working platform port of the seL4 kernel in hypervisor mode.
* A working platform port of the seL4 Core Platform where the kernel is built as a
* A working platform port of the seL4 Microkit where the kernel is built as a
hypervisor.

### Guest setup
Expand Down
12 changes: 6 additions & 6 deletions examples/ethernet/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@
# SPDX-License-Identifier: BSD-2-Clause
#

ifeq ($(strip $(SEL4CP_SDK)),)
$(error SEL4CP_SDK must be specified)
ifeq ($(strip $(MICROKIT_SDK)),)
$(error MICROKIT_SDK must be specified)
endif

ifeq ($(strip $(BOARD)),)
Expand Down Expand Up @@ -43,7 +43,7 @@ endif

CC := $(TOOLCHAIN)-gcc
LD := $(TOOLCHAIN)-ld
SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit

# @ivanv: need to have a step for putting in the initrd node into the DTB,
# right now it is unfortunately hard-coded.
Expand All @@ -54,7 +54,7 @@ SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp

# @ivanv: incremental builds don't work with IMAGE_DIR changing

BOARD_DIR := $(SEL4CP_SDK)/board/$(BOARD)/$(CONFIG)
BOARD_DIR := $(MICROKIT_SDK)/board/$(BOARD)/$(CONFIG)
VMM := ../../
VMM_TOOLS := $(VMM)/tools
VMM_SRC_DIR := $(VMM)/src
Expand Down Expand Up @@ -93,7 +93,7 @@ CFLAGS := -mstrict-align \
-DCONFIG_$(CONFIG) \

LDFLAGS := -L$(BOARD_DIR)/lib
LIBS := -lsel4cp -Tsel4cp.ld
LIBS := -lmicrokit -Tmicrokit.ld

all: directories $(IMAGE_FILE)

Expand Down Expand Up @@ -143,4 +143,4 @@ $(BUILD_DIR)/vmm.elf: $(addprefix $(BUILD_DIR)/, $(VMM_OBJS))
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@

$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(ELFS)) $(SYSTEM_DESCRIPTION) $(IMAGE_DIR)
$(SEL4CP_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
$(MICROKIT_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
4 changes: 2 additions & 2 deletions examples/ethernet/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ The example currently works on the following platforms:
## Building with Make

```sh
make BOARD=<BOARD> SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6
make BOARD=<BOARD> MICROKIT_SDK=/path/to/sdk
```

Where `<BOARD>` is one of:
Expand All @@ -20,7 +20,7 @@ and `BUILD_DIR`, see the Makefile for details.

If you would like to simulate the QEMU board you can run the following command:
```sh
make BOARD=qemu_arm_virt SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6 qemu
make BOARD=qemu_arm_virt MICROKIT_SDK=/path/to/sdk qemu
```

This will build the example code as well as run the QEMU command to simulate a
Expand Down
20 changes: 10 additions & 10 deletions examples/ethernet/vmm.c
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
*/
#include <stddef.h>
#include <stdint.h>
#include <sel4cp.h>
#include <microkit.h>
#include "util/util.h"
#include "arch/aarch64/vgic/vgic.h"
#include "arch/aarch64/linux.h"
Expand Down Expand Up @@ -58,28 +58,28 @@ extern char _guest_dtb_image_end[];
/* Data for the initial RAM disk to be passed to the kernel. */
extern char _guest_initrd_image[];
extern char _guest_initrd_image_end[];
/* seL4CP will set this variable to the start of the guest RAM memory region. */
/* Microkit will set this variable to the start of the guest RAM memory region. */
uintptr_t guest_ram_vaddr;

static void serial_ack(size_t vcpu_id, int irq, void *cookie) {
/*
* For now we by default simply ack the serial IRQ, we have not
* come across a case yet where more than this needs to be done.
*/
sel4cp_irq_ack(SERIAL_IRQ_CH);
microkit_irq_ack(SERIAL_IRQ_CH);
}

static void ethernet_ack(size_t vcpu_id, int irq, void *cookie) {
sel4cp_irq_ack(ETHERNET_IRQ_CH);
microkit_irq_ack(ETHERNET_IRQ_CH);
}

static void ethernet_phy_ack(size_t vcpu_id, int irq, void *cookie) {
sel4cp_irq_ack(ETHERNET_PHY_IRQ_CH);
microkit_irq_ack(ETHERNET_PHY_IRQ_CH);
}

void init(void) {
/* Initialise the VMM, the VCPU(s), and start the guest */
LOG_VMM("starting \"%s\"\n", sel4cp_name);
LOG_VMM("starting \"%s\"\n", microkit_name);
/* Place all the binaries in the right locations before starting the guest */
size_t kernel_size = _guest_kernel_image_end - _guest_kernel_image;
size_t dtb_size = _guest_dtb_image_end - _guest_dtb_image;
Expand Down Expand Up @@ -112,12 +112,12 @@ void init(void) {
success = virq_register(GUEST_VCPU_ID, ETHERNET_PHY_IRQ, &ethernet_phy_ack, NULL);
#endif
/* Just in case there is already an interrupt available to handle, we ack it here. */
sel4cp_irq_ack(SERIAL_IRQ_CH);
microkit_irq_ack(SERIAL_IRQ_CH);
/* Finally start the guest */
guest_start(GUEST_VCPU_ID, kernel_pc, GUEST_DTB_VADDR, GUEST_INIT_RAM_DISK_VADDR);
}

void notified(sel4cp_channel ch) {
void notified(microkit_channel ch) {
switch (ch) {
case ETHERNET_IRQ_CH: {
bool success = virq_inject(GUEST_VCPU_ID, ETHERNET_IRQ);
Expand Down Expand Up @@ -152,11 +152,11 @@ void notified(sel4cp_channel ch) {
* whenever our guest causes an exception, it gets delivered to this entry point for
* the VMM to handle.
*/
void fault(sel4cp_id id, sel4cp_msginfo msginfo) {
void fault(microkit_id id, microkit_msginfo msginfo) {
bool success = fault_handle(id, msginfo);
if (success) {
/* Now that we have handled the fault successfully, we reply to it so
* that the guest can resume execution. */
sel4cp_fault_reply(sel4cp_msginfo_new(0, 0));
microkit_fault_reply(microkit_msginfo_new(0, 0));
}
}
Loading

0 comments on commit 0d83b51

Please sign in to comment.