sel4 for armv5 architecture

vibi sreenivasan

8 Nov 2015 8 Nov '15

7:33 a.m.

Hi, Can any one please let me know whether sel4 is supported on armv5 ? I am specifically looking to run sel4 on arm926ej. Thanks & Best Regards Vibi

Attachments:

attachment.html (text/html — 233 bytes)

Show replies by date

Adrian Danis

9 Nov 9 Nov

8:30 a.m.

Hi Vibi, seL4 does not currently support armv5. We had support on an experimental branch for some time, but we chose not to keep it. The main reason armv5 is not supported is seL4 does not handle the virtually addressed caches that armv5 platforms are allowed to use. This is in comparison to armv6 and armv7, where the programmer is allowed to assume that the cache behaves live a physically indexed cache. seL4 also uses instructions that are not part of the armv5 ISA. Equivalents exist, just a matter of crating multiple versions of the code. I do not know the details of the arm926ej, but if its cache architecture is compatible then porting should be just a matter of converting the newer instructions to armv5 equivalents. If the cache is virtual addressed then some more thought and additional cache operations need to be placed through the kernel. Adrian On Sun 08-Nov-2015 7:33 AM, vibi sreenivasan wrote: Hi, Can any one please let me know whether sel4 is supported on armv5 ? I am specifically looking to run sel4 on arm926ej. Thanks & Best Regards Vibi _______________________________________________ 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.

Gernot Heiser

12:05 p.m.

On 9 Nov 2015, at 8:30 , Adrian Danis mailto:Adrian.Danis@nicta.com.au> wrote: I do not know the details of the arm926ej, but if its cache architecture is compatible then porting should be just a matter of converting the newer instructions to armv5 equivalents. If the cache is virtual addressed then some more thought and additional cache operations need to be placed through the kernel. the ARM926ej has virtually-addressed caches from memory, so you’ll have to flush in every context switch, or implement the complex fast-address-space switching logic we did on L4-embedded. Gernot ________________________________ 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.

Raymond Jennings

12:12 p.m.

Can I say btw that virtually addressed caches stink? On Sun, Nov 8, 2015 at 5:05 PM, Gernot Heiser wrote:

...

On 9 Nov 2015, at 8:30 , Adrian Danis wrote:

I do not know the details of the arm926ej, but if its cache architecture is compatible then porting should be just a matter of converting the newer instructions to armv5 equivalents. If the cache is virtual addressed then some more thought and additional cache operations need to be placed through the kernel.

the ARM926ej has virtually-addressed caches from memory, so you’ll have to flush in every context switch, or implement the complex fast-address-space switching logic we did on L4-embedded.

Gernot

------------------------------

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.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Gernot Heiser

3:17 p.m.

...

On 9 Nov 2015, at 12:12 , Raymond Jennings wrote:

Can I say btw that virtually addressed caches stink?

Not really, they are fun, but not the sort of fun formal verification people like Gernot ________________________________ 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.

3328

Age (days ago)

3330

Last active (days ago)

List overview

Download

4 comments

4 participants

participants (4)

Adrian Danis
Gernot Heiser
Raymond Jennings
vibi sreenivasan