Hi Anna and Alex,

thanks a lot for your inputs --

Anna,

you can put a printf in handleInterrupt in the kernel

I added it there and it seems there no interrupt executed at all.

Alex,

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.

it's done here: https://github.com/wwladikw/devel/blob/master/timer.c#L87 which is called in driver init, before timer gets configured: https://github.com/wwladikw/devel/blob/master/timer.c#L220

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.

yes, the interrupts are edge triggered for my understanding.

4. Check that your code that clears the interrupt status bit does not

clear the enable bit.

it's done when configuring the timer https://github.com/wwladikw/devel/blob/master/timer.c#L138 and in the IRQ handler https://github.com/wwladikw/devel/blob/master/timer.c#L173 where INTCTLSTAT_ACK_MASK is 0x03 which keeps the interrupts enabled and clears the status bit.

I've also extended the driver and the testcase with some debug prints to track the status info for the intctlstat register - like: ------ timer_start(env->timer->timer); timer_periodic(env->timer->timer, 100 * NS_IN_MS); while (timeout > 0) { printf("tick .. %llu ns \n", timer_get_time(env->timer->timer)); if (timeout == 45) sel4_timer_handle_single_irq(env->timer); timeout--; } for (int i = 0; i < 3; i++) { wait_for_timer_interrupt(env); printf("Tick\n"); } ----

output: (XXXX comes from the driver) ------- Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 XXXX keystone_timer_reset: 73: kt->hw->intctlstat init 0x0 XXXX keystone_timer_reset: 88: kt->hw->intctlstat done 0x1 Running test INTERRUPT0001 (Test interrupts with timer) timer_start .. timer_start done .. set timer_periodic .. XXXX keystone_set_timeo: 138: kt->hw->intctlstat 0x3 XXXX keystone_set_timeo: 141: kt->hw->intctlstat 0x1 XXXX keystone_set_timeo: 142: enable timer set timer_periodic done .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 1367513 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 743185 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 .. XXXX keystone_handle_irq: 177: kt->hw->intctlstat current status 0x3 (called manually by sel4_timer_handle_single_irq) XXXX keystone_handle_irq: 179: kt->hw->intctlstat clear 0x1 XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 17540752 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 1056723 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 2371025 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 3685205 ns ---------- and stays forever in wait_for_timer_interrupt.

I also wonder about a short flood of messages before the testsuite starts: --- _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 13 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 8192, error 1 --- But I guess this shouldn't have impact to the interrupts, right?

Thanks in advance! - Wladi

2017-02-22 1:32 GMT+01:00 Alexander.Kroh@data61.csiro.au:

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 +0000, Anna.Lyons@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

Hi Alex,

really great catch! When I am disabling interrupt 27 and 57 in maskInterrupt and keeping everything else enabled, like: switch (irq) { case 27: dist_enable_clr(irq); break; case 57: dist_enable_clr(irq); break; default: dist_enable_set(irq); break; }

I can see spurious interrupts from interrupt number 48 each second (depends on timer_periodic(env->timer->timer, 1 * NS_IN_S);) setting.

.. Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 Timer initialised Running test INTERRUPT0001 (Test interrupts with timer) <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> ..

But for some reason, even when configuring the timer interrupt to nr. 48, (in the kernel machine.h and userspace timer) the interrupt handler doesn't get called and keeps firing spurious interrupts.

Let me know if you have an idea for this as well :-)

Thanks a lot! - Wladi

2017-02-24 0:21 GMT+01:00 Alexander.Kroh@data61.csiro.au:

Hi Wladi,

Another problem could be that you are using the wrong IRQ number. The GIC handles two classes of IRQ: PPI and SPI. There are 32 PPIs. To ensure that each IRQ number is unique we offset each SPI by 32.

The reported SPI IRQ number in technical manuals is not always consistent. Sometimes the SPI IRQ number is reported, sometimes this offset in included, and sometimes both IRQ numbering systems are reported.

As a catch all, you could prevent seL4 from disabling some (or all) IRQs by modifying this function: https://github.com/seL4/seL4/blob/master/include/arch/arm/arch/machine/gic_p...

The catch is that this might trigger other IRQs that you aren't expecting, so watch out for false positives.

• Alex

On Wed, 2017-02-22 at 16:13 +0100, Wladislav Wiebe wrote:

...

Hi Anna and Alex,

thanks a lot for your inputs --

Anna,

...

you can put a printf in handleInterrupt in the kernel

I added it there and it seems there no interrupt executed at all.

Alex,

...

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.

it's done here: https://github.com/wwladikw/devel/blob/master/timer.c#L87 which is called in driver init, before timer gets configured: https://github.com/wwladikw/devel/blob/master/timer.c#L220

...

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.

yes, the interrupts are edge triggered for my understanding.

...

4. Check that your code that clears the interrupt status bit does not

clear the enable bit.

it's done when configuring the timer https://github.com/wwladikw/devel/blob/master/timer.c#L138 and in the IRQ handler https://github.com/wwladikw/devel/blob/master/timer.c#L173 where INTCTLSTAT_ACK_MASK is 0x03 which keeps the interrupts enabled and clears the status bit.

I've also extended the driver and the testcase with some debug prints to track the status info for the intctlstat register - like:

---

timer_start(env->timer->timer); timer_periodic(env->timer->timer, 100 * NS_IN_MS); while (timeout > 0) { printf("tick .. %llu ns \n", timer_get_time(env->timer->timer)); if (timeout == 45) sel4_timer_handle_single_irq(env->timer); timeout--; } for (int i = 0; i < 3; i++) { wait_for_timer_interrupt(env); printf("Tick\n"); }

---

output: (XXXX comes from the driver)

Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 XXXX keystone_timer_reset: 73: kt->hw->intctlstat init 0x0 XXXX keystone_timer_reset: 88: kt->hw->intctlstat done 0x1 Running test INTERRUPT0001 (Test interrupts with timer) timer_start .. timer_start done .. set timer_periodic .. XXXX keystone_set_timeo: 138: kt->hw->intctlstat 0x3 XXXX keystone_set_timeo: 141: kt->hw->intctlstat 0x1 XXXX keystone_set_timeo: 142: enable timer set timer_periodic done .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 1367513 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 743185 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 .. XXXX keystone_handle_irq: 177: kt->hw->intctlstat current status 0x3 (called manually by sel4_timer_handle_single_irq) XXXX keystone_handle_irq: 179: kt->hw->intctlstat clear 0x1 XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 17540752 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 1056723 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 2371025 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 3685205 ns

---

and stays forever in wait_for_timer_interrupt.

I also wonder about a short flood of messages before the testsuite starts:

_allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 13 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 8192, error 1

---

But I guess this shouldn't have impact to the interrupts, right?

Thanks in advance!

• Wladi

2017-02-22 1:32 GMT+01:00 Alexander.Kroh@data61.csiro.au:

...

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 +0000, Anna.Lyons@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

Hi Wladi,

I am sorry to say that IRQ 27 might be the IRQ of the preemption timer that the kernel uses. If not, it should at least be the IRQ of the ARM private timers rather than a third-party peripheral.

That being said, some vendors don't like to follow standards.

Do you receive the 'Tick' even if you don't set the enable bit on your timer? Have you checked that the timer status bit is actually being asserted?

- Alex

On Sun, 2017-02-26 at 11:58 +0100, Wladislav Wiebe wrote:

Hi Alex,

I've found the magic IRQ number -> 27.

Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 Running test INTERRUPT0001 (Test interrupts with timer) Tick Tick Tick Test INTERRUPT0001 passed Starting test 1: TEST_INTERRUPT00012 TEST_INTERRUPT0001 Running test INTERRUPT0001 (Test interrupts with timer) Tick Tick Tick Test INTERRUPT0001 passed Test suite passed. 2 tests passed.

2/2 tests passed. All is well in the universe.

Special thanks again for the great support!

• Wladi

2017-02-24 11:50 GMT+01:00 Wladislav Wiebe wladislav.kw@gmail.com:

...

Hi Alex,

really great catch! When I am disabling interrupt 27 and 57 in maskInterrupt and keeping everything else enabled, like: switch (irq) { case 27: dist_enable_clr(irq); break; case 57: dist_enable_clr(irq); break; default: dist_enable_set(irq); break; }

I can see spurious interrupts from interrupt number 48 each second (depends on timer_periodic(env->timer->timer, 1 * NS_IN_S);) setting.

.. Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 Timer initialised Running test INTERRUPT0001 (Test interrupts with timer) <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> ..

But for some reason, even when configuring the timer interrupt to nr. 48, (in the kernel machine.h and userspace timer) the interrupt handler doesn't get called and keeps firing spurious interrupts.

Let me know if you have an idea for this as well :-)

Thanks a lot!

• Wladi

2017-02-24 0:21 GMT+01:00 Alexander.Kroh@data61.csiro.au:

...

Hi Wladi,

Another problem could be that you are using the wrong IRQ number. The GIC handles two classes of IRQ: PPI and SPI. There are 32 PPIs. To ensure that each IRQ number is unique we offset each SPI by 32.

The reported SPI IRQ number in technical manuals is not always consistent. Sometimes the SPI IRQ number is reported, sometimes this offset in included, and sometimes both IRQ numbering systems are reported.

As a catch all, you could prevent seL4 from disabling some (or all) IRQs by modifying this function: https://github.com/seL4/seL4/blob/master/include/arch/arm/arch/machine/gic_p...

The catch is that this might trigger other IRQs that you aren't expecting, so watch out for false positives.

• Alex

On Wed, 2017-02-22 at 16:13 +0100, Wladislav Wiebe wrote:

...

Hi Anna and Alex,

thanks a lot for your inputs --

Anna,

...

you can put a printf in handleInterrupt in the kernel

I added it there and it seems there no interrupt executed at all.

Alex,

...

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.

it's done here: https://github.com/wwladikw/devel/blob/master/timer.c#L87 which is called in driver init, before timer gets configured: https://github.com/wwladikw/devel/blob/master/timer.c#L220

...

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.

yes, the interrupts are edge triggered for my understanding.

...

4. Check that your code that clears the interrupt status bit does not

clear the enable bit.

it's done when configuring the timer https://github.com/wwladikw/devel/blob/master/timer.c#L138 and in the IRQ handler https://github.com/wwladikw/devel/blob/master/timer.c#L173 where INTCTLSTAT_ACK_MASK is 0x03 which keeps the interrupts enabled and clears the status bit.

I've also extended the driver and the testcase with some debug prints to track the status info for the intctlstat register - like:

---

timer_start(env->timer->timer); timer_periodic(env->timer->timer, 100 * NS_IN_MS); while (timeout > 0) { printf("tick .. %llu ns \n", timer_get_time(env->timer->timer)); if (timeout == 45) sel4_timer_handle_single_irq(env->timer); timeout--; } for (int i = 0; i < 3; i++) { wait_for_timer_interrupt(env); printf("Tick\n"); }

---

output: (XXXX comes from the driver)

Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 XXXX keystone_timer_reset: 73: kt->hw->intctlstat init 0x0 XXXX keystone_timer_reset: 88: kt->hw->intctlstat done 0x1 Running test INTERRUPT0001 (Test interrupts with timer) timer_start .. timer_start done .. set timer_periodic .. XXXX keystone_set_timeo: 138: kt->hw->intctlstat 0x3 XXXX keystone_set_timeo: 141: kt->hw->intctlstat 0x1 XXXX keystone_set_timeo: 142: enable timer set timer_periodic done .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 1367513 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 743185 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 .. XXXX keystone_handle_irq: 177: kt->hw->intctlstat current status 0x3 (called manually by sel4_timer_handle_single_irq) XXXX keystone_handle_irq: 179: kt->hw->intctlstat clear 0x1 XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 17540752 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 1056723 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 2371025 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 3685205 ns

---

and stays forever in wait_for_timer_interrupt.

I also wonder about a short flood of messages before the testsuite starts:

_allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 13 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 8192, error 1

---

But I guess this shouldn't have impact to the interrupts, right?

Thanks in advance!

• Wladi

2017-02-22 1:32 GMT+01:00 Alexander.Kroh@data61.csiro.au:

...

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 +0000, Anna.Lyons@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

-- WBR, Wladislav WIebe

Hi,

seems all other interrupt ID's comes also back with ID 1023 (spurious interrupt).

A really dirty way to get it handled is to keep it in the kernel enabled and hardcode it in getActiveIRQ to the wanted interrupt ID, instead of mark it as invalid. I did it at least to verify if it is the timer interrupt.

May ask about this magic in the TI e2e forum.

Thanks! - Wladi

2017-02-27 16:59 GMT+01:00 Wladislav Wiebe wladislav.kw@gmail.com:

Hi Alex,

yes, you are right -- seems interrupt 27 is the virtual timer based on GIC 400 specification. http://infocenter.arm.com/help/topic/com.arm.doc.ddi0471b/DDI0471B_gic400_r0...

May I will try to loop through all interrupts > 31 (after the PPI's)..

Thanks!

• Wladi

2017-02-26 12:58 GMT+01:00 Alexander.Kroh@data61.csiro.au:

...

Hi Wladi,

I am sorry to say that IRQ 27 might be the IRQ of the preemption timer that the kernel uses. If not, it should at least be the IRQ of the ARM private timers rather than a third-party peripheral.

That being said, some vendors don't like to follow standards.

Do you receive the 'Tick' even if you don't set the enable bit on your timer? Have you checked that the timer status bit is actually being asserted?

• Alex

On Sun, 2017-02-26 at 11:58 +0100, Wladislav Wiebe wrote:

...

Hi Alex,

I've found the magic IRQ number -> 27.

Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 Running test INTERRUPT0001 (Test interrupts with timer) Tick Tick Tick Test INTERRUPT0001 passed Starting test 1: TEST_INTERRUPT00012 TEST_INTERRUPT0001 Running test INTERRUPT0001 (Test interrupts with timer) Tick Tick Tick Test INTERRUPT0001 passed Test suite passed. 2 tests passed.

2/2 tests passed. All is well in the universe.

Special thanks again for the great support!

• Wladi

2017-02-24 11:50 GMT+01:00 Wladislav Wiebe wladislav.kw@gmail.com:

...

Hi Alex,

really great catch! When I am disabling interrupt 27 and 57 in maskInterrupt and keeping everything else enabled, like: switch (irq) { case 27: dist_enable_clr(irq); break; case 57: dist_enable_clr(irq); break; default: dist_enable_set(irq); break; }

I can see spurious interrupts from interrupt number 48 each second (depends on timer_periodic(env->timer->timer, 1 * NS_IN_S);) setting.

.. Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 Timer initialised Running test INTERRUPT0001 (Test interrupts with timer) <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/48 T0xffdfaf00 "" @e001086c]: Spurious interrupt!>> ..

But for some reason, even when configuring the timer interrupt to nr. 48, (in the kernel machine.h and userspace timer) the interrupt handler doesn't get called and keeps firing spurious interrupts.

Let me know if you have an idea for this as well :-)

Thanks a lot!

• Wladi

2017-02-24 0:21 GMT+01:00 Alexander.Kroh@data61.csiro.au:

...

Hi Wladi,

Another problem could be that you are using the wrong IRQ number. The GIC handles two classes of IRQ: PPI and SPI. There are 32 PPIs. To ensure that each IRQ number is unique we offset each SPI by 32.

The reported SPI IRQ number in technical manuals is not always consistent. Sometimes the SPI IRQ number is reported, sometimes this offset in included, and sometimes both IRQ numbering systems are reported.

As a catch all, you could prevent seL4 from disabling some (or all) IRQs by modifying this function: https://github.com/seL4/seL4/blob/master/include/arch/arm/arch/machine/gic_p...

The catch is that this might trigger other IRQs that you aren't expecting, so watch out for false positives.

• Alex

On Wed, 2017-02-22 at 16:13 +0100, Wladislav Wiebe wrote:

...

Hi Anna and Alex,

thanks a lot for your inputs --

Anna, > you can put a printf in handleInterrupt in the kernel I added it there and it seems there no interrupt executed at all.

Alex, > 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.

it's done here: https://github.com/wwladikw/devel/blob/master/timer.c#L87 which is called in driver init, before timer gets configured: https://github.com/wwladikw/devel/blob/master/timer.c#L220

> 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.

yes, the interrupts are edge triggered for my understanding.

> 4) Check that your code that clears the interrupt status bit does not > clear the enable bit.

it's done when configuring the timer https://github.com/wwladikw/devel/blob/master/timer.c#L138 and in the IRQ handler https://github.com/wwladikw/devel/blob/master/timer.c#L173 where INTCTLSTAT_ACK_MASK is 0x03 which keeps the interrupts enabled and clears the status bit.

I've also extended the driver and the testcase with some debug prints to track the status info for the intctlstat register - like:

---

timer_start(env->timer->timer); timer_periodic(env->timer->timer, 100 * NS_IN_MS); while (timeout > 0) { printf("tick .. %llu ns \n", timer_get_time(env->timer->timer)); if (timeout == 45) sel4_timer_handle_single_irq(env->timer); timeout--; } for (int i = 0; i < 3; i++) { wait_for_timer_interrupt(env); printf("Tick\n"); }

---

output: (XXXX comes from the driver)

Starting test suite sel4test Starting test 0: TEST_INTERRUPT0001 TEST_INTERRUPT0001 XXXX keystone_timer_reset: 73: kt->hw->intctlstat init 0x0 XXXX keystone_timer_reset: 88: kt->hw->intctlstat done 0x1 Running test INTERRUPT0001 (Test interrupts with timer) timer_start .. timer_start done .. set timer_periodic .. XXXX keystone_set_timeo: 138: kt->hw->intctlstat 0x3 XXXX keystone_set_timeo: 141: kt->hw->intctlstat 0x1 XXXX keystone_set_timeo: 142: enable timer set timer_periodic done .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 1367513 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 743185 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 .. XXXX keystone_handle_irq: 177: kt->hw->intctlstat current status 0x3 (called manually by sel4_timer_handle_single_irq) XXXX keystone_handle_irq: 179: kt->hw->intctlstat clear 0x1 XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 tick .. 17540752 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x1 .. XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 1056723 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 2371025 ns XXXX keystone_get_time: 168: kt->hw->intctlstat 0x3 tick .. 3685205 ns

---

and stays forever in wait_for_timer_interrupt.

I also wonder about a short flood of messages before the testsuite starts:

_allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 13 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 8192, error 1

---

But I guess this shouldn't have impact to the interrupts, right?

Thanks in advance!

• Wladi

2017-02-22 1:32 GMT+01:00 Alexander.Kroh@data61.csiro.au: > 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 +0000, Anna.Lyons@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 >

-- WBR, Wladislav WIebe

-- WBR, Wladislav WIebe