Re: [seL4] CMake Error

Is there a kernel folder in the directory above your build directory, adjacent to the init script that you are calling? Can you instead try running ./init --plat pc99 --tut hello-camkes-2 --solution in the top directory of the project. It will create a build directory for you. >>>  Could not

Re: [seL4] Understanding Camkes Dataport Interface Access Rights

Camkes dataports on seL4 (seL4SharedData connector) are implemented as a shared memory mapping between the two components both pages are mapped to the same underlying frame of physical memory. The access rights are implemented via mapping attributes supported by the architecture. Your reads

Re: [seL4] Is there a "modern" seL4 manifest/configuration that is known to run on CMA34CR?

They were moved to camkes-vm-examples (https://github.com/sel4/camkes-vm-examples). You can checkout and build with the following: repo init -u https://github.com/sel4/camkes-vm-examples-manifest repo sync mkdir build cd build ../init-build.sh

Re: [seL4] CamkES support for waiting on multiple signals

> I could not find any example using seL4NotificationQueue() or > seL4GlobalAsynchCallback().  > I found only the CamkES template.  I don't believe seL4NotificationQueue is currently used anywhere. seL4GlobalAsynchCallback is used with some of the components in the system examples here:

Re: [seL4] sel4 on the Xilinx Zynq US+ ZCU104 Evaluation Kit

> According to this the UARTs are quite different. So the ZCU104 does not run > out of the box and may require (quite) some work. Do you concur? If you look through the flattened device trees for each platform and compare the compatibility string of the UART devices are they different or the

Re: [seL4] camkes error.h include problem

> "../muslibc/include/sys" // necessary for compilation as test_2.c > has "socket.h" This line shouldn't be here, and instead socket.h should be included via . Otherwise many other include directives are going to match on the incorrect files. Kent.

Re: [seL4] Devel Digest, Vol 65, Issue 24

> abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world > loading initial cache file ../settings.cmake > CMake Error: Error: generator : Ninja > Does not match the generator used previously: Unix Makefiles > Either remove the CMakeCache.txt file and CMakeFiles directory or choose a

Re: [seL4] releasing confidentiality

If only considering native components, it would be possible to extend camkes to support the notion of creating a shared data connector between 2 components that is defined by the address space of one end. It could currently be done with a custom connector type that assumed a maximum virtual

Re: [seL4] TLB issue

> since there are no converse suggestions/ideas by anyone, I opened up a > pull request which fixes (according to our TLB flush test) this seL4 > kernel bug on x86 in SMP setups. The patch is used with 9.0.0, however > cleanly applies to latest seL4 release (10.1.1). I can confirm that this fixes

Re: [seL4] Userspace debugging with QEMU/gdb

Does it work if you try using hardware breakpoints? The camkes-vm-linux tutorial uses hardware virtualisation via kvm so the software breakpoints likely won't work. Replacing break with hbreak may fix your issue. From: Devel on behalf of Jiusheng Liu Sent:

Re: [seL4] Fwd: port sel4 to RK3308(quad cortex-a35)

Hi Yun, There currently aren't any cortex-a35 platforms ported to seL4. There aren't any design limitations for this, so a GICv2 quad cortex-a35 platform shouldn't be too difficult to add support for. With regards to overall system delay lower than 3ms, this is going to depend on what other

Re: [seL4] Is there a "modern" seL4 manifest/configuration that is known to run on CMA34CR?

udp_new returning NULL" I'm not sure what you mean by this but it could have been caused by cascading failures from the time server? From: Nogin, Aleksey Sent: Tuesday, 19 November 2019 5:16 PM To: Mcleod, Kent (Data61, Kensington NSW) ; devel@sel4.systems

Re: [seL4] Nasty bug in global-components/templates/rpc-signalling.template.c

We now fixed this in the mainline repositories. Thanks for sharing. From: Devel on behalf of Nogin, Aleksey Sent: Thursday, 21 November 2019 7:52 PM To: devel@sel4.systems Subject: [seL4] Nasty bug in global-components/templates/rpc-signalling.template.c

Re: [seL4] Zynq UltraScale+ locks up after hours running

> I will appreciate any idea/direction for approaching this problem. Are you able to access a hardware debugger? At the point where the cores appear to lock up it's helpful to be able to see where all the threads are and what the hardware state is. Alternatively, are you able simulate your

Re: [seL4] seL4_FailedLookup in vmware

Hi Benjamin, I believe the issue is that this camkes application assumes an iommu but your vmware vm doesn't provide any iommus > ACPI: 0 IOMMUs detected This then likely results in seL4 not creating any iospace caps getting created. When these caps are created the kernel would ordinarily

Re: [seL4] Questions about building Raspberry Pi image on SEL4

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

Re: [seL4] Adding an Extra Component in Camkes

> Can you please suggest a possible solution. > DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES > components/Client1/src/client1.c) > DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES > components/Client2/src/client2.c) > DeclareTutorialsCAmkESComponent(Echo TEMPLATE_SOURCES >

Re: [seL4] (no subject)

> can someone help me here what did i do wrong ,i have been trying to do > camkes-vm-linux and i have followed the instruction  on sel4-tutorials when i > run ninja to build the file i have got an error as below > > and why this happing Hi, It seems that there are incompatible libraries that

Re: [seL4] Beginner ARM_HYP questions

Hi Anton, > I'm trying to understand how hypervisor functionality support is > working in seL4 for aarch32/aarch64. In the documentation there is a > list of platforms [1] for some of them ARM_HYP is said to be supported > for some not. I was trying to grep through the kernel, but it seemed > to

Re: [seL4] devices.camkes: vm#.untyped_mmios: What does the integer after the addresses in this array represent?

Hi Ben, > As stated in the question, I'm not certain about how the integer part of the > elements in the untyped_mmios array in devices.camkes are derived? > "0xF100:24", > "0xF200:25", > "0xF400:26", > "0xF800:24", You are right that the numbers represent the size of the

Re: [seL4] Problem booting camkes arm vmm on TK1 from SD Card

Hi Mike, > You mentioned that "A reason why ELF works for seL4test and not for > camkes-arm-vm is potentially because the Elfloader doesn't get started in > monitor mode and is unable to start the kernel in Hyp mode. " What I don't > understand about that is that I have a couple of images that

Re: [seL4] Problem booting camkes arm vmm on TK1 from SD Card

Hi Mike, Here is a copy of an EFI binary for the camkes-arm-vm tk1 project that runs on our tk1 development board internally: https://cloudstor.aarnet.edu.au/plus/s/FHVMZi0ei1Q6IYA. A reason why ELF works for seL4test and not for camkes-arm-vm is potentially because the Elfloader doesn't get

[seL4] Announcing new releases: seL4-11.0.0, camkes-3.8.0, CapDL-0.1.0,

Announcing the releases of seL4, CAmkES, CapDL and updates of other supporting projects. **Note that this announcement refers to a series of release commits that occurred on 19-Nov-2019.** See below for links to release notes. In addition there are new ways to discuss seL4 and trustworthy

Re: [seL4] Problem booting camkes arm vmm on TK1 from SD Card

Hi Mike, I tried the insecure setting and saw the exact same issue as you. The issue is that the insecure setting would disable access to a region of RAM at 0x4000 that should still be accessible. Re-enabling this device is a 1 line change which I'll put up a PR for soon (see the patch

Re: [seL4] Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b

) ; devel@sel4.systems Cc: Millar, Curtis (Data61, Kensington NSW) ; Mcleod, Kent (Data61, Kensington NSW) Subject: RE: [seL4] Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b Hi Shen, I have managed to confirm that the frequency is 54MHz and the MAX_IRQ is 127. Still

Re: [seL4] Initializing of the sel4 tutorials fails because of missing the CMakeLists.txt

> Hello, > I tried to initialize the simple hello-word example and I get the following > error. Maybe someone has an idea why the CmakeLists is not generated. I believe what you are seeing is caused by this issue: https://github.com/SEL4PROJ/sel4-tutorials/issues/40 The current work-around is to

Re: [seL4] some question about the compile of global-components in camkes_arm_vm project

> I found some example in odroid_vm, > I want to make sure my understanding is correct? > In CMakeLists.txt DeclareCAmkESComponent(HelloWorld) is just tell me there is > a component called “HelloWorld” > If you want this component to be compiled to project > You must add call in your assembly in

Re: [seL4] Error while building in docker

> This morning I saw this error when building sel4: > > /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found > > I noticed a warning when starting the docker container about > trustworthysystems/camkes:latest being over 30 days old. I thought that > using an up to date pull of: > >

Re: [seL4] Using seL4_DebugSnapshot()

> Can someone provide more information about using seL4_DebugSnapshot? > From its description in documentation, I would expect it to print out a > CapDL struct over a debugging port/console. Instead, it waits for user > commands for various data types sends back binary data[0]. > > Since the

Re: [seL4] camkes component consuming two events question.

Hi, > Hi sel4 experts, > > I started playing around with camkes using signals / events , data providers > and connections between 3 different components. > I tried to generate a component that can receive events from two different > endpoints by registering a callback for both endpoints. > >

Re: [seL4] intel-vtd.c::vtd_get_n_paging looks so suspicious

> Hello all, > > kernel/src/plat/pc99/machine/intel-vtd.c::vtd_get_n_paging() confused me a > lot. Wish to get any help. > > This func intends to calculate paging pages needed for all RMRRs. The > following code 'filter the identical regions by pci bus id', and use them to > figure out the final

Re: [seL4] Using sel4.xml/sel4arch.xml to generate custom bindings

> Hello, > > I would like to use the sel4.xml API description files to generate custom > bindings for a prototype language to interact directly with seL4 without > going through libsel4 C API. > > I assume that the structure of these files could change, which I'm willing to > accept, but wanted

Re: [seL4] RPi4: DTS memory device and vm_minimal

Hi Ben, Getting the memory configurations right can become pretty annoying as there are several different ways the memory can be insufficient and given that some of the "Untyped Retype: Insufficient memory" emitted are spurious it can quickly become pretty impossible to debug it all.  (There

Re: [seL4] Failed to find device frame in new verion on my environment

Hi, > a) ‘math(EXPR KernelPaddrUserTop "(1 << 40) - 1")’ > to ‘set(KernelPaddrUserTop "1099511627775")’ This issue looks like it was caused by the `math` statement not setting a correct value for KernelPaddrUserTop. Testing it under different versions of CMake I see KernelPaddrUserTop

Re: [seL4] Best starting point for running VM Linux on a raspberry pi?

Hi Travis, There have been some mailing list threads recently regarding porting the rpi4 to seL4 and the camkes-arm-vm: https://sel4.systems/pipermail/devel/2020-February/002685.html I'm not sure how far Ben has progressed with adding support. We find supporting the RPI harder than some of the

Re: [seL4] TimeServer "IRQ already mapped" error

Hi Grant, > I'm not sure what to make of this error. The only major difference between > my project and the reference above is that I am building atop the > camkes-arm-vm project. Could the VM be interfering here? The interrupt is likely allocated already either because you are using a

Re: [seL4] Trouble booting default cmakes-vm-arm project under QEMU

Hi Travis, > sel4platsupport_copy_irq_cap@device.c:41 > Failed to get cap for irq > irq_register_common@irq.c:316 Failed to > register an IRQ > Assertion failed: (cspace->bitmap[index / BITS_PER_WORD] & > BIT(index

Re: [seL4] TimeServer "IRQ already mapped" error

> I'm surprised that removing the device from the VM didn't seem to have an > adverse effect on its operation. The default configuration for the camkes-arm-vm VM component is to respond to guest faults on hardware device regions that aren't passed through by mapping in a page of memory so that

Re: [seL4] Running cmakes-arm-vm under QEMU.

Hi Travis, There is a README here > that lists the Linux kernel revision and configs and buildroot version and

Re: [seL4] Trouble with the tun/tap interface in linux guest

It could be that the camkes configuration doesn't pass through the PCI device to the Linux guest? You need to add the Interrupts and PCI MMIO configurations below:         vm0.untyped_mmios = [                     "0x804:12", // Interrupt Controller Virtual CPU interface (Virtual Machine

Re: [seL4] Configuring pinmux in am335x (beaglebone) can't be done from user mode

Hi Steve, When we have encountered this in the past we typically do one of the following: - Get an earlier stage boot loader to set up the device. Either uboot, or modifying the ELFLoader to set up a static pinmux configuration during initialization that seL4 and userlevel doesn't need to

Re: [seL4] CAmkES, Virtual Machines and Multicore Guarantees

Hi Ben, Someone else may provide a more complete answer than me, but here is a partial answer that may be sufficient. - The current kernel implementation for multicore uses a single lock for serializing any access to the kernel by different cores. One part of the multicore verification is to

[seL4] Plan to remove support for ARMv6 and KZM/imx31

We are planning on removing support for the KZM ARM11 platform in order to reduce maintenance burden. We are assuming that this is a dead platform and removing support won't affect anyone but it would be useful to know who if anyone is currently using this platform and how much interest there