[seL4] Rust application support

Using rust (https://www.rust-lang.org) in user applications on top of seL4 with existing C libaries and apps now has limited support. See here for more information: https://wiki.sel4.systems/Rust What you can do: + Build system support for using a rust cargo project as a library or app on s

Re: [seL4] quesitons about TK1 VMM

Hi Peng, Adding the ethernet card requires adding the 0 ASID in the vm.camkes file that I mentioned in the previous email. vm.smmu = [0, 10, 24]; This gives permission for PCIE devices to read and write to memory. I confirmed that on the TK1 Jetson the ethernet port works after this ch

Re: [seL4] CAmkES ARM VM boot on TK1

It works on our jetson. The uboot commands that we use are: `setenv autoload no && dhcp && tftpboot 0x8100 jetson1/sel4-image` and then `bootelf 0x8100` What compiler versions are you using? Kent. From: Devel on behalf of SHI, Yao Sent: Wednesday,

[seL4] Using Rump kernels to run unmodified NetBSD drivers on seL4

Last year for my honors thesis I evaluated rump kernels as a way of running unmodified NetBSD drivers on seL4.  This work has recently been pushed out with a corresponding blog post:  https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbsd-drivers-on-sel4/. This was done b

Re: [seL4] TK1 VMM SMMU Translation Error

Hi, We recently changed a configuration so that SMMU_INTERRUPT_ENABLE? was default enabled. This causes SMMU faults to be printed out (and sometimes prevent the system from making progress), if you want to stop this behavior, changing this setting to not enabled will prevent the errors from b

[seL4] Announcing seL4 5.0.0

you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Kent McLeod Kernel engineer DATA61 | CSIRO E kent.mcleod at data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital power

Re: [seL4] camkes-arm-vm not registering GPIO?

Hi Steven, Your problem could be that the GPIO MMIO frame is not being given to the VM. The config setting CONFIG_TK1_INSECURE increases the amount of hardware devices that are passed through to the VM. Once the GPIO device is accessible in the VM, Linux should be able to attach its own GPIO

Re: [seL4] camkes-arm-vm not registering GPIO?

Hi Steven, Some changes were pushed out last night to Github which may have fixed your issue of not being able to tftpboot. When I use the CONFIG_TK1_INSECURE config setting, once the device successfully boots I can see 6000d000.gpio under /sys/devices/soc0 however I haven't tested that they a

Re: [seL4] Using linux-tk1-debian on camkes-arm-vm

Hi Mike, We weren't able to get the official Nvidia Ubuntu distribution (R21.5) working on top of the version of Linux that we provide for the arm-camkes-vm. We created our own debian rootfs ourselves using debootstrap. The link to one we created is here (https://drive.google.com/uc?id=0B9-S

Re: [seL4] Using linux-tk1-debian on camkes-arm-vm

Hi Mike, You are probably right. At the moment the seL4 doesn't save and restore FPU state on ARM. I believe we are currently working on adding this currently within Data61. Once that's done, the vmm will need to be set up to provide the guest access to the FPU. Until then the guests have t

Re: [seL4] vmm documentation

Hi Mike, If you look at handle_page_fault(), the VMM can do limited instruction emulation if the relevant info is in the ISS segment of the HSR. Any other emulation isn't supported. handle_page_fault() handles cases of restarting a faulting instruction, emulating an instruction, or in the ht

Re: [seL4] vmm documentation

Hi Mike, Those coprocessor registers are not currently saved or restored in the VCPU. If they were you could use the ARMVCPUReadReg and ARMVCPUWriteReg invocations to control the value of those registers for the guest. There is an active task internally to add those coprocessor registers to t

Re: [seL4] vmm documentation

Hi Mike, I've pasted a sample of using those invocations to update banked registers from advance_fault() in libsel4arm-vmm/src/fault.c: /* register is banked, use vcpu invocations */ seL4_ARM_VCPU_ReadRegs_t res = seL4_ARM_VCPU_ReadRegs(vm_get_vcpu(fault->vm), reg); if

Re: [seL4] vmm documentation

Hi Mike, Looking at your back-trace and the code, it appears that during the process of mapping in the memory in order to read the instruction to calculate the instruction width copy_in_page() fails to map the page in. To debug where that failure is occurring it may be worthwhile inserting so

Re: [seL4] Why armel for the seL4 ARM VMM?

Hi John, This was answered recently here: http://sel4.systems/pipermail/devel/2017-June/001455.html In summary, we don't currently give threads access to the FPU on arm and the VMM cannot emulate the instructions but this should change soon. There is a patch internally for making the FPU ac

Re: [seL4] vmm documentation

Hi Mike, It is interesting that vspace_get_cap() is returning a null cap. Given that the VM is faulting on that instruction it therefore must be mapped in to the guest, and if it is mapped into the guest, the guest vspace should return the cap for the mapping. sel4utils_get_cap() is the funct

Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Hi, I can't tell from your output if the kernel had started the init task yet or not. If the init task has been started, this error usually indicates a toolchain that is trying to use FPU, which is not currently supported. FPU support that enables floating point toolchains on arm should be r

Re: [seL4] vmm documentation

I don't think this is possible with how seL4 manages the page tables in the ARM hyp model (Someone who is more familiar with this may need to correct me here). You may be able to achieve the same result by telling Linux that there is some device memory somewhere there is not and rely on a dat

Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Hi, I cannot think of any reasons why Linux3.10 wouldn't also work other than making similar modifications that we made to Linux4.3. The list of modifications that we made can be seen here: https://github.com/SEL4PROJ/linux-tegra/commits/sel4 If you wanted to try and add support for that ve

Re: [seL4] rump kernel test, compilation issues

Hi Steve, I believe this is due to the order that we automatically push our libraries to Github. If you try again now it should work. Kind regards, Kent. From: Devel on behalf of Steven Harp Sent: Saturday, July 29, 2017 3:27 AM To: devel@sel4.system

Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

This could be due to an IOMMU configuration issue. Have you tried turning on the CONFIG_SMMU_INTERRUPT_ENABLE as well as CONFIG_PRINTING options in the seL4 kernel configuration? This will print out IOMMU faults that indicate the IOMMU isn't configured correctly. Kent. __

Re: [seL4] camkes-vm cma34cr_picotcp doesn't build

Hi Michal, I fixed it now (so that it compiles). The PicoTCP components didn't appear to be connected to the VM at all so I temporarily removed the VM from the CAmkES spec as it was polluting the serial output. Do you have a tardec platform to run the app on? We do have CI but not for that

Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

ID 1 should correspond to the DC SMMU group which we assign ASSID 3, which is referred to in CAmkES as 2. We disable the video controller in our Linux configs and device tree file I believe, so I haven't tested if providing the correct SMMU configuration fixes your issue sorry. ?If you don't n

Re: [seL4] rumprum and camkes

Hi Michal, There are currently two ways to run rump kernels on seL4:  - A single process, created and started by a small root task that gets passed caps to most resources in the system.  This is what the blog post and thesis refers to.  It currently only supports running one rumpkernel in the s

Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

?The ID 99 refers to the "global memory client ID" specific to the Tegra platform. They can be found in the Technical reference manual under section: 16.7.1.3 MC_ERR_STATUS_0 In this case it refers to the group sdmmc4a?. Kent From: li94575 Sent: Saturday,

Re: [seL4] rumprun + rust + camkes

​Hello Michal, I haven't found a nice way of linking CAmkES generated symbols against the top level of rumprun apps yet. By top level I mean the POSIX app that gets linked against syscall layer, and the bottom level is the implementation of the syscall layer including the rump kernel, platfor

Re: [seL4] rumprun + rust + camkes

I think you need another pointer layer for variables. So: #[linkage = "extern_weak"] static camkes_buffer: *const*mut u8; And then another dereference when you assign to it. I don't know if this is a bug in rust - there is an example of it in a comment on the rust issue I linked in my las

Re: [seL4] rumprun + rust + camkes

​Oh, it worked that way for a const char* that I tested it with yesterday. I'll try have a look at your app. Kent From: Michal Podhradsky Sent: Friday, August 18, 2017 9:03 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4]

Re: [seL4] rumprun + rust + camkes

​I had to add brackets around one of the dereferences: *(*camkes_buffer).offset(0) = 'a' as u8; See here:https://github.com/kent-mcleod/camkes/tree/rustapp-buffer​ Kent. From: Devel on behalf of kent.mcl...@data61.csiro.au Sent: Friday, August 18, 2017 9:0

[seL4] Announcing 7.0.0 release

= seL4 Version 7.0.0 Release = Announcing the release of seL4 7.0.0 with the following changes: == Changes == * Support for building standalone ia32 kernel added in e7327fa6df3 * ia32: Set sensible defaults for FS and GS selectors in c2f6d48bcf2 * aarch64: Use tpidrro_el0 for IPC buffer instead

Re: [seL4] Problem making the manual

Hi Raymond, The issue occurs because some python scripts used to generate the manual were only python2 compatible. I've fixed this internally so that in the future the manual can be built using python3 or python2. In the meantime, you can force the manual to be build using python2 with the

Re: [seL4] Fw: sel4 on QEMU

Hi Ashok, The fix for this compilation error is currently going through our internal continuous integration process. I can let you know when the fix has been pushed to our external repositories. In the meantime, you can either: - Enable the HARDWARE_DEBUG_API config setting for the kernel.

Re: [seL4] Question about IO ports in CAmKES

Hi John, The purpose is to allow the attributes on the CMOS hardware component to have defaults but still able to be overridden by configuration settings of the RTC component that contains it. If in your assembly you had an instance of the RTC component called clock, then in your configurati

[seL4] seL4 8.0.0 and CAmkES camkes-3.2.0 release

seL4 8.0.0 and CAmkES camkes-3.2.0 release = seL4 8.0.0 = Note: Meltdown and Spectre patches are not included in this release and will be included in a forthcoming release once they have been verified. Once they are merged they will still be accessible through the master branch of seL4 on gith

Re: [seL4] Userspace Debugging for ia32

​​Hi Aslam, Here is an example of debugging sel4test on ia32. (note that the following assumes that you are running on a x86_64 host machine. If you don't then you will need to install gdb-multiarch) # Apply a sel4test config for simulating using qemu. make ia32_release_xml_defconfig # After

Re: [seL4] CamkesVM CMA34CR_centos app

Hi Michal, Which revision of default.xml are you using? Adrian thinks it could be potentially related to, and fixed by, this commit[1] if you don't have it yet. Kent [1] https://github.com/seL4/seL4/commit/3d6f4f9bb7bfe42628dfa555601401fa4efcdf2d​ From:

Re: [seL4] Fwd: CamkesVM CMA34CR_centos app

Hi Michal, I ran the default.xml from revision c4a64560668a05831e1b6b4d491e84f67e8650a4 on our CMA34cr using the same config as you and it boots successfully using pxeboot. Kent. From: Devel on behalf of Michal Podhradsky Sent: Wednesday, February 21, 2018

Re: [seL4] Camkes limitations

?Hi Sam, Thanks for your email. Regarding issue A, I was unable to reproduce your issue. In the source you sent, some of the include statements for myrtc.h had a # in front of them (in Duck.camkes and DuckHerd.camkes)? which causes the parser to treat them as a C preprocessor directive and s

Re: [seL4] seL4 VMM Hangs during loading time

​Hi Daniel, Two things to try: First is to confirm that CONFIG_PRINTING is enabled to distinguish if the kernel is successfully starting its init process. Second is ​to check what ${loadaddr} is set to. Yours seems correct, ours seems to be 0x8100, but that is for the tk1 jetson dev board

Re: [seL4] Compilation Error with version

Hi Daniel, To check out a particular version of default.xml you can pin it when you checkout via: repo init -u https://github.com/SEL4PROJ/camkes-arm-vm-manifest.git -b 15844a5f9ddd4a7b1a29144201e8a7431917efdb Having initialised a repo this way, running repo sync will not update anything.?

Re: [seL4] Questions about Vchan

As far as I am aware, the arm support for Vchans was never finished.? I tried to get it running once and I believe the issue was that it expected the same vmm_manager device that the x86 vmm provides, but this isn't implemented on the ARM vmm. Kind regards, Kent McLeod

Re: [seL4] irq_server example? Interrupt handlers?

​Hi Richard, Have you looked at the ​​ethernet-demo-x86-manifest[1]? It uses an ethernet driver in an interrupt driven way: https://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master/ethernet-demo-app/ethernet-demo.c#L125. I can't guarantee that the app works, but there does

Re: [seL4] Status of cmake support?

Hi Bruce, The clang bugs would have been referring to the camkes-accelerator, a cache tool for building camkes projects, only gcc is supported for building seL4 and user-level programs. The cmake support for sel4test is being regularly used internally so feel free to post issues that you are

[seL4] seL4 9.0.0 and CAmkES camkes-3.3.0 release

See an online copy of the release notes at: # seL4 Version 9.0.0 Release Announcing the release of `seL4 9.0.0` with the following changes: 9.0.0 2018-04-11: BREAKING # Changes * Debuggi

[seL4] New documentation website: https://docs.sel4.systems

​​We are pleased to annouce a new documentation website at ! The documentation site is now using GitHub pages, generated from a GitHub repository using a popular static site generator, Jekyll. GitHub pages hosted documentation is a s

[seL4] Announcing seL4 9.0.1: with RISC-V support

We are pleased to announce initial RISC-V support for the UC Berkeley Spike simulator platform. Instructions are available for building and running the seL4 test suite on RISC-V: ​See an online copy of the release notes at:

Re: [seL4] Problems with tk1 nonsecure

Hi Mike, I'm not sure what changes in the last 6 months would have changed your build from a working to broken state. The below commits[1] are the only changes that I am aware would change the behavior of smmu permissions. ID: 98? corresponds to sdmmc3 (there is a table in the tk1 reference

Re: [seL4] Problems with tk1 nonsecure

Hi Mike, For some reason, the Tk1Insecure setting gets reset to false during the initial configuration which is why you can't see the ethernet card. Running the below command, or opening the cmake cache using (ccmake .) you can correct the setting. cmake -DTk1Insecure=True . && ninja Kent.

Re: [seL4] Problems with tk1 nonsecure

Hi Mike, Do still get the error when you add ID 22 to this list yourself?: https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/vm_common.camkes#L278​ Kent. From: Mike Clark Sent: Tuesday, June 26, 2018 6:00 AM To: Mcleod, Kent (Data61, Kensi

Re: [seL4] ninja build tool error

Hi, Does it work if you try ../init --plat pc99 --tut hello-1 on version 10.0.0 or later of the tutorials? I am aware of an issue where the tutorial documentation on https://docs.sel4.systems/Tutorials was updated to reflect version 10.0.0, but the link to the sources wasn't updated from 9.0

Re: [seL4] seL4 vm examples with Qemu

Hi Mike, I am aware of this guide: https://github.com/GaloisInc/rustwall_vm/blob/32cd73ccb20357e1337b5420707504d6eff5c328/HOWTO_QEMU.md It has instructions for setting up qemu to be able to run simulations that require VT-x/d features. However it requires changes to the host kernel. Additi

Re: [seL4] Help ! Simulating SEL4 with Zero testcases running

Hi Sathya, Perhaps "" also matches everything. What about trying "$^" or "XCZAXCZXC"? Additionally, if you are building with the make build system, you might want to verify that the relevant config value is being updated in .config.? If you are building with the CMake build system, then

Re: [seL4] Implementing a Filesystem on CAmkES

Hi Grant, Additionally, if you wanted a basic example to look at, the camkes-vm-examples project uses a file server to share access to a CPIO filesystem across vmm instances. The fileserver component uses the cpio "filesystem" via musllibc syscalls to export a simple open, close, read, seek RP

Re: [seL4] CAmkES 3.5.0 Build Error

Hi Amit, The error message appears to be truncated by the python stack trace. There should be a build directory that was created by the command you ran named something like build_*. What error message do you get if you change into that directory and then run the command: /usr/local/bin/cmake -

Re: [seL4] camkes-project error

Does "qemu-system-arm -machine help" list sabrelite? Otherwise you may need to update your version of Qemu. I have 2.12.0? which works. Kent From: Devel on behalf of talos <2486580...@qq.com> Sent: Tuesday, August 7, 2018 5:25 PM To: devel Subject: Re: [seL4]

Re: [seL4] Cap fault in send phase while spawning processes

Hi Noah, Assuming that the issue is related to the new build scripts, have you checked that archive.o contains the other programs that you are trying to load? Is archive.o being included in the call to add_executable? Processes started by libsel4utils are expected to have the __vsyscall_ptr?

Re: [seL4] Demo build

​ Hi Chris, For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib. With regards to cpio --reproducible, what version of cpio are you using? The release

Re: [seL4] Demo build

​I added a check to only use the flag if it is supported, so once that propagates to the external repositories it should stop being an issue for you. The purpose of --reproducible is for generating identical binaries on subsequent rebuilds, so it isn't a critical flag. In the meantime, you can

Re: [seL4] building sel4test for zynqmp platform

Hi Leonid, You need to initialise CMake with the arm toolchains otherwise it will try and use your host toolchains by default. CMake will print out the toolchain it uses when you initialise it: ../init-build.sh -DSIMULATION=ON -DPLATFORM=sabre -DAARCH32=ON -- The C compiler identification is

Re: [seL4] 32 bit vs 64 bit

Hi Chris, This is expected. When the kernel is started by the bootloader, the processor is in protected mode and can only use 32-bit instructions. One of the first things the x86_64? kernel then does is to switch the processor to long mode and enable 64-bit instructions. Because of this, th

Re: [seL4] Camkes Build Error

Hi Amit, This issue was fixed in this commit: https://github.com/seL4/camkes-tool/commit/3ea3061f066051a7a099cabed140163d5907d0b8 You can upgrade to the current version of the tutorials with repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest instead of repo init -u https://github.c

Re: [seL4] Building/Running https://github.com/SEL4PROJ/docs with docker

What about if you run `make docker_serve`. There's a target `generatate_api` that needs to be run. Kent. From: Devel on behalf of Axel Heider Sent: Tuesday, September 18, 2018 12:14 AM To: devel@sel4.systems Subject: [seL4] Building/Running https://g

Re: [seL4] seL4 and rump kernel synchronization primitives limitations

Hi Jason, This is an issue that I have thought about before, but haven't had a chance to fix properly. As you point out, the underlying issue is that Camkes threading model maps one camkes thread to one seL4 thread (obviously camkes threads are just seL4 threads) while the rumprun threading m

Re: [seL4] Kernel Exception in seL4 Tutorial

Hi Jeremiah, According to your output, the kernel doesn't finish booting and crashes before user-mode is entered.  I am unable to replicate the error that you are experiencing unfortunately.  It is likely that the issue is being caused by different host tooling than what we use. Here are some

Re: [seL4] MCS tutorial

?Hi, The build error is higher up in the output. What you are seeing is output of a parallel job. What happens when you run ninja again? Or capture the full build output and look through the file. Kent. From: Devel on behalf of hedi delpazir Sent: Tuesda

Re: [seL4] CAmkES-VM Stalling

Hi Chris, Unfortunately I was not able to reproduce your issue. I did a checkout following your instructions and used this manifest:  https://github.com/seL4/camkes-vm-examples-manifest/blob/e37e3e259ff7dd5060eb3e8b7ddc8e46009d9ef7/default.xml I changed the FPU save method, and ran the resulting

Re: [seL4] seL4 IPC SMP

Hi, I attached two of the benchmark results that I pulled from the last run. Looking at the top of each of them I get similar results to you: "Benchmark": "One way IPC microbenchmarks", "Direction": "client->server", "Function": "seL4_Call", SMP on (mean, stddev)444.125, 5.17687164

Re: [seL4] Kernel Exception in seL4 Tutorial

​Happy that it is working for you in the Docker container. Based on the images you provided, it seems that the compiler is generating instructions for a newer microarchitecture than what qemu is simulating. This is why seL4test is getting a user exception. Do you tweak the microarchitecture set

Re: [seL4] can not build tutorials anymore

​Hi, If you change into the build directory (/home/john/sel4/hello-camkes-1_build) and just run cmake then it should remove a lot of the extra output (We should probably capture a lot of the python stack tracing). The actual error is     File "/home/john/sel4/projects/sel4-tutorials/tools/cont

Re: [seL4] Kernel Exception in seL4 Tutorial

Changing the VMware settings shouldn't cause the problem. If you find yourself trying to solve this again in the future, maybe run "ninja -j1 -v" into a log file, and see if gcc is being invoked with the correct flags: "-march=nehalem -mno-mmx -mno-sse -mno-sse2 -mno-3dnow". These should preve

Re: [seL4] Camkes x86 VM Build Error

Hi Amit, For your first error, installing the pip package enum34 may fix your error which appears to be due to an incompatible Enum library being imported (https://stackoverflow.com/a/1695250) For your second error, if you change into the directory projects/capdl/capDL-tool and run "make" doe

Re: [seL4] Booting seL4test on x86 hardware

Hi Alex, Are you able to make your images available for me to download? Has this worked before for you and has recently stopped working? Do the images work in Qemu (you may have to rebuild with -DSIMULATION=ON)? We do most of our development using PXELINUX with the following configuration:

Re: [seL4] can not build tutorials anymore

Hi, Alternatively, it is also possible that you need to install the python2 package enum34. Kent. From: Mcleod, Kent (Data61, Kensington NSW) Sent: Wednesday, October 24, 2018 11:04 PM To: Thad Seeberger; devel Subject: Re: [seL4] can not build tutorials

Re: [seL4] Camkes x86 VM Build Error

Hi Amit, We added a SIMULATION option to the camkes-vm-examples project today. To update the project with the new changes: repo sync then in the build directory, the following call will reconfigure the build for a simulated target: "cmake -DSIMULATION=ON ." (This requires an already initialised

Re: [seL4] Booting seL4test on x86 hardware

Hi Alex, I downloaded your images and ran them on one of our machines using pxeboot and all of the tests passed. I've attached a log for you. Given that you are constructing valid images, the error must be somewhere in the loading process. I notice that your log mentions loading "rootserver" b

Re: [seL4] Passing Network Resource to Linux VM in TK1-SOM

Hi Daniel, I don't know if this is still an issue for you, but if it is, do these instructions help? https://sel4.systems/pipermail/devel/2017-January/001232.html Setting the config option: Tk1Insecure to True should pass through the correct hardware access. Then "ifconfig eth0 up" should br

[seL4] seL4 10.1.0 and camkes-3.6.0

See an online copy of the release notes at: 10.1.0 2018-11-07: SOURCE COMPATIBLE ## Changes * structures in the boot info are not declared 'packed' - these were previously packed (in

Re: [seL4] Building seL4x86_64 on Debian

Hi Dave, This could be an issue where your python resolves to python3 instead of python2.7. The kernel is supposed to build with either, but it seems that the regression for building with python3 had itself broken and was only using python. For an immediate fix that doesn't involve using do

Re: [seL4] Camkes Cross-VM Communication

Hi Amit, It appears that some part of your configuration tries to use 8192 sized Dataport regions. The tutorial assumes 4096 sized regions. What happens when you try and run the solution version? Calling the following from the top level directory will create a new camkes-vm-crossvm tutorial che

Re: [seL4] CAmkES tutorial build system

Hi, Renaming the source directory and the build directories aren't supported as CMake and Ninja rely on the absolute and relative paths remaining consistent. You are still able to copy the contents of the source directory from the solution into the source directory of the non solution and use