- Devel - lists.sel4.systems

Untyped Retype destination not empty?
by Richard Clark 18 May '18

18 May '18

Hi! I could use a clue as to the cause of this problem. The program has its free slots start index set correctly. It is trying to allocate a dma buffer. (4k with a known physical address). The vspace has been properly set up and knows the phys addresses of its free memory. This used to work fine in a different process, but I can't find anything I've done different/wrong in this one... I've added some extra printfs, and some debug code (in kernel/src/object/untyped.c). /* Ensure that the destination slots are all empty. */ slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap)); slots.offset = nodeOffset; slots.length = nodeWindow; for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) { status = ensureEmptySlot(slots.cnode + i); if (status != EXCEPTION_NONE) { userError("Untyped Retype: Slot #%d from %p in destination window non-empty.", (int)i, (void *)slots.cnode); userError("Untyped Retype: At offset #%d length %d.", (int)nodeOffset, (int)nodeWindow); int j = 0; for(j=0;j<2048;j++){ status = ensureEmptySlot(slots.cnode + (i + j)); if (status == EXCEPTION_NONE) { userError("Next Free Slot at #%d from %p.", (int)(i+j), (void *)slots.cnode); status = EXCEPTION_SYSCALL_ERROR; break; } } return status; } } And finally, here is the output from the console: <<seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff8001a25400 "Lockmaproc" @4196e8]: CNode Copy/Mint/Move/Mutate: Destination not empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/166 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: Slot #196 from 0xffffff807f000000 in destination window non-empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/167 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: At offset #196 length 1.>> <<seL4(CPU 0) [decodeUntypedInvocation/172 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Next Free Slot at #197 from 0xffffff807f000000.>> _refill_pool@split.c:187 Failed to retype untyped, error 8 vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1 dma_alloc@page_dma.c:92 Failed to allocate untyped of size 12 I need a hint... help? Thanks! Richard ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Automatic testing using qemu
by Paolo Crisafulli 18 May '18

18 May '18

Hi there, I have written a seL4 app using CAmkES, that I am continuously building using Jenkins. I'd like to add a test step to this continuous integration process, launching the app with qemu and parsing the output to validate my expectations. The thing is, although all the active ("control") components reach their last instruction after a while, seL4 does not "exit" (which is expected I guess) and qemu does not stop, keeping my continuous integration job running for ever. Any idea on how to achieve this? Thank you very much in advance. Cheers, Paolo Crisafulli

3 5

Booting seL4, MMU configuration on armv7a-ve
by Jonas Persson 30 Apr '18

30 Apr '18

Hello, I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE extensions (NXP IMX6UL). One of the experiments I wish to do is measure how fast I can get from POR to seL4 doing something meningful. To achive optimal boot speed I have a custom bootloader that does the bare minimum. The boot flow looks like this; 1. POR 2. Init HW 3. Load & verify blobs for trust zone and seL4 4. Jump to TEE init (OP-TEE) 5. Tee init code returns to bootloader with the CPU in HYP mode At this point we're back in the bootloader, there is no MMU, D cache or I cache active 6. Configure MMU 7. Jump to seL4 kernel entry I'm currently struggling with getting the MMU properly setup and I was hoping that someone here might shed some light on what I would need to do. I've looked at the elf-loader and from what I can understand it will setup a basic memory-mapping for the kernel only. Some of the questions that stand out in my head are : 1) How should the hand over work between the BL and seL4 with respect to setting up more mappings, for example IO memory. Should the PGD & PMD tables created by the bootloader be shared with the kernel? 2) What needs to be configured before calling the seL4 entry? Thanks, Jonas

1 0

Announcing seL4 9.0.1: with RISC-V support
by Kent.Mcleod＠data61.csiro.au 26 Apr '18

26 Apr '18

We are pleased to announce initial RISC-V support for the UC Berkeley Spike simulator platform. Instructions are available for building and running the seL4 test suite on RISC-V: <https://docs.sel4.systems/Hardware/RISCV> See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_9.0.1> <https://docs.sel4.systems/camkes_release/CAmkES_3.4.0> # seL4 Version 9.0.1 Release Announcing the release of `seL4 9.0.1` with the following changes: 9.0.1 2018-04-18: BINARY COMPATIBLE ## Changes * On 64-bit architectures, the `label` field of `seL4_MessageInfo` is now 52 bits wide. User-level programs which use any of the following functions may break, if the program relies on these functions to mask the `label` field to the previous width of 20 bits. - `seL4_MessageInfo_new` - `seL4_MessageInfo_get_label` - `seL4_MessageInfo_set_label` * Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or or multicore support on the Spike simulation platform. There is *no verification* for this platform. ## Upgrade Notes --- # Full changelog Refer to the git log in <https://github.com/seL4/seL4> using `git log 9.0.0..9.0.1` # More details See the [9.0.1 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf) included in the release or ask on the mailing list!# CAmkES Version camkes-3.3.0 Release ---- # CAmkES Version camkes-3.4.0 Release Announcing the release of `` with the following changes: camkes-3.4.0 2018-04-18 Using seL4 version 9.0.1 ## Changes ## Upgrade Notes --- # Full changelog Use `git log camkes-3.3.0..camkes-3.4.0` in <https://github.com/seL4/camkes-tool> # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.4.0/docs/i… or ask on the mailing list!

7 10

Further use of Device Tree?
by Jeff Waugh 23 Apr '18

23 Apr '18

Hello, Congrats on the RISC-V release! I noticed some Device Tree code snuck in, replacing some hard coded bits in the platform, and is intended to be exposed to the rootserver… Any interest or intention to bring that to the ARM code, and possibly avoid building kernels for specific platforms? Thanks, Jeff

2 1

UART1 getchar
by Wei Xiang Leow 19 Apr '18

19 Apr '18

Hello all, I'm new to seL4 and embedded systems, please bear with me. I'm trying to use Sabrelite's UART1 (PS_SERIAL0), while I can make it write data (putchar), I can't make it read (getchar). The code is as follows on sel4 7.0.0, using platsupport/sel4platsupport: ps_io_ops_t io_ops; error = sel4platsupport_new_io_ops(vspace, vka, &io_ops); printf("Initialising io_ops: %d\n",error); ps_chardevice_t serial0; ps_cdev_init(PS_SERIAL0,&io_ops,&serial0) ps_chardevice_t serial1; ps_cdev_init(PS_SERIAL1,&io_ops,&serial1); //CONSOLE int character; while (1) { character = ps_cdev_getchar(&serial0); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial1,character); printf("%d\n",character); } } This runs fine on QEMU with -serial file/ttyUSB -serial mon:stdio. Next I tried to run this on the Sabrelite board: -Clone the 08-09 uboot from git, according to https://sel4.systems/Info/ Hardware/sabreLite/ -Apply patches 1 and 2 (applying 3 and 4 caused uboot to stall) -Put uboot into SPI flash -Restart, run the sel4 image on the SD card, with UART2 connected to PC's RS232 and displayed by minicom, and UART1 connected to /dev/ttyUSB0 -Have a python script writing 'A's to /dev/ttyUSB0 sel4 loads but fails to read anything from /dev/ttyUSB0, UART1 just receives EOFs (-1s). The rxd seems to always be 0. Swapping the UARTs works, at the cost of losing the console: while (1) { character = ps_cdev_getchar(&serial1); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial0,character); printf("%d\n",character); } } So UART2 (default console) can read and write, while UART1 can write but not read. Has anyone encountered the same problem? Suggestions much appreciated. Regards, Leow Wei Xiang

1 0

Camkes manifest now requires cmake 3.7.2 or higher to be built
by Amit Goyal 13 Apr '18

13 Apr '18

I was running the following commands to build camkes: 1. repo init -u https://github.ls com/sel4/camkes-manifest.git 2. repo sync 3. make clean 4. make ia32_simple_defconfig; make silentoldconfig 5. make -j4 6. qemu-system-i386 -nographic -m 512 -cpu Haswell -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 Earlier it used to work perfectly fine but now it requires cmake 3.7.2 or higher which can be obviously be done by using pip install. I just wanted to convey this so that the same may be updated on prerequisites page. (https://github.com/SEL4PROJ/sel4-tutorials/blob/master/Prerequisites.md) -- Thanks and Regards, Amit Goyal

1 0

Unable to Run seL4test
by Amit Goyal 13 Apr '18

13 Apr '18

Hi Kofi, I am getting the attached error (Error Log.txt) while running seL4test. Earlier it used to run perfectly fine. I am running the following commands: $ repo init -u https://github.com/seL4/sel4test-manifest.git $ repo sync $ make clean $ make ia32_simulation_release_xml_defconfig $ make -j libmuslc && make $ make simulate-ia32 Can you please look into this. -- Thanks and Regards, Amit Goyal

2 2

New documentation website: https://docs.sel4.systems
by Kent.Mcleod＠data61.csiro.au 12 Apr '18

12 Apr '18

We are pleased to annouce a new documentation website at <https://docs.sel4.systems>! The documentation site is now using GitHub pages, generated from a GitHub repository <https://github.com/SEL4PROJ/docs> using a popular static site generator, Jekyll. GitHub pages hosted documentation is a standard documentation pattern familiar to many in the open-source community. Content from the previous wiki has been migrated to the new site, while the wiki itself is no longer available. The new documentation format should welcome community contributions, and be easier to maintain for the following reasons: * Contributions are welcome via pull request. * Easier editing through Markdown (GFM), an open document format. * Content styling is now separate from presentation. * The site can be checked out and hosted locally. * Contributions are versioned and reviewed, and tagged at released versions of seL4. We hope that this will lead to the quality of our documentation increasing as it is easier and more accessible to update. Contributions, via pull requests or feature requests on github, are welcome. Kent

1 0

seL4 9.0.0 and CAmkES camkes-3.3.0 release
by Kent.Mcleod＠data61.csiro.au 12 Apr '18

12 Apr '18

See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_9.0.0> <https://docs.sel4.systems/camkes_release/CAmkES_3.3.0> # seL4 Version 9.0.0 Release Announcing the release of `seL4 9.0.0` with the following changes: 9.0.0 2018-04-11: BREAKING # Changes * Debugging option on x86 for syscall interface to read/write MSRs (this is an, equally dangerous, alternative to dangerous code injection) * Mitigation for Meltdown (https://meltdownattack.com) on x86-64 implemented. Mitigation is via a form of kernel page table isolation through the use of a Static Kernel Image with Microstate (SKIM) window that is used for trapping to and from the kernel address space. This can be enabled/disabled through the build configuration depending on whether you are running on vulnerable hardware or not. * Mitigation for Spectre (https://spectreattack.com) on x86 against the kernel implemented. Default is software mitigation and is the best performing so users need to do nothing. This does *not* prevent user processes from exploiting each other. * x86 configuration option for performing branch prediction barrier on context switch to prevent Spectre style attacks between user processes using the indirect branch predictor * x86 configuration option for flushing the RSB on context switch to prevent Spectre style attacks between user processes using the RSB * Define extended bootinfo header for the x86 TSC frequency * x86 TSC frequency exported in extended bootinfo header * `archInfo` is no longer a member of the bootinfo struct. Its only use was for TSC frequency on x86, which can now be retrieved through the extended bootinfo * Invocations to set thread priority and maximum control priority (MCP) have changed. - For both invocations, users must now provide a TCB capability `auth` - The requested MCP/priority is checked against the MCP of the `auth` capability. - Previous behavior checked against the invoked TCB, which could be subject to the confused deputy problem. * `seL4_TCB_Configure` no longer takes prio, mcp as an argument. Instead these fields must be set separately with `seL4_TCB_SetPriority` and `seL4_TCB_SetMCPriority`. * `seL4_TCB_SetPriority` and `seL4_TCB_SetMCPriority` now take `seL4_Word` instead of `seL4_Uint8`. - `seL4_MaxPrio` remains at 255. * `seL4_TCB_SetSchedParams` is a new method where MCP and priority can be set in the same sytsem call. * Size of the TCB object is increased for some build configurations # Upgrade notes * `seL4_TCB_Configure` calls that set priority should be changed to explicitly call `seL4_TCB_SetSchedParams` or `SetPriority` * `seL4_TCB_Configure` calls that set MCP should be changed to explicitly call `seL4_TCB_SetSchedParams` or `seL4_TCB_SetMCPriority` --- # Full changelog Refer to the git log in <https://github.com/seL4/seL4> using `git log 8.0.0..9.0.0` # More details See the [9.0.0 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.0.pdf) included in the release or ask on the mailing list! ---- # CAmkES Version camkes-3.3.0 Release Announcing the release of `camkes-3.3.0` with the following changes: camkes-3.3.0 2018-04-11 Using seL4 version 9.0.0 ## Changes * Hardware dataport with large frame sizes issue has been fixed * Bug fix: Enumerating connections for hierarchical components with custom connection types is now done correctly * Bug fix: Data structure caching is now correctly invalidated between builds * Initial CMake implementation for CAmkES. See the CAmkES test apps for examples. ## Upgrade notes * No special upgrade requirements. ## Known issues * Hierarchical components that export dataport connectors create compilation errors as the templates cannot accurately tell that the connector of the parent component is exported from the child and no code should be generated. A temporary workaround involves making the dataport connection explicitly available to the parent component. --- # Full changelog Use `git log camkes-3.2.0..camkes-3.3.0` in <https://github.com/seL4/camkes-tool> # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.3.0/docs/i… or ask on the mailing list!

1 0