- Devel - lists.sel4.systems

Re: [seL4] xilinx ultrascale+: Spurious interrupt
by Shen, Yanyan (Data61, Kensington NSW) 05 Jun '19

05 Jun '19

Hi Leonid, One possible cause I can think of is the trigger type (level vs edge) of an interrupt is incorrect. The Linux device tree should have interrupt type for each interrupt source, so you can change the GIC init code to configure the interrupt types (GICD_ICFGR, assuming GICv2) accordingly and see if the messages disappear. Regards, Yanyan From: Devel <devel-bounces(a)sel4.systems> on behalf of Leonid Meyerovich <lmeyerovich(a)i-a-i.com> Date: Wednesday, 5 June 2019 at 4:28 am To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: [seL4] xilinx ultrascale+: Spurious interrupt Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ 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.

1 0

xilinx ultrascale+: Spurious interrupt
by Leonid Meyerovich 04 Jun '19

04 Jun '19

Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) >From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ 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.

1 0

回复: Devel Digest, Vol 60, Issue 18
by KIM MK 03 Jun '19

03 Jun '19

Hello Sel4 developer, Thanks for your support. Aditya and me are debugging physical memory sel4. Is there visual tool or analysis module or anything to debugging that physical memory to virtual mapping table. If you have any question, please let me know. BR, MK

2 2

Multicore for 64-bit ARM
by Rutherford, Luke 24 May '19

24 May '19

I see this on your roadmap: https://sel4.systems/Info/Roadmap/ planned Multicore for 64-bit ARM and x64 master Do you have any updates on when this will be implemented?

2 1

How to add conditional compilation in .Camkes files
by yogidk 21 May '19

21 May '19

Hi, I try to add support for UART on one platform and disable this UART for another platform. As my application is Camkes based, I need to define the UART connections (Dataport, Interface functions etc) between the 2 Camkes components. However I need to use the same application on another platform without UART support. How can this be got in .Camkes files ? I already tried including a .h file where I define something like this In main.h #ifdef PLATFORM_X #define UART 1 #else #define UART 0 #endif Then include main.h file in Camkes files using a .idl4 file . However it did not work. .Camkes file is not able to see these defines to use it further for conditional compilation in .camkes files to enable or disable UART between the two components. Is there any way to get it done ? Regards yk

2 4

Compiling seL4
by Yousif Kako 21 May '19

21 May '19

Hello, I am a student researcher, I am trying to compile seL4 using the Configuring and building an seL4 project guidelines on your website ( https://docs.sel4.systems/Developing/Building/Using) And on the site, it says that after the command "ninja", I will be given binaries in the folder "images". But, I do not get such folder nor any images. I tried re-configuring some settings using cmake-gui but still nothing. I am want to write a user-level application but I am not sure if I am going about this the right way. If you have any suggestions or if you can point me in the right direction, that would be great. Thank You

2 1

Compilation Errors for the MCS tutorial
by Zeyu Mi 20 May '19

20 May '19

Hi, I was trying the MCS tutorial but encountered a few compilation errors which I cannot resolve. And the previous tutorials can be compiled normally. The building environment is based on Docker, as recommended by the tutorials. Steps: 1. cd kernel 2. git fetch seL4 mcs-tutorials 3. git checkout mcs-tutorials 4. cd .. && ./init --tut mcs 5. cd mcs && ninja Compilation output about the errors: [79/161] Building C object projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/elf.c.obj FAILED: projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/elf.c.obj ccache /usr/bin/gcc --sysroot=/host/mcs_build -DHAVE_AUTOCONF -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utic ../projects/seL4_libs/libsel4utils/src/elf.c: In function ‘rights_from_elf’: ../projects/seL4_libs/libsel4utils/src/elf.c:35:12: error: too many arguments to function ‘seL4_CapRights_new’ return seL4_CapRights_new(false, false, canRead, canWrite); In file included from ../kernel/libsel4/include/sel4/types.h:30:0, from ../kernel/libsel4/include/sel4/sel4.h:16, from ../projects/seL4_libs/libsel4utils/src/elf.c:15: libsel4/include/sel4/shared_types_gen.h:317:1: note: declared here seL4_CapRights_new(seL4_Uint64 capAllowGrant, seL4_Uint64 capAllowRead, seL4_Uint64 capAllowWrite) [82/161] Building C object projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/vspace/bootstrap.c.obj FAILED: projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/vspace/bootstrap.c.obj ccache /usr/bin/gcc --sysroot=/host/mcs_build -DHAVE_AUTOCONF -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utic In file included from ../projects/seL4_libs/libsel4utils/src/vspace/bootstrap.c:20:0: ../projects/seL4_libs/libsel4utils/src/vspace/bootstrap.c: In function ‘common_init_post_bootstrap’: ../projects/seL4_libs/libsel4utils/include/sel4utils/vspace.h:43:43: error: ‘seL4_UserTop’ undeclared (first use in this function) #define KERNEL_RESERVED_START (ALIGN_DOWN(seL4_UserTop, PAGE_SIZE_4K)) Thanks in advance. Zeyu

2 5

Changing initial thread cnode guard
by Clifford, Alexandra - 0553 - MITLL 16 May '19

16 May '19

I am attempting to prototype an seL4 based system that ideally will have multiple threads, each with their own CSpaces which are each a tree e.g. not rooted in the initial cnode. My strategy here is to 1. chain new cnodes off of the initial cnode in the initial thread, and 2. Create a new thread TCB etc., revoke the initial cnode caps and set the new cnode cap as it’s own cnode root in that new thread. I have run into some issues at step 1 and am writing to ask if this is a viable strategy. Perhaps I am misunderstanding something but chaining in this way does not seem possible if all 32 bits are to be resolved in searching the initial cnode, so I am not certain if this strategy will work. Is it possible to configure the initial cnode guard to be something other than 32 bits? I have searched through the config of the kernel and cannot find some easily changed parameter for compile time, and for runtime I have tried to use the TCB_SetSpace and TCB_Configure on the initial thread to change the guard but this has lead to other problems. If I set it to something like 16, does this mean that all of the slot indices in the bootinfo struct are no longer valid as being set at 0x0, 0x1, etc and now will be at half word indices? It is very unclear to me from the documentation how this works but perhaps I am missing something. Setting it to something like 4 leads to an explicit TCB illegal operation and something larger like 19 returns seL4_Error 3 illegal op when I try to create new cnodes via untyped_retype from the init cnode. Is there something obvious that I am missing? I wonder if this is even possible—having cnodes not rooted in the initial cnode. Or if it is possible, is there some other mechanism to create a new cnode that is not rooted in the initial cnode? It is also probably important to note that due to constraints I am not able to use any of the nice sel4_libs provided to help with this. Thanks very much in advance for any help. Alexandra Clifford, MS 05-53 Secure Resilient Systems and Technology MIT Lincoln Laboratory 244 Wood st., Lexington MA 02421 Email: Alexandra.Clifford(a)ll.mit.edu

2 1

Possible newbie question: What are ".bf"-files belonging to the seL4 code base?
by Mike Epoch 15 May '19

15 May '19

Hi! I am new to this list so please forgive me if this question has been asked before. The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words. An example of that would be file kernel/libsel4/mode_include/64/sel4/shared_types.bf which can be obtained (as part of an entire source tree, of course) via repo init -u https://github.com/seL4/sel4test-manifest.git followed by repo sync. What I find curious is that these files do not adhere to (common) C syntax yet they are fed into GCC and GCC swallows them. This file format appears to be an extension to GCC. I could not find any documentation on any such extension. I would be grateful if anyone could point me to some kind of documentation pertaining to it. Regards Mike

3 5

Using ARM GIC Virtualization Extensions with seL4
by dan pittman 10 May '19

10 May '19

Hi all! I'm currently trying to understand something about the use of the virtualization extensions available in the PL-400 interrupt controller in seL4. It all starts with this sentence: > The hypervisor supports virtualization also by using address translation tables to trap accesses that the virtual machines make to the virtual distributor. The hypervisor determines the effect of these accesses and might typically update the virtual interface control registers as a result. Source: http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0471b/CHDIHI… My interpretation of this is that by using the IPA which is available with arm hyp, the hardware can trap accesses to the GIC from the guest and "redirect" those accesses to the physical GIC. From this, I draw the conclusion that the need for a completely virtualized GIC when using these extensions is not necessary. However, in seL4—due to the way in which it manages interrupts by handling the hardware interactions itself and instead invoking an endpoint—the use of these extensions in this way is not possible. I'm curious if this understanding is correct, and if not, I welcome any clarity y'all can provide! cheers, dan

2 1