sel4 / sel4test Goto Github PK

View Code? Open in Web Editor NEW

24.0 30.0 59.0 1.27 MB

Test suite for seL4.

Home Page: http://sel4.systems

License: Other

Shell 0.27% Python 1.87% Perl 0.94% C 92.83% C++ 0.71% Assembly 1.50% CMake 1.89%

sel4test's Introduction

sel4test

Library for creating and running tests for seL4.

Setup

See the Getting Started page for instructions for installing required Host dependencies and how to checkout, build and run the tests in seL4test (this project).

Usage

Small unit tests can be defined anywhere, such as libraries outside of sel4test or in sel4test-driver. Larger tests that do things like creating processes need to be declared inside sel4test-tests.

Unit tests

To define a small unit test in a library outside of sel4test or in sel4test-driver:

Declare libsel4test as a dependency for your library and include <sel4test/test.h>. You may also find the functions in <sel4test/testutil.h> handy.
Write your tests. Then, for each test you want to run, call one of the macros that define a test, such as the DEFINE_TEST macro. They are declared here.
Add your library as dependency to libsel4testsupport. Add a call to any function in your test file to testreporter.c in dummy_func(). If you have multiple test files, then you need to call one function for each test file.

For an example, take a look at libsel4serialserver/src/test.c in sel4_libs.

Assumptions

Currently unit tests are assumed to be running sequentially, standalone (i.e. not multi-threaded). Some tests rely on being the highest priority running thread in the system.

Other tests

To define a larger test in sel4test-tests:

Place your test in apps/sel4test-tests/src/tests.
Include <../helpers.h>.
Write your tests. Then, for each test you want to run, call one of the macros that define a test, such as the DEFINE_TEST macro. They are declared here.

For an example, take a look at trivial.c in sel4test.

sel4test's People

Contributors

Stargazers

Watchers

sel4test's Issues

SCHED0000 fails for PC99_release with clang 11

The failure happens only when compiled with clang 11 (gcc 10 is fine), and only in release configs (works for debug), and only for PC99 (both 32 and 64 bit, Arm and RISCV are fine).

The test fails only under simulation/qemu. It passes fine for all configs on hardware.

<testcase classname="sel4test" name="SCHED0000">
  <failure type="failure">result == SUCCESS at line 291 of file /workspace/projects/sel4test/apps/sel4test-driver/src/testtypes
  <error>result == SUCCESS at line 217 of file /workspace/projects/sel4test/apps/sel4test-driver/src/main.c</error>
</testcase>

This is the last remaining known blocker for seL4/seL4-CAmkES-L4v-dockerfiles#39

Couldn't understand error in simulation

While running ninja command, it fails returning these
[1/62] Running C++ protocol buffer com...el4_projects_libs/libsel4rpc/rpc.proto FAILED: apps/sel4test-driver/sel4_projects_libs/libsel4rpc/rpc.pb.c apps/sel4test-driver/sel4_projects_libs/libsel4rpc/rpc.pb.h cd /home/ali/Desktop/sel4-x86/build-x86/apps/sel4test-driver/sel4_projects_libs/libsel4rpc && PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND -I/home/ali/Desktop/sel4-x86/build-x86/nanopb/generator -I/home/ali/Desktop/sel4-x86/build-x86/nanopb/generator/proto -I/home/ali/Desktop/sel4-x86/build-x86/apps/sel4test-driver/sel4_projects_libs/libsel4rpc -I/home/ali/Desktop/sel4-x86/projects/sel4_projects_libs/libsel4rpc --plugin=protoc-gen-nanopb=/home/ali/Desktop/sel4-x86/build-x86/nanopb/generator/protoc-gen-nanopb --nanopb_out=:/home/ali/Desktop/sel4-x86/build-x86/apps/sel4test-driver/sel4_projects_libs/libsel4rpc /home/ali/Desktop/sel4-x86/projects/sel4_projects_libs/libsel4rpc/rpc.proto /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found [3/62] Linking C executable kernel/kernel.elf ninja: build stopped: subcommand failed.
I do not really understand what is missing :/

Test x86 with x2apic

Run sel4test on at least one configuration with KernelLAPICMode=X2APIC, either on real hardware or in qemu.

How run sel4 test on TX2 board?

I have build the sel4test by following this guide: https://docs.sel4.systems/Hardware/JetsonTX2.html#building-sel4test, and get the sel4test-driver-image-arm-tx2 file successfully.
But how to run the image on TX2 board? I have tested to use uboot cmdline by tftp to load the image, but cant run.
Anyone can give some guide how run on TX2 board?
Thanks.

Below is the uboot log FYR:
Tegra186 (P2771-0000-500) # tftp 0x80a88000 sel4test-driver-image-arm-tx2;go 0x80a88000
ethernet@2490000 Waiting for PHY auto negotiation to complete...... done
Using ethernet@2490000 device
TFTP from server 192.168.42.16; our IP address is 192.168.42.17
Filename 'sel4test-driver-image-arm-tx2'.
Load address: 0x80a88000
Loading: #################################################################
#################################################################
#################################################################
#################################################################
#################################################################
#################################################################
###########
993.2 KiB/s
done
Bytes transferred = 5874752 (59a440 hex)

Starting application at 0x80A88000 ...
"Synchronous Abort" handler, esr 0x02000000
ELR: 80a88000
LR: fff3d3d4
x0 : 0000000000000001 x1 : 00000000ffb3a5a8
x2 : 00000000ffb3a5a8 x3 : 0000000080a88000
x4 : 0000000000000000 x5 : 0000000000000030
x6 : 00000000fff87775 x7 : 000000000000000f
x8 : 00000000ffb2fe70 x9 : 0000000000000008
x10: 00000000ffb2f6fa x11: 0000000000000008
x12: 00000000ffffffff x13: 0000000000000200
x14: 0000000000000004 x15: 0000000000000000
x16: 0000000000002090 x17: 0000000000000001
x18: 00000000ffb32de0 x19: 00000000ffb3a5a8
x20: 0000000000000002 x21: 0000000080a88000
x22: 00000000ffb3a5a0 x23: 00000000fffaa7f4
x24: 0000000000000002 x25: 0000000000000000
x26: 0000000000000000 x27: 0000000000000000
x28: 00000000ffb3a600 x29: 00000000ffb2ffc0

Resetting CPU ...

resetting ...

hifive: TIMER0001 test isn't working (it passes instantly instead of taking 3 seconds)

Can be observed by the logs (with timestamps enabled). The test completes instantly, but it's expected to take 3 seconds.

Sun, 23 Apr 2023 06:11:03 GMT   	<testcase classname="sel4test" name="TIMER0001">
Sun, 23 Apr 2023 06:11:03 GMT   	</testcase>
Sun, 23 Apr 2023 06:11:03 GMT   	<testcase classname="sel4test" name="TIMER0002">
Sun, 23 Apr 2023 06:11:03 GMT   	</testcase>
Sun, 23 Apr 2023 06:11:03 GMT

Add tests for vCPU objects

There are not really (to my knowledge) any tests for vCPUs. We should, at least, add basic tests for all of the libsel4 API for vCPU objects.

TIMEOUTFAULT0002 stuck on ODROID_XU4_release_MCS_clang_32

Logging this here, because I have not seen this fail before and it is likely (very) intermittent only -- TIMEOUTFAULT0002 got stuck on this run. The corresponding commit had no code changes, so definitely did not introduce an error.

Wed, 31 Jan 2024 04:01:07 GMT  	<testcase classname="sel4test" name="TIMEOUTFAULT0002">
Wed, 31 Jan 2024 04:14:21 GMT  
Wed, 31 Jan 2024 04:14:21 GMT  [[Timeout]]

The failing config was ODROID_XU4_release_MCS_clang_32 on the board odroidxu4_1.

Might be a hardware fluke, just logging it here in case it is related to something else.

TK1 and ODROID_XU4 fail `CACHEFLUSH0001`

In config ODROID_XU4_debug_hyp_MCS_clang_32 (and apparently only this config and only on clang), ODROID_XU4 is failing the test CACHEFLUSH0001. The configuration is disabled for tests for now.

It looks like this might be a problem with the test setup, not with MCS.

interspersed IOMMU messages in skylake output

skylake produces output such as

IOMMU: DMA write page fault from 0xa0 (bus: 0x0/dev: 0x14/fun: 0x0) on address 0x0:dc2f9000 with reason code 0x5

interleaved with normal test output, which sometimes confuses the test driver into thinking tests have not succeeded.

If the message is expected, it should be suppressed. If it is not expected, it should be investigated.

An example is here

Create thread with setting pc and call seL4_Send cause vm fault

when i creat thread in the end of main.c(sel4test-driver) like this:

//for simple test my code use InitThreadVSpace,not really ipc
seL4_TCB_Configure(new_tcb[0].cptr,0,seL4_CapInitThreadCNode,0,seL4_CapInitThreadVSpace,0, 
                                 (seL4_Word)new_ipc_frame_va,new_ipc_frame.cptr);    
seL4_UserContext regs = {};
sel4utils_arch_init_local_context(thread1,(void *)1,(void *)2,(void *)3,new_stack_top ,&regs);
seL4_Error err = seL4_TCB_WriteRegisters(new_tcp.cptr, true, 0, sizeof(regs)/sizeof(seL4_Word), &regs);

In thread1 function code like this:

printf("thread1 run\n");
seL4_Send(new_ep.cptr,seL4_MessageInfo_new(0,0,0,0));

I will get vm fault because __sel4_ipc_buffer is thread local variable.
I guess that i creat the thread1 with set pc = thread1 and not init the thread local variable.
But actually i alloc the ipc buffer and set successfully,i wanna know that the situation is seL4_Send function bug or feature?

DOMAINS0001 runs into a assert in sel4test-tests/src/main.c@:250

I've just seen these assertions during test runs on all architectures. Seems this happen reqularly. Is this just a QEMU issue, or could DOMAINS0001 be improved to avoid this message, or it these a real problem?

[...]
Running test DOMAINS0001 (Change domain successfully())
Test DOMAINS0001 passed
Assertion failed: !"unreachable" (/github/workspace/projects/sel4test/apps/sel4test-tests/src/main.c: main: 250)
	</testcase>
	<testcase classname="sel4test" name="DOMAINS0002">
Running test DOMAINS0002 (Try non-existant domain())
<<seL4(CPU 0) [decodeDomainInvocation/1584 T0xfc411400 "32" @80654eb]: Domain Configure: invalid domain (14 >= 4).>>
Test DOMAINS0002 passed
[...]
All is well in the universe

int main(int argc, char **argv)
{
   [...]
   printf("Test %s %s\n", init_data->name, result == SUCCESS ? "passed" : "failed");
    /* send our result back */
    seL4_MessageInfo_t info = seL4_MessageInfo_new(seL4_Fault_NullFault, 0, 0, 1);
    seL4_SetMR(0, result);
    seL4_Send(endpoint, info);

    /* It is expected that we are torn down by the test driver before we are
     * scheduled to run again after signalling them with the above send.
     */
    assert(!"unreachable");
    return 0;
}

SCHED0021 fails on star64 platform when config `LibUtilsDefaultZfLogLevel` is `0`

I suspect the extra debug prints might be causing the timing measurements to be off.

I'm testing this on the pinetab-v hardware as described in seL4/seL4#1019 (comment).

When building sel4test like this, all is well in the universe:

../init-build.sh -DPLATFORM=star64 -DKernelRiscvExtD=true -DUseRiscVOpenSBI=false -DSIMULATION=false -DMCS=true -DSMP=false

Output: sel4test-star64-mcs.txt

However, when built with verbose logging, SCHED0021 fails:

../init-build.sh -DPLATFORM=star64 -DKernelRiscvExtD=true -DUseRiscVOpenSBI=false -DSIMULATION=false -DMCS=true -DSMP=false -DLibUtilsDefaultZfLogLevel=0

Output: sel4test-star64-mcs-verbose.txt

develop program for sel4

Hi, I am trying to develop some programs on top of sel4. Let's say I've written some C programs under Linux with dependencies and compiled it into binary files. Those binary files would be pretty self-contained, i.e., not dependent on os, Is it possible to port those binary files to sel4?

seL4test/projects/musllibc/configure: not found

I have successfully executed repo sync，and ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE executed successfully. But when I do ninja, I get the following error:

[15/263] Invoking muslc build system
FAILED: apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a
cd /home/wang/Documents/sel4/seL4test/build-x86/apps/sel4test-driver/musllibc && rm -r build-temp && mkdir -p build-temp && /usr/bin/cmake -E env TOOLPREFIX= C_COMPILER=/usr/bin/gcc MAKEFLAGS="${MAKEFLAGS:--s}" NK_CFLAGS="-nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mtls-direct-seg-refs -m64 -D__KERNEL_64__ -march=nehalem " TARGET=x86_64 make -C build-temp -j18 -f /home/wang/Documents/sel4/seL4test/projects/musllibc/Makefile STAGE_DIR=/home/wang/Documents/sel4/seL4test/build-x86/apps/sel4test-driver/musllibc/build-temp/stage SOURCE_DIR=/home/wang/Documents/sel4/seL4test/projects/musllibc && mkdir -p /home/wang/Documents/sel4/seL4test/.sel4_cache/musllibc/1d8a33c8cb8209203aed9a0a99fb54c9 && tar -zcf code.tar.gz -C /home/wang/Documents/sel4/seL4test/build-x86/apps/sel4test-driver/musllibc/build-temp/stage . && mv code.tar.gz /home/wang/Documents/sel4/seL4test/.sel4_cache/musllibc/1d8a33c8cb8209203aed9a0a99fb54c9/
/bin/sh: 2: /home/wang/Documents/sel4/seL4test/projects/musllibc/configure: not found
sed: can't read config.mak: No such file or directory
Please set ARCH in config.mak before running make.
make[1]: *** [Makefile.muslc:83: all] Error 1
make: *** [/home/wang/Documents/sel4/seL4test/projects/musllibc/Makefile:73: build_muslc] Error 2
[23/263] Generate syscall invocations
ninja: build stopped: subcommand failed.

I try to only execute the sh command independently, and I get the error:

cmake -E env TOOLPREFIX= C_COMPILER=/usr/bin/gcc MAKEFLAGS="${MAKEFLAGS:--s}" NK_CFLAGS="-nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mtls-direct-seg-refs -m64 -D__KERNEL_64__ -march=nehalem " TARGET=x86_64 make -C build-temp -j18 -f /home/wang/Documents/sel4/seL4test/projects/musllibc/Makefile STAGE_DIR=/home/wang/Documents/sel4/seL4test/build-x86/apps/sel4test-driver/musllibc/build-temp/stage SOURCE_DIR=/home/wang/Documents/sel4/seL4test/projects/musllibc
/bin/sh: 2: /home/wang/Documents/sel4/seL4test/projects/musllibc/configure: not found
sed: can't read config.mak: No such file or directory
Please set ARCH in config.mak before running make.
make[1]: *** [Makefile.muslc:83: all] Error 1
make: *** [/home/wang/Documents/sel4/seL4test/projects/musllibc/Makefile:73: build_muslc] Error 2

MIN_BUDGET definition in sel4test breaks test for TK1

We introduced a MIN_BUDGET test in b572953 which succeeded for everything tested at the time, but since then the TK1 board has come online.

The TK1 board is defined with a kernel WCET of 100 instead of 10 as most other boards, which affects MIN_BUDGET, which in turn means the MIN_BUDGET here in sel4test is out of sync with the one in seL4.

See eg here for a test failure log.

We either need to define this conditionally in sel4test, which is ugly, but which I will submit as a quick fix for now, or we need to properly export MIN_BUDGET so that sel4test can make use of the value directly.

sel4test builds are not reproducible

Not having reproducible builds may not be an error, but it is a very good property to have.

I ran the following script in a cleanly synced sel4test repo:
~/Repo/seL4/sel4test$ cat reproducible-builds.sh
#!/bin/sh

for i in {1..10} ; do
make mrproper > /dev/null 2>&1
make bbone_black_release_xml_defconfig > /dev/null 2>&1
make > /dev/null 2>&1
sha1sum images/sel4test-driver-image-arm-am335x.bin
done
~/Repo/seL4/sel4test$ . reproducible-builds.sh
7c83aa31c988bef3d34f0c03f0e71f0dd23c0087 images/sel4test-driver-image-arm-am335x.bin
34fecfcad3b984ba117633807bab98c5e8d1acaf images/sel4test-driver-image-arm-am335x.bin
6c4ff733a495614adc37ab88a7b44156db576c06 images/sel4test-driver-image-arm-am335x.bin
c5ccd2967d41ab629d27343d243f0f4a05b38a68 images/sel4test-driver-image-arm-am335x.bin
84e750754afb9ffa54897d0f030bee262f67adab images/sel4test-driver-image-arm-am335x.bin
9ffe2e35159475ea50d7a4db5dfdc71fc5479d68 images/sel4test-driver-image-arm-am335x.bin
a276e16cfa78b5a783d3831fa4e4d69a40d13568 images/sel4test-driver-image-arm-am335x.bin
0a753a04c7882cded39f85adad5924e6a76ea509 images/sel4test-driver-image-arm-am335x.bin
afda6bf5d398cc950a1ce1eb9b7431388ed0923d images/sel4test-driver-image-arm-am335x.bin
c07bed74c7f6d04f72bcc01eb545da13707e1fc9 images/sel4test-driver-image-arm-am335x.bin

Diff:ing the binaries show that only a few bytes differ in a few places. If the root cause is in the sel4test git then this issue can be ignored, but currently I don't know if this comes from the sel4test git, the seL4_tools git or some other git involved in the build.

Building sel4 with sel4test fails, show "kernel/src/arch/x86/idle.c:25:1: error: 'noreturn' function does return [-Werror]"

I'm trying to build sel4, but fails. The errors are :

[96/263] Building C object apps/sel4test-driver/seL4_libs/libsel4debug/CMakeFiles/sel4debug.dir/src/caps.c.obj
/workspace/s42/projects/seL4_libs/libsel4debug/src/caps.c: In function 'debug_cap_identify':
/workspace/s42/projects/seL4_libs/libsel4debug/src/caps.c:17:18: warning: format '%d' expects argument of type 'int', but argument 2 has type 'seL4_CPtr {aka long unsigned int}' [-Wformat=]
     printf("Cap %d has type %d\n", cap, type);
                 ~^
                 %ld
[260/263] Building C object kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj
FAILED: kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj
/usr/bin/ccache /usr/bin/gcc --sysroot=/workspace/s42/build-x86  -I/workspace/s42/kernel/include -I/workspace/s42/kernel/include/64 -I/workspace/s42/kernel/include/arch/x86 -I/workspace/s42/kernel/include/arch/x86/arch/64 -I/workspace/s42/kernel/include/plat/pc99 -I/workspace/s42/kernel/include/plat/pc99/plat/64 -I/workspace/s42/kernel/libsel4/include -I/workspace/s42/kernel/libsel4/arch_include/x86 -I/workspace/s42/kernel/libsel4/sel4_arch_include/x86_64 -I/workspace/s42/kernel/libsel4/sel4_plat_include/pc99 -I/workspace/s42/kernel/libsel4/mode_include/64 -I/workspace/s42/build-x86/kernel/gen_config -I/workspace/s42/build-x86/kernel/autoconf -I/workspace/s42/build-x86/kernel/gen_headers -I/workspace/s42/build-x86/kernel/generated -m64  -march=nehalem -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=kernel -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -fno-common -mno-mmx -mno-sse -mno-sse2 -mno-3dnow -MD -MT kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj -MF kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj.d -o kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj -c /workspace/s42/build-x86/kernel/kernel_all.c
/workspace/s42/kernel/src/arch/x86/idle.c:17:1: error: 'naked' attribute directive ignored [-Werror=attributes]
 {
 ^
/workspace/s42/kernel/src/arch/x86/idle.c: In function 'idle_thread':
/workspace/s42/kernel/src/arch/x86/idle.c:25:1: error: 'noreturn' function does return [-Werror]
 }
 ^
cc1: all warnings being treated as errors
ninja: build stopped: subcommand failed.

Then I check the code of idle.c:

__attribute__((naked)) NORETURN void idle_thread(void)
{
    /* We cannot use for-loop or while-loop here because they may
     * involve stack manipulations (the compiler will not allow
     * them in a naked function anyway). */
    asm volatile(
        "1: hlt\n"
        "jmp 1b"
    );
}

Actually the function idle_thread does not return.

I'm running on Ubuntu 18.04 with gcc 7.5,python 3.7.

Sel4test freezes on imx8mq

Dear all,

I am new to sel4 and currently trying to run sel4test on an imx8mq Nitrogen8m device.
As there is already support for imx8mq-evk I first tried building and booting an sel4image for this platform. Fortunately it seems already to be able to boot into user space.
However, right after the beginning of sel4Test it freezes. The last line look as follows:

seL4 Test
=========

[email protected]:58 Failed to allocate object of size 2147483648, error 1
[email protected]:58 Failed to allocate object of size 1073741824, error 1

Comparing this to the output of a sel4test simulation for an ia32 build, the error messages seem to be expected behaviour.

As I am quite new I am unsure how to get further information about the problem's cause. As suggested in https://docs.sel4.systems/projects/sel4-tutorials/debugging-guide.html I have already built the image with -DRELEASE=FALSE. Is there another way to gather more information why it stops executing?

Thank you and best regards!

image stops at "Jumping to kernel-image entry point..."

Hello everyone;

I am working on master branch and trying to port sel4 to allwinnerR40 board. When I tried to run the image on board, it stoped at "Jumping to kernel-image entry point..." when I run it on the board. Following is the printed messages:

sunxi#fatload mmc 0 0x40000000 sel4test_ding && bootelf 0x40000000
reading sel4test_ding
1568324 bytes read in 69 ms (21.7 MiB/s)

Starting application at 0x40644000 ...

ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p5
paddr=[40644000..407bc0a7]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 40681880.
Loaded DTB from 40681880.
paddr=[4002b000..40032fff]
ELF-loading image 'kernel'
paddr=[40000000..4002afff]
vaddr=[a0000000..a002afff]
virt_entry=a0000000
ELF-loading image 'sel4test-driver'
paddr=[40033000..40249fff]
vaddr=[10000..226fff]
virt_entry=164e8
Enabling MMU and paging
Jumping to kernel-image entry point...

Any suggestion is appreciated, thanks.

Nitrogen6_SoloX board serial output doesn't work when sel4test `-DRELEASE=ON` is used

When running sel4test on the Nitrogen6_SoloX board with release settings configured, seL4_DebugPutchar() is disabled and the platform serial driver from libplatsupport will be used instead. The error occurs when re-configuring the divider settings for the serial baud (if the baud reconfiguration is disabled such that the device is assumed to be initialized already then the serial works).

U-Boot 2018.07-36618-g616d48151d (Oct 08 2020 - 10:15:22 -0700), Build: jenkins-uboot_v2018.07-240

CPU:   Freescale i.MX6SX rev1.3 at 792 MHz
Reset cause: POR
Board: nitrogen6sx
I2C:   ready
DRAM:  1 GiB
MMC:   FSL_SDHC: 0, FSL_SDHC: 1
Loading Environment from SPI Flash...
SF: Detected gd25q16c with page size 256 Bytes, erase size 4 KiB, total 2 MiB
*** Warning - bad CRC, using default environment

Failed (-5)
Display: lcd:1280x720M@60 (1280x720)
In:    serial
Out:   serial
Err:   serial
Net:   AR8035 at 4
AR8035 at 5
FEC0 [PRIME], FEC1, usb_ether
Hit any key to stop autoboot:  0 
=> dhcp
BOOTP broadcast 1
DHCP client bound to address 10.0.121.29 (4 ms)
*** Warning: no boot file name; using '0A00791D.img'
Using FEC0 device
TFTP from server 0.0.0.0; our IP address is 10.0.121.29; sending through gateway 10.0.121.100
Filename '0A00791D.img'.
Load address: 0x82000000
Loading: *
TFTP error: 'File not found' (1)
Not retrying...
=> setenv serverip 10.0.121.19
=> tftp sel4test-driver-image-arm-imx6
Using FEC0 device
TFTP from server 10.0.121.19; our IP address is 10.0.121.29
Filename 'sel4test-driver-image-arm-imx6'.
Load address: 0x82000000
Loading: #################################################################
	 ########################################################
	 7 MiB/s
done
Bytes transferred = 1763056 (1ae6f0 hex)
=> bootm
## Booting kernel from Legacy Image at 82000000 ...
   Image Name:   
   Image Type:   ARM Linux Kernel Image (uncompressed)
   Data Size:    1762992 Bytes = 1.7 MiB
   Load Address: 80657000
   Entry Point:  80657000
   Verifying Checksum ... OK
   Loading Kernel Image ... OK

Starting kernel ...


ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10
  paddr=[80657000..808056af]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 8069d410.
Loaded DTB from 8069d410.
   paddr=[80030000..80033fff]
ELF-loading image 'kernel' to 80000000
  paddr=[80000000..8002ffff]
  vaddr=[e0000000..e002ffff]
  virt_entry=e0000000
ELF-loading image 'sel4test-driver' to 80034000
  paddr=[80034000..8025afff]
  vaddr=[10000..236fff]
  virt_entry=17ad4
Enabling MMU and paging
Jumping to kernel-image entry point...

��<�<�<<<�����<�<�<�<�<<�<�<<<<��<<<�<<<�<�<��������<�<<�<<�<��<<<�<�<<<�<���������<�����������<�<<<��<<�<�<���<�<�<�<�<���������<���<����<<<<����<�<����<<<�<��<�<<�<<<�<<�<<��<<<�<��������<��<<<<����<<<�<<�<�<<<�<��<��<<�<<<<�<<��<<<�<�����<�������<<<<���<�������<<<�<<�<�<<<�<��<��<<�<<<<<<�<��<�<�<�����<<�<���<<<<���<��<<<�<<�<�<�<�<<<<�<�<������������<<��������<<<<������<���<<<�<<�<�<��<�<��<<�<��<�<�<<<<�<��<�<��<<��<�<����<�<<�<�<��<�<��<<�<��<�<�<<<<�<��<�<�<�<<<���<��<�<<<���<����<�<�<��<�<�<���<�<�<�<�<�<�<<<<�<�<��<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<�<<<<�<�<�<����<���<<�<�<<<���<�<<<�<��<<<<��<��<��������<�<�<�<�<�������<����<��<�<�<�<�<<��������<�<�����<�<�<�<�<<�������<�<����<�<�<�<�<<������<�<�<���<�<�<�<�<<������<�<�����<�<�<�<�<<�������<�<�����<�<�<�<�<<�������<�<���<�<�<�<�<<������<�<�<��<�<�<�<�<<������<������<�<�<�<�<<������<��������<�<�<�<�<��������<�������<�<�<�<�<���������<����<���<�<�<�<�<���������<��������<�<�<�<�<��������<��������<�<�<�<�<���������<������<�<�<�<�<����������<����<��<�<�<�<�<����������<����<��<�<�<�<�<����������<����<��<�<�<�<�<����<�<������<������<�<�<�<�<<��������<����<��<�<�<�<�<<��������<����<��<�<�<�<�<<<��������<������<�<�<�<�<�<��������<��������<�<�<�<�<�<��������<��������<�<�<�<�<�<<�������<����<���<�<�<�<�<�<<<�������<�������<�<�<�<�<�<�<�������<��������<�<�<�<�<�<�<�������<��������<�<�<�<�<�<�<<������<����<��<�<�<�<�<�<�<<<������<������<�<�<�<�<�<�<�<������<�<�<��<�<�<�<�<�<�<�<������<�<���<�<�<�<�<�<�<�<<�����<�<�����<�<�<�<�<�<�<�<<<�����<�<�����<�<�<�<�<�<�<�<�<�����<�<�<���<�<�<�<�<�<�<�<�<�����<�<����<�<�<�<�<�<�<�<�<<����<�<�����<�<�<�<�<�<�<�<�<<<����<�<�����<�<�<�<�<�<�<�<�<�<����<�<�<��<�<�<�<�<�<�<�<�<�<����<�<���<�<�<�<�<�<�<�<�<�<<���<�<��<�<�<�<�<�<�<�<�<

riscv: FRAMEEXPORTS0001

FRAMEEXPORTS0001 test tries to test all architecture-supported frame sizes. For RISCV64/Sv39 these are 1 GiB, 2 MiB and 4 KiB.

Testing 1 GiB will fail on platforms that have less than or equal 1 GiB and/or fail to get a 1 GiB-aligned untyped physical memory.

This can be seen noticed on simulators with 2 GiB of default memory.

Ensure that the RESTART and BADGED bits are not set

sel4test/apps/sel4test-tests/src/tests/faults.c

Line 760 in 7eea79d

test_leq(reply_cptr, BIT(BADGED));

Inform the user that their settings might be getting overridden

It would be nice to notify the developer that some of their setting might get overridden. I have personally been burned by this many times, where I would like to create a binary and set it in the easy-settings but just to find that it was silently overridden as an elf. Often times, a bootloader won't tell me what is wrong and I usually spend more time than I'd like to admit trying to find what the issue is. I understand where setting some sane defaults by be helpful across projects. Is there a way in CMake to check if a variable has been set by the user or if it was set by the default value of config_string?

I'm not sure where the best place is but some possibilities might be the conditionals that check it [1][2] or the Data61 override function [3]. It might be better to check at each variable that is being set in the override functions too. I'm not sure what the best course of action would be.

sel4test/settings.cmake

Line 50 in 7b1f1fc

if(NOT Sel4testAllowSettingsOverride)

sel4test/CMakeLists.txt

Line 31 in 90a835e

if((NOT Sel4testAllowSettingsOverride) AND (KernelArchARM OR KernelArchRiscV))

3: https://github.com/seL4/seL4_tools/blob/ffe3305d8d3926ccfa0fa8019063c786b75850d6/cmake-tool/helpers/application_settings.cmake#L10

sched0022_to_fn() does not return a value

The function sched0022_to_fn() does not return a value and the compiler complains

  [249/267] Building C object .../src/tests/scheduler.c.obj
  .../src/tests/scheduler.c:1653:1: warning: control reaches end of non-void function [-Wreturn-type]
  }
  ^
  1 warning generated.

I wonder, is there just a return sel4test_get_result(); missing?

when I build sel4 with sel4test, error occors that "UnicodeDecodeError: 'ascii' codec can't decode byte"

I build sel4 with the guide from https://docs.sel4.systems/GettingStarted.html. but failed, error occors that:

[1/24] Generating from generated/plat_mode/machine/hardware.bf.pbf
FAILED: kernel/generated/plat_mode/machine/hardware_gen.h /workspace/s42/build-x86/kernel/generated/plat_mode/machine/hardware_gen.h
cd /workspace/s42/build-x86/kernel && python3 /workspace/s42/kernel/tools/bitfield_gen.py --prune /workspace/s42/build-x86/kernel/kernel_all_pp_prune.c /workspace/s42/build-x86/kernel/generated/plat_mode/machine/hardware.bf.pbf /workspace/s42/build-x86/kernel/generated/plat_mode/machine/hardware_gen.h
Traceback (most recent call last):
  File "/workspace/s42/kernel/tools/bitfield_gen.py", line 2772, in <module>
    string = f.read()
  File "/usr/lib/python3.6/encodings/ascii.py", line 26, in decode
    return codecs.ascii_decode(input, self.errors)[0]
UnicodeDecodeError: 'ascii' codec can't decode byte 0xc2 in position 593714: ordinal not in range(128)
ninja: build stopped: subcommand failed.

My environment is ubuntu 18.04.

Test SCHED0021 has a race condition

    /* Configure all of the threads */
    for (size_t thread = 0; thread < PREEMPTION_THREADS; thread += 1) {
[...]
        /* Thread must run at same prio as monitor */
        set_helper_priority(env, &threads[thread], OUR_PRIO);
[...]
    }
[...]
    /* Start executing other threads */
    ZF_LOGD("Releasing Threads");
    test_simple_preempt_start = 1;
    /* Yield should cause all other threads to execute before returning
     * to the current thread. */
    seL4_Yield();

Isn't there a tiny chance that the preemptive scheduler will kick in after test_simple_preempt_start = 1? So all threads get their time slice to run. Then seL4_Yield() is executed and each thread again gets a time slice to run?
Wouldn't is be better to do this:

    /* Start executing other threads */
    ZF_LOGD("Releasing Threads");
    /* Release our time slice now to get a new one. That should ensure we are
     * not interrupted due to bad luck by the preemptive scheduler right after 
     * setting test_simple_preempt_start to 1 and then voluntarily yielding. For
     * the same reason we are also printing the doing the ZF_LOGD() above 
     * already.
     */
    seL4_Yield();
    /* Set a timeout for the test. Each thread should run for one tick. */
    uint64_t start = time_now(env);
    test_simple_preempt_start = 1;
    /* Yield should cause all other threads to execute before returning
     * to the current thread. 
     */
    seL4_Yield();
    test_simple_preempt_start = 0;

There is still a risk because we can't be really sure what time_now(env) does and how long this may take.

Aside from this, the line

    uint64_t now = start;

is the original code seems quite useless to me, as nobody is using the value assigned to now, it is overwritten a few lines later. This might be a left over from a time where another debug message was printed with it?

Running test under SMP conditions on spike platform gets stuck.

The build command is as follows:

../init-build.sh -DPLATFORM=spike -DSIMULATION=TRUE -DSMP=1 -DKernelMaxNumNodes=2 && ninja
./simulate

The qemu emulator is stuck in the following place:

./simulate: QEMU command: qemu-system-riscv64 -machine spike -cpu rv64 -nographic -serial mon:stdio -m size=4095M -bios none -kernel images/sel4test-driver-image-riscv-spike
OpenSBI v0.9
   ____                    _____ ____ _____
  / __ \                  / ____|  _ \_   _|
 | |  | |_ __   ___ _ __ | (___ | |_) || |
 | |  | | '_ \ / _ \ '_ \ \___ \|  _ < | |
 | |__| | |_) |  __/ | | |____) | |_) || |_
  \____/| .__/ \___|_| |_|_____/|____/_____|
        | |
        |_|

Platform Name             : ucbbar,spike-bare,qemu
Platform Features         : timer,mfdeleg
Platform HART Count       : 1
Firmware Base             : 0x80000000
Firmware Size             : 100 KB
Runtime SBI Version       : 0.2

Domain0 Name              : root
Domain0 Boot HART         : 0
Domain0 HARTs             : 0*
Domain0 Region00          : 0x0000000080000000-0x000000008001ffff ()
Domain0 Region01          : 0x0000000000000000-0xffffffffffffffff (R,W,X)
Domain0 Next Address      : 0x0000000080200000
Domain0 Next Arg1         : 0x0000000082200000
Domain0 Next Mode         : S-mode
Domain0 SysReset          : yes

Boot HART ID              : 0
Boot HART Domain          : root
Boot HART ISA             : rv64imafdcsu
Boot HART Features        : scounteren,mcounteren
Boot HART PMP Count       : 16
Boot HART PMP Granularity : 4
Boot HART PMP Address Bits: 54
Boot HART MHPM Count      : 0
Boot HART MHPM Count      : 0
Boot HART MIDELEG         : 0x0000000000000222
Boot HART MEDELEG         : 0x000000000000b109
ELF-loader started on (HART 0) (NODES 4)
  paddr=[80200000..806b8047]
Looking for DTB in CPIO archive...found at 80300290.
Loaded DTB from 80300290.
   paddr=[8402d000..8402dfff]
ELF-loading image 'kernel' to 84000000
  paddr=[84000000..8402cfff]
  vaddr=[ffffffff84000000..ffffffff8402cfff]
  virt_entry=ffffffff84000000
ELF-loading image 'sel4test-driver' to 8402e000
  paddr=[8402e000..84423fff]
  vaddr=[10000..405fff]
  virt_entry=1b9e0
Main entry hart_id:0
Hart ID 0 core ID 0

Is there something wrong with my build and run commands?

ZCU102: Enable HAVE_TIMER tests and fix failing ones

(Moved from https://sel4.atlassian.net/browse/SELFOUR-2272)
The timer tests are failing and are disabled for the zynqmp platform in settings.cmake currently. This appears to be due to using the same timers as the zc706 platform, but without updating the input clk frequencies for the different platform (see also seL4/util_libs#119)

Analyze test case BREAKPOINT_002 for race conditions

seL4/seL4#462 had a failure in BREAKPOINT_002 that seems completely unrelated to the changes in the PR, especially sicne the changes affect ARM and RISC-V only, but the test failed for PC99_release_gcc_32.

<testcase classname="sel4test" name="BREAKPOINT_002">
    <failure type="failure">
        result == SUCCESS 
        at line 291 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/testtypes.c
    </failure>
    <error>
        result == SUCCESS 
        at line 217 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/main.c
    </error>
</testcase>

Analysze BREAKPOINT_002 for potential race conditions.

TX1 failed on seL4test

Help me!
I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port.
At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format.
Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line.
Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000:
ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
go 0x82000000
Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output：

Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
5247256 bytes read in 260 ms (19.2 MiB/s)
Tegra210 (P2371-2180) # go 0x82000000
## Starting application at 0x82000000 ...

ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1
paddr=[80a57000..80f58117]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 80b825e0.
Loaded DTB from 80b825e0.
paddr=[8023d000..8024afff]
ELF-loading image 'kernel' to 80000000
paddr=[80000000..8023cfff]
vaddr=[ffffff8080000000..ffffff808023cfff]
virt_entry=ffffff8080000000
ELF-loading image 'sel4test-driver' to 8024b000
paddr=[8024b000..80661fff]
vaddr=[400000..816fff]
virt_entry=40f0b8
Enabling MMU and paging
Jumping to kernel-image entry point...

Warning: gpt_cntfrq 19200000, expected 12000000
Bootstrapping kernel
available phys memory regions: 2
[80000000..ff000000]
[100000000..180000000]
reserved virt address space regions: 3
[ffffff8080000000..ffffff808023d000]
[ffffff808023d000..ffffff808024b000]
[ffffff808024b000..ffffff8080662000]
seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert
halting...
Kernel entry via Interrupt, irq 0

I'm about to collapse. I really need your help. How can I solve this problem?

1. Why did I get this warning？ "Warning:  gpt_cntfrq 19200000, expected 12000000" ,  It exists in this file  "/sel4test/kernel/src/drivers/timer/generic_timer.c:21"

2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) )  -> cap.words[0] " is equals to  0xffffffffffffffff, so that the         cap_get_capType(destSlot->cap) <=>   (slot_ptr_t) (rootserver.tcb) )  -> cap.words[0]  & 0x1full  != 0 .     I guess it caused the mistake, but i don't know why.

I'm about to collapse. I really need your help. How can I solve this problem?

pc99: SCHED0011 sometimes times out

In this run: https://github.com/seL4/util_libs/actions/runs/4920068732/jobs/8789972531?pr=156#step:4:3957 we're getting:

Tue, 09 May 2023 02:21:49 GMT  Test SCHED0010 passed
Tue, 09 May 2023 02:21:49 GMT  </testcase>
Tue, 09 May 2023 02:21:49 GMT  <testcase classname="sel4test" name="SCHED0011">
Tue, 09 May 2023 02:21:49 GMT  Running test SCHED0011 (Test scheduler accuracy)
Tue, 09 May 2023 02:36:11 GMT
Tue, 09 May 2023 02:36:11 GMT  [[Timeout]]
Tue, 09 May 2023 02:36:11 GMT  None
Tue, 09 May 2023 02:36:12 GMT  
Tue, 09 May 2023 02:36:12 GMT  console_run returned -1
Tue, 09 May 2023 02:36:12 GMT  Shutting down haswell4

Note the 15min passing between start of SCHED011 and the timeout.

The failing config was PC99_debug_MCS_clang_32

rockpro64: sel4test freezes at BIND0001 when SMP is enabled

When I run sel4test with SMP enabled on my pinebook pro, sel4test freezes while running BIND0001.

I found this issue while investigating seL4/seL4#184. See that issue for further analysis. This does not appear to be a kernel issue.

Steps to reproduce:

mkdir sel4test
cd sel4test
repo init -u https://github.com/seL4/sel4test-manifest.git -b master
repo sync
cd kernel
git checkout master
cd ..
mkdir build
cd build
../init-build.sh -DPLATFORM=rockpro64 -DSIMULATION=false -DSMP=on -DNUM_NODES=4 -DLibUtilsDefaultZfLogLevel=0
ninja
cd images
../../tools/seL4/cmake-tool/helpers/make-uimage /usr/bin/aarch64-linux-gnu-objcopy ../elfloader/elfloader arm64 sel4test-driver-image-arm-rockpro64-uboot

When run on the pinebook pro (rockpro64 platform), this resulted in a freeze while running this test:

Starting test 18: BIND0001
[email protected]:383 Starting process at 0x4001c8, stack 0x10011df0

Here's the full serial output for the test that failed: serial3.txt

Investigate running MCS on Qemu simulation targets

(Imported form https://sel4.atlassian.net/browse/SELFOUR-2377)

simulation sel4test builds don't run any MCS configurations. Historically this was because of many of the tests are time sensitive and don't handle Qemu's emulation of time very well.

When done, switch on in CI (see seL4/ci-actions#188).

Test MULTICORE0005 fails on SABRE sporadically

After the merge of seL4/seL4#712 the CI run https://github.com/seL4/seL4/actions/runs/1606856772 failed. The change in the merge seems quite unrelated.

Running test MULTICORE0005 (Test remote delete thread running on other cores)
  		<error>counter != old_counter at line 153 of file /github/workspace/projects/sel4test/apps/sel4test-tests/src/tests/multicore.c</error>
  Test MULTICORE0005 failed
  		<failure type="failure">result == SUCCESS at line 291 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/testtypes.c</failure>
  		<error>result == SUCCESS at line 217 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/main.c</error>

The code is https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/multicore.c#L143

    volatile seL4_Word counter;
    ...
    create_helper_thread(env, &t1);
    ...
    old_counter = counter;
    /* Let it run on the current core. */
    sleep_busy(env, 10 * NS_IN_MS);
    /* Now, counter should not have moved. */
    test_check(counter == old_counter);

TK1 sometimes fails CACHEFLUSH0001

The TK1 (jetson1) board sometimes fails the CACHEFLUSH0001 test:

<testcase classname="sel4test" name="CACHEFLUSH0001">
  Running test CACHEFLUSH0001 (Test a cache maintenance on pages)
  		<failure type="failure">*ptrc == 0xBEEFCAFE at line 104 of file /github/workspace/projects/sel4test/apps/sel4test-tests/src/tests/cache.c</failure>
  Test CACHEFLUSH0001 failed
  		<failure type="failure">result == SUCCESS at line 291 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/testtypes.c</failure>
  		<error>result == SUCCESS at line 217 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/main.c</error>
  	</testcase>

I've only seen this for clang-11 so far, in the configuration TK1_debug_hyp_MCS_clang_32, but it doesn't occur extremely often, so the may be others as well.

Example run: https://github.com/seL4/seL4/runs/4491614422?check_suite_focus=true#step:4:5733

provide seL4test in Rust

As a Follow-up from the discussion around seL4/seL4#733, having a Rust version of sel4test is needed to ensure the Rust bindings can be tested automatically and breaking changes are detected immediately.

sel4testdriver causes vmfault on completion; expected or not?

When the seL4 test root server exits it causes a NULL pointer dereference.

Is this expected behavior? Discussion with some developers indicated it was not, but reading the code seems to suggest this would be expected.

The output is:

All is well in the universe


Caught cap fault in send phase at address 0
while trying to handle:
vm fault on code at address 0 with status 0x82000006
in thread 0xffffff80bffe9400 "sel4test-driver" at address 0
With stack:
0x6d3ea0: 0x6d3ec0
0x6d3ea8: 0x40e88c
0x6d3eb0: 0x6d3f20
0x6d3eb8: 0x7e8000
0x6d3ec0: 0x6d3f00
0x6d3ec8: 0x40e9cc
0x6d3ed0: 0x0
0x6d3ed8: 0x6d3f40
0x6d3ee0: 0x6d3f30
0x6d3ee8: 0x6d3f20
0x6d3ef0: 0x2
0x6d3ef8: 0x4045a4
0x6d3f00: 0x0
0x6d3f08: 0x40e78c
0x6d3f10: 0x0
0x6d3f18: 0x7e8000

There is something disconcerting about seeing All is well in the universe following by a VM fault and a stack dump!

Reading through the run time the comment on the exit path is:

    /* If the exit is never set this will try and call a NULL function
     * pointer which should result in a fault. This is as good a way as
     * any to exit the process if we don't know anything better about
     * the environment. */
    env.exit_cb(code);

Which, seems reasonable, but the customer experience of seeing a stack trace at the end of testing is still not ideal.

Thoughts on addressing this are (in roughly difficulty order)

Put an additional print in sel4test to inform the user you should expect to see a NULL pointer dereference as the root task exits now
Put an infinite loop at the end of testing
Put a board shutdown or reset at the end of testing

test MULTICORE_0004 sometimes hangs

The test is already marked as flaky. If at all possible we should make this non-flaky.

There is also a comment inside the test that says it can never properly fail and would crash if not succesful. The hang behaviour we're seeing might be such a crash, and the issue might therefore be real (or just a race in the test).

I've seen this mostly come up on sabre, but not sure it was only there. (Edit: some specific configs are SABRE_verification_SMP_clang_32 *1 in 15 runs, IMX8MM_EVK_release_SMP_clang_64 * 2 in the same 15 runs)

Edit: also frequently on zynqm and zynqmp106 for HYP + clang + SMP.

hifive on MSC+SMP too often fails IPC0001

The config HIFIVE_verification_SMP_MCS_gcc_64 seem to now very often fail the test IPC0001 by hanging at that test.

This may be a result of the new build environment with downgrades riscv-gcc from version 10 to version 8 (as opposed to the upgrade from 8 to 10 on all other platforms).

The other configurations on hifive pass and this configuration passes on other boards.

For a sample, see https://github.com/seL4/seL4/runs/4494651972?check_suite_focus=true#step:4:12004

Cannot build sel4test for Rocketchip

Trying to build sel4test following the instructions on https://docs.sel4.systems/Hardware/rocketchip.html fails with:

[1/34] Linking C executable apps/sel4test-driver/sel4test-driver
FAILED: apps/sel4test-driver/sel4test-driver 
: && /usr/bin/ccache /opt/riscv64-unknown-elf-toolchain-10.2.0-2020.12.8-x86_64-linux-ubuntu14/bin/riscv64-unknown-elf-gcc --sysroot=/tmp/test/rocketchip  -D__KERNEL_64__ -march=rv64imac -mabi=lp64 -g -D__KERNEL_64__ -march=rv64imac -mabi=lp64   -static -nostdlib -z max-page-size=0x1000    -Wl,-u_sel4_start -Wl,-e_sel4_start  -Wl,-T /tmp/test/tools/seL4/cmake-tool/helpers/tls_rootserver.lds   -Wl,-umuslcsys_init_muslc /tmp/test/rocketchip/lib/crt0.o /tmp/test/rocketchip/lib/crti.o /opt/riscv64-unknown-elf-toolchain-10.2.0-2020.12.8-x86_64-linux-ubuntu14/bin/../lib/gcc/riscv64-unknown-elf/10.2.0/rv64imac/lp64/crtbegin.o apps/sel4test-driver/archive.o apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/main.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/tests/interrupt.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/tests/smmu.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/tests/syscall.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/tests/timer.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/testtypes.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/timer.c.obj -Wl,--start-group         -lgcc  libsel4/libsel4.a  apps/sel4test-driver/sel4runtime/libsel4runtime.a  apps/sel4test-driver/seL4_libs/libsel4allocman/libsel4allocman.a  apps/sel4test-driver/seL4_libs/libsel4vka/libsel4vka.a  apps/sel4test-driver/seL4_libs/libsel4utils/libsel4utils.a  apps/sel4test-driver/sel4_projects_libs/libsel4rpc/libsel4rpc.a  apps/sel4test-driver/seL4_libs/libsel4test/libsel4test.a  apps/sel4test-driver/seL4_libs/libsel4platsupport/libsel4platsupport.a  apps/sel4test-driver/seL4_libs/libsel4muslcsys/libsel4muslcsys.a  apps/sel4test-driver/libsel4testsupport/libsel4testsupport.a  -Wl,-u -Wl,__vsyscall_ptr  apps/sel4test-driver/seL4_libs/libsel4test/libsel4test.a  apps/sel4test-driver/sel4_projects_libs/libsel4rpc/libsel4rpc.a  apps/sel4test-driver/sel4_projects_libs/libsel4nanopb/libsel4nanopb.a  apps/sel4test-driver/sel4_projects_libs/libsel4nanopb/libnanopb.a  apps/sel4test-driver/seL4_libs/libsel4sync/libsel4sync.a  apps/sel4test-driver/seL4_libs/libsel4serialserver/libsel4serialserver.a  apps/sel4test-driver/seL4_libs/libsel4utils/libsel4utils.a  apps/sel4test-driver/util_libs/libelf/libelf.a  apps/sel4test-driver/util_libs/libcpio/libcpio.a  apps/sel4test-driver/seL4_libs/libsel4platsupport/libsel4platsupport.a  apps/sel4test-driver/sel4runtime/libsel4runtime.a  apps/sel4test-driver/util_libs/libplatsupport/libplatsupport.a  apps/sel4test-driver/util_libs/libfdt/libfdt.a  -Wl,--undefined=riscv_plic_ptr  apps/sel4test-driver/seL4_libs/libsel4simple-default/libsel4simple-default.a  apps/sel4test-driver/seL4_libs/libsel4vspace/libsel4vspace.a  apps/sel4test-driver/seL4_libs/libsel4simple/libsel4simple.a  apps/sel4test-driver/seL4_libs/libsel4vka/libsel4vka.a  apps/sel4test-driver/seL4_libs/libsel4debug/libsel4debug.a  libsel4/libsel4.a  apps/sel4test-driver/util_libs/libutils/libutils.a  apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a -Wl,--end-group /opt/riscv64-unknown-elf-toolchain-10.2.0-2020.12.8-x86_64-linux-ubuntu14/bin/../lib/gcc/riscv64-unknown-elf/10.2.0/rv64imac/lp64/crtend.o /tmp/test/rocketchip/lib/crtn.o -o apps/sel4test-driver/sel4test-driver && :
/opt/riscv64-unknown-elf-toolchain-10.2.0-2020.12.8-x86_64-linux-ubuntu14/bin/../lib/gcc/riscv64-unknown-elf/10.2.0/../../../../riscv64-unknown-elf/bin/ld: apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/main.c.obj: in function `init_env':
/tmp/test/projects/sel4test/apps/sel4test-driver/src/main.c:117: undefined reference to `ltimer_default_init'
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.

‘Caught cap fault …’ while trying to read/write device register

Hello:
I have ported the sel4 to my im6ull board. It runs will before dropping to the user space. after that, serical com arise errors like:

Caught cap fault in send phase at address 0
while trying to handle:
vm fault on data at address 0x10076008 with status 0x1008
in thread 0xffeef200 “sel4test-driver” at address 0x5fdfc
With stack:
0x10074e38: 0x0
0x10074e3c: 0x513
0x10074e40: 0x1
0x10074e44: 0x0
0x10074e48: 0x5
0x10074e4c: 0x90820
0x10074e50: 0x0
0x10074e54: 0x907e8
0x10074e58: 0x1000
0x10074e5c: 0x10074e6c
0x10074e60: 0x1000
0x10074e64: 0x907e8
0x10074e68: 0x10074e84
0x10074e6c: 0x0
0x10074e70: 0x10074e84
0x10074e74: 0x5fab4

Errors trigger by Location file:sel4test/projects/sel4test/apps/sel4test-driver/src/main.c
Errors tracing: main->main_continued->plat_init->clk_set_freq->_arm_set_freq->clk_get_freq(_arm_get_freq):uint32_t v = clk_regs.alg->pll_arm.val;
then it jump to kernel like:arm_vector_table-> arm_data_abort_exception->c_handle_data_fault->c_handle_data_fault->c_handle_vm_fault->handleVMFaultEvent->handleFault->handleDoubleFault
then the above error occurs.

How could I do? and the problem also occurs when init the GPT and UART. those device can be access correctly in the kernel but not the root server.