Major improvements from evaluation (#10)

* Fixes to readme

* Refine README.md

* Fixes formatting

* Sets current process to 'tp' and streamline system calls

* Improves revocation

* Remove tp as current process, improve IPC code

* Fixes trapped project for sifive_unleashed

* Fixes ping-pong for sifive_unleashed

* Fixes proc_acquire+ipc_wait race condition

* Fixes IPC and revocation

* Typo in default.ld

* Remove cap_is_revocable

* Adds NPREMPT option.

Define NPREMPT for the kernel to diable in-kernel preemption.

* Fixes reply when there is no receiver

* Adds another qemu platform.

qemu_virt: One core, deterministic.
qemu_virt4: Four core, non-deterministic.

* Adds more descriptive QEMU script

* Adds description of qemu for sifive_unleashed

* Add debug output to kernel with different verbosity levels.

* Improves scheduler debug output

* Fixes PMP revocation

* Improves printing of initial capabilities

* Formatting

* Adds kernel assert statements

* Improves revoke efficiency

* Improves delete

* Improves userland libraries

* Fixes a bug in syscall mon_reg_write mon_reg_read

* Improves altio

* Streamlines cap_ops

* Fixes cap_is_valid, which checks that the capability has a valid form

* Fixes NDEBUG and NPREEMPT macro

* Simplifies CSR

* Sets registers s1-s11 to call used registers

* Enables fence.i instruction

* Aligns kernel stack to 8-byte

* Sets INSTRUMENT macro in head.S

* Fixes alt_printf

* Improves cap_pmp_load/unload

* Improves cap_pmp_load/unload

* Improves scheduler

* Reorganize system call code and arguments

* Adds size target to makefiles

* Improves 'make format' and removes 'make docs'

* Adds 'make size' to demonstrator

* Adds demonstrator to project list

* Improves Makefile

* Various minor improvements

* Fixes syscall.c, IPC copy data bug.

* Fixes a bug

* Fixes cap_ipc.c reply.cap getting the wrong value.

Makefile

@@ -1,27 +1,24 @@
 .POSIX:
-export ROOT=${abspath .}
+.SECONDARY:
 
-
-PROJECTS:=projects/hello projects/trapped projects/ping-pong
-PLATFORM?=qemu_virt
-
-include tools.mk
-include common/plat/${PLATFORM}.mk
+PROJECTS:=projects/hello \
+	  projects/trapped \
+	  projects/ping-pong \
+	  projects/demonstrator
 
 all: ${PROJECTS}
 
+${PROJECTS}: common
+
 common ${PROJECTS}:
-	make -C $@ all PLATFORM=${PLATFORM}
+	@${MAKE} -C $@ all
 
 clean:
-	for i in ${PROJECTS}; do \
-		make -C $$i clean PLATFORM=${PLATFORM}; \
+	@for i in common ${PROJECTS}; do \
+		${MAKE} -C $$i clean; \
 	done
 
-docs:
-	doxygen
-
 format:
-	clang-format -i $(shell find -name '*.[hc]' -not -path '*/.*')
+	clang-format -i $$(find * -type f -name '*.[hc]')
 
-.PHONY: all docs clean common ${PROJECTS}
+.PHONY: all clean format common ${PROJECTS}

README.md

@@ -1,23 +1,31 @@
-s3k - Simple Secure Separation Kernel
+S3K - Simple Secure Separation Kernel
 =====================================
 
-s3k is a separation kernel targetting embedded RISC-V systems.
+S3K is a capability-based separation kernel targetting embedded RISC-V systems.
 
-- [Documentation Index](https://github.com/kth-step/s3k/wiki)
-- [S3K Design](https://github.com/kth-step/s3k/wiki/S3K-Design)
-- [S3K API](https://github.com/kth-step/s3k/wiki/S3K-API)
+Documentation
+-------------
+
+| Page | Description |
+| --- | --- |
+| [Home](https://github.com/kth-step/s3k/wiki)                  | Documentation Index |
+| [S3K Design](https://github.com/kth-step/s3k/wiki/S3K-Design) | High-level design of S3K |
+| [S3K Implementation](https://github.com/kth-step/s3k/wiki/S3K-Implementation) | Description of S3K implementation |
+| [S3K API](https://github.com/kth-step/s3k/wiki/S3K-API)       | User-level Kernel API |
+
+More documenation will be added.
 
 Configuration
 -------------
 
 Set your compiler toolchain in `tools.mk`. By default we have the following:
 ```
-CC=riscv64-unknown-elf-gcc
-AR=riscv64-unknown-elf-ar
-LD=riscv64-unknown-elf-ld
-SIZE=riscv64-unknown-elf-size
-OBJDUMP=riscv64-unknown-elf-objdump
-OBJCOPY=riscv64-unknown-elf-objcopy
+CC      =riscv64-unknown-elf-gcc
+AR      =riscv64-unknown-elf-ar
+LD      =riscv64-unknown-elf-ld
+SIZE    =riscv64-unknown-elf-size
+OBJDUMP =riscv64-unknown-elf-objdump
+OBJCOPY =riscv64-unknown-elf-objcopy
 ```
 
 Build and Run
@@ -73,7 +81,5 @@ Repository structure
   - hello - Hello, world example with two processes
   - ping-ping - IPC example
   - trapped - Trap handling example
-  - wcet - deprecated project (for now)
-- API.md - Kernel API
 - LICENSE - MIT License file
 - tools.mk - Set the compiler tools here

common/Makefile

@@ -1,57 +1,15 @@
 .POSIX:
+.SECONDARY:
 
-include plat/${PLATFORM}.mk
+PLATFORM?=${patsubst plat/%.mk, %, ${wildcard plat/*.mk}}
 
-include ${ROOT}/tools.mk
+all: ${addsuffix .all, ${PLATFORM}}
+clean: ${addsuffix .clean, ${PLATFORM}}
 
-# CFLAGS
-CFLAGS:=-march=${ARCH} -mabi=${ABI} -mcmodel=${CMODEL} \
-	-DPLATFORM_${PLATFORM} \
-	-Os -flto -ffat-lto-objects \
-	-nostdlib -Iinc \
+%.all: 
+	${MAKE} -f build.mk PLATFORM=${@:.all=} all
 
-BUILD :=build/${PLATFORM}
-SRCS2OBJS=${patsubst src/%.S, ${BUILD}/%.o, ${filter %.S, ${1}}} \
-	  ${patsubst src/%.c, ${BUILD}/%.o, ${filter %.c, ${1}}}
-
-ALTC_SRCS :=${wildcard src/altc/*.[cS]}
-S3K_SRCS  :=${wildcard src/s3k/*.[cS]}
-START_SRCS:=${wildcard src/start/*.S}
-
-PLAT_OBJS :=${call SRCS2OBJS, ${PLAT_SRCS}}
-ALTC_OBJS :=${call SRCS2OBJS, ${ALTC_SRCS}}
-S3K_OBJS  :=${call SRCS2OBJS, ${S3K_SRCS}}
-START_OBJS:=${call SRCS2OBJS, ${START_SRCS}}
-
-TARGETS:=${BUILD}/libplat.a \
-	 ${BUILD}/libaltc.a \
-	 ${BUILD}/libs3k.a \
-	 ${START_OBJS}
-
-
-all: ${TARGETS}
-
-clean:
-	rm -rf ${TARGETS}
-
-${BUILD}/libplat.a: ${PLAT_OBJS}
-	@mkdir -p ${@D}
-	${AR} cr $@ $^
-
-${BUILD}/libaltc.a: ${ALTC_OBJS}
-	@mkdir -p ${@D}
-	${AR} cr $@ $^
-
-${BUILD}/libs3k.a: ${S3K_OBJS}
-	@mkdir -p ${@D}
-	${AR} cr $@ $^
-
-${BUILD}/%.o: src/%.c
-	@mkdir -p ${@D}
-	${CC} -o $@ $< -c ${CFLAGS}
-
-${BUILD}/%.o: src/%.S
-	@mkdir -p ${@D}
-	${CC} -o $@ $< -c ${CFLAGS}
+%.clean:
+	${MAKE} -f build.mk PLATFORM=${@:.clean=} clean
 
 .PHONY: all clean

common/build.mk

@@ -0,0 +1,64 @@
+.POSIX:
+
+ROOT:=${abspath ..}
+
+include plat/${PLATFORM}.mk
+
+include ${ROOT}/tools.mk
+
+# CFLAGS
+CFLAGS:=-march=${ARCH} -mabi=${ABI} -mcmodel=${CMODEL} \
+	-DPLATFORM_${PLATFORM} \
+	-Os -flto -ffat-lto-objects \
+	-nostdlib -Iinc \
+
+BUILD :=build/${PLATFORM}
+SRCS2OBJS=${patsubst src/%.S, ${BUILD}/%.o, ${filter %.S, ${1}}} \
+	  ${patsubst src/%.c, ${BUILD}/%.o, ${filter %.c, ${1}}}
+
+ALTC_SRCS :=${wildcard src/altc/*.[cS]}
+S3K_SRCS  :=${wildcard src/s3k/*.[cS]}
+START_SRCS:=${wildcard src/start/*.S}
+
+PLAT_OBJS :=${call SRCS2OBJS, ${PLAT_SRCS}}
+ALTC_OBJS :=${call SRCS2OBJS, ${ALTC_SRCS}}
+S3K_OBJS  :=${call SRCS2OBJS, ${S3K_SRCS}}
+START_OBJS:=${call SRCS2OBJS, ${START_SRCS}}
+
+TARGETS:=${BUILD}/libplat.a \
+	 ${BUILD}/libaltc.a \
+	 ${BUILD}/libs3k.a \
+	 ${START_OBJS}
+
+
+all: ${TARGETS}
+
+clean:
+	rm -rf ${BUILD}
+
+${BUILD}/libplat.a: ${PLAT_OBJS}
+	@mkdir -p ${@D}
+	@${AR} cr $@ $^
+	@printf "AR\t$@\n"
+
+${BUILD}/libaltc.a: ${ALTC_OBJS}
+	@mkdir -p ${@D}
+	@${AR} cr $@ $^
+	@printf "AR\t$@\n"
+
+${BUILD}/libs3k.a: ${S3K_OBJS}
+	@mkdir -p ${@D}
+	@${AR} cr $@ $^
+	@printf "AR\t$@\n"
+
+${BUILD}/%.o: src/%.c
+	@mkdir -p ${@D}
+	@${CC} -o $@ $< -c ${CFLAGS}
+	@printf "CC\t$@\n"
+
+${BUILD}/%.o: src/%.S
+	@mkdir -p ${@D}
+	@${CC} -o $@ $< -c ${CFLAGS}
+	@printf "CC\t$@\n"
+
+.PHONY: all clean

common/inc/altc/altio.h

@@ -1,8 +1,13 @@
 #pragma once
+#include <stdarg.h>
+#include <stddef.h>
 
 int alt_getchar(void);
 int alt_putchar(char c);
 int alt_putstr(const char *str);
 int alt_puts(const char *str);
 int alt_gets(char *str);
 int alt_printf(const char *fmt, ...);
+int alt_snprintf(char *restrict s, size_t n, const char *restrict fmt, ...);
+int alt_vsnprintf(char *restrict s, size_t n, const char *restrict fmt,
+		  va_list ap);

common/inc/plat/config.h

@@ -2,8 +2,16 @@
 
 #if defined(PLATFORM_qemu_virt)
 #include "plat/qemu_virt.h"
+#elif defined(PLATFORM_qemu_virt4)
+#include "plat/qemu_virt4.h"
 #elif defined(PLATFORM_sifive_unleashed)
 #include "plat/sifive_unleashed.h"
+#elif defined(PLATFORM_sifive_unleashed4)
+#include "plat/sifive_unleashed4.h"
 #else
 #error "Unsupported platform or platform not found"
 #endif
+
+#if S3K_HART_CNT > 1
+#define SMP
+#endif

common/inc/plat/qemu_virt.h

@@ -11,7 +11,7 @@
 
 // Min and max usable hart ID.
 #define S3K_MIN_HART 0
-#define S3K_MAX_HART 3
+#define S3K_MAX_HART 0
 
 // Total number of usable harts.
 #define S3K_HART_CNT (S3K_MAX_HART - S3K_MIN_HART + 1ul)
@@ -28,13 +28,10 @@
 #define INIT_CAPS                                                     \
 	{                                                             \
 		[0] = cap_mk_pmp(0x20005fff, MEM_RWX),                \
-		[1] = cap_mk_memory(0x80020000, 0x80100000, MEM_RWX), \
+		[1] = cap_mk_memory(0x80020000, 0x88000000, MEM_RWX), \
 		[2] = cap_mk_memory(0x10000000, 0x10001000, MEM_RW),  \
 		[3] = cap_mk_memory(0x200b000, 0x200c000, MEM_R),     \
 		[4] = cap_mk_time(0, 0, S3K_SLOT_CNT),                \
-		[5] = cap_mk_time(1, 0, S3K_SLOT_CNT),                \
-		[6] = cap_mk_time(2, 0, S3K_SLOT_CNT),                \
-		[7] = cap_mk_time(3, 0, S3K_SLOT_CNT),                \
 		[8] = cap_mk_monitor(0, S3K_PROC_CNT),                \
 		[9] = cap_mk_channel(0, S3K_CHAN_CNT),                \
 	}