- Devel - lists.sel4.systems

Thank you very much. 答复: question about stash and pop between templates
by yadong.li 23 Mar '20

23 Mar '20

-----邮件原件----- 发件人: Matthew Fernandez [mailto:matthew.fernandez@gmail.com] 发送时间: 2020年3月22日 2:00 收件人: yadong.li 抄送: devel(a)sel4.systems 主题: Re: [seL4] question about stash and pop between templates I think I wrote the text you’re quoting, so I’ll attempt an answer. In connection templates, ‘me’ is not unique. I can’t remember exactly how this works, but ‘me’ either refers to the component instance of the end of the template you’re instantiating or to the connection itself. If you want to try and unravel the relevant code, it’s around lines 278-300 of the main function [0]. The ‘stash’ and ‘pop’ functions were implemented to expose some internals to advanced CAmkES users who wanted functionality beyond the template API. They were not widely used, and many of these users sidestepped them and used the even more questionable ‘_stash’ and ‘_pop’ variants. I would not be surprised if they do not work the way the documentation describes, and they should mostly be considered foot guns at this point. This is based on my ~5 year old memories so may be inaccurate or out of date. HTH [0]: https://github.com/seL4/camkes-tool/blob/master/camkes/runner/__main__.py#L… > On Mar 20, 2020, at 22:56, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi， > Recently, I try to learning about CMAKES > I have some question about stash and pop described as followes: > > “ > Passing Information Between Templates > You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” > What is the meaning of “between templates that share related me references.” ? > It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: > connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from > ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ > where can I found the code to share related ‘me’ between the instance. > > Thanks for your answer _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

question about stash and pop between templates
by yadong.li 22 Mar '20

22 Mar '20

Hi， Recently, I try to learning about CMAKES I have some question about stash and pop described as followes: “ Passing Information Between Templates You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” What is the meaning of “between templates that share related me references.” ? It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ where can I found the code to share related ‘me’ between the instance. Thanks for your answer

2 1

Plan to remove support for ARMv6 and KZM/imx31
by Mcleod, Kent (Data61, Kensington NSW) 20 Mar '20

20 Mar '20

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

1 0

Would verifying ARM64 be any more difficult than verifying ARM32 was?
by Demi M. Obenour 19 Mar '20

19 Mar '20

Would verifying seL4 on ARM64 be any more difficult than verifying seL4 on ARM32 was? What about other architectures like POWER9? I hope I am not asking too many questions; I am just a curious outsider who hopes they can use seL4 someday. Sincerely, Demi

4 3

CAmkES, Virtual Machines and Multicore Guarantees
by Turner, Ben 18 Mar '20

18 Mar '20

Hi, In the seL4 FAQ section it states: "Multicore is presently supported on x64 and Arm v7 (32-bit) and v8 (64-bit). Verification of the multicore kernel is in progress (but presently as an unfunded background activity)." Considering only seL4 ----------------------------- My interpretation of this is that given a single seL4 application running on a device, it is not possible to currently guarantee the protections seL4 provides if the application invokes multiple threads across more than 1 core. Is this correct? Considering CAmkES ---------------------------- I would also like to know how CAmkES affects this. For example, looking at the vm_multi app for the exynos5422 in the camkes-arm-vm repository, what would the effect be of assigning unique CPU affinities to each of the VM components? Do the guarantees still hold in this situation? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ 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. ________________________________________

5 4

Configuring pinmux in am335x (beaglebone) can't be done from user mode
by Stephen Sherratt 18 Mar '20

18 Mar '20

Hi all, I've been experimenting with seL4 running on a Ninjablocks (https://www.engadget.com/2013/05/01/ninja-blocks/) that I had lying around. Inside there is a beaglebone, with a custom shield (or cape) containing a microcontroller (atmega328p), some LEDs and a radio. The beaglebone (which normally runs linux) sends json-encoded commands over a serial connection to the on-cape microcontroller, which runs firmware that decodes these commands and controls the LEDs and radio. The complication is that the am335x pins connected to the custom shield are multiplexed, and don't connect to a uart device by default (they are gpio pins by default). The "Control Module" in the am335x can be used to configure pin multiplexing, but it can't be written to in user-mode. From the am335x manual (http://www.ti.com/lit/ug/spruh73q/spruh73q.pdf, page 1449): "Note: For writingto the controlmoduleregisters,the MPUwill need to be in privileged modeof operationand writes will not work fromusermode." To test that the rest of my app works I added the control module to the beaglebone device tree overlay and hacked the kernel to configure the relevant pins to connect to the uart device during boot: https://github.com/stevebob/seL4/commit/4295035ac7fd720fb531b7e0893f1f1191e… And now I have a little rootserver that can control the colours of LEDs on the shield: https://github.com/stevebob/sel4ninja/blob/master/apps/hello-ninja/src/main… What would be the right way of configuring the control module in a seL4-based system, given that it has to happen in kernel mode? To configure the uart pins when running linux on the board, I had to add the following to the device tree: scm@0 { ... pinmux@800 { ... pinmux_uart0_pins { // <-- this was already here pinctrl-single,pins = <0x170 0x30 0x174 0x00>; phandle = <0x20>; }; pinmux_uart1_pins { // <-- I had to add this pinctrl-single,pins = <0x180 0x30 0x184 0x00>; phandle = <0x60>; }; The (seL4) kernel build system already has basic support for interpreting device trees. Would a reasonable solution to my problem be extending this support with a minimal statically-generated control module driver that configures pinmux during boot based on the device tree? There would still be a problem where each board could only have a single pinmux config (as specified by that board's device tree). It seems like an easy fix for this would be a config variable passed to the build system (similar to -DPLATFORM) that overrides the default device tree file. That way projects that want non-standard pinmux configs could bring their own device trees. Cheers, Steve

2 1

seL4 design principles
by Heiser, Gernot (Data61, Kensington NSW) 15 Mar '20

15 Mar '20

I’ve just posted a blog that tries to explain why de do things the way we de in seL4, and why we don’t do some other things, such as hardware abstraction. I hope this helps people understand better which kind of kernel changes are acceptable and which aren’t, and why the API isn’t designed for ease of use. https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/ Gernot

3 4

intel-vtd.c::vtd_get_n_paging looks so suspicious
by laokz 15 Mar '20

15 Mar '20

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

2 2

Using sel4.xml/sel4arch.xml to generate custom bindings
by Alexandre Mutel 12 Mar '20

12 Mar '20

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?

2 1

May be an error in "alloc_free_io_port_range" of projects/seL4_projects_libs/libsel4vmmplatsupport/src/ioports.c
by yadong.li 12 Mar '20

12 Mar '20

Hi: background: I run virtio_net and virt_con in the lastest version, it is run OK, but I try to add another virito blk, I meet run error below: "Unhandled offset of 0x400 of size 4, reading Assertion failed: !"panic" (/home/yadong.li/seL4_vm_11/sel4_horizon/camkes-arm-vm/projects/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_in: 71)" I add print on my enviornmen, found: ********************start[0x1000], end[0x1400] /*net*/ ********************start[0x1400], end[0x1800] /*con*/ ********************start[0x1800], end[0x1c00] /*blk*/ ---------------------------virtio_con_io_in, con = 0x55f3238, offset = 0x400[0x1800:0x1400] port_no:1800 should belong "blk", but it recongnize as belong "con"(con may be not use the offset 0 feature), the boundary may be have some problem the function: static int alloc_free_io_port_range(vmm_io_port_list_t *io_list, ioport_range_t *io_range) { uint16_t free_port_addr = io_list->alloc_addr; if (free_port_addr + io_range->size < free_port_addr) { /* Possible overflow */ return -1; } io_list->alloc_addr += io_range->size; io_range->start = free_port_addr; io_range->end = free_port_addr + io_range->size; return 0; } I think "io_range->end = free_port_addr + io_range->size;" should change to "io_range->end = free_port_addr + io_range->size - 1;" ? Thank you very much!

2 1