About timer tests (CONFIG_HAVE_TIMER) in sel4test testsuites
Hi seL4-hackers, I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core. The porting work is based on NVidia TK1 Cortex-A15 platform. In current stage, the seL4 kernel has booted up and the test benches can be tested. I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER). In my target, only ARM generic timer is used. My questions are: 1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer? If I only use ARM generic timer, should these timer tests be passed? 2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific. If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer? If yes, is there any example for me to reference? BRs, Jesse
Hi Jesse, The ARM generic timer is typically used by the kernel as its timer source for scheduling preemption. The CONFIG_HAVE_TIMER require an additional timer that is passed to user level. On the TK1 this is TMR1, on the hikey its the DMTIMER, on other platforms it's the EPIT etc. What timer did you use to implement sel4platsupport_get_default_timer? If the CONFIG_HAVE_TIMER tests are not passing then that indicates a bug in that time driver. The ARM generic timer cannot be exported to user level as it would be unsafe for the kernel to share it, and the kernel needs the generic timer as its the only per-core timer. For this reason you'll need an implementation of another platform specific timer. Adrian On Wed 24-May-2017 7:48 PM, Jesse-SC Chou (周書正) wrote: Hi seL4-hackers, I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core. The porting work is based on NVidia TK1 Cortex-A15 platform. In current stage, the seL4 kernel has booted up and the test benches can be tested. I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER). In my target, only ARM generic timer is used. My questions are: 1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer? If I only use ARM generic timer, should these timer tests be passed? 2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific. If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer? If yes, is there any example for me to reference? BRs, Jesse _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Adrian, Thanks for your explanation. It’s very clear. We’ll find another platform timer to satisfy the design of seL4 timer driver. BRs, Jesse From: Adrian.Danis@data61.csiro.au [mailto:Adrian.Danis@data61.csiro.au] Sent: Thursday, May 25, 2017 10:26 AM To: Jesse-SC Chou (周書正); devel@sel4.systems Subject: Re: [seL4] About timer tests (CONFIG_HAVE_TIMER) in sel4test testsuites Hi Jesse, The ARM generic timer is typically used by the kernel as its timer source for scheduling preemption. The CONFIG_HAVE_TIMER require an additional timer that is passed to user level. On the TK1 this is TMR1, on the hikey its the DMTIMER, on other platforms it's the EPIT etc. What timer did you use to implement sel4platsupport_get_default_timer? If the CONFIG_HAVE_TIMER tests are not passing then that indicates a bug in that time driver. The ARM generic timer cannot be exported to user level as it would be unsafe for the kernel to share it, and the kernel needs the generic timer as its the only per-core timer. For this reason you'll need an implementation of another platform specific timer. Adrian On Wed 24-May-2017 7:48 PM, Jesse-SC Chou (周書正) wrote: Hi seL4-hackers, I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core. The porting work is based on NVidia TK1 Cortex-A15 platform. In current stage, the seL4 kernel has booted up and the test benches can be tested. I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER). In my target, only ARM generic timer is used. My questions are: 1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer? If I only use ARM generic timer, should these timer tests be passed? 2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific. If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer? If yes, is there any example for me to reference? BRs, Jesse _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
participants (2)
-
Adrian.Danis＠data61.csiro.au -
Jesse-SC Chou (周書正)