AOS

AOS is a small event-driven operating system built on the seL4 microkernel for AArch64. It runs as a userspace root server and manages processes, memory, files, timers, and hardware events.

Architecture

• A single seL4 receive loop dispatches system calls, interrupts, capability faults, and virtual-memory faults.
• Continuations represent pending I/O, paging, timer, and cleanup work, allowing callbacks to advance operations without blocking the root server.
• Reply capabilities are retained while a process waits and used to resume it when an asynchronous operation completes.

Subsystems

• File system: A virtual file system provides common file operations over console and NFS backends, including open, close, read, write, directory listing, stat, seek, and unlink.
• Asynchronous handling: NFS I/O, user-buffer mapping, page loading, timers, and resource cleanup are composed with continuations and completion callbacks. Synchronous system calls can still reply immediately.
• Process management: Processes have independent identities, capability spaces, address spaces, and file-descriptor tables, with support for creation, termination, status queries, parent-child waiting, and cleanup.
• Paging: Page faults load anonymous, executable, memory-mapped, or swapped pages on demand. When physical frames are exhausted, a second-chance eviction path selects pages for reclamation or write-back.
• Virtual memory: Per-process address spaces track regions and software page-table metadata. The system implements heap growth, mmap, munmap, frame ownership, swap-slot tracking, and page-by-page access to multi-page user buffers.
• Timers: A sorted timeout queue programs the next hardware deadline rather than using a periodic tick. Timer callbacks resume sleeping processes asynchronously.

System calls

dispatch.c maps syscall numbers to handlers split across syscall_fs.c, syscall_proc.c, syscall_timer.c, and vmsys.c. Handlers use proc_block() and proc_resume() as a common reply mechanism; the distinction below describes whether completion crosses an event-loop iteration.

• Immediate completion: debug/hello, timestamp, process ID, seek, heap growth, mmap, and munmap calculate their result and reply before returning to the receive loop.
• Deferred completion: open, close, read, write, directory listing, stat, unlink, process creation, process-status copying, and non-zero sleep may retain the reply capability while continuations wait for I/O, user-buffer mapping, ELF loading, or a timer callback.
• Conditionally blocking: process wait replies immediately for an exited child or an error, but otherwise retains the reply capability until a matching child exits. Console reads can likewise wait for input while other events continue to be serviced.
• Failure handling: setup and validation failures resume the caller immediately with a negative error code; unsupported syscall numbers return -ENOSYS through the same process-reply path.

Implementation map

• Event loop and continuations: main.c, dispatch.c, and continuation.c. A single root-server receive loop handles IPC, faults, and IRQs; longer operations return to the loop and continue from callbacks.
• File system: vfs.c, nfs_backend.c, and console_backend.c. Backend operation tables keep syscall handling independent of storage type, while NFS transfers map user buffers one page at a time to avoid eviction races.
• Processes: proc.c and syscall_proc.c. PID, IPC-badge, and VSpace mappings provide direct process lookup; stored reply capabilities support blocking and later resumption.
• Demand paging and eviction: vmfault.c, pager.c, eviction.c, and page_ops.c. Page backing is selected per region, and a second-chance policy reclaims frames when direct allocation fails.
• Virtual memory and swap: vmem.c, addrspace.c, pagetable/, and swap/. Software page-table metadata records mappings and ownership, while explicit swap-slot state prevents duplicate ownership during asynchronous write-back and page-in.
• Timers: clock.c and syscall_timer.c. Timeouts are ordered by absolute expiry, and the hardware timer is reprogrammed only for the earliest pending deadline.

The current configuration targets the AArch64 ODROID-C2 platform and uses the seL4 MCS kernel.