June 2019 - Devel - lists.sel4.systems

Re: [seL4] Checking if an endpoint is a badged version of another
by Millar, Curtis (Data61, Kensington NSW) 15 Jun '19

15 Jun '19

Hi Demi, Any time you perform an seL4_Call operation on an endpoint and block waiting for a reply you are trusting that endpoint in a variety of ways. You trust that the messages will eventually get a reply and allow you to resume. You also trust that the message will eventually be received. If you want to perform an seL4_Call on an untrusted endpoint you will require a monitor thread that can handle a timeout and reset the calling thread if it is still blocked. In general, you want to avoid using endpoints where you can't trust that the message will be received and replied to in a timely manner. Asynchronous notifications do not suffer from this trust requirement so it is recommended that communication between mutually distrusting servers use shared memory and notifications. The client should seL4_Signal the server to notify a message has been sent via the shared memory and the server should signal in response to notify the client the message has been handled and the reply is in the shared memory. The problem of setting up a connection, sending the reply badged notification object to the server, acquiring a send notification object from the server, and mapping the shared memory would require either the connection being statically configured at process creation or dynamically configured by some mutually trusted shared component. Cheers, Curtis

1 0

Re: [seL4] camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

sorry, previous email sent by mistake. #include "sys/socket.h" actually solved the problem instead of only "socket.h" many thanks. Regards yk On Fri, Jun 14, 2019 at 10:30 AM yogidk . <yogidk(a)gmail.com> wrote: > thanks Kent and Peter, > > however if I remove > > > On Fri, Jun 14, 2019 at 2:14 AM Mcleod, Kent (Data61, Kensington NSW) < > Kent.Mcleod(a)data61.csiro.au> wrote: > >> > "../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 >> <sys/socket.h>. Otherwise many other include directives are going to match >> on the incorrect files. >> >> Kent. >> ------------------------------ >> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Chubb, Peter >> (Data61, Kensington NSW) <Peter.Chubb(a)data61.csiro.au> >> *Sent:* Friday, 14 June 2019 8:03 AM >> *To:* yogidk . >> *Cc:* devel(a)sel4.systems >> *Subject:* Re: [seL4] camkes error.h include problem >> >> >>>>> "yogidk" == yogidk <yogidk(a)gmail.com> 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 <errno.h>" picks up sys/errno.h instead >> of errno.h. >> >> Get rid of it. Instead, do '#include <sys/socket.h> instead of >> '#include <socket.h>' >> >> 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(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel >> >

1 0

camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

Hi , I have a test_1.c file which includes <camkes.h> camkes.h which is automatically generated has following includes #include <camkes/dataport.h> #include <camkes/error.h> #include <stdint.h> #include <stdlib.h> #include <utils/util.h> #include <platsupport/io.h> and another file test_2.c which includes "socket.h" In CMakeLists.txt, where I compile my test_1.c and test_2.c looks like this DeclareCAmkESComponent(test INCLUDES "../muslibc/include/sys"* // necessary for compilation as test_2.c has "socket.h"* SOURCES "test_1.c" "test_2.c" C_FLAGS -Wall -Werror LIBS seos_libs ) However when I compile , I start getting these errors: In file included from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20:0, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] *#warning redirecting incorrect #include <sys/errno.h> to <errno.h>* ^~~~~~~ In file included from ../projects/musllibc/include/sys/errno.h:2:0, from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] #warning redirecting incorrect #include <sys/errno.h> to <errno.h> How could this be solved ? thanks --yk

3 2

Roadmap - Status
by Rutherford, Luke 08 Jun '19

08 Jun '19

I see these on your development road map. Any updates on the status of them? Development Roadmap Microkernel in progress 64-bit ARM virtualisation support branch Low-level Userland Status Date Feature Location planned SMP-capable virtual-machine monitor (VMM) master

3 2

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 05 Jun '19

05 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