Hello
I set up VMware according to this guide https://docs.sel4.systems/Hardware/VMware/ (using serial output to file) and compiled the picoserver CAmkES application (for x86_64) to run inside the VMware machine.
However, I do encounter a seL4_FailedLookup error. I understand the error message but cannot figure out why it occurs nor how to fix it (probably my pci configuration is wrong). Attached you find the serial_output file.
For the ethernet configuration I used linux in the same VM to …
[View More]figure out the details:
1) ip addr:
2: ens32: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc fq_codel state UNKNOWN group default qlen 1000
link/ether 00:0c:29:90:a7:4a brd ff:ff:ff:ff:ff:ff
2) lspci -vvv:
02:00.0 Ethernet controller: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] (rev 10)
Subsystem: Advanced Micro Devices, Inc. [AMD] PCnet - Fast 79C971
Physical Slot: 32
Control: I/O+ Mem+ BusMaster+ SpecCycle- MemWINV- VGASnoop- ParErr- Stepping- SERR- FastB2B- DisINTx-
Status: Cap- 66MHz- UDF- FastB2B+ ParErr- DEVSEL=medium >TAbort- <TAbort- <MAbort- >SERR- <PERR- INTx-
Latency: 64 (1500ns min, 63750ns max)
Interrupt: pin A routed to IRQ 18
Region 0: I/O ports at 2000 [size=128]
[virtual] Expansion ROM at fd500000 [disabled] [size=64K]
Kernel driver in use: pcnet32
Kernel modules: pcnet32
3) dmesg | grep "02:00.0":
...
[ 0.378516] pci 0000:02:00.0: BAR 6: assigned [mem 0xfd500000-0xfd50ffff pref]
...
4) lspci -nn:
02:00.0 Ethernet controller [0200]: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] [1022:2000] (rev 10)
And here the configuration part inside picoserver.camkes (anything else NOT pasted here is unmodified):
picoserver.ethdriver_mac = [0x00, 0x0c, 0x29, 0x90, 0xa7, 0x4a];
....
hwethdriver.mmio_paddr = 0xfd500000
hwethdriver.mmio_size = 0x10000
hwethdriver.irq_irq_type = "pci";
hwethdriver.irq_irq_ioapic = 0;
hwethdriver.irq_irq_ioapic_pin = 18;
hwethdriver.irq_irq_vector = 18;
ethdriver.iospaces = "0x0:0x02:0x00:0";
ethdriver.iospace_id = 0x0200;
ethdriver.pci_bdf = "0x02:0x00.0";
I am sorry to bother you with this; I am fairly new to low level stuff.
Any help would be very much appreciated.
Best regards,
Benjamin
[View Less]
Hi,
I was trying to add an extra component in hello-camkes-1 example. Here are
the small tweaks that I did.
a) hello-camkes-1-camkes.template
import <std_connector.camkes>;
import "components/Client1/Client1.camkes";
import "components/Client2/Client2.camkes";
import "components/Echo/Echo.camkes";
assembly {
composition {
component Client1 client1;
component Client2 client2;
component Echo echo;
connection seL4RPC hello_con(from client1.hello1,…
[View More] to echo.hello2);
}
}
--------------------------------------------------------------------------------------------------------------------------
b) CMakeLists.text
cmake_minimum_required(VERSION 3.7.2)
project(hello-camkes-1 C)
DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES
components/Client1/src/client1.c)
DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES
components/Client2/src/client2.c)
DeclareTutorialsCAmkESComponent(Echo TEMPLATE_SOURCES
components/Echo/src/echo.c)
DeclareCAmkESComponent(EmptyComponent)
DeclareTutorialsCAmkESRootserver(hello-camkes-1.camkes ADL_IS_TEMPLATE
TEMPLATE_SOURCES interfaces/HelloSimple.camkes
TUTORIAL_SOURCES components/Client1/Client1.camkes
components/Client2/Client2.camkes components/Echo/Echo.camkes
)
------------------------------------------------------------------------------------------------------------------------
I am getting the following error:
STDERR:
CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message):
Kernel supports hardware floating point but toolchain does not
Call Stack (most recent call first):
tools/seL4/cmake-tool/base.cmake:58 (include)
tools/seL4/cmake-tool/all.cmake:16 (include)
CMakeLists.txt:21 (include)
CMake Error at build/projects/sel4-tutorials/camkes-gen.cmake:192
(target_link_libraries):
Error evaluating generator expression:
$<TARGET_PROPERTY:CAmkESComponent_Client1,COMPONENT_LIBS>
Target "CAmkESComponent_Client1" not found.
Call Stack (most recent call first):
tools/camkes/camkes.cmake:591 (include)
projects/sel4-tutorials/CMakeLists.txt:257 (GenerateCAmkESRootserver)
CMake Error at build/projects/sel4-tutorials/cam... (2531 more, please see
e.stderr)
-----------------------------------------------------------------------------------------------------------------
Can you please suggest a possible solution.
--
Thanks and Regards,
Amit Goyal
[View Less]
Hi,
I am Zhonghao Liao, a graduate student from Iowa State University. We are
doing a security related project and would like to deploy the code to the
SEL 4.
The hardware we use is Raspberry Pi 3 B+. We follow the tutorial here
<https://docs.sel4.systems/Hardware/Rpi3.html> and have successfully
loaded the SEL4 test image. We think the next step should be building the
image for the application and run it on the Raspberry Pi. We followed
the CAmKES
tutorial <https://docs.sel4.systems/…
[View More]CAmkES/> and tried to use the command:
../init-build.sh -DPLATFORM=sabre -DAARCH32=1 -DCAMKES_APP=adder
-DSIMULATION=1
to build the image for the Raspberry Pi but we failed. In fact, we change
the settings.cmake file in the camkes-project folder and add "rpi3" at line
36:
set(valid_arm_platform
"am335x;sabre;kzm;exynos5410;exynos5422;tx1;tx2;zynq7000;rpi3")
and the command we used is:
../init-build.sh -DPLATFORM=rpi3-DAARCH32=1 -DCAMKES_APP=adder
-DSIMULATION=1
We did get an image but we cannot simulate using QEMU:
ninja:
Image Name:
Created: Tue Sep 17 09:30:30 2019
Image Type: ARM Linux Kernel Image (uncompressed)
Data Size: 2110464 Bytes = 2061.00 KiB = 2.01 MiB
Load Address: 0157c000
Entry Point: 0157c000
./simulate:
Unsupported platform or architecture for simulation
Also we tried to load the image into the RPi3 but we are also defeated:
bootelf {loadaddr}
## No elf image at address {loadaddr}
I think our problem is that we don't provide enough dependencies to support
building the RPi image. But we have no idea where to start. Could you
please give us any advice? Otherwise, If the CAmkES can not be used, how do
I build an application on SEL4 and run it on the Raspberry Pi?
Thanks for your patient and looking forward to your reply.
Thank you!
Best,
Zhonghao
[View Less]
Hi,
I am going to measure the resource consumption of process on SEL4 and I
found the tutorial here:
https://docs.sel4.systems/BenchmarkingGuide.html
One thing I am confused about is how to enable the benchmark feature shown
below:
"This feature can be enabled from the menuconfig list (seL4 Kernel > Enable
benchmarks > Track threads and kernel CPU utilisation time)."
It seems like there should be a file "menuconfig" or some other similar
object I can modify. But I cannot find such …
[View More]an object. I would
appreciate if you could give me any suggestions. Thank you!
Best,
Zhonghao
[View Less]
Hi,
I just used hello-camkes-1 tutorial to send and receive a message between a
client and an echo. My understanding is that both client and echo are in
the same machine but different address. What changes do I need to make so
that client and echo are in different machine? I have used docker for using
seL4 environment. I was thinking about using container1 for client and
container2 for echo and communicate between them. Is there any way I can do
it by modifying the hello-camkes-1tutorial? If …
[View More]not, can anyone suggest a
way to do it?
Thanks!
--
Regards'
Shahnewaz Karim Sakib
[View Less]
Hi,
I was trying to generate a simple broadcasting message in sel4. I have used
a c code I found in the internet.
#include <stdio.h>
#include <sys/socket.h>
#include <arpa/inet.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>
void DieWithError(char *errorMessage)
{
perror(errorMessage);
exit(1);
}
int main(int argc, char *argv[]) {
int sock;
struct sockaddr_in broadcastAddr;
char *broadcastIP;
unsigned short …
[View More]broadcastPort;
char *sendString;
int broadcastPermission;
unsigned int sendStringLen;
broadcastIP = "0.0.0.0";
broadcastPort = 6741;
sendString = "Hello World!";
printf("start\n");
printf("Socket is about to be created!\n");
if ( (sock = socket(AF_INET, SOCK_DGRAM, 0)) < 0 ) {
perror("socket creation failed");
exit(EXIT_FAILURE);
}
printf("Socket is created! \n");
broadcastPermission = 1;
if (setsockopt(sock, SOL_SOCKET, SO_BROADCAST, (void *)
&broadcastPermission,
sizeof(broadcastPermission)) < 0)
DieWithError("setsockopt() failed");
memset(&broadcastAddr, 0, sizeof(broadcastAddr));
broadcastAddr.sin_family = AF_INET;
broadcastAddr.sin_addr.s_addr = inet_addr(broadcastIP);
broadcastAddr.sin_port = htons(broadcastPort);
sendStringLen = strlen(sendString);
for (;;)
{
if (sendto(sock, sendString, sendStringLen, 0, (struct sockaddr *)
&broadcastAddr, sizeof(broadcastAddr)) != sendStringLen)
DieWithError("sendto() sent a different number of bytes
than expected");
sleep(3);
}
return 0;
}
However, I get the error in syscall 41. What I understood is that for
some reason the socket
is not created successfully and can't find an endpoint. What can be
the reason for that?
libsel4muslcsys: Error attempting syscall 41
Caught cap fault in send phase at address (nil)
while trying to handle:
vm fault on data at address 0x28 with status 0x4
in thread 0xffffff801fe09400 "rootserver" at address 0x40e3af
With stack:
0x41ce28: 0x40c0fe
0x41ce30: 0x418720
0x41ce38: 0x0
0x41ce40: 0x41ceb0
0x41ce48: 0x0
0x41ce50: 0x0
0x41ce58: 0x4011bd
0x41ce60: 0x41cf10
0x41ce68: 0x200402323
0x41ce70: 0x3
0x41ce78: 0x3
0x41ce80: 0x41ceb0
0x41ce88: 0x401ce2
0x41ce90: 0xffffffff00000000
0x41ce98: 0x412008
0x41cea0: 0x1a5500000041cf20
Thanks!
--
Regards'
Shahnewaz Karim Sakib
[View Less]
Hi,
I am porting an old application from CAmkES 2.x to CAmkES 3.7.0. But I am
having an issue with a very large dataport. The data structure mapped
between components needs to be about 25 MiB. I have defined the size of the
connection to be 64 MiB. But compilation fails.
Looking at the generated code for the shared data I see this
struct {
char content[ROUND_UP_UNSAFE(sizeof(ui_config_t),
PAGE_SIZE_4K)];
} to_0_ui_configbuf_data
ALIGN(16777216)
SECTION("…
[View More]align_24bit")
USED;
extern typeof(to_0_ui_configbuf_data) to_0_ui_configbuf_data
ALIGN(67108864) VISIBLE;
static_assert(sizeof(to_0_ui_configbuf_data) <= 67108864,
"typeof(to_0_ui_configbuf_data) size greater than dataport size.");
static_assert(sizeof(to_0_ui_configbuf_data) % 16777216 == 0,
"to_0_ui_configbuf_data not page-sized. Template bug in its declaration?
Suggested formulation: `char
to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`");
But compilation fails with
projects/musllibc/build-temp/stage/include/assert.h:12:23: error: static
assertion failed: "to_0_ui_configbuf_data not page-sized. Template bug in
its declaration? Suggested formulation: `char
to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`"
The assert is looking for the buffer to be a multiple of 16MiB but the
ROUND_UP_UNSAFE is only doing working to a multiple of 4KiB. PAGE_SIZE_4K
is hard coded in the template but the alignment has changed from 12bit to
24bit so CAmkES is aware of the large data structure.
I guess I could pad and align my data structure to a multiple of 16MiB.
Also, having hard coded numbers in my top level CAmkES configuration for
the dataport size is a bit of a maintenance nightmare. Being able to use a
#define from the code base would be ideal but this doesn't work. It does
work for paddr and irq_number specifications!
Cheers,
Zippy
[View Less]
Hi all,
I am trying to understand how the camkes system works. I get stuck up on a
problem where I tried to change the code of camkes 1 tutorial (
https://docs.sel4.systems/Tutorials/hello-camkes-1.html) a bit.
In a simple sender receiver code, I tried to write the contents, received
by the receiver, in a file. But, while doing it I got the following error
message. The error message was not letting me to create a file in any mode.
When using read mode with
FILE *fptr = fopen("xxxyyyzzz", "r");…
[View More]
I encountered the following message:
sys_open_impl@sys_io.c:205 Failed to open file xxxyyyzzz
FAULT HANDLER: data fault from client1.control (ID 0x1) on address 0, pc =
0x411754, fsr = 0x4
FAULT HANDLER: rip = 0x411754
FAULT HANDLER: rsp = 0x528ae8
When using write mode with
FILE *fptr = fopen("xxxyyyzzz", "w");
I encountered the following message:
sys_open_impl@sys_io.c:191 Open only supports O_RDONLY, not 0x241 on
xxxyyyzzz
Assertion failed: flags == O_RDONLY
(../projects/seL4_libs/libsel4muslcsys/src/sys_io.c: sys_open_impl: 192)
Kindly, suggest me a way out or let me know the reason if not possible.
-Akshat
[View Less]
Hi,
I was trying to compile hello world using the tutorial here
<https://docs.sel4.systems/Tutorials/#get-the-code>. I was able to compile
sel4test before and I built the dependencies using docker. For running
hello world, I used the command "../init --plat pc99 --tut hello-world".
Then I got the following error message:
Traceback (most recent call last):
File "../init", line 16, in <module>
import common
File
"/home/bikas/sel4-tutorials-manifest/projects/sel4-tutorials/…
[View More]common.py",
line 16, in <module>
import sh
ModuleNotFoundError: No module named 'sh'
I have looked into my machine and I do have sh in "/usr/bin/sh". I am not
sure what is the source of the error. Please let me know.
Thanks!
--
Shahnewaz Karim Sakib
[View Less]
