Servaled paging

C library handling page allocation and page mapping mechanisms. Intended to be proved correct by Serval.

How to prove with Serval

From the root directory of this repository, run the following commands:

docker run -it --name serval unsat/serval-tools:artifact

This will open a shell in the Serval container. Open another terminal and go to the root directory of this repository again, then run from there:

docker cp $(pwd) serval:/serval/racket/test

Then, from inside the Serval container :

cp /usr/riscv64-linux-gnu/include/gnu/stubs-lp64d.h /usr/riscv64-linux-gnu/include/gnu/stubs-lp64.h
cd /serval/racket/test/
cp servaled-paging/{src/all.c,include/all.h,specs/all.rkt} .
make -C ../../ raco-test

There should be 2 errors: they come from a missing library required by some of Serval's own tests. They can be ignored. Any other error should come from the allocation spec and implementation.

To make the verification faster, you can remove some of the verifications done on other Serval test files by replacing in /serval/racket/racket.mk :

RACO_TESTS      += $(wildcard racket/test/*.rkt)

by

override RACO_TESTS = racket/test/all.rkt

With only the tests of the allocation/paging library remaining, all tests should pass. Otherwise send me an email.

Directory structure

The headers are in include/ and the source files are in src/.