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

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

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

[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

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

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"

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

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

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

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

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

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

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:

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

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

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

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,

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

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

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

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,

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.

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

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,

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

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

[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

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

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

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:

[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

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

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

[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

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

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

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

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

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

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

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

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

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

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

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

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

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

[seL4] Announcing seL4 5.0.0

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

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

[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

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