Is it possible to build and run sel4-test against the "experimental" kernel tree? if so, whats the process?
On RefOS for my port, I'm seeing a weird problem with the timer code. It is mapping in the right phys addr for my timer device, and I can read the right ID register out, so it appears to be mapping the right memory, but the code to do a timer reset, which sets a reset bit then polls for the bit to return to zero, is getting stuck in an infinite loop. I verified that the loop isn't being altered by the compiler, and I verified that the same code runs fine in sel4 test. At this point I suspect one of two things 1) refos is allowing the mapping to happen with caching on (even though I asked it not to) or 2) something is wrong elsewhere with the "experimental" kernel (sel4-test is running on the "master" tree, and refos is using the kernel from the "experimental" tree).
is there anything else I could be missing? any thoughts?
Hi Tim,
It might take a little time to get back to you on this. RefOS was a student project, which means the more arcane low-level details tend to move on with the student. We'll do our best to answer questions, it just might take a little longer than I would like.
In general, I'd love to get RefOS moving again (I did not catch a student with it this semester). It was intended to be a "reference" example of a dynamic system on seL4. However, locally our limited resources are focussed on other priorities at the moment.
It does sound like a caching bug, as you allude to. I'll ask around on Monday and see if I can uncover anything helpful.
- Kevin
-----Original Message----- From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Tim Newsham Sent: Sunday, 15 March 2015 3:43 PM To: devel@sel4.systems Subject: [seL4] refos and sel4-test questions
Is it possible to build and run sel4-test against the "experimental" kernel tree? if so, whats the process?
On RefOS for my port, I'm seeing a weird problem with the timer code. It is mapping in the right phys addr for my timer device, and I can read the right ID register out, so it appears to be mapping the right memory, but the code to do a timer reset, which sets a reset bit then polls for the bit to return to zero, is getting stuck in an infinite loop. I verified that the loop isn't being altered by the compiler, and I verified that the same code runs fine in sel4 test. At this point I suspect one of two things
- refos is allowing the mapping to happen with caching on (even though I asked it not to) or
- something is wrong elsewhere with the "experimental" kernel (sel4-test is running on the "master" tree, and refos is using the kernel from the "experimental" tree).
is there anything else I could be missing? any thoughts?
-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
Devel mailing list 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.
Thank you, I tracked it down and it is indeed a caching problem. I'll submit patches after I work through some other bugs, but basically the caching flag got inverted in refos's device_io.c and later there's an exact match against DSPACE_FLAG_DEVICE_PADDR which should be a bit test instead, in data_syscall.c, which also needs to be fixed. I still have some timer bugs to work through, but these seem to be of my own doing :)
On Sat, Mar 14, 2015 at 7:45 PM, Kevin Elphinstone Kevin.Elphinstone@nicta.com.au wrote:
Hi Tim,
It might take a little time to get back to you on this. RefOS was a student project, which means the more arcane low-level details tend to move on with the student. We'll do our best to answer questions, it just might take a little longer than I would like.
In general, I'd love to get RefOS moving again (I did not catch a student with it this semester). It was intended to be a "reference" example of a dynamic system on seL4. However, locally our limited resources are focussed on other priorities at the moment.
It does sound like a caching bug, as you allude to. I'll ask around on Monday and see if I can uncover anything helpful.
- Kevin
-----Original Message----- From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Tim Newsham Sent: Sunday, 15 March 2015 3:43 PM To: devel@sel4.systems Subject: [seL4] refos and sel4-test questions
Is it possible to build and run sel4-test against the "experimental" kernel tree? if so, whats the process?
On RefOS for my port, I'm seeing a weird problem with the timer code. It is mapping in the right phys addr for my timer device, and I can read the right ID register out, so it appears to be mapping the right memory, but the code to do a timer reset, which sets a reset bit then polls for the bit to return to zero, is getting stuck in an infinite loop. I verified that the loop isn't being altered by the compiler, and I verified that the same code runs fine in sel4 test. At this point I suspect one of two things
- refos is allowing the mapping to happen with caching on (even though I asked it not to) or
- something is wrong elsewhere with the "experimental" kernel (sel4-test is running on the "master" tree, and refos is using the kernel from the "experimental" tree).
is there anything else I could be missing? any thoughts?
-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
Devel mailing list 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.
-
Kevin Elphinstone -
Tim Newsham -
Tim Newsham