Sel4bench is not working for me on x86_64

Hi

I’m trying to run the sel4bench. I followed the instructions over at https://github.com/seL4/sel4bench-manifest .
The only difference is that I’m trying to run it on the x86_64 platform as such:

../init-build.sh -DRELEASE=TRUE -DPLATFORM=x86_64

It doesn’t seem to work and I’m getting the following output:

seL4 Benchmark
==============

Switching to a safer, bigger stack... 
Setting up global fault handler...
Failed to allocate object of size 140737488355328, error 1
Failed to allocate object of size 70368744177664, error 1
Failed to allocate object of size 35184372088832, error 1
Failed to allocate object of size 17592186044416, error 1
Failed to allocate object of size 8796093022208, error 1
Failed to allocate object of size 4398046511104, error 1
Failed to allocate object of size 2199023255552, error 1
Failed to allocate object of size 1099511627776, error 1
Failed to allocate object of size 549755813888, error 1
Failed to allocate object of size 274877906944, error 1
Failed to allocate object of size 137438953472, error 1
Failed to allocate object of size 68719476736, error 1
Failed to allocate object of size 34359738368, error 1
Failed to allocate object of size 17179869184, error 1
Failed to allocate object of size 8589934592, error 1
Failed to allocate object of size 4294967296, error 1
Failed to allocate object of size 2147483648, error 1
Failed to allocate object of size 1073741824, error 1
Failed to allocate object of size 536870912, error 1
Failed to allocate object of size 268435456, error 1

ipc Benchmarks
==============


irquser Benchmarks
==============

arch_simple_get_IOPort_cap not implemented
Failed to get capability for IOPort range 0x43-0x43
PIT command failed!
[Cond failed: error]
	Failed to init timer
Benchmark failed, result 1

Register dump:
rip	:0x4133d0
rsp	:0x100116c0
rflags	:0x246
rax	:0x10000000
rbx	:0x100116e0
rcx	:0x41fce8
rdx	:0xffffffffffffffff
rsi	:0x1
rdi	:0x2
rbp	:0x10011700
r8	:0x2b
r9	:0x12008180c100f
r10	:0x1
r11	:0x202
r12	:0x7235a0
r13	:0x1
r14	:0x0
r15	:0x0
fs_base	:0x723a50
gs_base	:0x0
[Cond failed: result == NULL]
	Failed to run benchmark irquser

I also tried the docker build method, but that made no difference.
I also tried without -DRELEASE=TRUE, with -DSIMULATE=TRUE, but neither of those made a difference.

Thanks in advance

1 Like

Hi,

I also tried to simulate seL4bench on QEMU, I am not even able to start the test.
I am getting compilation warning & runtime error as below
Can you please share as how you were able to get it running to some level & is your issue resolved ?
/***************************************************************************************/

./simulate
./simulate: QEMU command: qemu-system-x86_64 -cpu Haswell,-vme,+pdpe1gb,+xsave,+xsaveopt,-xsavec,+fsgsbase,+invpcid,+syscall,+lm,enforce -nographic -serial mon:stdio -m size=512M -kernel images/kernel-x86_64-pc99 -initrd images/sel4benchapp-image-x86_64-pc99 qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.01H:ECX.fma [bit 12]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.01H:ECX.pcid [bit 17]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.01H:ECX.x2apic [bit 21]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.01H:ECX.tsc-deadline [bit 24]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.01H:ECX.avx [bit 28]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.01H:ECX.f16c [bit 29]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.07H:EBX.hle [bit 4]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.07H:EBX.avx2 [bit 5]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.07H:EBX.invpcid [bit 10]
qemu-system-x86_64: warning: TCG doesn’t support requested feature: CPUID.07H:EBX.rtm [bit 11]
qemu-system-x86_64: TCG doesn’t support requested features

./simulate: QEMU failed; resetting terminal in 5 seconds–interrupt to abort

/****************************************************************************************/

Regards,
Misbah

Running sel4bench under qemu isn’t supported, because it does not make much sense to do so. qemu is not cycle accurate and doesn’t simulate enough of the machine (looks like that is what the run above is hitting) for the results of sel4bench to have any value – they would just be wrong.

Thank for the clarification.

But it should be mentioned in the Documation of seL4bench.
I request that this should be updated in the seL4 documentation.

We are going to port seL4bench for custom hardware running seL4 to measure the performance of the components.