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

[Mcleod, Kent (Data61, Kensington NSW)]

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 view)
                    "0x1004:17", // QEMU PCI MMIO
                    "0x3eff:16", // QEMU PCI IO ports
                    "0x4000:29", // Linux kernel memory regions
                    ];
        vm0.dtb_irqs =  [35, 36, 37, 38];


The device should then appear in the guest under eth0.

Kent.


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 the guest just gets to read back what they wrote.  
So often removing a device can still lead to the guest being able to continue 
running. It's helpful to mark the devices as disabled in the device tree that 
the guest sees to prevent Linux from trying to initialize the driver too, but 
sometimes this isn't possible if the device is a platform driver with too many 
other dependencies.

Kent.

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 gets assigned with the correct values.  Has this 
issue kept occurring for you or was it only when you first updated your 
projects to the newer version?

Kent.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 are some pending kernel 
patches that should remove the spurious kernel error messages).
The memory requirements for a VM component in the vm_minimal app configuration 
come from a series of different constraints:
- The Ram device that gets given to the guest needs to be directly mapped if 
the guest has access to any DMA capable devices and there isn't an IOMMU 
available to support a virtual-physical address space.
- The VMM needs enough untyped objects to create all of the additional kernel 
objects required to support creating the guest.  These get used for creating 
threads, paging structures, VCPU objects etc.
- In addition, camkes implicitly allocates the untyped objects required for 
setting up the VMMs address space and backing data for its code and data 
program segments.
- All of these objects are initially allocated by the capdl-loader-app which 
has to be able to allocate everything from the initial untyped objects that the 
kernel provides to it at boot time.
- The kernel creates the initial untypeds based on the static description of 
Ram it has, minus any memory that it uses for its own static memory usage.

So when you try and run an app you can see an allocation failure it could be 
due to: 
- There isn't enough memory available in the system for the ELFLoader to load 
the kernel and user programs into. The system will crash before the kernel even 
has a chance to start.
- The kernel doesn't have enough memory available to create the initial objects 
required to finish initializing it and the first user task (the 
capdl-loader-app).  The kernel init would crash at this point.
- Then when the capdl-loader-app runs, the untypeds that it has been given may 
not be enough to fit all of the objects that it needs to create into.  The 
loader would print an error and crash at this point.
- Then once the camkes VM component starts it might run out of memory while 
trying to setup the VM if it hasn't been configured properly. Or it might not 
have been given the untypeds corresponding to the exact Ram range it requires 
for creating the guest's Ram device.  
- Then once the guest is started, it may run out of Ram while trying to bring 
up Linux.  And then Linux will print its own error message (or everything will 
appear to hang if this occurs before Linux has started writing to a console).

Debugging these failures requires knowing which memory setting to change based 
on what part is failing.
- vm0.simple_untyped24_pool = 12;  is the camkes configuration used to give 12 
* 2^24 Untyped objects to the vm component.  If it is running out of memory 
while trying to setup the VM then increasing this is required.
- vm0.untyped_mmios = ["0x4000:28"]; // RAM is the configuration for giving 
the component the exact region of memory from [0x4000, 0x4000 + 2^28). 
If this can't be given to the component then the capdl-loader-app would print 
an error and stop loading the system.  If this happens, then that means either 
the kernel isn't making the right untypeds available at start up or that some 
other camkes component is trying to use the same memory. If the error is 
because of the first case, then we usually turn to creating a reserved region 
description in the device tree file for that platform so that the kernel 
doesn't use the memory and it is therefore ensured to be in the initial set of 
untypeds passed to memory.
If there is less memory available in the system than what the camkes components 
are requesting, then the above configuration options need to be reduced if 
memory can't be unlocked from elsewhere somehow. On a system with at least 1GiB 
of memory available then it is more common that these options are too low or 
way too high.

I'm not quite sure what you mean about the 1GB highmem issue sorry. Are you 
able to elaborate more?

Kent.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 % BITS_PER_WORD)) == 0 
> (/home/trickdev/cmakes-arm-vm/projects/seL4_libs/libsel4allocman/src/cspace/single_level.c:
> _cspace_single_level_free: 100)

This was an issue recently fixed in this commit: 
https://github.com/SEL4PROJ/camkes-arm-vm/commit/3f2c4bd8cf5483d930af03a6a36d2ccf27e87c09


If you update your sources, the qemu-arm-virt application should be able to 
load Linux.

Kent

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 
camkes-arm-vm configuration that's using a virtual console configuration and an 
instance of the TimeServer alreay exists as a dependency of the SerialServer 
component.
Or as was already suggested, one of the devices being configured as passed 
through to the VM is the same timer device that the TimeServer is trying to 
use.  Which platform are you targeting?

Kent.


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 other platforms that we 
support due to the lack of easily accessible SOC documentation and only the 
RPI4 has started using a compatible Arm GIC interrupt controller with the 
virtualization extensions that seL4 requires.

Have you considered using other common low-cost embedded boards such as the 
odroid-c2?

Kent.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

Hi Travis,

There is a README here 
>
 that lists the Linux kernel revision and configs and buildroot version and 
configs for building a set of Kernel, DTB and userlevel ramdisk used in the 
qemu-arm-virt variant of the camkes-arm-vm project.
If you don't care about building the images yourself, then that repository also 
has the pre-built binaries that camkes-arm-vm will use.  We are planning on 
adding some documentation for common workflows related to working with the Arm 
VMs such as how to provide custom Linux kernel and userlevel variants in the 
near future.

Thanks,
Kent.

From: Devel  on behalf of Travis Wheatley 

Sent: Wednesday, 1 April 2020 7:18 AM
To: devel@sel4.systems 
Subject: [seL4] Running cmakes-arm-vm under QEMU.

Greetings sel4 developers.

Thus far I have successfully been able to build and boot the cmakes-arm-vm 
project on a Jetson TK1 board. However, my project requires a 64 bit target. I 
have built the TX1 version of this project but unfortunately do not have a TX1 
board to try it out on. I would like to be able to run under QEMU but am not 
quite sure how to assemble all of the bits needed to do so. I believe what I 
need is a raw kernel image, a ramdisk, and a dtb file but not sure how to 
extract these in the proper formats from the files produced in the build 
process.

Is there any existing documentation or guidance that can help me get a 64 bit 
buildroot kernel running under an sel4 vm to boot under QEMU?

— Travis


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 is in 
ongoing support.  The platform was the original verification target of seL4 
over 10 years ago and by now there doesn't appear to be any ways to obtain new 
hardware.  It is starting to require more attention as the physical board we 
have is starting to intermittently fail independently from the KZM Qemu 
simulation target.

Currently, the KZM platform is the only ARMv6 platform that we support and 
supporting it requires a few work-arounds for emulating mechanisms that newer 
hardware supports.  Removing this platform also implies removing armv6 support. 

There is an older discourse topic for discussion on this topic here: 
https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-imx31/46

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

Hi Ben,
The kernel requires knowledge of the platform layout at 
configuration/compilation time. My understanding is that on a platform like the 
RPI the RAM available for the CPU is shared with the GPU and while isn't 
statically defined, is still user controlled by a boot config file.  Changes to 
the config file that change the amount of ram available to the kernel would 
require a reconfiguration of the kernel. You can take a look at how this is 
handled for the qemu-arm-virt platform, where the qemu instance can have an 
arbitrary amount of memory: 
https://github.com/seL4/seL4/blob/master/src/plat/qemu-arm-virt/config.cmake#L69.
 The build scripts update the dts based on how much memory is available.  

If you don't want to continuously change the kernel build upon changes to the 
RPI4's memory layout, you could fix a minimum size of memory that the kernel 
has as a memory node in the device tree. Any additional address ranges will 
still get given to userlevel as device untyped memory but will only be able to 
be used as frames and won't be able to be used for kernel objects that the 
kernel writes to, such as CNodes or page tables. Userlevel could then 
dynamically interpret the memory layout based on the supplied device tree and 
still use the memory that the GPU isn't using.

The camkes-arm-vm/camkes also requires knowledge of what RAM will be at 
configuration/compilation time in order to statically allocate memory resources 
also.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 modify.  In these 
scenarios UBoot or the ELFloader already have mechanisms for parsing a device 
tree and doing platform specific initialization.
- Add the initialization to a kernel platform init function.  In some cases 
where a kernel driver such as a timer needs to depend on some additional 
configuration then this is added to the device's platform initialization 
functions.  The am335x platform already has some of this in am335x-timer.c and 
plat/am335x/machine/hardware.c.  This approach is usually used when there is a 
reasonably unambiguous configuration requirement that the kernel has such as 
disabling a reset watchdog timer.
- Pick a different platform that doesn't use additional physical memory 
protection on hardware registers that limits access from unprivileged processor 
modes. This additional limitation that some platforms have is a bit outside of 
seL4's assumptions of what mechanisms in the ISA's system architecture are 
available for it to use.  This is similar to how seL4 can't support platforms 
that don't have a memory management unit.

In your case, adding an initialization model to the kernel or to the elfloader 
would be an option. It would likely be better to target the ELFloader as it's 
where we try and put most platform initialization that the kernel doesn't have 
to be aware of.

Cheers,
Kent.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 incorporate this into the abstract models and 
existing security proofs.  I'm not 100% sure how extensive the changes to the 
abstract model are expected to be, but these changes would likely result in 
changes to the existing implementation to maintain the refinement proofs.
- The implementation of the locking mechanisms for implementing the abstract 
model will likely be incorrect. A big part of the verification effort will be 
ensuring that executing parts of the kernel that happen outside of the lock 
don't update or access shared state incorrectly as this is new behavior that 
doesn't exist in the current verified configurations.
- Additionally, there are additional kernel object invocations to support 
multicore, such as for pinning a thread to a different core, registering 
interrupts on different cores etc.  These are currently unverified under any 
configuration as they don't exist for the existing verified configurations.
Using camkes to statically pin threads to different cores still depends on a 
correct implementation of the above mechanisms and so will require a verified 
multicore kernel to leverage any proof guarantees.

The closest you could get to a multicore system that leverages verified kernel 
configurations would be to setup a multikernel implementation where each core 
had its own instance of a verified seL4 configuration where any hardware 
resources are strictly partitioned between them.  I'm not aware of any examples 
of this setup but there have been research projects that have used multikernel 
implementations of seL4 in the past. Also this still wouldn't give you an 
overall system with the same guarantees as a single seL4 as the different 
instances would need to trust each other to not overwrite each other's kernel 
data structures and is outside of the current proof assumptions.

I hope this answered your questions.

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 result.
> ```
>     for (word_t i = 1; i < rmrr_list->num; i++) {
>     if (vtd_get_root_index(rmrr_list->entries[i].device) !=
>     vtd_get_root_index(filtered.entries[filtered.num - 1].device) &&
>     rmrr_list->entries[i].base != filtered.entries[filtered.num - 
> 1].base &&
>     rmrr_list->entries[i].limit != filtered.entries[filtered.num - 
> 1].limit) {
>     filtered.entries[filtered.num] = rmrr_list->entries[i];
>     filtered.num++;
>     }
>     }
> ```
> But vtd_map_reserved_page() says, every different devices(with diff bus-dev-
> func ID) have their own paging structures. Then why do filter here like this
> , yet the logic looks so confusing.
>
> And on line 313, it counts pages according to the specified level address
> bits.
> ```
>     size += get_n_paging(region, 32 - (VTD_PT_INDEX_BITS * i + 
> seL4_PageBits));
> ```
> So what does 32 mean? Maybe a typo?
>
> Thanks,
> laokz

Hi laokz,

`vtd_get_n_paging()` tries to pre-calculate how many page tables will be needed 
to set up the initial VTD mappings.  The value that it returns gets used to 
preallocate the memory required and then later on in the boot process the page 
tables are allocated using `it_alloc_paging`. Part of the logic in 
vtd_get_n_paging appears to try and calculate how many page tables are required 
for creating the reserved memory mapping regions. As you identify, the logic 
doesn't seem to be correct in several places. Currently, the final result is 
that it overcalculates the amount of page tables required by quite a lot, so 
the consequence for the overall system is some memory gets leaked during boot 
due to the overallocation.  I'm working on a patch and I'll notify you when 
it's up on GitHub.  Thanks for tracking this down!

Kent
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 to know if these files are here to stay in the future?
> I understand also that I will still have to parse libsel4 C headers to 
> recover the full API which I'm fine with too.
>
> Do you see any trouble following this approach or would you recommend 
> something else?

Hi, (sorry for the laggy response).
There is a wish to represent the libsel4 API in a language agnostic format to 
make generating bindings for other languages easier but at the moment it isn't 
being actively worked on.
Currently the parts of the API that are generated from language agnostic 
formats are the invocation and syscall bindings from the *.xml files and some 
data type definitions that are generated from *.bf (bitfield) files.  The 
bitfield language is used to generate bitfield struct access methods in C as 
well as automatically generating some of the Isabelle theory scripts relating 
to the C methods.

In the future, the .xml files could get replaced with a more domain specific 
interface language format but it is likely that that transition would happen 
after more of the C definitions get converted to either .xml or .bf formats 
first.

I'm not sure whether you would want to manually translate all of the non-xml 
definitions or also try and generate them.  The definitions that change the 
most across build configurations are already likely to be in a .xml 
representation as that was the motivation for adding the .xml representation in 
the first place.

As for staying up to date with any changes, this discussion page 
(https://sel4.discourse.group/t/procedural-generation-of-the-sel4-api/24) will 
likely get updated with any changes. Also feel free to weigh in on the 
discussion there too. 


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 untyped mmios being 
created, 0xF100:24 -> [0xF100, 0xF100 + 0x100).
In the example you gave, the four elements are defining a single ram region, 
but because the objects being created are seL4 untypeds that the vmm uses to 
construct the RAM device, there is an seL4 constraint that untyped objects 
can't be larger than their alignment.
So camkes wouldn't be able to create an untyped object defined as: 
"0xF100:27" as this object would only have an alignment of 2^24 and seL4 
would reject the retype invocation.

Hope this answers your question.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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

- seL4 Discourse at , a forum for attempting to 
build up an seL4 knowledge base.
- seL4 Mattermost at  for 
online messaging.
  (Signup link can be found on seL4 
Discourse: 
with a valid account).
- seL4 RFCs at  for open discussion 
about major changes to the seL4 ecosystem.

For more information see: 


Versioned Releases

* seL4 11.0.0: The seL4 microkernel
  
* CAmkES camkes-3.8.0: Component Architecture for microkernel-based Embedded 
Systems
  
* CapDL 0.1.0: Collection of tools for generating, parsing and loading CapDL 
specifications of systems
  

Update notes

* seL4 Buildsystem: System configuration and building using mostly CMake
  
* seL4Test: Test suite for seL4
  
* sel4bench: sel4bench contains benchmarking applications and a support library 
for seL4
  
* user_libs: Userlevel libraries on seL4
  
* The seL4 Run-time: A minimal runtime for running a C or C-compatible process 
in a minimal seL4 environment
  
* Elfloader: For preparing the hardware for seL4 on ARM and RISC-V
  
* seL4 tutorials: Collection of tutorials for learning to use seL4 and its 
ecosystem
  
* camkes-vm: x86 Virtual Machine build as a CAmkES component
  
* camkes-arm-vm: Arm Virtual Machine build as a CAmkES component
  
* seL4webserver: A reference for implementing applications on seL4
  

An seL4 discourse version of this email can be found at:

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

Hi Ben,

There is a tool in kernel/tools called reciprocal.py.  It calculates CLK_MAGIC 
and CLK_SHIFT from an input frequency like so:
```
./reciprocal.py --divisor 5400
magic number is: 5337599559, shift amount is 58
```
With an input frequency of 3125 CLK_MAGIC=5337599559, CLK_SHIFT=58.
KERNEL_WCET is the worst case execution time of a path through the kernel in 
microseconds. Without an actual measurement, most platforms configure this to 
10us.



From: Turner, Ben 
Sent: Thursday, 20 February 2020 8:14 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
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 no luck finding much on KERNEL_WCET, CLK_MAGIC or CLK_SHIFT so far. I’ll 
keep digging but any other tips you can throw my way would be appreciated!



Thanks,



Ben Turner



Follow Us: LinkedIn<http://www.linkedin.com/company/roke-manor-research> | 
Twitter<https://twitter.com/rokemanor> | 
Facebook<https://www.facebook.com/rokemanor>

Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom. Part 
of the Chemring Group. Registered in England & Wales. Registered No: 00267550. 
The information contained in this e-mail and any attachments is proprietary to 
Roke Manor Research Limited and must not be passed to any third party without 
permission. This communication is for information only and shall not create or 
change any contractual relationship.
www.roke.co.uk<http://www.roke.co.uk/?utm_source=Roke&utm_medium=Email&utm_content=Company%20Signature&utm_campaign=Roke>



From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: 20 February 2020 03:55
To: Turner, Ben ; 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 Ben,



You could also read the register CNTFRQ_EL0 
[https://developer.arm.com/docs/ddi0595/b/aarch64-system-registers/cntfrq_el0] 
to double check the value.



As to the max IRQ, you can read it from the GICD_TYPER 
[https://developer.arm.com/docs/ihi0048/b/arm-generic-interrupt-controller-architecture-version-20-architecture-specification].
 The ITLinesNumber field indicates the maximum number of interrupts supported 
by the GIC.



Hope that will help.





Regards,

Yanyan







From: "Turner, Ben" mailto:ben.tur...@roke.co.uk>>
Date: Thursday, 20 February 2020 at 3:06 am
To: "Shen, Yanyan (Data61, Kensington NSW)" 
mailto:yanyan.s...@data61.csiro.au>>, 
"devel@sel4.systems<mailto:devel@sel4.systems>" 
mailto:devel@sel4.systems>>
Cc: "Millar, Curtis (Data61, Kensington NSW)" 
mailto:curtis.mil...@data61.csiro.au>>, "Mcleod, 
Kent (Data61, Kensington NSW)" 
mailto:kent.mcl...@data61.csiro.au>>
Subject: RE: [seL4] Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: 
Raspberry Pi 3b



Hi Shen,



Thanks for the advice. I may have found the TIMER_FREQUENCY (although I’m not 
certain) – the boot log has an entry:



arch_timer: cp15 timer(s) running at 54.00MHz



This is the only possibly relevant timer reference I can find?



I haven’t had any luck with the MAX_IRQ value though. The only value in the 
boot log that could relate is:



NR_IRQS: 16, nr_irqs: 16, preallocated irqs: 16



But 16 seems way lower than I would expect… The value for the RPi3, for 
example, is 127!



Thanks,



Ben Turner



Follow Us: LinkedIn<http://www.linkedin.com/company/roke-manor-research> | 
Twitter<https://twitter.com/rokemanor> | 
Facebook<https://www.facebook.com/rokemanor>

Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom. Part 
of the Chemring Group. Registered in England & Wales. Registered No: 00267550. 
The information contained in this e-mail and any attachments is proprietary to 
Roke Manor Research Limited and must not be passed to any third party without 
permission. This communication is for information only and shall not create or 
change any contractual relationship.
www.roke.co.uk<http://www.roke.co.uk/?utm_source=Roke&utm_medium=Email&utm_content=Company%20Signature&utm_campaign=Roke>


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Beginner ARM_HYP questions

[Mcleod, Kent (Data61, Kensington NSW)]

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 me that ARM_HYP can be enabled on any ARM-based platform.

> I've tried to compile sel4test for exynos5422 (for which ARM_HYP is
> said to be enabled) and odroidc2 (for which it is said that it's not
> supported) with -DARM_HYP=ON manually set, and for both compilation
> succeeded. It failed for hikey, that should support it, but that's a
> different story.

The kernel arm hypervisor support is mostly tied to a particular Arm 
micro-architecture.  Currently CortexA15, CortexA57 or CortexA53 are the 
supported ones. Platforms that use one of these cores will generally be able to 
be configured with hypervisor support enabled. 

> So my questions are
> - How is it defined whether ARM_HYP is supported for a board/SoC,
> provided that processor architecture supports it? What the platform
> support code should provide for hypervisor to work?
> - For platforms not supported by camkes-arm-vm (like, most of the
> platforms) how ARM_HYP can be tested?

We typically only document support for platforms that the camkes-arm-vm 
supports: tk1, tx1, tx2, odroid-xu, odroid-xu4 and qemu-arm-virt.  Other 
platforms, such as imx8 and odroidc2 are theoretically supported by seL4, but 
without the camkes-arm-vm support, we don't test that the hyp support works. 

> Thanks a lot,
> Anton Gerasimov

> [1] https://docs.sel4.systems/Hardware/

Hope this answers your questions.
Kent.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] (no subject)

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 are trying to be built?  
Does the issue still occur if you have a fresh checkout of the tutorials? 
Calling `repo sync` in the project directory may be sufficient to update 
everything, otherwise you would need to reinitialize a new project with `repo 
init`.

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 below). Once I've made this 
change the insecure version boots to login.

project projects/vm/
diff --git a/components/VM/src/modules/plat/tk1/init.c 
b/components/VM/src/modules/plat/tk1/init.c
index dce7809..4bae973 100644
--- a/components/VM/src/modules/plat/tk1/init.c
+++ b/components/VM/src/modules/plat/tk1/init.c
@@ -38,7 +38,6 @@ static const struct device *linux_pt_devices[] = {
 static const struct device *linux_ram_devices[] = {
 #ifndef CONFIG_TK1_INSECURE
 &dev_rtc_kbc_pmc,
-&dev_data_memory,
 &dev_exception_vectors,
 &dev_system_registers,
 &dev_ictlr,
@@ -46,6 +45,7 @@ static const struct device *linux_ram_devices[] = {
 &dev_fuse,
 &dev_gpios,
 #endif /* CONFIG_TK1_INSECURE */
+&dev_data_memory,
 };
 
 extern reboot_hooks_list_t reboot_hooks_list;

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 I built back in 
> August 2018 that still work just fine on this device when I use bootelf to 
> boot them. seL4 starts up and drops to the VM and I can log into the VM. 
Ok.

>  Tegra124 (Jetson TK1) # fatload mmc 1 ${loadaddr} capdl-loader-image-arm-tk1
What is loadaddr set to? Does it fail with loadaddr set to 0x8100?

>Tegra124 (Jetson TK1) # bootelf ${loadaddr}
> ## Starting application at 0x817f ...
When trying to load an ELF with bootelf, I'm not sure what different versions 
of U-Boot do with regards to giving you an error if it unpacks the ELF over the 
top of the ELF.  How does elfloading work with a loadaddr of around 0x8400?

Which Jetson-tk1 board are you using?
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 started in monitor mode and is unable to 
start the kernel in Hyp mode.  Here is some output from our build logs:
U-Boot 2019.04-00592-g6c5f8dd540 (Apr 24 2019 - 12:42:58 +1000)

TEGRA124
Model: NVIDIA Jetson TK1
Board: NVIDIA Jetson TK1
DRAM:  2 GiB
MMC:   sdhci@700b0400: 1, sdhci@700b0600: 0
Loading Environment from MMC... OK
In:serial
Out:   serial
Err:   serial
Net:   No ethernet found.
Hit any key to stop autoboot:  2
 0
Tegra124 (Jetson TK1) # pci enum && setenv autoload no && dhcp && tftpboot 
0x8100 jetson1/sel4-image
pci enum && setenv autoload no && dhcp && tftpboot 0x8100 jetson1/sel4-image

Warning: eth_rtl8169 using MAC address from ROM
BOOTP broadcast 1
BOOTP broadcast 2
BOOTP broadcast 3
DHCP client bound to address 10.13.1.186 (1262 ms)
Using eth_rtl8169 device
TFTP from server 10.13.0.28; our IP address is 10.13.1.186
Filename 'jetson1/sel4-image'.
Load address: 0x8100
Loading: *#
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 #
 ##
 4 MiB/s
done
Bytes transferred = 20762864 (13cd0f0 hex)
Tegra124 (Jetson TK1) # bootelf 0x8100 || bootefi 0x8100
bootelf 0x8100 || bootefi 0x8100
## No elf image at address 0x8100
78MMC: no card present
Scanning disk sd...@700b0400.blk...
Disk sd...@700b0400.blk not ready
Scanning disk sd...@700b0600.blk...
Found 3 disks
WARNING: booting without device tree
## Starting EFI application at 8100 ...
ELF loader: monitor mode init done
Copy monitor mode vector from fb6785bc to a7f0 size 50
Number of IRQs: 192
Load seL4 in nonsecure HYP mode 61da
ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3
  paddr=[fb671000..fca3efff]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at fb7423a4.
Loaded DTB from fb7423a4.
   paddr=[80059000..80069fff]
ELF-loading image 'kernel'
  paddr=[8000..80058fff]
  vaddr=[e000..e0058fff]
  virt_entry=e000
ELF-loading image 'capdl-loader'
  paddr=[8006a000..81442fff]
  vaddr=[1..13e8fff]
  virt_entry=17b1c
relocating from fb671000-fca3f000 to dec3-dfffe000... size=0x13ce000 
(padded size = 0x13d)
ELF loader relocated, continuing boot...
Enabling hypervisor MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
Total 28 IOASID set up
Region [c to 28) for SMMU caps
Booting all finished, dropped to user space
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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.
>
> echo_reg_callback(callback_handler_EchoIn, NULL);
> echo1_reg_callback(callback_handler_EchoOut, NULL);
>
> component Echo
> { 
>     ………...
>     consumes TheEvent echo;
>     consumes TheEvent echo1;  
>     …...
> }
> assembly {
>     composition {
>     ..
>     connection seL4Notification echo_event_in(from producer.echo, to 
> echo.echo);   
>     connection seL4Notification echo_event_out(from consumer.echo1, 
> to echo.echo1);
>     .
>     }
>
> Everything compiles without errors. But, if I start now the simulation I 
> noticed that event .echo1 is never received by the Echo C component.
>
> Also I noticed that the connection seems to be depending on the event name. 
> If I rename the echo event I also miss that event.
>
> So my question: How can I make the second event (echo1) received by the echo 
> C component?

The architecture that you have described should generate the behavior that you 
are expecting.  Having 2 emitters linked up to a single receiver that registers 
2 handlers, 1 for each event type, would experience the handler getting called 
once for each incoming event.  I can't easily see what is causing your issue 
without more source code, but you could maybe try disabling each connection and 
see if you receive each different event individually before enabling them both. 
 


> Thanks for your help.
> Florian

Thanks,
Kent.

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Using seL4_DebugSnapshot()

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 commands are all 0xa0-0xff[1], it doesn't seem like
> DebugSnapshot expects a human and a keyboard to be present on the other
> end. Is there some internal debugging tool that is supposed to be used
> with this system call? Is DebugSnapshot still used? Any advice or
> information is appreciated.
This debug feature isn't currently maintained and not well supported.
There was an internal tool that interacted with DebugSnapshot to translate the 
binary data into a human readable format but hasn't been updated until recently 
and is still not functional enough for release.
At present it is better to assume DebugSnapshot is unsupported sorry.

> ras
>
> [0]
> https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/capdl.c
>
> [1] https://github.com/seL4/seL4/blob/master/include/machine/capdl.h

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 use an older version of CMake than 3.16.0.  You 
can follow that issue for a notification when the underlying problem is fixed.
>  
> ./init --tut hello-world --verbose
> INFO:sh.command: -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world -C 
> ../projects/sel4-tutorials/settings.cmake 
> /home/flo/sel4-tutorials-manifest/hello-world'>: starting process
> DEBUG:sh.command.process: -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world -C 
> ../projects/sel4-tutorials/settings.cmake 
> /home/flo/sel4-tutorials-manifest/hello-world'>. [b'/usr/local/bin/cmake',
>  b'-G', b'Ninja', b'-DTUT_BOARD=pc', b'-DTUT_ARCH=x86_64', 
> b'-DTUTORIAL_DIR=hello-world', b'-C', 
> b'../projects/sel4-tutorials/settings.cmake', 
> b'/home/flo/sel4-tutorials-manifest/hello-world']>: started process
> INFO:sh.command: -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world -C 
> ../projects/sel4-tutorials/settings.cmake 
> /home/flo/sel4-tutorials-manifest/hello-world', pid 4805>: process started
> DEBUG:sh.command.process: -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world -C 
> ../projects/sel4-tutorials/settings.cmake 
> /home/flo/sel4-tutorials-manifest/hello-world'>. [b'/usr/local/bin/cmake',
>  b'-G', b'Ninja', b'-DTUT_BOARD=pc', b'-DTUT_ARCH=x86_64', 
> b'-DTUTORIAL_DIR=hello-world', b'-C', 
> b'../projects/sel4-tutorials/settings.cmake', 
> b'/home/flo/sel4-tutorials-manifest/hello-world']>: acquiring wait lock to 
> wait for completion
> DEBUG:sh.command.process: -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world -C 
> ../projects/sel4-tutorials/settings.cmake 
> /home/flo/sel4-tutorials-manifest/hello-world'>. [b'/usr/local/bin/cmake',
>  b'-G', b'Ninja', b'-DTUT_BOARD=pc', b'-DTUT_ARCH=x86_64', 
> b'-DTUTORIAL_DIR=hello-world', b'-C', 
> b'../projects/sel4-tutorials/settings.cmake', 
> b'/home/flo/sel4-tutorials-manifest/hello-world']>: got wait lock
> DEBUG:sh.command.process: -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world -C 
> ../projects/sel4-tutorials/settings.cmake 
> /home/flo/sel4-tutorials-manifest/hello-world'>. [b'/usr/local/bin/cmake',
>  b'-G', b'Ninja', b'-DTUT_BOARD=pc', b'-DTUT_ARCH=x86_64', 
> b'-DTUTORIAL_DIR=hello-world', b'-C', 
> b'../projects/sel4-tutorials/settings.cmake', 
> b'/home/flo/sel4-tutorials-manifest/hello-world']>: exit code not set, 
> waiting on pid
> loading initial cache file ../projects/sel4-tutorials/settings.cmake
> -- Found capdl: /home/flo/sel4-tutorials-manifest/projects/capdl  
> -- Found camkes-tool: 
> /home/flo/sel4-tutorials-manifest/projects/sel4-tutorials  
> CMake Error: The source directory 
> "/home/flo/sel4-tutorials-manifest/hello-world" does not appear to contain 
> CMakeLists.txt.
> Specify --help for usage, or press the help button on the CMake GUI.
> Traceback (most recent call last):
>   File "./init", line 96, in 
>   File "./init", line 85, in main
>   File "/home/flo/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", 
> line 106, in init_directories
> return _init_build_directory(config, initialised, build_directory, 
> tute_directory, output, config_dict=config_dict)
>   File "/home/flo/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", 
> line 74, in _init_build_directory
> return sh.cmake(args + [tute_directory], _cwd=directory, _out=output, 
> _err=output)
>   File "/usr/local/lib/python3.6/dist-packages/sh.py", line 1427, in __call__
> return RunningCommand(cmd, call_args, stdin, stdout, stderr)
>   File "/usr/local/lib/python3.6/dist-packages/sh.py", line 774, in __init__
> self.wait()
>   File "/usr/local/lib/python3.6/dist-packages/sh.py", line 792, in wait
> self.handle_command_exit_code(exit_code)
>   File "/usr/local/lib/python3.6/dist-packages/sh.py", line 815, in 
> handle_command_exit_code
> raise exc
> sh.ErrorReturnCode_1:
>   RAN: /usr/local/bin/cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 
> -DTUTORIAL_DIR=hello-world -C ../projects/sel4-tutorials/settings.cmake 
> /home/flo/sel4-tutorials-manifest/hello-world
>   STDOUT:
>   STDERR:
>  
> Thanks and Regards
> Florian

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 .cmakes file like below:

Correct.  Camkes builds a different binary for each component instance.  
DeclareCAmkESComponent(HelloWorld) declares a component type HelloWorld, but 
because each instance of a HelloWorld component could have different 
connections or configuration there is a separate binary built for each one.  
Therefore if a component instance doesn't exist for a component type then 
nothing for that component will be built.

>     assembly {
>      composition {
>     component HelloWorld hello;

>          }
>       
> Thank you very much
 
> hi，
> I have some question about the compile of global-components in camkes_arm_vm 
> project.
> 1、In projects/global-components/components, there are some directory include 
> FileServer, SerialServer, TimeServer and the others.
>    I found FileServer had been compiled to project， but the other directory 
>have not been compiled
>    Is there some on-off switch control the compile
？ But I did not find it.
> 2、The CAmkES of FileServer component did not have a "int run(void) {},

>  If I want to add an new component with run entry， but it is not 
>rootserver（I think one
 project only have one rootserver），it run with vm rootserver parallelly？
> what should I do ？ Is there some example.
>   
> Thank you very much

Try looking at the sample serialserver camkes app 
(https://github.com/seL4/camkes/blob/master/apps/serialserver/serialserver.camkes)
 for a project that uses the SertialServer and TimeServer components.  
Alternatively the vm_serial_server app 
(https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/apps/vm_serial_server/vm_serial_server.camkes)
 in the camkes_arm_vm project uses all of the components you listed.



___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Error while building in docker

[Mcleod, Kent (Data61, Kensington NSW)]

> 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:
>
> https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git
>
> would keep the build env up to date but that apparently is either not
> the case or there is a problem with the repo.
>
> I ran:
>
> docker pull trustworthysystems/camkes
>
> and the warning was resolved and I could build seL4. Is pulling that
> docker image supposed to be necessary?

I believe so.  Looking at the documentation in the README and how the Makefile 
is implemented, the first time you run `make user` docker will pull a version 
of trustworthysystems/camkes and then build the extras.dockerfile using 
trustworthysystems/camkes as a base.  Future calls to make user will rebuild 
extras.dockerfile, but will use the existing trustworthysystems/camkes image 
from before.  I'm guessing the intention was to require explicit updates of 
trustworthysystems/camkes due to the large image sizes and the warning is there 
to alert any potential issues of staleness.  I'm not experienced enough with 
docker to know if there is an easy way to detect that the 
trustworthysystems/camkes image is stale based on the source dockerfiles in the 
repository without requiring a full build of trustworthysystems/camkes the 
first time `make user` is run.

>
> Thanks!

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Userspace debugging with QEMU/gdb

[Mcleod, Kent (Data61, Kensington NSW)]

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: Wednesday, 27 November 2019 1:51 PM
To: devel@sel4.systems 
Subject: [seL4] Userspace debugging with QEMU/gdb

Hi,

>From the page https://docs.sel4.systems/DebuggingGuide.html (section Userspace 
>debugging), I know we can debug userspace process by command below:

 cmd example start 

gdb ./dynamic-2
Reading symbols from ./dynamic-2...done.
(gdb) target remote :1234
Remote debugging using :1234
0xfff0 in ?? ()
(gdb) break main
Breakpoint 1 at 0x402011: file sel4-tutorials-manifest/dynamic-2/main.c, line 
161.
(gdb) c
Continuing.

Breakpoint 1, main () at sel4-tutorials-manifest/dynamic-2/main.c:161
161
(gdb)
 cmd example end  


It works for normal userspace process (such as the example code in tutorials:  
https://docs.sel4.systems/Tutorials/dynamic-2.html ).

But when I want to debug the userspace process for the code in the tutorials 
page https://docs.sel4.systems/Tutorials/camkes-vm-linux.html (one virtual 
machine in seL4), I cannot catch the breakpoints.

So can you help me to explain why I cannot catch the breakpoint? and can we 
debug the vmm create process with qemu/gdb?

Thanks.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 user level components you use to build your system.  Costs for 
performing inter-process communication and context switching are measured in 
orders of hundreds (or thousands) of cycles, but the overall cost for 
processing audio in a system will depend on how the final system is architected.

From: Devel  on behalf of Yun Zhou 

Sent: Saturday, 26 October 2019 1:35 PM
To: devel@sel4.systems 
Subject: [seL4] Fwd: port sel4 to RK3308(quad cortex-a35)



-- Forwarded message -
发件人： Yun Zhou mailto:shiny725...@gmail.com>>
Date: 2019年10月25日周五 下午9:52
Subject: port sel4 to RK3308(quad cortex-a35)
To: 


Dear sel4 Experts
  How are you
 I found some information about sel4, and sel4 is great microkernel OS, i want 
port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal 
processing. Form the Tutorials I found sel4 just support cortex-a53, I would 
like to ask does sel4 support cortex-a35 SMP mode. and because our application 
is real time audio processing so system delay must lower than 3ms and hard 
real-time determinism.
Will sel4 support real-time signal processing?
Looking forward to your reply

Thanks &Kind regards
Yun


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

The CAMKES_VM_APP=cma34cr_centos configuration still works in the mainline 
repositories.
I went through and altered some of the error messaging to only warn in 
situations where the errors are expected.
For other outputs:

IOMMU: DMA read page fault from 0xd0 (bus: 0x0/dev: 0x1a/fun: 0x0) on address 
0x0:aae16000 with reason code 0x6

This occurs sometimes when devices try to access memory but don't have access 
via the IOMMU. They are spurious and the kernel prints the faults for 
diagnostic reasons, but don't indicate any errors unless a driver is trying to 
communicate with the device at the same time.

acpi_init@acpi.c:386 Failed to find rsdp



hpet_parse_acpi@hpet.c:274 arguments cannot be NULL

sel4platsupport_get_num_pmem_regions@pmem.c:23 Could not find info

The acpi, hpet and pmem errors are all paths where the caller is able to handle 
failures so I downgraded these messages to warnings for now.

FAULT HANDLER: user exception (number 13, code 0) from 
time_server.time_server_0_control (ID 0x2), pc = 0x423a47, sp = 0x453cf0, flags 
= 0x10202

This is a legitimate error, which you tracked down to be the lexicographical 
ordering bug.

> "because of lwip’s 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 
Subject: RE: Is there a "modern" seL4 manifest/configuration that is known to 
run on CMA34CR?


With a recent version of everything, I get the following on startup of the 
“CAMKES_VM_APP=cma34cr_centos”(*) build



…

Booting all finished, dropped to user space

IOMMU: DMA read page fault from 0xd0 (bus: 0x0/dev: 0x1a/fun: 0x0) on address 
0x0:aae16000 with reason code 0x6

acpi_init@acpi.c:386 Failed to find rsdp



hpet_parse_acpi@hpet.c:274 arguments cannot be NULL

sel4platsupport_get_num_pmem_regions@pmem.c:23 Could not find info

…



Does this indicate problems that I should worry about? The reason for my 
question is that in porting some simple code (without any VMs) that worked fine 
on the 32-bit seL4 from ~2 years ago to a more recent version of everything, I 
get the following on startup:



Booting all finished, dropped to user space

IOMMU: DMA read page fault from 0xd0 (bus: 0x0/dev: 0x1a/fun: 0x0) on address 
0x0:aae16000 with reason code 0x6

acpi_init@acpi.c:386 Failed to find rsdp



hpet_parse_acpi@hpet.c:274 arguments cannot be NULL

FAULT HANDLER: user exception (number 13, code 0) from 
time_server.time_server_0_control (ID 0x2), pc = 0x423a47, sp = 0x453cf0, flags 
= 0x10202



followed by some of my components failing to initialize correctly because of 
lwip’s udp_new returning NULL, and something else also spewing two copies of 
“sel4platsupport_get_num_pmem_regions@pmem.c:23 Could not find info” message…



I will try to figure this out myself, but would appreciate any pointers. Thanks!



(*) I am running on a CMA34CR + CAN board, so some of the HW parameters might 
be slightly different from the version of the HW we all used in the previous 
projects. I’ve updated HW parameters in the cma34cr_centos.camkes accordingly, 
but may have missed something.



Aleksey



From: Mcleod, Kent (Data61, Kensington NSW) 
Sent: Friday, August 16, 2019 3:56 PM
To: Nogin, Aleksey ; devel@sel4.systems
Subject: Re: 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<https://protect2.fireeye.com/url?k=ba944cfd-e60e3618-ba97b6f5-861cd9c308db-6186e0c9cb6b06be&q=1&u=https%3A%2F%2Fgithub.com%2Fsel4%2Fcamkes-vm-examples>).
  You can checkout and build with the following:

repo init -u 
https://github.com/sel4/camkes-vm-examples-manifest<https://protect2.fireeye.com/url?k=0311632d-5f8b19c8-03129925-861cd9c308db-8f2f8fe5de1fe3e7&q=1&u=https%3A%2F%2Fgithub.com%2Fsel4%2Fcamkes-vm-examples-manifest>

repo sync

mkdir build

cd build

../init-build.sh -DCAMKES_VM_APP=cma34cr_centos

ninja







From: Devel mailto:devel-bounces@sel4.systems>> on 
behalf of Nogin, Aleksey mailto:ano...@hrl.com>>
Sent: Saturday, 17 August 2019 8:25 AM
To: devel@sel4.systems<mailto:devel@sel4.systems> 
mailto:devel@sel4.systems>>
Subject: [seL4] Is there a "modern" seL4 manifest/configuration that is known 
to run on CMA34CR?



Unless I am looking in the wrong place, all the CMA34CR support was removed in 
https://github.com/seL4/camkes-vm/commit/aab3478acc4705a3161f5bf59625f7c96a801544<https://protect2.fireeye.com/url?k=66b8fd91-3a228774-66bb0799-861cd9c308db-80a54263f32b72ed&q=1&u=https%3A%2F%2Fgithub.com%2FseL4%2Fcamkes-vm%2Fcommit%2Faab3478acc4705a3161f5bf59625f7c96a801544>.
 Is there something that re

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

[Mcleod, Kent (Data61, Kensington NSW)]

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


After spending a few hours debugging time server not working for me, I realized 
that global-components/templates/rpc-signalling.template.c that was added 
earlier this year contains the following



/*- set badge = str(configuration[c.instance.name].get("%s_attributes" % 
c.interface.name)).strip('"') -*/

[…]

/*- do badges.sort() -*/

[…]

int /*? me.interface.name ?*/_largest_badge(void) {

   return /*? badges[len(badges) - 1] ?*/;

}



Unfortunately for me, my Trusted Build generated camkes had the attributes 
numbered 1,2,3,10,11,12,13 and therefore the above core was claiming that the 
time_server_largest_badge is 3 :(. Obviously, the issue is the combination of 
the str and sort, resulting in the last badge being the one largest 
lexicographically, not numerically :(. Replacing the str with int (and 
correspondingly removing the strip) solved the problem for me.



P.S. Well, solved that particular problem for me, not the problem of time 
server not working – looks like now I will have to debug



FAULT HANDLER: data fault from time_server.time_server_0_control (ID 0x2) on 
address 0x84b8ba, pc = 0x42439d, fsr = 0x4

FAULT HANDLER: Register dump:

FAULT HANDLER: rip  :0x42439d

FAULT HANDLER: rsp  :0x454cf0

FAULT HANDLER: rflags   :0x10202

FAULT HANDLER: rax  :0x413a33

FAULT HANDLER: rbx  :0x437e88

FAULT HANDLER: rcx  :0x0

FAULT HANDLER: rdx  :0x437e98

FAULT HANDLER: rsi  :0x28

FAULT HANDLER: rdi  :0x437e98

FAULT HANDLER: rbp  :0x454d70

FAULT HANDLER: r8   :0x

FAULT HANDLER: r9   :0x0

FAULT HANDLER: r10  :0xe8

FAULT HANDLER: r11  :0x293

FAULT HANDLER: r12  :0x413a32

FAULT HANDLER: r13  :0x84b8ba

FAULT HANDLER: r14  :0x0

FAULT HANDLER: r15  :0x0

FAULT HANDLER: fs_base  :0x44a460

FAULT HANDLER: gs_base  :0x0

FAULT HANDLER:   memory map:

FAULT HANDLER: +-- 0x00458fff --

FAULT HANDLER: |   guard page

FAULT HANDLER: +-- 0x00458000 --

FAULT HANDLER: |   IPC buffer

FAULT HANDLER: +-- 0x00457000 --

FAULT HANDLER: |   guard page

FAULT HANDLER: +-- 0x00456000 --

FAULT HANDLER: |   guard page

FAULT HANDLER: +-- 0x00455000 --

FAULT HANDLER: |   stack

FAULT HANDLER: +-- 0x00451000 --

FAULT HANDLER: |   guard page

FAULT HANDLER: +-- 0x0045 --

FAULT HANDLER: |   code and data

FAULT HANDLER: +-- 0x0040 –



:(



Aleksey

CONFIDENTIALITY NOTICE: The information transmitted in this email, including 
attachments, is intended only for the person(s) or entity to which it is 
addressed and may contain confidential, proprietary and/or privileged material 
exempt from disclosure under applicable law. Any review, retransmission, 
dissemination or other use of, or taking of any action in reliance upon this 
information by persons or entities other than the intended recipient is 
prohibited. If you received this message in error, please contact the sender 
immediately and destroy any copies of this information in their entirety.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] releasing confidentiality

[Mcleod, Kent (Data61, Kensington NSW)]

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 address of the 
target component I believe, but adding specific support into camkes would 
likely allow specifying the elf program segments as something a shared 
connector could be connected to.

But because camkes is a static system where you can specify that the monitor 
component has read only access to the other native component.

For native Linux processes in a vm, you would probably need to trust modules 
inside the vmm and the Linux kernel to describe where the process's address 
space ends up in memory in order to scan it.

From: Devel  on behalf of Heiser, Gernot (Data61, 
Kensington NSW) 
Sent: Saturday, 26 October 2019 2:07:23 PM
To: devel@sel4.systems 
Subject: Re: [seL4] releasing confidentiality

On 26 Oct 2019, at 08:00, Michael Neises  wrote:
>
> Hi,
>
> I know that seL4 provides confidentiality, which is described as a property 
> that "means that data cannot be read without permission." Given this wording, 
> I wonder if it is not possible to revoke those permissions in certain cases. 
> In particular, I would like for one camkes component to be able to perform 
> runtime measurements, such as heap analysis, on another component. Or even 
> better, I would like for a component to be able to perform runtime 
> measurements on a program running within the camkes linux vm. Is such a feat 
> possible?

Hi Michael

seL4’s confidentiality (and other security) enforcement means that the kernel 
guarantees that you can only access objects to which you have been given 
explicit permission (in the form of a capability). How those permissions are 
allocated is a matter of policy, the kernel doesn’t care, it only enforces.

In particular, it is totally possible in seL4 to give one component access to 
another component’s address space, that’s for the user-level policy framework 
to decide.

Whether the present CAmkES framework supports this is a different question, 
which I’ll leave to someone who’s more up to date with CAmkES details.

Gernot

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] TLB issue

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 the issue that was reported.
This has now been merged in https://github.com/seL4/seL4/pull/107. 

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 
> different binary directory.

These errors indicate that CMake already believes a project has been created in 
the target directory and that this project was a Makefile based project.  Is 
there any CMakeCache.txt files located anywhere in the project structure that 
may be causing CMake to get confused? Otherwise you could reinitialise the 
tutorial project and try initialising hello-world again and that would also fix 
your problem.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Sel4 for quadcore riscv64imafd

[Mcleod, Kent (Data61, Kensington NSW)]

> I want to build sel4 for  quadcore riscv64imafd and run the test programs, 
> how to do that? 
Unfortunately only single core riscv64imac is supported at this time.

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] seL4_FailedLookup in vmware

[Mcleod, Kent (Data61, Kensington NSW)]

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 print something like: 
IOMMU 0x0: 8-bit domain IDs supported
IOMMU: Using 4 page-table levels (max. supported: 4)
IOMMU: Create VTD context table for PCI bus 0x0 (pptr=0xff841a6cc000)
IOMMU: Create VTD context table for PCI bus 0x1 (pptr=0xff841a6d9000)
IOMMU: Create VTD context table for PCI bus 0x2 (pptr=0xff841a6da000)
IOMMU: Create VTD context table for PCI bus 0x3 (pptr=0xff841a6db000)
As the caps aren't created, this is what is likely causing the failed lookup 
error.
I'm not familiar with vmware workstation, but maybe this is something that can 
be enabled for the guest.


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Initialising Camkes App before another dependent Camkes app

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 ?
Explicitly ordering components via signalling connectors is currently the main 
way for ordering component startups.  We've considered adding better built in 
support for this in the past but it isn't currently on our upcoming roadmap. 
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Adding an Extra Component in Camkes

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 
> components/Echo/src/echo.c)
It seems that the second call to DeclareTutorialsCAmkESComponent should name 
the component Client2.

Also these seem to be really old sources for the tutorials.  It may be easier 
to extend an application from the camkes sample project 
(https://github.com/seL4/camkes/tree/master/apps/adder) which can be 
initialised via:
repo init -u https://github.com/seL4/camkes-manifest.git
repo sync
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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:
A simulation target isn't supported. If someone knows how to convince the qemu 
rpi3 platform to accept an aarch32 kernel then this could change.
If you have already run a sel4test image on hardware, then following the same 
procedure for camkes should also work.
../init-build.sh -DPLATFORM=rpi3 -DCAMKES_APP=adder -DAARCH32=ON
ninja
And then when loading on hardware I get the following: 
U-Boot> setenv autoload no && dhcp && tftpboot 0x1000 rpi3/sel4-image
setenv autoload no && dhcp && tftpboot 0x1000 rpi3/sel4-image
Waiting for Ethernet connection... done.
BOOTP broadcast 1
BOOTP broadcast 2
BOOTP broadcast 3
DHCP client bound to address 10.13.1.66 (1005 ms)
Waiting for Ethernet connection... done.
Using sms0 device
TFTP from server 10.13.0.28; our IP address is 10.13.1.66
Filename 'rpi3/sel4-image'.
Load address: 0x1000
Loading: #
 #
 ###
 3.1 MiB/s
done
Bytes transferred = 2588852 (2780b4 hex)
U-Boot> bootelf
bootelf
## Starting application at 0x015a6000 ...

ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
  paddr=[15a6000..1826037]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 16a4760.
Loaded DTB from 16a4760.
   paddr=[1037000..103afff]
ELF-loading image 'kernel'
  paddr=[100..1036fff]
  vaddr=[e000..e0036fff]
  virt_entry=e000
ELF-loading image 'capdl-loader'
  paddr=[103b000..11b3fff]
  vaddr=[1..188fff]
  virt_entry=18674
ELF loader relocated, continuing boot...
Enabling MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
Booting all finished, dropped to user space
client: what's the answer to 342 + 74 + 283 + 37 + 534 ?
adder: Adding 342
adder: Adding 74
adder: Adding 283
adder: Adding 37
adder: Adding 534
client: result was 1270

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 application 
with the zcu102 qemu platform?
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

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 -DCAMKES_VM_APP=cma34cr_centos
ninja



From: Devel  on behalf of Nogin, Aleksey 

Sent: Saturday, 17 August 2019 8:25 AM
To: devel@sel4.systems 
Subject: [seL4] Is there a "modern" seL4 manifest/configuration that is known 
to run on CMA34CR?


Unless I am looking in the wrong place, all the CMA34CR support was removed in 
https://github.com/seL4/camkes-vm/commit/aab3478acc4705a3161f5bf59625f7c96a801544.
 Is there something that remains? If not, what would be the best starting point 
to try to port a demo running on CMA34CR board from an old (early 2017) version 
of the sel4/camkes/etc to a recent stable release (e.g, 10.1.1)?



Thanks.



Aleksey

CONFIDENTIALITY NOTICE: The information transmitted in this email, including 
attachments, is intended only for the person(s) or entity to which it is 
addressed and may contain confidential, proprietary and/or privileged material 
exempt from disclosure under applicable law. Any review, retransmission, 
dissemination or other use of, or taking of any action in reliance upon this 
information by persons or entities other than the intended recipient is 
prohibited. If you received this message in error, please contact the sender 
immediately and destroy any copies of this information in their entirety.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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 same?  
You could try swapping out the zcu102's device tree with the zcu104's when 
building seL4 and see what happens.

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Mcleod, Kent (Data61, Kensington NSW)]

> 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: https://github.com/seL4/camkes-vm-examples
> Is there any tutorial on usage of these custom connectors that you have ?
You could look at the camkes picotcp example 
(https://github.com/seL4/camkes/blob/master/apps/picoserver/picoserver.camkes#L75)
 to see how seL4GlobalAsynchCallback is used to get multiple signals on a 
single thread.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Understanding Camkes Dataport Interface Access Rights

[Mcleod, Kent (Data61, Kensington NSW)]

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 and writes through 
your dataport pointers are acting on this shared memory directly.  The fault is 
generated by a hardware exception that seL4 handles by creating a fault and 
sending it to a registered fault handler (sendFaultIPC is the function in the 
kernel).  There is a setting (that is enabled by default) that causes each 
Camkes component to set up a fault handler for all of its threads.  If any of 
these threads cause a fault, such as by writing to read only memory, the fault 
handler will receive a message from the kernel.

These mapping attributes are set when the kernel creates the page 
mapping for each component using the relevant Map invocation [1].  The result 
of building a Camkes system for seL4 is a system spec that contains all of the 
seL4 kernel objects and capabilities described by the system.  Within this 
spec, dataports are described as a capability to physical memory where each 
capability has the specified access rights.  When the system initialiser 
(capdl-loader-app in our case) is started by seL4 as the root task, it 
constructs the system following the spec and starts each Camkes component. By 
this point, the seL4 invocations for setting up the shared data page mappings 
have been performed.
You can look through the generated spec in the build directory by finding the 
file with the .cdl extension.  If you search for the name of the dataport you 
can find the capabilities and objects to validate that the rights are as you 
would expect.

Hope this answers your questions.

@Matthew: Write only mappings are still coerced by the capdl-loader to read 
write mappings before calling the mapping invocation.

[1] https://docs.sel4.systems/ApiDoc.html#map-4
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] CMake Error

[Mcleod, Kent (Data61, Kensington NSW)]

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 find toolchain file: ../kernel/gcc.cmake
>>> Call Stack (most recent call first):
>>>  CMakeLists.txt
>>>
>>>
>>> CMake Error: CMake was unable to find a build program corresponding
>>> to "Ninja".  CMAKE_MAKE_PROGRAM is not set.  You probably need to
>>> select a different build tool.
>>> CMake Error: CMAKE_C_COMPILER not set, after EnableLanguage
>>> CMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguage


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] camkes error.h include problem

[Mcleod, Kent (Data61, Kensington NSW)]

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

From: Devel  on behalf of Chubb, Peter (Data61, 
Kensington NSW) 
Sent: Friday, 14 June 2019 8:03 AM
To: yogidk .
Cc: devel@sel4.systems
Subject: Re: [seL4] camkes error.h include problem

> "yogidk" == yogidk   writes:

yogidk> and another file

yogidk> test_2.c which includes "socket.h"

yogidk> DeclareCAmkESComponent(test
yogidk>INCLUDES "../muslibc/include/sys"*  // necessary for
yogidk>compilation as test_2.c has "socket.h"*

This line means that "#include " picks up sys/errno.h instead
of errno.h.

Get rid of it.  Instead, do '#include  instead of
'#include '

Peter C
--
Dr Peter Chubb Tel: +61 2 9490 5852  http://ts.data61.csiro.au/
Trustworthy Systems Group Data61, CSIRO (formerly NICTA)
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel