ports-foc/contrib/l4linux/fs/buffer.c:1231

Sorry for my last mail, with was invalid formatted with html. Here is a version in a plain text:

Thanks for fast fixing of ‘SD card doesn’t start due to I/O pages caching’ bug.

But SD card still doesn’t normally work on PandaBoard.
It seems that there are 2 more problems with it.

Bug 1.

File cache subsystem generates an interrupt processing error at intensive read/write access to SD card: in Vcpu interrupts are disabled in the place where they should be allowed (ports-foc/contrib/l4linux/fs/buffer.c:1231).
The same error occurs in qemu in other sub-system (ports-foc/contrib/l4linux/kernel/softirq.c:159)

Solution:

Function prototype in ports-foc/src/lib/l4lx/include/linux.h:
FASTCALL void l4x_irq_save(unsigned long flags);

should be:
FASTCALL void l4x_irq_save(unsigned long *flags);

So, value of interrupt state (enabling/disabling) was not properly stored before above correction.

Bug 2.

L4Linux ‘hangs’ because of problem with its virtual block device at intensive read/write access to SD card on PandaBoard.
In Genode block driver memory for storing of packages sent via IPC sometimes is over (ports-foc/src/lib/l4lx/genode_block.cc:281).
In such case L4Linux virtual block driver is blocked on semaphore (ports-foc/src/drivers/genode_block.c:98).
When memory for IPC packages storage in Genode block driver becomes ready for use, driver sends signal to the thread ‘blk-signal-thread’ (ports-foc/src/lib/l4lx/genode_block.cc:126).
Thread ‘blk-signal-thread’ catches the signal and generates interrupt by calling function ‘l4_irq_trigger’ (ports-foc/src/lib/l4lx/genode_block.cc:154).
But, L4Linux doesn’t catch the interrupt and hangs.
In normal case interrupt is to be catched and interrupt handler ‘event_interrupt’ (ports-foc/src/drivers/genode_block.c:172) should be called; increment semaphore counter by 1 (ports-foc/src/drivers/genode_block.c:146) and thus un-block L4Linux driver.