search

seL4 / sel4test

Test suite for seL4.
http://sel4.systems
Other
24 stars 60 forks source link

Running test under SMP conditions on spike platform gets stuck. #103

Open CtrlZ233 opened 11 months ago

CtrlZ233 commented 11 months ago

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?

axel-h commented 11 months ago

Your QEMU emulates just one core, so the boot is stuck waiting for the other core to come up. There is no timeout in the seL4 boot process, so the boot will always be stuck if the machine has less cores than expected.

CtrlZ233 commented 11 months ago

Your QEMU emulates just one core, so the boot is stuck waiting for the other core to come up. There is no timeout in the seL4 boot process, so the boot will always be stuck if the machine has less cores than expected.

It seems that I should specify parameters to the simulate script. What parameters should I specify?