Hi, As per instructions from here[1, 2], I tried booting seL4 on an x86_64-desktop, x86_64-server as RPi4. I was able to get it to work on RPi4 with one minor change to the instructions, but I could not boot it on the x86_64-desktop or the x86_64-server. Below is my experience and the issues I faced.
RPi4 ------ Spec: 8GB standard Rpi4 The final command "fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711" gave the following error:
** Reading file would overwrite reserved memory ** Failed to load 'sel4test-driver-image-arm-bcm2711
I could get around it by using a load address that was smaller by a factor of 0x10.( 0x1000000 instead of 0x10000000 i.e. one less zero). I cannot claim I understand why the first address failed and the second worked. Any pointers on that would help. After the change in the address, I saw the sel4 tests run as expected.
x86_64 server ------------------ Spec: Dell R520, two quad-core Xeons (E5-2407 v2 @ 2.40GHz), 32GB of memory.
The server's serial is redirected to the IPMI console. On the IPMI console, I see many messages related to the bios, etc. And finally, I see this:
MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading rootserver... ok
But nothing after this. Any thoughts of what could be going wrong here? I did not see any sel4 prints.
x86_64 Desktop ---------------------- Spec: Core 2 Quad, 4 GB ram
It was able to find the pinout for the serial port on the motherboard and connected to it(just like for RP). There was no output on the serial console. Even when bios-related messages were printed on the monitor, there was no output on the serial pins. I might need to enable the serial output on those pins in the bios or something similar.
Fortunately, even though the serial pins did not have any output, the monitor output was the same as for the server. Unfortunately, it did not get any farther along than the server.
MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading rootserver... ok
Any pointers here would be helpful.
Thanks, Sid UBC Graduate Student ARM Research Intern
[1] https://docs.sel4.systems/Hardware/IA32 [2] https://docs.sel4.systems/Hardware/Rpi4.html
"Sid" == Sid Agrawal siagraw@cs.ubc.ca writes:
Sid> x86_64 server ------------------ Spec: Dell R520, two quad-core Sid> Xeons (E5-2407 v2 @ 2.40GHz), 32GB of memory.
Sid> The server's serial is redirected to the IPMI console. On the Sid> IPMI console, I see many messages related to the bios, etc. And Sid> finally, I see this:
The serial port redirected over IPMI is usually com2 not com1.
If you change the boot command to:
kernel mboot.c32 append sel4kernel console_port=0x2f8 debug_port=0x2f8 --- sel4rootserver
you may see the correct output.
Sid> x86_64 Desktop ---------------------- Spec: Core 2 Quad, 4 GB ram
Sid> Fortunately, even though the serial pins did not have any output, Sid> the monitor output was the same as for the server. Unfortunately, Sid> it did not get any farther along than the server.
Sid> MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading Sid> rootserver... ok
Again, check *which* serial port you hooked up. Booting linux, and doing something like stty 115200 < /dev/ttyS0 echo foo > /dev/ttyS0
will tell you if you have serial hooked up right. Possibilities are: -- need to swap Rx and Tx lines on the connector -- talking to wrong port (com2 instead of com1)
Peter C
Thanks a lot Peter. The issues were on my end.
Desktop ----------- COM1 was the right port, but I was connecting the wrong physical connector on the motherboard. After connecting the connector I am seeing output on the port. However, the output is garbled, but it is the right amount of output. Even the non-sel4 o/p is garbled, *so this is not a seL4 issue*. If you have any insights on what could be happening here, that would be great.
Looking at the serial_init() https://github.com/seL4/seL4/blob/master/src/plat/pc99/machine/io.c#L15 function in the kernel for pc99. I see that baudrate is 115200, with no parity and 1 stop bit. Based on that I used the following picocom command:
picocom -b 115200 -p n -f n -s 1 /dev/ttyUSB0
I tried different baudrates and settings, but no luck.
Server: -------- I did not get a chance to try on a server. I will do that only if I cannot make it work on the desktop.
Thanks again, sid
On Thu, May 26, 2022 at 8:58 PM Peter Chubb peter.chubb@unsw.edu.au wrote:
[CAUTION: Non-UBC Email]
"Sid" == Sid Agrawal siagraw@cs.ubc.ca writes:
Sid> x86_64 server ------------------ Spec: Dell R520, two quad-core Sid> Xeons (E5-2407 v2 @ 2.40GHz), 32GB of memory.
Sid> The server's serial is redirected to the IPMI console. On the Sid> IPMI console, I see many messages related to the bios, etc. And Sid> finally, I see this:
The serial port redirected over IPMI is usually com2 not com1.
If you change the boot command to:
kernel mboot.c32 append sel4kernel console_port=0x2f8 debug_port=0x2f8 ---sel4rootserver
you may see the correct output.
Sid> x86_64 Desktop ---------------------- Spec: Core 2 Quad, 4 GB ram
Sid> Fortunately, even though the serial pins did not have any output, Sid> the monitor output was the same as for the server. Unfortunately, Sid> it did not get any farther along than the server.
Sid> MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading Sid> rootserver... ok
Again, check *which* serial port you hooked up. Booting linux, and doing something like stty 115200 < /dev/ttyS0 echo foo > /dev/ttyS0
will tell you if you have serial hooked up right. Possibilities are: -- need to swap Rx and Tx lines on the connector -- talking to wrong port (com2 instead of com1)
Peter C
-- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.
An update for the archives.
Desktop: ----------- I tried doing the same experiment Peter suggested - i.e., try from Linux to check if the serial port worked fine. But I was still getting garbled data, I played with baud, parity, stop bits, etc., but no luck. The serial to USB cables I tried was:
- USB to TTL Serial Cable - Debug / Console Cable for Raspberry Pi from Adafruit https://www.adafruit.com/product/954: This is often sold with raspberry pies. - USB 2.0 to TTL Level https://www.aliexpress.com/item/33001930568.html?spm=a2g0o.productlist.0.0.47dd5428RdUDOc&algo_pvid=8c8abdcc-160b-4eab-9a2d-ae8d0ff7f9c8&algo_exp_id=8c8abdcc-160b-4eab-9a2d-ae8d0ff7f9c8-6&pdp_ext_f=%7B%22sku_id%22%3A%2212000027174900820%22%7D&pdp_npi=2%40dis%21CAD%21%212.68%21%21%21%21%21%402101e9cf16540569516133604e7863%2112000027174900820%21sea: This one let me change the logic's voltage level to either 5V or 3.3V. I thought that the desktops logic level may be 5V instead of the typical 3.3 for raspberry pi.
Neither of these cables worked. But the following cable worked with pretty much the default baud of 115200, parity options.
- https://www.amazon.ca/gp/product/B075YHFMC7
I do not plan to dig into why I got garbled data with the first two cables and correct data with the last cable - as I already spent way too much time on this :)
On Fri, May 27, 2022 at 2:54 PM Sid Agrawal siagraw@cs.ubc.ca wrote:
Thanks a lot Peter. The issues were on my end.
Desktop
COM1 was the right port, but I was connecting the wrong physical connector on the motherboard. After connecting the connector I am seeing output on the port. However, the output is garbled, but it is the right amount of output. Even the non-sel4 o/p is garbled, *so this is not a seL4 issue*. If you have any insights on what could be happening here, that would be great.
Looking at the serial_init() https://github.com/seL4/seL4/blob/master/src/plat/pc99/machine/io.c#L15 function in the kernel for pc99. I see that baudrate is 115200, with no parity and 1 stop bit. Based on that I used the following picocom command:
picocom -b 115200 -p n -f n -s 1 /dev/ttyUSB0
I tried different baudrates and settings, but no luck.
Server:
I did not get a chance to try on a server. I will do that only if I cannot make it work on the desktop.
Thanks again, sid
On Thu, May 26, 2022 at 8:58 PM Peter Chubb peter.chubb@unsw.edu.au wrote:
[CAUTION: Non-UBC Email]
> "Sid" == Sid Agrawal siagraw@cs.ubc.ca writes:
Sid> x86_64 server ------------------ Spec: Dell R520, two quad-core Sid> Xeons (E5-2407 v2 @ 2.40GHz), 32GB of memory.
Sid> The server's serial is redirected to the IPMI console. On the Sid> IPMI console, I see many messages related to the bios, etc. And Sid> finally, I see this:
The serial port redirected over IPMI is usually com2 not com1.
If you change the boot command to:
kernel mboot.c32 append sel4kernel console_port=0x2f8 debug_port=0x2f8 ---sel4rootserver
you may see the correct output.
Sid> x86_64 Desktop ---------------------- Spec: Core 2 Quad, 4 GB ram
Sid> Fortunately, even though the serial pins did not have any output, Sid> the monitor output was the same as for the server. Unfortunately, Sid> it did not get any farther along than the server.
Sid> MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading Sid> rootserver... ok
Again, check *which* serial port you hooked up. Booting linux, and doing something like stty 115200 < /dev/ttyS0 echo foo > /dev/ttyS0
will tell you if you have serial hooked up right. Possibilities are: -- need to swap Rx and Tx lines on the connector -- talking to wrong port (com2 instead of com1)
Peter C
-- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.
"Sid" == Sid Agrawal siagraw@cs.ubc.ca writes:
Sid> An update for the archives. Desktop: ----------- I tried doing Sid> the same experiment Peter suggested - i.e., try from Linux to Sid> check if the serial port worked fine. But I was still getting Sid> garbled data, I played with baud, parity, stop bits, etc., but no Sid> luck. The serial to USB cables I tried was:
Desktops/servers etc., use the RS232 standard for their serial ports. Embedded X86 boards can use RS232 or RS422, or occasionally other standards. These use ±12V levels, referenced to ground for RS232, and floating in pairs for RS422.
The embedded development boards we use bring out the UART pins directly, without an RS232 or RS422 driver, so they are at whatever voltage the UART chip runs at, using gound as a reference. Usually, that's 1.8V, 3.3V or 5V. Your typical FTDI cable will talk one of these.
Peter C
Hi Peter, Thanks, for the explanation. Shall we add this to PC99 https://docs.sel4.systems/Hardware/IA32 site? Could potentially save people a lot of time :)
Sid
On Thu, Jun 9, 2022 at 4:01 PM Peter Chubb peter.chubb@unsw.edu.au wrote:
[CAUTION: Non-UBC Email]
"Sid" == Sid Agrawal siagraw@cs.ubc.ca writes:
Sid> An update for the archives. Desktop: ----------- I tried doing Sid> the same experiment Peter suggested - i.e., try from Linux to Sid> check if the serial port worked fine. But I was still getting Sid> garbled data, I played with baud, parity, stop bits, etc., but no Sid> luck. The serial to USB cables I tried was:
Desktops/servers etc., use the RS232 standard for their serial ports. Embedded X86 boards can use RS232 or RS422, or occasionally other standards. These use ą12V levels, referenced to ground for RS232, and floating in pairs for RS422.
The embedded development boards we use bring out the UART pins directly, without an RS232 or RS422 driver, so they are at whatever voltage the UART chip runs at, using gound as a reference. Usually, that's 1.8V, 3.3V or 5V. Your typical FTDI cable will talk one of these.
Peter C
Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.
-
Peter Chubb -
Sid Agrawal