Re: [seL4] Hardware Platform for sel4 and running linux as guest os

So, there is no chance for running linux on top of sel4 on a beagleboard black? On Mon, Jan 4, 2016 at 4:30 PM, Peter Chubb wrote: > > "Andrea" == Andrea Sorbini writes: > > Andrea> I can confirm from experience that seL4 supports both serial >

Re: [seL4] seL4 & camkes questions

Ihor > > -- > Dr. Ihor Kuz > Senior Research Engineer | Trustworthy Systems > > DATA61 | CSIRO > E ihor@nicta.com.au T + 61 2 8306 0582 > Locked Bag 6016, UNSW, Sydney NSW 1466, Australia > www.data61.csiro.au > > CSIRO’s Digital Productivity business unit

Re: [seL4] Tutorial error

> 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 > > > On 23 Dec 2015, at 4:31 am, Julien Delange <julien.dela...@gmail.com&g

[seL4] Camkes dependencies & development environment

Dear all, First of all, sorry if this question has been asked several times already. I am currently trying to use sel4 & camkes on a debian stable. I installed all the dependencies but I am facing an error message when trying to build the tool (see below). My version of cabal is 1.20, so, version

[seL4] Tutorial error

Hello, I am trying to reproduce the tutorial. I followed the steps from the slides on https://github.com/seL4-projects/sel4-tutorials/blob/master/docs/seL4Tutorial.pdf When trying to compile, I got the following error in [1]. It seems to be a warning from the compiler, so, I edit the CFLAGS in

Re: [seL4] Camkes dependencies & development environment

Research Engineer | Trustworthy Systems > > DATA61 | CSIRO > E ihor@nicta.com.au 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 digita

Re: [seL4] CAmkES parsing issue

ed moving the import statements above the UART component > definition? > > Kent. > > On 11/06/2016, at 1:54 AM, Julien Delange <julien.dela...@gmail.com> > wrote: > > In fact, I do not have such a file. My assembly looks like this (see > below). I connect the hardware c

[seL4] Beaglebone black/CAmkES issue

I am using the second serial interface of the beaglebone black. According to the source code (in libsel4platsupport/plat_include/am335x/sel4platsupport/plat/hw/soc_AM335x.h), the address is 0x48022000). The following line is found in the source #define SOC_UART_1_REGS

Re: [seL4] Beaglebone black/CAmkES issue

/src/plat/am335x/machine/hardware.c > for this. > > On Fri, Jun 10, 2016 at 8:37 AM, Julien Delange <julien.dela...@gmail.com> > wrote: > >> I am using the second serial interface of the beaglebone black. According >> to the source code (in >> libsel4platsup

Re: [seL4] CAmkES parsing issue

this is set, but in this case it didn’t seem to be > any help. > > Kent. > > > On 11/06/2016, at 2:03 AM, Julien Delange <julien.dela...@gmail.com> > wrote: > > Yep. I tried many things in order to see where the mistake is or if there > are any parser limitatio

Re: [seL4] Beaglebone black/CAmkES issue

; *UART_REG(TLR) = 0x11; > > *UART_REG(MCR) = 0x00; > *UART_REG(FCR) = 0x07; > > > > > Jeffrey L. Hieb > Department of Engineering Fundamentals > University of Louisville > Louisville Kentucky 40292(502) 852 0465 > > On 6/10/2016 3:05 PM, Julien Delang

[seL4] CAmkES parsing issue

Hi, I am trying to build a camked application with a UART driver. When trying to build the application, I got the following error: While rendering uart_mem.from.source: 'drv' However, the component is well define. How can I try to get more information/debug of the camkes assembly and find out

Re: [seL4] Beaglebone black/CAmkES issue

> // config to fifo with interrupt but no DMA >> *UART_REG(LCR) = 0xBF; >> *UART_REG(EFR) = 0x10; >> *UART_REG(LCR) = 0x80; >> *UART_REG(SCR) = 0x01; >> *UART_REG(MCR) = 0x40; >> *UART_REG(TLR) = 0x11; >> >> *UAR

[seL4] RT branch questions

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

Re: [seL4] RT branch questions

, 2016 at 2:08 PM, Ihor Kuz UNSW <ihor@nicta.com.au> wrote: > > > On 27 May 2016, at 1:16 am, Julien Delange <julien.dela...@gmail.com> > wrote: > > > > I am currently trying the RT branch and have some questions: > > > > 1. What emulator to use

Re: [seL4] Will the codes in branch rt be merged into master

Last week, Ihor and Gernot said that they will merge the RT branch - I do not remember the date. There should be a white paper this week about the new features and how to use it. As far as I remember, the branch is working only on few architecture and works only on real hardware. Julien. On

Re: [seL4] Beaglebone black/CAmkES issue

If anyone is interested, I put something related on supporting the UART1 on the beaglebone here: http://julien.gunnm.org/geek/sel4/beaglebone%20black/2016/06/15/beaglebone-black-sel4-uart1/ On Mon, Jun 13, 2016 at 11:59 AM, Julien Delange <julien.dela...@gmail.com> wrote: > Hi all, &g

[seL4] handling timer with camkes

Dear all, I would like to build a scheduler on top of camkes. I figure that I have to get access to the timer irq and start from there (e.g. then, dispatch other tasks according to the number of elapsed ticks). I did find some relevant examples, especially in the camkes-vm (

Re: [seL4] handling timer with camkes

ve implemented for different > platforms. > > Cheers, > Siwei > > On Mon, Feb 15, 2016 at 02:20:01PM -0500, Julien Delange wrote: > #Dear all, > # > #I would like to build a scheduler on top of camkes. I figure that I have > to get > #access to the timer irq and s

Re: [seL4] handling timer with camkes

nd the actual driver implementation at, > > https://github.com/seL4/libplatsupport > > This library has all the drivers we have implemented for different > platforms. > > Cheers, > Siwei > > On Mon, Feb 15, 2016 at 02:20:01PM -0500, Julien Delange wrote: > #Dear all, > #

[seL4] Timer for AM335x

I am trying to develop a camkes application with one component having access to the timer. I got some inspiration from the time server for the kzm machine. Now, I am trying to port that to the am335x machine to execute on a beagleboard black. I dig into the code and found the appropriate

Re: [seL4] Timer for AM335x

ons exist in libplatsupport/src/plat/am335x/dm.c in > some source trees I have. (I don't have any experience with > camkes and never tried to build it for am335x...) > > On Wed, Feb 17, 2016 at 6:23 AM, Julien Delange <julien.dela...@gmail.com> > wrote: > >> I am trying to develop

Re: [seL4] seL4 Tutorial Idea

1. The tutorials from the dev days already contain a lot of things. Check it and try. The main issue is that sometimes, they are out of date so that you might reach out to the NICTA folks and/or issue a bug report. 2. There are some work you can take. For example rust for sel4 (

Re: [seL4] using camkesvm with qemu

he region = 2^n bytes. > > Adrian > > On Thu 10-Mar-2016 7:26 AM, Corey Richardson wrote: > > On Wed, Mar 09, 2016 at 03:10:58PM -0500, Julien Delange wrote: > > Any idea about how to run this example with qemu and/or how to test it? > > > Assuming you're on Linu

[seL4] sel4 job offer

For information, we are looking for people to work on sel4. See https://www.appone.com/maininforeq.asp?Ad=250944_ID=1243309=http://sei.cmu.edu/careers/_ID=44 If you have any question, do not hesitate to contact me and/or apply! Julien. ___ Devel

Re: [seL4] Getting timer info from seL4 kernel

problem you identify with interrupt latencies and acknowledgment is > inherent in any partitioning approach, there’s no way around. > > Gernot > > On 17 May 2016, at 1:28 , Julien Delange <julien.dela...@gmail.com> wrote: > > I assume this can be an issue when you are man