Re: [seL4] [Non-DoD Source] Devel Digest, Vol 65, Issue 5

5 Oct 2019

      Hi Thad,

Could you please let us know which seL4 (and CAmkES if applicable)
version you are using?

Regards,
Yanyan

On Thu, 2019-10-03 at 15:50 +0000, Seeberger, John T CIV USN NAS PAX MD
(USA) wrote:
...
I have noticed this also.
Thad
________________________________________
From: Devel [devel-bounces@sel4.systems] on behalf of 
devel-request@sel4.systems [devel-request@sel4.systems]
Sent: Thursday, October 03, 2019 8:24 AM
To: devel@sel4.systems
Subject: [Non-DoD Source] Devel Digest, Vol 65, Issue 5
Send Devel mailing list submissions to
        devel@sel4.systems
To subscribe or unsubscribe via the World Wide Web, visit
        https://sel4.systems/lists/listinfo/devel
or, via email, send a message with subject or body 'help' to
        devel-request@sel4.systems
You can reach the person managing the list at
        devel-owner@sel4.systems
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Devel digest..."
Today's Topics:
1. Re: Zynq UltraScale+ locks up after hours running
      (Shen, Yanyan (Data61, Kensington NSW))
   2. Re: How to use sel4runtime
      (Millar, Curtis (Data61, Kensington NSW))
   3. Re: Zynq UltraScale+ locks up after hours running
      (Leonid Meyerovich)
-------------------------------------------------------------------
---
Message: 1
Date: Thu, 3 Oct 2019 06:43:52 +0000
From: "Shen, Yanyan (Data61, Kensington NSW)"

To: "lmeyerovich@i-a-i.com" ,
        "devel@sel4.systems" 
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running
Message-ID:
        <
78ebf24ad9274ca75e18b5fca8575a09bc423b82.camel@data61.csiro.au>
Content-Type: text/plain; charset="utf-8"
Hi Leonid,
Could you provide a bit more about your software configuration? For
instance, do you have multiple VMs running on dedicated hardware
cores?
How are the VM and processes configured?
Also, you mean there were no interrupts at all on all the four cores?
Regards,
Yanyan
On Wed, 2019-10-02 at 16:01 +0000, Leonid Meyerovich wrote:
...
Hello,
We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102
board). The implementation includes multiple processes, hypervisor
and virtual machine running on dedicated core. After several hours
running (it could be 2 or even 8 hours) the whole microkernel locks
up. After some investigation I have found that no interrupts
generated anymore - at least there is no interrupts coming to ISR.
Inside ISR I have monitored PL2 Physical Timer Control register,
which feeds a scheduler and didn't find any problems - it stays
enabled and not masked.
I will appreciate any idea/direction for approaching this problem.
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.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
------------------------------
Message: 2
Date: Thu, 3 Oct 2019 07:04:41 +0000
From: "Millar, Curtis (Data61, Kensington NSW)"

To: "devel@sel4.systems" 
Subject: Re: [seL4] How to use sel4runtime
Message-ID:
        <
ad55f3a5de7838e0f9d16a94905647a0ead42249.camel@data61.csiro.au>
Content-Type: text/plain; charset="utf-8"
Hi Baltazar,
...
Another (less exclusively RISC-V related, though I am targeting
RISC-V
still) question - I've been trying to figure out the sel4runtime
repo,
but I'm a bit confused on how to set it up. Specifically:
* How much of a "minimal seL4 environment" do I need to initialize
  first?
The sel4runtime is a minimal C runtime specifically for seL4. It
handles
the initialization of all applications (root servers and System-V ELF
processes) on an seL4 system.
A minimal project will require a repo project containing seL4,
seL4_tools, musl, and sel4runtime (along with a root task
application).
sel4runtime is then used as the C runtime for all applications built
in
the project and is responsible for providing the entrypoints and
calling
into the main function.
...
* Do does my program with main() also need to specify a root task,
or
  is that part of the minimal environment?
You will still need to provide a root task application. sel4runtime
is
only responsible for handling process startup for C applications.
...
* Is there a specific recommended location for the sel4runtime
repo?
The sel4runtime repo is usually placed in the projects directory. You
can see sel4-tutorials-manifest[^1]  repository on github for an
example
of how the dependecies are laid out.
[^1]: https://github.com/SEL4PROJ/sel4-tutorials-manifest
Cheers,
Curtis Millar
Systems Engineer,
Trustworthy Systems, CSIRO's Data61
curtis.millar@data61.csiro.au
Data61, CSIRO
Level 3, K17 Building
UNSW Gate 14, Barker St
Kensington NSW 2033 Australia
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: This is a digitally signed message part
URL: <
http://sel4.systems/pipermail/devel/attachments/20191003/7df9bd07/attachment...
...
------------------------------
Message: 3
Date: Thu, 3 Oct 2019 12:23:44 +0000
From: Leonid Meyerovich 
To: "Mcleod, Kent (Data61, Kensington NSW)"
        , "devel@sel4.systems"

Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running
Message-ID:
        <
SN4PR0401MB3648273F2FDA18C4F3824796A59F0@SN4PR0401MB3648.namprd04.prod.outlook.com
...
Content-Type: text/plain; charset="us-ascii"
I can connect JTAG, but I am not sure how I can attach it to the
running system. seL4 project it pretty big and I don't know how I can
load it to the board through JTAG.
I can run this project on zcu102. It seems to me that zcu102 is
running a little bit faster than my target device. The system is also
locked from time to time but with lower rate.
Thank you,
Leonid
-----Original Message-----
From: Mcleod, Kent (Data61, Kensington NSW) <
Kent.Mcleod@data61.csiro.au>
Sent: Wednesday, October 2, 2019 11:50 PM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running
...
I will appreciate any idea/direction for approaching this problem.
Are you able to access a hardware debugger? At the point where the
cores appear to lock up it's helpful to be able to see where all the
threads are and what the hardware state is.  Alternatively, are you
able simulate your application with the zcu102 qemu platform?
________________________________
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.
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
------------------------------
End of Devel Digest, Vol 65, Issue 5
************************************
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel