- Devel - lists.sel4.systems

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

25 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 12 Apr '18

12 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 12 Apr '18

12 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

camkes tutorial build compilation error
by Thad Seeberger 03 Apr '18

03 Apr '18

Good day, I am working thru the examples. make arm_hello-camkes-0_defconfig; make -- compiles and run on qemu The I tried x86 architecture make ia32_hello-camkes-0_defconfig; make -- build error I cant find declarations for any of the listed errors. I'm guessing these should be dynamically defined before the build based on the architecture. Please let me know what I'm doing wrong. thx [CC] kernel_final.s /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c: In function ‘decodeIA32PageDirectoryInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: error: ‘X86PageDirectoryGetStatusBits’ undeclared (first use in this function); did you mean ‘performIA32PageDirectoryGetStatusBits’? case X86PageDirectoryGetStatusBits: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ performIA32PageDirectoryGetStatusBits /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: note: each undeclared identifier is reported only once for each function it appears in /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86FrameInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:854:10: error: ‘X86PageMap’ undeclared (first use in this function); did you mean ‘ARMPageMap’? case X86PageMap: { /* Map */ ^~~~~~~~~~ ARMPageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1012:10: error: ‘X86PageRemap’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageRemap: { /* Remap */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1143:10: error: ‘X86PageUnmap’ undeclared (first use in this function); did you mean ‘X86PageRemap’? case X86PageUnmap: { /* Unmap */ ^~~~~~~~~~~~ X86PageRemap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1166:10: error: ‘X86PageMapIO’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageMapIO: { /* MapIO */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1175:10: error: ‘X86PageGetAddress’ undeclared (first use in this function); did you mean ‘ARMPageGetAddress’? case X86PageGetAddress: { ^~~~~~~~~~~~~~~~~ ARMPageGetAddress /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86PageTableInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1236:21: error: ‘X86PageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86PageTableUnmap) { ^~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1246:21: error: ‘X86PageTableMap’ undeclared (first use in this function); did you mean ‘X86PageTableUnmap’? if (invLabel != X86PageTableMap ) { ^~~~~~~~~~~~~~~ X86PageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86MMUInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1365:25: error: ‘X86ASIDControlMakePool’ undeclared (first use in this function); did you mean ‘ARMASIDControlMakePool’? if (invLabel != X86ASIDControlMakePool) { ^~~~~~~~~~~~~~~~~~~~~~ ARMASIDControlMakePool /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1434:25: error: ‘X86ASIDPoolAssign’ undeclared (first use in this function); did you mean ‘ARMASIDPoolAssign’? if (invLabel != X86ASIDPoolAssign) { ^~~~~~~~~~~~~~~~~ ARMASIDPoolAssign /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c: In function ‘Arch_decodeIRQControlInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:122:10: error: ‘X86IRQIssueIRQHandlerIOAPIC’ undeclared (first use in this function); did you mean ‘invokeIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerIOAPIC: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~ invokeIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:144:10: error: ‘X86IRQIssueIRQHandlerMSI’ undeclared (first use in this function); did you mean ‘X86IRQIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerMSI: { ^~~~~~~~~~~~~~~~~~~~~~~~ X86IRQIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c: In function ‘decodeX86PortInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:21: error: ‘X86IOPortOut8’ undeclared (first use in this function) if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~ /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:50: error: ‘X86IOPortOut16’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:80: error: ‘X86IOPortOut32’ undeclared (first use in this function); did you mean ‘X86IOPortOut16’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:75:10: error: ‘X86IOPortIn8’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? case X86IOPortIn8: { /* inport 8 bits */ ^~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:89:10: error: ‘X86IOPortIn16’ undeclared (first use in this function); did you mean ‘X86IOPortIn8’? case X86IOPortIn16: { /* inport 16 bits */ ^~~~~~~~~~~~~ X86IOPortIn8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:103:10: error: ‘X86IOPortIn32’ undeclared (first use in this function); did you mean ‘X86IOPortIn16’? case X86IOPortIn32: { /* inport 32 bits */ ^~~~~~~~~~~~~ X86IOPortIn16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c: In function ‘decodeX86IOPTInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:195:21: error: ‘X86IOPageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86IOPageTableUnmap) { ^~~~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:201:21: error: ‘X86IOPageTableMap’ undeclared (first use in this function); did you mean ‘X86IOPageTableUnmap’? if (invLabel != X86IOPageTableMap ) { ^~~~~~~~~~~~~~~~~ X86IOPageTableUnmap make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Error 2

2 1

Status of cmake support?
by Bruce Mitchener 30 Mar '18

30 Mar '18

Hello! I've been looking at doing some builds with cmake and ninja experimentally again. Is anyone else doing this? I noticed that some bugs are being filed about warnings from clang, but I was only able to get some of the cmake + ninja stuff working when I used gcc. How are people using clang? So far, I haven't gotten a working build with cmake of sel4-tests. Is there a good way to trouble shoot this or should I post more detailed info in a thread on this list? Thanks, - Bruce

2 1

Haskell and language support
by jonas.cl＠protonmail.com 27 Mar '18

27 Mar '18

Hi, Does anyone know when the Haskell support will be released in public? In the Language support section of https://wiki.sel4.systems/Suggested%20projects is says that it will be released in the near future, but the page was last edited on June 2016. I propose that the language section also contains links to where the source can be found. I am also writing since I am working on porting the sel4-tutorial to Idris, which could be added to the list of languages, with a link to https://github.com/mokshasoft/sel4-idris-manifest There is a long way to go before it is finished, but if people want to help I accept patches. /Jonas Sent from [ProtonMail](https://protonmail.com), Swiss-based encrypted email.

2 3