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.