- Devel - lists.sel4.systems

[FOSDEM] [Fwd: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom] (fwd)
by Stefan Kalkowski 04 Oct '19

04 Oct '19

Hello sel4 community, I think below announcement might be interesting for you too. Best regards Stefan Kalkowski -------- Forwarded Message -------- From: Julian Stecklina <js(a)alien8.de> Reply-To: microkernel-devroom(a)lists.fosdem.org To: l4-hackers(a)os.inf.tu-dresden.de, users(a)lists.genode.org, microkernel-devroom(a)lists.fosdem.org, ukvly-announce(a)freelists.org, helenos-devel(a)lists.modry.cz Subject: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom Date: Fri, 04 Oct 2019 00:38:35 +0200 [Resent due to wrong Reply-To: header] FOSDEM 2020 - Microkernels and Component-based OS devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2020 [1] in Brussels, Belgium and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-, unikernel-, and component-based operating systems. Possible topics include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * used languages and tools * enabling support for hardware (architectures, device drivers) * enabling support for programming languages * maintenance and testing * security and robustness * trends and challenges * use cases, experiences, lessons learned and demos The deadline for your proposal is on December 1, 2019. Please use the Pentabarf [2] system to submit your proposals. You do not need to create a new account if you already have one. Make sure to include the following in your proposal: * title of your talk (will be printed in the FOSDEM booklet) * your full name (will be printed in the FOSDEM booklet) * a short abstract (one or two paragraphs) * duration of your talk (at least 25 and no longer than 55 min) The official devroom schedule (along with the accepted talks) will be announced on December 15 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. You are invited to send any other suggestions for what you want to see or do at the devroom to the list. We will also use this list to organize the traditional devroom dinner that will happen on the first day of FOSDEM. About the devroom Since the first Microkernel devroom at FOSDEM 2012, this devroom has been part of each following FOSDEM. The focus gradually widened to include component-based operating systems. By now it has become a somewhat institutionalized tradition for the community to meet there; to this date over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Social events It also has become a habit that the microkernel projects dine together somewhere in Brussels. The year 2020 will not be any different, so there is going to be a dinner on Saturday night. We try place a reservation, so we will inform you about the exact location and time later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. Important dates recap * 2019-12-01: Deadline for submissions * 2019-12-15: Schedule published and speakers notified of acceptance * 2020-02-01: Devroom Dinner (details to be announced) * 2020-02-01/2020-02-02: The devroom takes places (check the schedule) Links [1] https://fosdem.org/ [2] https://penta.fosdem.org/submission/FOSDEM20 [3] https://lists.fosdem.org/listinfo/microkernel-devroom _______________________________________________ FOSDEM mailing list FOSDEM(a)lists.fosdem.org https://lists.fosdem.org/listinfo/fosdem ----- End forwarded message ----- -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

1 0

Re: [seL4] CapDL output to isabelle file
by Lim, Japheth (Data61, Kensington NSW) 04 Oct '19

04 Oct '19

Hi Norrathep, Norrathep Rattanavipanon wrote: > I have been trying to generate Isabelle file from CapDL specification. But > I run into an error when I'm running the command: > > ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml > example-arm.cdl > We recently put in a major change to the Isabelle translator. The input capDL file is now required to be pre-allocated, i.e. every object must be placed in an untyped with a known physical address. The existing example files date from before this change, and so they don't meet the requirements to be translated into Isabelle. Sorry that you got confusing error messages as a result. We plan to make this more consistent in the near future. > Is there any step I'm missing? Or does the tool not support the conversion > to Isabelle? The standard way is to build a CAmkES application with the option `CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL file for proofs. Based on your other question thread, you may be interested in our README for CAmkES proofs: https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests This generates proofs between the CAmkES high-level model and the capDL system representation. However, we are not working on C glue code proofs at the moment. This is all work in progress, and quite rough around the edges. Nevertheless, we're happy to try to answer any questions you might have. It would help if we knew more about your work, so that we can give more specific replies. Cheers, Japheth Lim Proof Engineer, Trustworthy Systems

3 5

Initialising Camkes App before another dependent Camkes app
by yogidk . 03 Oct '19

03 Oct '19

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

3 2

Re: [seL4] How to use sel4runtime
by Millar, Curtis (Data61, Kensington NSW) 03 Oct '19

03 Oct '19

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 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

1 0

Run VM guest on seL4 using CAmkEs
by Khalid Amen 03 Oct '19

03 Oct '19

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. I have found a tutorial on how to run it from these links. https://github.com/seL4/camkes-vm-examples/blob/master/README.md https://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

2 1

Sel4 for quadcore riscv64imafd
by Sreenadh S 03 Oct '19

03 Oct '19

I want to build sel4 for quadcore riscv64imafd and run the test programs, how to do that? Regards, Sreenadh S, CDAC, Trivandrum, India

2 1

seL4_FailedLookup in vmware
by KAP Benjamin 03 Oct '19

03 Oct '19

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 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

2 1

Adding an Extra Component in Camkes
by Amit Goyal 03 Oct '19

03 Oct '19

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, 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

2 1

Questions about building Raspberry Pi image on SEL4
by Zhonghao Liao 03 Oct '19

03 Oct '19

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/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

2 1

Enable benchmarking tools on SEL4
by Zhonghao Liao 20 Sep '19

20 Sep '19

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 an object. I would appreciate if you could give me any suggestions. Thank you! Best, Zhonghao

2 1