Hello everyone, We have ported seL4 to allwinnerA20, although the cache cannot still work well. All tests passed, except for CACHEFLUSH0001 and CACHEFLUSH0002. A git clone can be gotten from here [1]. And the 'zener' directory in this project has a similar structure to sel4test. But there is a problem about TIMER API. For allwinnerA20, there are several registers (Timer IRQ Enable/Status Register) used by all timers. Both kernel and libsel4platsupport will use timers, and they have to use different timers. But some registers can be accessed by both kernel and libsel4platsupport. That's very dangerous! Because libsel4platsupport can disable the timer of kernel by modifying the register. How to solve this problem? [1] git clone http://elastos.org/review/HD-Elastos -- Jensen Zhang Tongji University