From 034f655e01705b2f81bd72540021f2aeef3ef441 Mon Sep 17 00:00:00 2001 From: james Date: Wed, 29 Jul 2026 20:16:00 +0100 Subject: [PATCH] feat(pager): resolve write faults and recycle scrubbed frames --- Makefile | 46 +++++++++ client.c | 19 ++++ microkit.patch | 73 +++++++++++++++ pager.c | 249 +++++++++++++++++++++++++++++++++++++++++++++++++ setup.sh | 17 ++++ split.h | 43 +++++++++ split.system | 76 +++++++++++++++ 7 files changed, 523 insertions(+) create mode 100644 Makefile create mode 100644 client.c create mode 100644 microkit.patch create mode 100644 pager.c create mode 100644 setup.sh create mode 100644 split.h create mode 100644 split.system diff --git a/Makefile b/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..6c66466d0fb7da5ade790b32909696d176440122 --- /dev/null +++ b/Makefile @@ -0,0 +1,46 @@ +SDK ?= $(HOME)/.cache/split/microkit-sdk-2.3.1 +TOOL ?= $(HOME)/.cache/split/microkit-2.3.1/target/release/microkit +BOARD := $(SDK)/board/qemu_virt_aarch64/debug +CC := aarch64-linux-gnu-gcc +LD := aarch64-linux-gnu-ld +CFLAGS := -std=gnu11 -O2 -g -Wall -Wextra -Werror -Wno-unused-function -ffreestanding -nostdlib -mstrict-align -I$(BOARD)/include +QEMU := qemu-system-aarch64 -machine virt,virtualization=on -cpu cortex-a53 -m 2G -nographic -monitor none -serial stdio + +.PHONY: all proof clean +all: build/loader.img + +build: + mkdir -p build + +build/pager.o: pager.c split.h | build + $(CC) $(CFLAGS) -c $< -o $@ + +build/alpha.o: client.c split.h | build + $(CC) $(CFLAGS) -DCLIENT=0 -c $< -o $@ + +build/beta.o: client.c split.h | build + $(CC) $(CFLAGS) -DCLIENT=1 -c $< -o $@ + +build/unsafe.o: pager.c split.h | build + $(CC) $(CFLAGS) -DSHARED_WRITE=1 -c $< -o $@ + +build/%.elf: build/%.o + $(LD) -L$(BOARD)/lib $< -lmicrokit -Tmicrokit.ld -o $@ + +build/loader.img: build/pager.elf build/alpha.elf build/beta.elf split.system + MICROKIT_SDK=$(SDK) $(TOOL) --board qemu_virt_aarch64 --config debug --search-path build -o $@ -r build/report.txt split.system + +build/unsafe.img: build/unsafe.elf build/alpha.elf build/beta.elf split.system + sed 's/pager.elf/unsafe.elf/' split.system > build/unsafe.system + MICROKIT_SDK=$(SDK) $(TOOL) --board qemu_virt_aarch64 --config debug --search-path build -o $@ -r build/unsafe.txt build/unsafe.system + +proof: + isabelle build -D . + +build/split.ml: Export.thy Reuse.thy Snapshot.thy Execution.thy Protocol.thy Isolation.thy Model.thy ROOT | build + isabelle build -D . + isabelle export -n -d . -O build/generated -x 'Split.Export:code/**' Split + cp build/generated/Split.Export/code/split.ocaml $@ + +clean: + rm -rf build diff --git a/client.c b/client.c new file mode 100644 index 0000000000000000000000000000000000000000..3ead0fc01e91e5decb9e7257ee87a0ffef6d8bb6 --- /dev/null +++ b/client.c @@ -0,0 +1,19 @@ +#include "split.h" + +void init(void) {} + +void notified(microkit_channel channel) { + require(channel == 0, "unknown notification"); + volatile struct job *job = (void *)TASK; + unsigned p = job->page, length = job->length; + require(p < PAGES && length <= LIMIT, "edit bounds"); + volatile unsigned char *page = (void *)(BASE + p * BYTES); + for (unsigned i = 0; i <= length; ++i) { + page[i] = job->text[i]; + microkit_mr_set(0, p); + microkit_mr_set(1, i); + microkit_mr_set(2, page[i]); + (void)microkit_ppcall(0, microkit_msginfo_new(1, 3)); + } + (void)microkit_ppcall(0, microkit_msginfo_new(2, 0)); +} diff --git a/microkit.patch b/microkit.patch new file mode 100644 index 0000000000000000000000000000000000000000..19ed0c46e1c1e06134935bace91667280671f448 --- /dev/null +++ b/microkit.patch @@ -0,0 +1,73 @@ +--- a/tool/microkit/src/sdf/cspace.rs ++++ b/tool/microkit/src/sdf/cspace.rs +@@ -17,6 +17,7 @@ + Tcb, + Sc, + VSpace, ++ Frame, + } + + #[derive(Debug, PartialEq, Eq)] +@@ -45,9 +46,9 @@ + // At the moment the four cap maps we support all have the 'pd' element, + // so we can include it here. When that stops being the case we will + // have to rework this a bit. +- check_attributes(xml_sdf, node, &["slot", "pd"])?; +- +- let pd = Rc::from(checked_lookup(xml_sdf, node, "pd")?); ++ let source = if cap_type == CapMapType::Frame { "mr" } else { "pd" }; ++ check_attributes(xml_sdf, node, &["slot", source])?; ++ let pd = Rc::from(checked_lookup(xml_sdf, node, source)?); + + let slot: u64 = sdf_parse_required_attribute(xml_sdf, node, "slot")?; + +@@ -91,6 +92,7 @@ + "cap_tcb" => CapMap::from_xml(CapMapType::Tcb, xml_sdf, &*child)?, + "cap_sc" => CapMap::from_xml(CapMapType::Sc, xml_sdf, &*child)?, + "cap_vspace" => CapMap::from_xml(CapMapType::VSpace, xml_sdf, &*child)?, ++ "cap_frame" => CapMap::from_xml(CapMapType::Frame, xml_sdf, &*child)?, + child_name => { + let location = loc_string(xml_sdf, child.range().start); + if let Some(type_name) = child_name.strip_prefix("cap_") { +--- a/tool/microkit/src/sdf.rs ++++ b/tool/microkit/src/sdf.rs +@@ -310,7 +310,11 @@ + + for pd in pds.values() { + for cap_map in pd.cap_maps.iter() { +- if !pds.contains_key(&cap_map.pd) { ++ if cap_map.cap_type == CapMapType::Frame { ++ if !mrs.iter().any(|mr| mr.name.as_str() == cap_map.pd.as_ref()) { ++ return Err(format!("Unknown frame region {}", cap_map.pd)); ++ } ++ } else if !pds.contains_key(&cap_map.pd) { + return Err(format!( + "Error: unknown PD name '{}': {}", + cap_map.pd, +--- a/tool/microkit/src/capdl/builder.rs ++++ b/tool/microkit/src/capdl/builder.rs +@@ -1332,12 +1332,23 @@ + for cap_map in pd.cap_maps.iter() { + // TODO: Once we add more CapMap options, they might not all have + // the pd_name. But for now, they do. +- let pd_src_shadow_cspace = &pd_shadow_cspaces[&cap_map.pd]; ++ let pd_src_shadow_cspace = if cap_map.cap_type == CapMapType::Frame { ++ &pd_shadow_cspaces[&pd.name] ++ } else { ++ &pd_shadow_cspaces[&cap_map.pd] ++ }; + + let cap_map_obj = match cap_map.cap_type { + CapMapType::Tcb => capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb), + CapMapType::Sc => capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context), + CapMapType::VSpace => capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace), ++ CapMapType::Frame => { ++ let frames = &mr_name_to_frames[cap_map.pd.as_ref()]; ++ if frames.len() != 1 { ++ return Err(format!("Frame region {} must contain one page", cap_map.pd)); ++ } ++ capdl_util_make_frame_cap(frames[0], true, true, false, true) ++ }, + }; + + // Map this into the destination pd's cspace and the specified slot. diff --git a/pager.c b/pager.c new file mode 100644 index 0000000000000000000000000000000000000000..5a6a3f6d4ef91cacca85e94ab849203417fa033f --- /dev/null +++ b/pager.c @@ -0,0 +1,249 @@ +#include "split.h" + +#ifndef SHARED_WRITE +#define SHARED_WRITE 0 +#endif + +static unsigned mapping[SLOTS], next = PAGES; +static unsigned available[FRAMES - PAGES], returned; +static seL4_CPtr caps[SLOTS]; +static int started, busy = -1; +static char line[384]; +static unsigned used; +static volatile uint32_t *uart = (void *)0x70000000ul; + +static unsigned char *frame(unsigned f) { + return (unsigned char *)(BACKING + f * BYTES); +} + +static void done(void) { microkit_dbg_puts("@done\n"); } + +static seL4_Word physical(seL4_CPtr cap) { + seL4_ARM_Page_GetAddress_t result = seL4_ARM_Page_GetAddress(cap); + require(result.error == seL4_NoError, "frame address query"); + return result.paddr; +} + +static int length(const char *text, unsigned *size) { + unsigned n = 0; + while (text[n]) if (++n > LIMIT) return 0; + *size = n; + return 1; +} + +static void map(unsigned k, seL4_CPtr page, int write) { + seL4_CapRights_t rights = seL4_CapRights_new(0, 0, 1, write); + require(seL4_ARM_Page_Map(page, microkit_cspace_root_slot_to_cptr(1 + k / PAGES), + BASE + (k % PAGES) * BYTES, rights, + seL4_ARM_Default_VMAttributes | seL4_ARM_ExecuteNever) == seL4_NoError, + "page map"); +} + +static void table(void) { + microkit_dbg_puts("SPLIT TABLE"); + for (unsigned k = 0; k < SLOTS; ++k) { + microkit_dbg_puts(" "); number(mapping[k]); + } + microkit_dbg_puts("\n"); +} + +void init(void) { + for (unsigned f = 0; f < FRAMES; ++f) + for (unsigned b = 0; b < BYTES; ++b) frame(f)[b] = 0; + for (unsigned k = 0; k < SLOTS; ++k) { + mapping[k] = k % PAGES; + caps[k] = microkit_cspace_root_slot_to_cptr(10 + k); + map(k, caps[k], SHARED_WRITE); + } + uart[0x30 / 4] |= 0x301; + uart[0x2c / 4] = 0x60; + uart[0x44 / 4] = 0x7ff; + uart[0x38 / 4] = 0x10; + microkit_irq_ack(5); + table(); + microkit_dbg_puts("@ready\n"); +} + +seL4_Bool fault(microkit_child child, microkit_msginfo info, microkit_msginfo *reply) { + require(child < CLIENTS && microkit_msginfo_get_label(info) == seL4_Fault_VMFault, + "unexpected fault"); + seL4_Word address = microkit_mr_get(seL4_VMFault_Addr); + seL4_Word fsr = microkit_mr_get(seL4_VMFault_FSR); + seL4_Word ip = microkit_mr_get(seL4_VMFault_IP); + require(address >= BASE && address < BASE + PAGES * BYTES && (fsr & (1ul << 6)), + "not a managed write fault"); + unsigned k = child * PAGES + (address - BASE) / BYTES; + unsigned old = mapping[k], fresh = returned ? available[--returned] : next++; + require(old < PAGES && fresh < FRAMES, "frame pool exhausted"); + seL4_Word source = physical(caps[k]); + seL4_CPtr destination = microkit_cspace_root_slot_to_cptr(30 + fresh - PAGES); + seL4_Word target = physical(destination); + for (unsigned b = 0; b < BYTES; ++b) frame(fresh)[b] = frame(old)[b]; + require(seL4_ARM_Page_Unmap(caps[k]) == seL4_NoError, "page unmap"); + caps[k] = microkit_cspace_root_slot_to_cptr(30 + fresh - PAGES); + map(k, caps[k], 1); + mapping[k] = fresh; + microkit_dbg_puts("SPLIT COPY "); number(k); + microkit_dbg_puts(" "); number(old); + microkit_dbg_puts(" "); number(fresh); microkit_dbg_puts("\n"); + table(); + microkit_dbg_puts("SPLIT FAULT "); number(k); + microkit_dbg_puts(" "); number(address); + microkit_dbg_puts(" "); number(ip); + microkit_dbg_puts(" "); number(fsr); + microkit_dbg_puts(" "); number(source); + microkit_dbg_puts(" "); number(target); microkit_dbg_puts("\n"); + *reply = microkit_msginfo_new(0, 0); + return seL4_True; +} + +microkit_msginfo protected(microkit_channel channel, microkit_msginfo info) { + require(channel < CLIENTS && (int)channel == busy, "unexpected worker"); + if (microkit_msginfo_get_label(info) == 1) { + unsigned p = microkit_mr_get(0), offset = microkit_mr_get(1), byte = microkit_mr_get(2); + require(p < PAGES && offset <= LIMIT && byte < 256, "write bounds"); + unsigned k = channel * PAGES + p; + require(frame(mapping[k])[offset] == byte, "write observation"); + microkit_dbg_puts("SPLIT W "); number(k); + microkit_dbg_puts(" "); number(offset); + microkit_dbg_puts(" "); number(byte); microkit_dbg_puts("\n"); + } else { + require(microkit_msginfo_get_label(info) == 2, "unknown worker request"); + busy = -1; + done(); + } + return microkit_msginfo_new(0, 0); +} + +static void request(void) { + if (busy >= 0) { microkit_dbg_puts("@error worker busy\n"); return; } + if (line[0] == 'B' && !started && line[1] == ' ' && line[2] >= '0' && line[2] <= '3' && line[3] == ' ') { + unsigned p = line[2] - '0', size; + if (!length(line + 4, &size)) { microkit_dbg_puts("@error field too long\n"); return; } + for (unsigned b = 0; b < BYTES; ++b) frame(p)[b] = 0; + for (unsigned i = 0; i < size; ++i) frame(p)[i] = line[4 + i]; + done(); + } else if (line[0] == 'S' && !line[1] && !started) { + started = 1; + done(); + } else if (!started) { + microkit_dbg_puts("@error document not opened\n"); + } else if (line[0] == 'E' && line[1] == ' ' && line[2] >= '0' && line[2] <= '1' && line[3] == ' ' && line[4] >= '0' && line[4] <= '3' && line[5] == ' ') { + unsigned c = line[2] - '0', p = line[4] - '0', size; + if (!length(line + 6, &size)) { microkit_dbg_puts("@error field too long\n"); return; } + volatile struct job *job = (void *)(TASK + c * BYTES); + job->page = p; + for (unsigned i = 0; i < size; ++i) job->text[i] = line[6 + i]; + job->text[size] = 0; + job->length = size; + busy = c; + microkit_notify(c); + } else if (line[0] == 'Q' && line[1] == ' ' && line[2] >= '0' && line[2] <= '2' && !line[3]) { + unsigned c = line[2] - '0'; + for (unsigned p = 0; p < PAGES; ++p) { + unsigned k = c * PAGES + p, f = c == 2 ? p : mapping[k]; + if (c < CLIENTS) { + for (unsigned b = 0; b <= LIMIT; ++b) { + microkit_dbg_puts("SPLIT R "); number(k); + microkit_dbg_puts(" "); number(b); + microkit_dbg_puts(" "); number(frame(f)[b]); microkit_dbg_puts("\n"); + if (!frame(f)[b]) break; + } + } + microkit_dbg_puts("@field "); number(p); microkit_dbg_puts(" "); + for (unsigned b = 0; b < LIMIT && frame(f)[b]; ++b) { + char text[2] = {(char)frame(f)[b], 0}; microkit_dbg_puts(text); + } + microkit_dbg_puts("\n"); + } + done(); + } else if (line[0] == 'P' && !line[1]) { + for (unsigned k = 0; k < SLOTS; ++k) { + microkit_dbg_puts("@map "); number(k); + microkit_dbg_puts(" "); number(BASE + (k % PAGES) * BYTES); + microkit_dbg_puts(" "); number(physical(caps[k])); + microkit_dbg_puts(" "); number(mapping[k] >= PAGES); microkit_dbg_puts("\n"); + } + done(); + } else if (line[0] == 'D' && line[1] == ' ' && line[2] >= '0' && line[2] <= '1' && !line[3]) { + unsigned c = line[2] - '0'; + require(seL4_TCB_Suspend(BASE_TCB_CAP + c) == seL4_NoError, "worker suspend"); + microkit_dbg_puts("SPLIT STOP "); number(c); microkit_dbg_puts("\n"); + for (unsigned p = 0; p < PAGES; ++p) { + unsigned k = c * PAGES + p, f = mapping[k]; + if (f < PAGES) continue; + seL4_Word old = physical(caps[k]); + require(seL4_ARM_Page_Unmap(caps[k]) == seL4_NoError, "private page unmap"); + caps[k] = microkit_cspace_root_slot_to_cptr(10 + k); + map(k, caps[k], 0); + mapping[k] = p; + volatile unsigned char *bytes = frame(f); + for (unsigned b = 0; b < BYTES; ++b) bytes[b] = 0; + unsigned cleared = 0; + for (unsigned b = 0; b < BYTES; ++b) cleared += bytes[b] == 0; + require(cleared == BYTES && returned < FRAMES - PAGES, "frame scrub"); + available[returned++] = f; + microkit_dbg_puts("SPLIT RELEASE "); number(k); + microkit_dbg_puts(" "); number(f); + microkit_dbg_puts(" "); number(old); + microkit_dbg_puts(" "); number(physical(caps[k])); + microkit_dbg_puts(" "); number(cleared); microkit_dbg_puts("\n"); + } + table(); + require(seL4_TCB_Resume(BASE_TCB_CAP + c) == seL4_NoError, "worker resume"); + microkit_dbg_puts("SPLIT RUN "); number(c); microkit_dbg_puts("\n"); + done(); + } else if (line[0] == 'F' && !line[1]) { + for (unsigned i = returned; i > 0; --i) { + unsigned f = available[i - 1], cleared = 0; + volatile unsigned char *bytes = frame(f); + for (unsigned b = 0; b < BYTES; ++b) cleared += bytes[b] == 0; + microkit_dbg_puts("@free "); number(f); + microkit_dbg_puts(" "); number(physical(microkit_cspace_root_slot_to_cptr(30 + f - PAGES))); + microkit_dbg_puts(" "); number(cleared); microkit_dbg_puts("\n"); + for (unsigned b = 0; b < 32; ++b) { + microkit_dbg_puts("@zero "); number(f); + microkit_dbg_puts(" "); number(b); + microkit_dbg_puts(" "); number(bytes[b]); microkit_dbg_puts("\n"); + } + } + done(); + } else if (line[0] == 'H' && line[1] == ' ' && line[2] >= '0' && line[2] <= '2' && line[3] == ' ' && line[4] >= '0' && line[4] <= '3' && !line[5]) { + unsigned c = line[2] - '0', p = line[4] - '0', k = c * PAGES + p; + unsigned f = c == 2 ? p : mapping[k]; + seL4_CPtr cap = c == 2 ? microkit_cspace_root_slot_to_cptr(10 + p) : caps[k]; + microkit_dbg_puts("@addr "); number(c == 2 ? BACKING + p * BYTES : BASE + p * BYTES); + microkit_dbg_puts(" "); number(physical(cap)); microkit_dbg_puts("\n"); + for (unsigned b = 0; b < 64; ++b) { + if (c < CLIENTS) { + microkit_dbg_puts("SPLIT R "); number(k); + microkit_dbg_puts(" "); number(b); + microkit_dbg_puts(" "); number(frame(f)[b]); microkit_dbg_puts("\n"); + } + microkit_dbg_puts("@byte "); number(b); + microkit_dbg_puts(" "); number(frame(f)[b]); microkit_dbg_puts("\n"); + } + done(); + } else if (line[0] == 'M' && !line[1]) { + table(); + done(); + } else { + microkit_dbg_puts("@error unknown request\n"); + } +} + +void notified(microkit_channel channel) { + require(channel == 5, "unknown interrupt"); + uart[0x44 / 4] = 0x7ff; + while (!(uart[0x18 / 4] & 0x10)) { + unsigned ch = uart[0] & 255; + if (ch == '\n') { + line[used] = 0; + request(); + used = 0; + } else if (ch >= 32 && ch < 127 && used < sizeof(line) - 1) { + line[used++] = ch; + } + } + microkit_irq_ack(5); +} diff --git a/setup.sh b/setup.sh new file mode 100644 index 0000000000000000000000000000000000000000..80e53c58026b03e1ece4fb24a4b54c700b6203c6 --- /dev/null +++ b/setup.sh @@ -0,0 +1,17 @@ +#!/bin/sh +set -eu +cache="${SPLIT_CACHE:-$HOME/.cache/split}" +mkdir -p "$cache" +if [ ! -f "$cache/sdk.tar.gz" ]; then + curl -fL --retry 2 https://github.com/seL4/microkit/releases/download/2.3.1/microkit-sdk-2.3.1-linux-x86-64.tar.gz -o "$cache/sdk.tar.gz" +fi +if [ ! -f "$cache/source.tar.gz" ]; then + curl -fL --retry 2 https://codeload.github.com/seL4/microkit/tar.gz/refs/tags/2.3.1 -o "$cache/source.tar.gz" +fi +printf '%s %s\n' b1b285b8785db7557eba6d0665dd4fbf2f265ea5c0b39d6f91ae3dcc43d2c424 "$cache/sdk.tar.gz" 67ae034628465c35169c398dd7d9ea61dbe8bd93c7a9adb05b9bb31bae25c22f "$cache/source.tar.gz" | sha256sum -c - +if [ ! -d "$cache/microkit-sdk-2.3.1" ]; then + tar -xzf "$cache/sdk.tar.gz" -C "$cache" +fi +tar -xzf "$cache/source.tar.gz" -C "$cache" +patch -s -p1 -d "$cache/microkit-2.3.1" < "$(dirname "$0")/microkit.patch" +cargo build --release --locked -p microkit-tool --manifest-path "$cache/microkit-2.3.1/Cargo.toml" diff --git a/split.h b/split.h new file mode 100644 index 0000000000000000000000000000000000000000..8d808a4a2a8257efc9404cfdd74926fc0caa7671 --- /dev/null +++ b/split.h @@ -0,0 +1,43 @@ +#ifndef SPLIT_H +#define SPLIT_H +#include +#include + +#define PAGES 4u +#define CLIENTS 2u +#define SLOTS (PAGES * CLIENTS) +#define FRAMES (PAGES + SLOTS) +#define BYTES 4096u +#define BASE 0x40000000ul +#define BACKING 0x60000000ul +#define TASK 0x50000000ul +#define LIMIT 255u + +struct job { + unsigned page, length; + char text[LIMIT + 1]; +}; + +static inline void number(unsigned long n) { + char s[24]; + unsigned i = sizeof(s) - 1; + s[i] = 0; + do { + s[--i] = '0' + n % 10; + n /= 10; + } while (n); + microkit_dbg_puts(s + i); +} + +static inline unsigned char seed(unsigned page, unsigned offset) { + return (page * 17u + offset) % 256u; +} + +static inline void require(int ok, const char *message) { + if (ok) return; + microkit_dbg_puts("@error "); + microkit_dbg_puts(message); + microkit_dbg_puts("\n"); + for (;;) seL4_Yield(); +} +#endif diff --git a/split.system b/split.system new file mode 100644 index 0000000000000000000000000000000000000000..161984323ed925865f0c786701e7acc23d850c5f --- /dev/null +++ b/split.system @@ -0,0 +1,76 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +