Thanks all! Is it possible to send the white paper on this mailing-list once it is done?
Reading at the manual, there are still some unclear behavior: how the signals are managed (e.g. what happens when issuing a seL4_Wait/seL4_Signal() between threads having different criticality which then raise the question of priority inversion and impact on budgets), how one can design a fixed timelime schedule with several timeslices per threads (as in ARINC653/MILS kernels). Anyway, I will wait the white paper, it will probably address most (if not all) these questions! Julien. On Thu, May 26, 2016 at 2:08 PM, Ihor Kuz UNSW <[email protected]> wrote: > > > On 27 May 2016, at 1:16 am, Julien Delange <[email protected]> > wrote: > > > > I am currently trying the RT branch and have some questions: > > > > 1. What emulator to use in order to try the examples? I am trying to use > x86 with qemu but it seems that it does not work. I got the following trace > at execution > > > > Starting node #0 > > APIC: unsupported platform, TSC-deadline mode is not supported > > seL4 called fail at > /home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in > function boot_sys, saying "boot_sys failed for some reason :( > > > > So, is there an emulator (for any supported platform) to try it? > > So far the RT kernel only works on actual hardware. > > Emulators don’t have accurate timing, and so it hasn’t been interesting > for us to make it work on them. Of course for development, using an > emulator would be useful, so it’s in our plan to add qemu support, but not > a top priority at the moment. Doing so would basically require adding an > appropriate kernel driver for the timer provided by the emulator. > > Ihor > > -- > Dr. Ihor Kuz > Senior Research Engineer | Trustworthy Systems | DATA61 | CSIRO > Conjoint Senior Lecturer | CSE | UNSW > E [email protected] T + 61 2 8306 0582 > Locked Bag 6016, UNSW, Sydney NSW 1466, Australia > www.data61.csiro.au > > CSIRO’s Digital Productivity business unit and NICTA have joined forces to > create digital powerhouse Data61 > > > ________________________________ > > 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 [email protected] https://sel4.systems/lists/listinfo/devel
