Hi Jorge, these drivers are not part of the kernel, but user-level libraries, i.e. there would be no additional verification effort involved. As far as I’ve seen the kernel itself already supports the platform, it’s “only” all the user libraries that aren’t there yet. In any case, we do welcome contributions to these and to the kernel as well (see also http://sel4.systems/Contributing/ ) If there is a contribution to the verified code base, it would be ideal if the contribution included a fix to the proof as well, but we can have a look at what exactly is involved in each case and potentially accept a change on the experimental branch instead. New platform ports for instance usually have little impact on the verification, since the verification talks about one specific platform only. Cheers, Gerwin On 7 Aug 2014, at 11:57 am, Jorge Ventura mailto:jorge.araujo.ventura@gmail.com> wrote: You are right. There are many other drivers missing. There is a lot of code from TI that can be used as start point but I don't know how to include something in the seL4 tree. Another point is that although seL4 became open source, based in the philosophy from the code that has to be proofed, contributions from outside the community of original developers it's probably not much stimulated (what make sense). On Wed, Aug 6, 2014 at 5:49 PM, Peter Chubb mailto:peter.chubb@nicta.com.au> wrote:

...

...

...

...

"Jorge" == Jorge Ventura mailto:jorge.araujo.ventura@gmail.com> writes:

Jorge> I am trying to create a test for Jorge> beaglebone using the seL4test suite but I am having the Jorge> following error: Jorge> seL4Test/libs/libplatsupport/src/plat/am335x/dm.c:56:25: error: Jorge> ‘timer’ undeclared (first use in this function) dm_t *dm = Jorge> (dm_t *) timer->data; I don't think libplatsupport is finished for the Beaglebone. Even if you fix this error (not too difficult) you'll run into other issues =-- for instance the clock driver hasn't been finished. Here's a patch that'll get the timer compiling -- it's untested. diff --git a/src/plat/am335x/dm.c b/src/plat/am335x/dm.c index f49779a..b0adbaa 100644 --- a/src/plat/am335x/dm.c +++ b/src/plat/am335x/dm.c @@ -8,6 +8,7 @@ * @TAG(NICTA_BSD) */ +#include /* BIT() */ #include #include #include @@ -53,30 +54,35 @@ typedef volatile struct dm { static int dm_stop_timer(const pstimer_t *device) { - dm_t *dm = (dm_t *) timer->data; + dm_t *dm = (dm_t *) device->data; /* Disable timer. */ dm->tier = 0; dm->tclr = 0; dm->tisr = TISR_OVF_FLAG; + return 0; } static int dm_start_timer(const pstimer_t *device) { /* Do nothing */ + return 0; } static int -dm_periodic(uint64_t ns) +dm_periodic(const pstimer_t *timer, uint64_t ns) { + dm_t *dm = (dm_t *)timer->data; + /* Stop time. */ dm->tclr = 0; /* Reset timer. */ dm->cfg = TIOCP_CFG_SOFTRESET; - while (dm->cfg & TIOCP_CFG_SOFTRESET); + while (dm->cfg & TIOCP_CFG_SOFTRESET) + ; /* Enable interrupt on overflow. */ dm->tier = TIER_OVERFLOWENABLE; @@ -92,17 +98,19 @@ dm_periodic(uint64_t ns) /* Set autoreload and start the timer. */ dm->tclr = TCLR_AUTORELOAD | TCLR_STARTTIMER; + + return 0; } static int -dm_oneshot_absolute(uint64_t ns) +dm_oneshot_absolute(const pstimer_t *timer, uint64_t ns) { assert(!"Not implemented"); return ENOSYS; } static int -dm_oneshot_relative(uint64_t ns) +dm_oneshot_relative(const pstimer_t *timer, uint64_t ns) { assert(!"Not implemented"); return ENOSYS; @@ -115,13 +123,13 @@ dm_get_time(const pstimer_t *timer) { } static void -dm_handle_irq(const pstimer_t *timer) { +dm_handle_irq(const pstimer_t *timer, uint32_t irq) { /* nothing */ } static uint32_t dm_get_nth_irq(const pstimer_t *timer, uint32_t n) { - return DMTIMER2_INTTERRUPT; + return DMTIMER2_INTERRUPT; } static pstimer_t singleton_timer; @@ -131,15 +139,15 @@ dm_get_timer(void *vaddr) { pstimer_t *timer = &singleton_timer; - timer->properties.upcounter = false; + timer->properties.upcounter = 0; timer->properties.timeouts = 1; - timer->properties.bitwidth = 32; + timer->properties.bit_width = 32; timer->properties.irqs = 1; /* data just points to the dm itself for now */ timer->data = vaddr; - timer->start = dm_timer_start; - timer->stop = dm_timer_stop; + timer->start = dm_start_timer; + timer->stop = dm_stop_timer; timer->get_time = dm_get_time; timer->oneshot_absolute = dm_oneshot_absolute; timer->oneshot_relative = dm_oneshot_relative; _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.