Hi,
I have a Camkes app (app1) which depends on another Camkes app (app2),
which means my app1 must start only after app2 is completely initialized.
For this currently I use a signal RPC wait in app1 and the corresponding
RPC emit from app2 after app2 is completely initialized.
Is there any other way in CamkES which will ensure that app1 starts only
after app2 is completely initialized without using RPC signalling (emit and
wait) ?
How can this dependency be built ?
Regards
yk
Hi Baltazar,
> Another (less exclusively RISC-V related, though I am targeting RISC-V
> still) question - I've been trying to figure out the sel4runtime repo,
> but I'm a bit confused on how to set it up. Specifically:
>
> * How much of a "minimal seL4 environment" do I need to initialize
> first?
The sel4runtime is a minimal C runtime specifically for seL4. It handles
the initialization of all applications (root servers and System-V ELF
processes) on an seL4 system.
A …
[View More]minimal project will require a repo project containing seL4,
seL4_tools, musl, and sel4runtime (along with a root task application).
sel4runtime is then used as the C runtime for all applications built in
the project and is responsible for providing the entrypoints and calling
into the main function.
> * Do does my program with main() also need to specify a root task, or
> is that part of the minimal environment?
You will still need to provide a root task application. sel4runtime is
only responsible for handling process startup for C applications.
> * Is there a specific recommended location for the sel4runtime repo?
The sel4runtime repo is usually placed in the projects directory. You
can see sel4-tutorials-manifest[^1] repository on github for an example
of how the dependecies are laid out.
[^1]: https://github.com/SEL4PROJ/sel4-tutorials-manifest
Cheers,
Curtis Millar
Systems Engineer,
Trustworthy Systems, CSIRO's Data61
curtis.millar(a)data61.csiro.au
Data61, CSIRO
Level 3, K17 Building
UNSW Gate 14, Barker St
Kensington NSW 2033 Australia
[View Less]
Hello,
I am trying to run VM guest on seL4 using CAmkEs. I have setup my linux
machine and installed dependencies. I have run seL4 hello world example.
What do I need to do run VM guest in seL4?
I have serached online to see. The documentation says that to create VM
guests and applications on seL4, I need to use CAmkES. I followed this link:
https://docs.sel4.systems/Tutorials/camkes-vm-linux.html. What do I need to
create VM on top of seL4 using CAmkES? Also, I want seL4 to run as
hypervisor.
…
[View More]
I have found a tutorial on how to run it from these links.
https://github.com/seL4/camkes-vm-examples/blob/master/README.mdhttps://docs.sel4.systems/Tutorials/camkes-vm-linux
But, I did not understand the following:
You can boot the tutorial on an x86 hardware platform with a multiboot boot
loader, or use the QEMU <https://www.qemu.org/> simulator. *Note if you are
using QEMU it is important to ensure that your host machine has VT-x
support and KVM <https://www.linux-kvm.org/page/Main_Page> installed. You
also need to ensure you have enabled nested virtulisation with KVM guests
as described here <https://www.linux-kvm.org/page/Nested_Guests>.*
After building is completed with ninja, how do I excute the following:
Then boot images/kernel-x86_64-pc99 and
images/capdl-loader-experimental-image-x86_64-pc99 (or *.ia32-pc99 if built
for 32-bit) with the multiboot boot loader of your choice.
--
Regards,
Khalid Ameen
[View Less]
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]
