Re: [seL4] ARM timer driver and interrupts

[Alexander.Kroh]

Hi Wladi,

If the problem is with your driver, the problem could be in your
management of the INTCTLSTAT register (Chapter 5.10).

1) ARM devices tend to only support 32bit read/write
2) Check that the interrupt enable flag is set before returning from
your timer set up code.
3) The status bits must be written as 1 to clear. If interrupts are edge
triggered, failing to clear this bit (by writing a 1 to it) will stop
interrupts from coming in.
4) Check that your code that clears the interrupt status bit does not
clear the enable bit.

 - Alex Kroh


On Tue, 2017-02-21 at 23:17 +, anna.ly...@data61.csiro.au wrote:
> Hey, 
> 
> First I'd check if the kernel is getting the interrupts in the kernel from 
> this timer - you can put a printf in handleInterrupt in the kernel to see if 
> this is the case and see if the correct interrupt number comes in.
> 
> If so,  then check if those irqs are being sent to the signal handler and not 
> reserved (again by printing / asserting in handle interrupt).
> 
> If not, this points to a problem with your driver.
> 
> Hope this pushes you in the right direction,
> Anna. 
> 
> -Original Message-
> From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Wladislav Wiebe
> Sent: Wednesday, 22 February 2017 10:05 AM
> To: devel@sel4.systems
> Subject: [seL4] ARM timer driver and interrupts
> 
> Hello,
> 
> I wrote a new timer driver for this timer device:
> http://www.ti.com/lit/ug/sprugv5a/sprugv5a.pdf
> 
> I am already able to run the seL4 testsuite successfully, except the 
> interrupt/timer tests.
> It waits forever @ wait_for_timer_interrupt(env);
> 
> I've uploaded the driver temporary to:
> https://github.com/wwladikw/devel/blob/master/timer.c
> 
> Any idea what could be wrong?
> I am able to run the timer periodically or as oneshot.
> The gic_390 interrupt driver in the kernel should also be compatible with the 
> gic_400, for my understanding, right?
> The SoC I am using contains a Coretex A15.
> 
> Thanks a lot in advance!
> Wladislav Wiebe
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

[seL4] Clarification on seL4 on RPi3b

[Joseph Adam Powers]

It seems to be necessary for me to use the debug output using a serial cable on 
UART0
u-boot seems to be waiting for a Ethernet or serial cable connection to finish 
boot process.
I don't have the serial cable so I just need some understanding that that is 
the case considering that I followed the rest of the instructions on the blog 
at https://research.csiro.au/tsblog/sel4-raspberry-pi-3/
, newbie question btw.___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] RT and domains

[rad021993]

Anna, Gernot, thank you for your answers. I want to add domains as analogues to 
arinc-653 partitions. I know that there will be some time restrictions, but the 
main goal is compliance with functional requirements of the standard.



From: gernot.hei...@data61.csiro.au

Sent: Tuesday, February 21, 5:00 AM

Subject: Re: [seL4] RT and domains

To: devel@sel4.systems



On 21 Feb 2017, at 10:57, anna.ly...@data61.csiro.au wrote:


 


For the first release of the RT kernel (which is a pre-release) we excluded the 
domain scheduler to make development easier. The final version of the RT kernel 
will probably include the domain scheduler. 


 


However, it should be noted that if using RT + domain scheduler the max 
deadline miss time is the length of the longest domain, as domains are not 
pre-emptible. 








Further to what Anna says, it is unclear (to me at last) whether there are any 
realistic use cases of real-time systems that would work with the domain 
scheduler. The whole idea of maintaining confidentiality and timeliness at the 
same time requires some serious thinking, which I’m not aware of having 
happened. Absent that, you need to assume that the two are incompatible. And we 
certainly make no claims that our kernel (once mixed-criticality support is 
merged with master) is in any way able to support both at the same time.



If anyone knows better, I’d love to hear about it.



Gernot



___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] seL4 no longer support zynq7000 board?

[Gapry Un]

Dear wang

The following reference can help you.

1. [seL4] on Zynq

2. [seL4] seL4 on Zedboard (Tue Jan 31 09:39:45 AEDT 2017)

3. [seL4] seL4 on Zedboard (Wed Feb 1 14:21:12 AEDT 2017)

2. [seL4] seL4 on Zinq7000 on QEMU

Best regards, Gapry

2017-02-21 21:33 GMT+08:00 wang :

> Hello,
>
> https://wiki.sel4.systems/Hardware
> On this seL4wiki hardware page I find the link of Zynq7000 turns grey, and
> the page says "This page does not exist yet. You can create a new empty
> page, or use one of the page templates."
> So it means seL4 do not support zynq7000 any more?
> And how can I run seL4/seL4test on zynq7000 board?
>
> Thanks!
>
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
>
>
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

[seL4] seL4 no longer support zynq7000 board?

[wang]

Hello,


https://wiki.sel4.systems/Hardware
On this seL4wiki hardware page I find the link of Zynq7000 turns grey, and the 
page says "This page does not exist yet. You can create a new empty page, or 
use one of the page templates."
So it means seL4 do not support zynq7000 any more?
And how can I run seL4/seL4test on zynq7000 board?


Thanks!___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel