Re: [seL4] Deriving and Revoking IRQControl caps

[Andrew Gacek]

I have no idea how seL4 tracks derivations, but how reasonable is an
answer like 'infinity'? Is anything in seL4 tracked to infinity? How
far are untypeds tracked?

-Andrew

On Wed, Feb 15, 2017 at 5:49 PM,  <gernot.hei...@data61.csiro.au> wrote:
> Andrew’s use case makes sense to me at first glance.
>
> I think IRQ caps are special in a way here, as there is a difference to other 
> derived caps: A cap for a single IRQ is logically a top-level cap, similar to 
> a frame cap. This present model basically means that you can’t delegate them, 
> unlike other objects. Seems like a weakness (if not conceptual inconsistency) 
> in our present model.
>
> As Gerwin indicates, just moving to two levels is not necessarily a good 
> solution. I tend to think that the only valid magic numbers are zero, one, 
> and infinity ;-)
>
> Gernot
>
>> On 16 Feb 2017, at 10:31, gerwin.kl...@data61.csiro.au wrote:
>>
>> Currently, this is mostly implementation driven - there is one bit reserved 
>> for the derivation level in the data structure that tracks it. It’s possible 
>> that IRQControl caps specifically have some space left that could be used 
>> for more levels, but it would make them a special case.
>>
>> If we reserved 2 bits for the level, you’d hit the same problem somewhat 
>> later, though, and the argument at the time was that (very small) finiteness 
>> of derivation levels of these control caps has to be solved at user level 
>> anyway and it’s better to make you think of it immediately rather than when 
>> you’ve designed yourself into a corner.
>>
>> Maybe you do have a very good use case here, though, and we should rethink 
>> that argument (as we did for endpoint caps - their level of specialness is 
>> pretty messy, but we considered it worth the pain). I should probably leave 
>> that part to Kevin.
>>
>> Cheers,
>> Gerwin
>>
>>> On 16.02.2017, at 03:20, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>>>
>>> Based on the seL4 manual it sounds like IRQControl caps only support
>>> one level of derivation. What is the reason for this restriction? We
>>> encountered a case where we wanted to hand out an IRQControl for a
>>> specific irq and then later revoke access, but we couldn't do it
>>> because the IRQControl for a specific irq is already a derived
>>> capability.
>>>
>>> -Andrew
>>>
>>> ___
>>> Devel mailing list
>>> Devel@sel4.systems
>>> https://sel4.systems/lists/listinfo/devel
>>
>> ___
>> Devel mailing list
>> Devel@sel4.systems
>> https://sel4.systems/lists/listinfo/devel
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

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

[seL4] Deriving and Revoking IRQControl caps

[Andrew Gacek]

Based on the seL4 manual it sounds like IRQControl caps only support
one level of derivation. What is the reason for this restriction? We
encountered a case where we wanted to hand out an IRQControl for a
specific irq and then later revoke access, but we couldn't do it
because the IRQControl for a specific irq is already a derived
capability.

-Andrew

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

Re: [seL4] seL4 System Utilization / Benchmark

[Andrew Gacek]

Thanks Hesham. I also had an issue when I compiled for the Jetson Tegra K1:

 [CC] kernel_final.s
In file included from
/home/ajgacek/phase3-workspace/camkes/kernel/include/arch/arm/arch/32/mode/machine.h:19:0,
 from
/home/ajgacek/phase3-workspace/camkes/kernel/include/machine.h:17,
 from
/home/ajgacek/phase3-workspace/camkes/kernel/include/api/syscall.h:14,
 from
/home/ajgacek/phase3-workspace/camkes/kernel/src/api/faults.c:16:
/home/ajgacek/phase3-workspace/camkes/kernel/include/plat/tk1/plat/machine/hardware.h:
In function 'handleReservedIRQ':
/home/ajgacek/phase3-workspace/camkes/kernel/include/plat/tk1/plat/machine/hardware.h:157:9:
error: implicit declaration of function 'handleOverflowIRQ'
[-Werror=implicit-function-declaration]
 handleOverflowIRQ();
 ^
/home/ajgacek/phase3-workspace/camkes/kernel/include/plat/tk1/plat/machine/hardware.h:157:9:
error: nested extern declaration of 'handleOverflowIRQ'
[-Werror=nested-externs]
cc1: all warnings being treated as errors
/home/ajgacek/phase3-workspace/camkes/kernel/Makefile:611: recipe for
target 'kernel_final.s' failed
make[1]: *** [kernel_final.s] Error 1
tools/common/project.mk:254: recipe for target 'kernel_elf' failed
make: *** [kernel_elf] Error 2

On Thu, Jan 19, 2017 at 12:20 AM,  <hesham.almat...@data61.csiro.au> wrote:
> Hi Andrew,
>
> Thanks for reporting this. This issue only exists for KZM/ARMv6. I submitted 
> a fix internally (1d8be141afa). Should be pushed to github by tomorrow.
>
> Cheers,
>
> Hesham
> ____
> From: Andrew Gacek <andrew.ga...@gmail.com>
> Sent: Thursday, January 19, 2017 9:18 AM
> To: Almatary, Hesham (Data61, Kensington NSW)
> Cc: devel@sel4.systems
> Subject: Re: [seL4] seL4 System Utilization / Benchmark
>
> Hi Hesham,
>
> I am using the master branch of seL4 which includes that commit.
> Here's how to duplicate the error:
>
> repo init -u https://github.com/seL4/camkes-manifest.git
> repo sync
> make arm_simple_defconfig
> make menuconfig # enable benchmarks
> make
>
> On Wed, Jan 18, 2017 at 4:11 PM,  <hesham.almat...@data61.csiro.au> wrote:
>> Hi Andrew,
>>
>> Regarding the error you get when you enable benchmarks, which kernel 
>> revision are you using?
>> This error should be fixed after this commit (530852b) [1].
>>
>> [1] 
>> https://github.com/seL4/seL4/commit/530852bbdc31b7bbc2ba920c4299714896ba0cd4
>>
>> Cheers,
>> Hesham
>> 
>> From: Devel <devel-bounces@sel4.systems> on behalf of Andrew Gacek 
>> <andrew.ga...@gmail.com>
>> Sent: Thursday, January 19, 2017 8:17 AM
>> To: Kuz, Ihor (Data61, Kensington NSW)
>> Cc: Danis, Adrian (Data61, Kensington NSW); devel@sel4.systems
>> Subject: Re: [seL4] seL4 System Utilization / Benchmark
>>
>> Thanks again Adrian and Ihor for the help. I was able to get something
>> working which was good enough for my needs.
>>
>> In case anybody else is interested, I made a small change to the
>> kernel to get the TCB names back from
>> seL4_SysBenchmarkGetThreadUtilisation():
>>
>>   
>> https://github.com/agacek/seL4/commit/d46d8bda0de9f359ddd5a121072da8fbd78dd5e0#diff-552047e74fda361e39f4612989dc0acf
>>
>> I modified camkes to give a component called 'perfmon' access to all TCB 
>> caps:
>>
>>   
>> https://github.com/agacek/camkes-tool/commit/4a1c21f441ce0fa57879c29756e4908cfe58c7ce
>>
>> Then I created a user space perfmon component which would generate a
>> report when requested:
>>
>>   
>> https://github.com/smaccm/smaccm/commit/1eb9c5ce4cb1cb5475de7f832a1b69065f1e9946
>>
>> Most of this is brittle and hacked together of course, but it was good
>> enough for me to see how much of the CPU each component was using.
>> Here's some sample output from my application:
>>
>> 86.3%   Virtual_Machine_inst.vm_shim_obj(1) (cap 0x22)
>> 2.8%CAN_Driver_inst.spi_obj(5) (cap 0x37)
>> 2.2%CAN_Driver_inst.spi_obj(7) (cap 0x26)
>> 1.3%dispatch_periodic_inst(3) (cap 0x21)
>> 1.1%CAN_Driver_inst.gpio_obj(7) (cap 0x17)
>> 0.7%UART_Driver_inst.uart_shim_obj(6) (cap 0x42)
>> 0.7%time_server.time_server(8) (cap 0x3e)
>> 0.6%CAN_Framing_inst(9) (cap 0x28)
>> 0.6%Decrypt_inst(7) (cap 0x2d)
>> ...
>>
>> -Andrew
>>
>> On Wed, Jan 18, 2017 at 8:16 AM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>>> I got an error when enabling benchmarking:
>>>
>>> /home/ajgacek/phase3-wo

Re: [seL4] seL4 System Utilization / Benchmark

[Andrew Gacek]

Hi Hesham,

I am using the master branch of seL4 which includes that commit.
Here's how to duplicate the error:

repo init -u https://github.com/seL4/camkes-manifest.git
repo sync
make arm_simple_defconfig
make menuconfig # enable benchmarks
make

On Wed, Jan 18, 2017 at 4:11 PM,  <hesham.almat...@data61.csiro.au> wrote:
> Hi Andrew,
>
> Regarding the error you get when you enable benchmarks, which kernel revision 
> are you using?
> This error should be fixed after this commit (530852b) [1].
>
> [1] 
> https://github.com/seL4/seL4/commit/530852bbdc31b7bbc2ba920c4299714896ba0cd4
>
> Cheers,
> Hesham
> 
> From: Devel <devel-bounces@sel4.systems> on behalf of Andrew Gacek 
> <andrew.ga...@gmail.com>
> Sent: Thursday, January 19, 2017 8:17 AM
> To: Kuz, Ihor (Data61, Kensington NSW)
> Cc: Danis, Adrian (Data61, Kensington NSW); devel@sel4.systems
> Subject: Re: [seL4] seL4 System Utilization / Benchmark
>
> Thanks again Adrian and Ihor for the help. I was able to get something
> working which was good enough for my needs.
>
> In case anybody else is interested, I made a small change to the
> kernel to get the TCB names back from
> seL4_SysBenchmarkGetThreadUtilisation():
>
>   
> https://github.com/agacek/seL4/commit/d46d8bda0de9f359ddd5a121072da8fbd78dd5e0#diff-552047e74fda361e39f4612989dc0acf
>
> I modified camkes to give a component called 'perfmon' access to all TCB caps:
>
>   
> https://github.com/agacek/camkes-tool/commit/4a1c21f441ce0fa57879c29756e4908cfe58c7ce
>
> Then I created a user space perfmon component which would generate a
> report when requested:
>
>   
> https://github.com/smaccm/smaccm/commit/1eb9c5ce4cb1cb5475de7f832a1b69065f1e9946
>
> Most of this is brittle and hacked together of course, but it was good
> enough for me to see how much of the CPU each component was using.
> Here's some sample output from my application:
>
> 86.3%   Virtual_Machine_inst.vm_shim_obj(1) (cap 0x22)
> 2.8%CAN_Driver_inst.spi_obj(5) (cap 0x37)
> 2.2%CAN_Driver_inst.spi_obj(7) (cap 0x26)
> 1.3%dispatch_periodic_inst(3) (cap 0x21)
> 1.1%CAN_Driver_inst.gpio_obj(7) (cap 0x17)
> 0.7%UART_Driver_inst.uart_shim_obj(6) (cap 0x42)
> 0.7%time_server.time_server(8) (cap 0x3e)
> 0.6%CAN_Framing_inst(9) (cap 0x28)
> 0.6%Decrypt_inst(7) (cap 0x2d)
> ...
>
> -Andrew
>
> On Wed, Jan 18, 2017 at 8:16 AM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>> I got an error when enabling benchmarking:
>>
>> /home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:
>> In function 'handleOverflowIRQ':
>> /home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:22:9:
>> error: implicit declaration of function 'armv_handleOverflowIRQ'
>> [-Werror=implicit-function-declaration]
>>  armv_handleOverflowIRQ();
>>  ^
>> /home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:22:9:
>> error: nested extern declaration of 'armv_handleOverflowIRQ'
>> [-Werror=nested-externs]
>>
>> I'll just hack around it, but I thought you guys would want to know.
>>
>> -Andrew
>>
>> On Tue, Jan 17, 2017 at 9:04 PM,  <ihor@data61.csiro.au> wrote:
>>> You should be able to call seL4 syscalls from a CAmkES component. Just 
>>> include the right headers (and link the library if necesary).
>>>
>>> Note that if the syscalls require caps, then you are on your own wrt how to 
>>> get the caps.
>>>
>>> Ihor
>>>
>>>> On 18 Jan 2017, at 12:29 pm, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>>>>
>>>> Thanks Adrian. This is a useful start. It sounds like the easiest
>>>> thing may be to overwrite some syscall that I don't use to loop over
>>>> all the threads in the kernel and print out their debugging info.
>>>>
>>>> Also, I've never called raw seL4 system calls from a camkes component
>>>> before. Is it just a matter of calling seL4_BenchmarkResetLog() or
>>>> seL4_BenchmarkFinalizeLog() directly in the control code for one of my
>>>> components?
>>>>
>>>> -Andrew
>>>>
>>>> On Tue, Jan 17, 2017 at 7:23 PM,  <adrian.da...@data61.csiro.au> wrote:
>>>>> Hi Andrew,
>>>>>
>>>>> There is some code already in the kernel to help you do this, although it 
>>>>> is
>>>>> tested an

Re: [seL4] seL4 System Utilization / Benchmark

[Andrew Gacek]

Thanks again Adrian and Ihor for the help. I was able to get something
working which was good enough for my needs.

In case anybody else is interested, I made a small change to the
kernel to get the TCB names back from
seL4_SysBenchmarkGetThreadUtilisation():

  
https://github.com/agacek/seL4/commit/d46d8bda0de9f359ddd5a121072da8fbd78dd5e0#diff-552047e74fda361e39f4612989dc0acf

I modified camkes to give a component called 'perfmon' access to all TCB caps:

  
https://github.com/agacek/camkes-tool/commit/4a1c21f441ce0fa57879c29756e4908cfe58c7ce

Then I created a user space perfmon component which would generate a
report when requested:

  
https://github.com/smaccm/smaccm/commit/1eb9c5ce4cb1cb5475de7f832a1b69065f1e9946

Most of this is brittle and hacked together of course, but it was good
enough for me to see how much of the CPU each component was using.
Here's some sample output from my application:

86.3%   Virtual_Machine_inst.vm_shim_obj(1) (cap 0x22)
2.8%CAN_Driver_inst.spi_obj(5) (cap 0x37)
2.2%CAN_Driver_inst.spi_obj(7) (cap 0x26)
1.3%dispatch_periodic_inst(3) (cap 0x21)
1.1%CAN_Driver_inst.gpio_obj(7) (cap 0x17)
0.7%UART_Driver_inst.uart_shim_obj(6) (cap 0x42)
0.7%time_server.time_server(8) (cap 0x3e)
0.6%CAN_Framing_inst(9) (cap 0x28)
0.6%Decrypt_inst(7) (cap 0x2d)
...

-Andrew

On Wed, Jan 18, 2017 at 8:16 AM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
> I got an error when enabling benchmarking:
>
> /home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:
> In function 'handleOverflowIRQ':
> /home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:22:9:
> error: implicit declaration of function 'armv_handleOverflowIRQ'
> [-Werror=implicit-function-declaration]
>  armv_handleOverflowIRQ();
>  ^
> /home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:22:9:
> error: nested extern declaration of 'armv_handleOverflowIRQ'
> [-Werror=nested-externs]
>
> I'll just hack around it, but I thought you guys would want to know.
>
> -Andrew
>
> On Tue, Jan 17, 2017 at 9:04 PM,  <ihor@data61.csiro.au> wrote:
>> You should be able to call seL4 syscalls from a CAmkES component. Just 
>> include the right headers (and link the library if necesary).
>>
>> Note that if the syscalls require caps, then you are on your own wrt how to 
>> get the caps.
>>
>> Ihor
>>
>>> On 18 Jan 2017, at 12:29 pm, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>>>
>>> Thanks Adrian. This is a useful start. It sounds like the easiest
>>> thing may be to overwrite some syscall that I don't use to loop over
>>> all the threads in the kernel and print out their debugging info.
>>>
>>> Also, I've never called raw seL4 system calls from a camkes component
>>> before. Is it just a matter of calling seL4_BenchmarkResetLog() or
>>> seL4_BenchmarkFinalizeLog() directly in the control code for one of my
>>> components?
>>>
>>> -Andrew
>>>
>>> On Tue, Jan 17, 2017 at 7:23 PM,  <adrian.da...@data61.csiro.au> wrote:
>>>> Hi Andrew,
>>>>
>>>> There is some code already in the kernel to help you do this, although it 
>>>> is
>>>> tested and fixed on an as used basis so may or may not work as I describe.
>>>> You can enable the the thread utilization tracking with
>>>> make menuconfig -> seL4 Kernel -> Build Options -> Enable benchmarks ->
>>>> Track threads and kernel utilisation time
>>>> Once enabled you gain the following relevant functions
>>>>
>>>> seL4_BenchmarkResetLog()
>>>> Reset idle time and total run time and start capturing utilization
>>>> information
>>>>
>>>> seL4_BenchmarkFinalizeLog()
>>>> Calculate idle time, total run time and stop capturing utilization
>>>> information
>>>>
>>>> seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
>>>> Retrieve the utilization for a particular thread where
>>>> seL4_GetMR(0) == Thread utilization (in cycles) of this (tcb_cptr) thread
>>>> seL4_GetMR(1) == Idle thread utilization (in cycles) between the last call
>>>> to Reset and Finalize log
>>>> seL4_GetMR(2) == Totall execution time (in cycles) between the last call to
>>>> Reset and Finalize log
>>>>
>>>> seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
>>>> Reset the utilization of this thread.
>>>&

Re: [seL4] seL4 System Utilization / Benchmark

[Andrew Gacek]

I got an error when enabling benchmarking:

/home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:
In function 'handleOverflowIRQ':
/home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:22:9:
error: implicit declaration of function 'armv_handleOverflowIRQ'
[-Werror=implicit-function-declaration]
 armv_handleOverflowIRQ();
 ^
/home/ajgacek/phase3-workspace/perf/kernel/include/arch/arm/arch/benchmark_overflowHandler.h:22:9:
error: nested extern declaration of 'armv_handleOverflowIRQ'
[-Werror=nested-externs]

I'll just hack around it, but I thought you guys would want to know.

-Andrew

On Tue, Jan 17, 2017 at 9:04 PM,  <ihor@data61.csiro.au> wrote:
> You should be able to call seL4 syscalls from a CAmkES component. Just 
> include the right headers (and link the library if necesary).
>
> Note that if the syscalls require caps, then you are on your own wrt how to 
> get the caps.
>
> Ihor
>
>> On 18 Jan 2017, at 12:29 pm, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>>
>> Thanks Adrian. This is a useful start. It sounds like the easiest
>> thing may be to overwrite some syscall that I don't use to loop over
>> all the threads in the kernel and print out their debugging info.
>>
>> Also, I've never called raw seL4 system calls from a camkes component
>> before. Is it just a matter of calling seL4_BenchmarkResetLog() or
>> seL4_BenchmarkFinalizeLog() directly in the control code for one of my
>> components?
>>
>> -Andrew
>>
>> On Tue, Jan 17, 2017 at 7:23 PM,  <adrian.da...@data61.csiro.au> wrote:
>>> Hi Andrew,
>>>
>>> There is some code already in the kernel to help you do this, although it is
>>> tested and fixed on an as used basis so may or may not work as I describe.
>>> You can enable the the thread utilization tracking with
>>> make menuconfig -> seL4 Kernel -> Build Options -> Enable benchmarks ->
>>> Track threads and kernel utilisation time
>>> Once enabled you gain the following relevant functions
>>>
>>> seL4_BenchmarkResetLog()
>>> Reset idle time and total run time and start capturing utilization
>>> information
>>>
>>> seL4_BenchmarkFinalizeLog()
>>> Calculate idle time, total run time and stop capturing utilization
>>> information
>>>
>>> seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
>>> Retrieve the utilization for a particular thread where
>>> seL4_GetMR(0) == Thread utilization (in cycles) of this (tcb_cptr) thread
>>> seL4_GetMR(1) == Idle thread utilization (in cycles) between the last call
>>> to Reset and Finalize log
>>> seL4_GetMR(2) == Totall execution time (in cycles) between the last call to
>>> Reset and Finalize log
>>>
>>> seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
>>> Reset the utilization of this thread.
>>>
>>> The main problem with this API is that it requires you to have caps to all
>>> the threads you wish to get the information of, which in CAmkES is generally
>>> only the capdl-loader application. It is also designed with the idea that
>>> you want to reset the utilization counts at the point you're querying them,
>>> i.e. you're doing some kind of benchmark and you just want utilization over
>>> that benchmark.
>>>
>>> Hope this provides some use to you.
>>>
>>> Adrian
>>>
>>>
>>> On Wed 18-Jan-2017 9:59 AM, Andrew Gacek wrote:
>>>
>>> Hi,
>>>
>>> I'm interested in seeing how much of the CPU is being used by the
>>> various threads in my (camkes) application. I'd like a simple "Task
>>> Manager" style report of the form:
>>>
>>> 70% idle
>>> 25% can_obj_7_0_control_9_tcb
>>> 5% can_obj_7_Int_3__tcb
>>> 0% can_obj_7_0_fault_handler_15_
>>> _tcb
>>> etc
>>>
>>> I've tried poking around libsel4bench, but I don't see any obvious way
>>> of benchmarking the whole system. From what I can tell, it's mostly
>>> designed to get cycle counts from specific code segments. Is that
>>> right? What's the best way to go about benchmarking the whole system?
>>> It's only for debugging, so I'm willing to make some quick-and-dirty
>>> changes to the kernel just to see the results.
>>>
>>> Thanks,
>>> Andrew
>>>
>>> ___
>>> Devel mailing list
>>> Devel@sel4.systems
>>> https://sel4.systems/lists/listinfo/devel
>>>
>>>
>>
>> ___
>> Devel mailing list
>> Devel@sel4.systems
>> https://sel4.systems/lists/listinfo/devel
>

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

Re: [seL4] seL4 System Utilization / Benchmark

[Andrew Gacek]

Actually, is there any easy way to get all TCBs even from within the
kernel? I see ksReadyQueues has all the runnable TCBs, but what about
the rest?

-Andrew

On Tue, Jan 17, 2017 at 7:29 PM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
> Thanks Adrian. This is a useful start. It sounds like the easiest
> thing may be to overwrite some syscall that I don't use to loop over
> all the threads in the kernel and print out their debugging info.
>
> Also, I've never called raw seL4 system calls from a camkes component
> before. Is it just a matter of calling seL4_BenchmarkResetLog() or
> seL4_BenchmarkFinalizeLog() directly in the control code for one of my
> components?
>
> -Andrew
>
> On Tue, Jan 17, 2017 at 7:23 PM,  <adrian.da...@data61.csiro.au> wrote:
>> Hi Andrew,
>>
>> There is some code already in the kernel to help you do this, although it is
>> tested and fixed on an as used basis so may or may not work as I describe.
>> You can enable the the thread utilization tracking with
>> make menuconfig -> seL4 Kernel -> Build Options -> Enable benchmarks ->
>> Track threads and kernel utilisation time
>> Once enabled you gain the following relevant functions
>>
>> seL4_BenchmarkResetLog()
>> Reset idle time and total run time and start capturing utilization
>> information
>>
>> seL4_BenchmarkFinalizeLog()
>> Calculate idle time, total run time and stop capturing utilization
>> information
>>
>> seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
>> Retrieve the utilization for a particular thread where
>> seL4_GetMR(0) == Thread utilization (in cycles) of this (tcb_cptr) thread
>> seL4_GetMR(1) == Idle thread utilization (in cycles) between the last call
>> to Reset and Finalize log
>> seL4_GetMR(2) == Totall execution time (in cycles) between the last call to
>> Reset and Finalize log
>>
>> seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
>> Reset the utilization of this thread.
>>
>> The main problem with this API is that it requires you to have caps to all
>> the threads you wish to get the information of, which in CAmkES is generally
>> only the capdl-loader application. It is also designed with the idea that
>> you want to reset the utilization counts at the point you're querying them,
>> i.e. you're doing some kind of benchmark and you just want utilization over
>> that benchmark.
>>
>> Hope this provides some use to you.
>>
>> Adrian
>>
>>
>> On Wed 18-Jan-2017 9:59 AM, Andrew Gacek wrote:
>>
>> Hi,
>>
>> I'm interested in seeing how much of the CPU is being used by the
>> various threads in my (camkes) application. I'd like a simple "Task
>> Manager" style report of the form:
>>
>> 70% idle
>> 25% can_obj_7_0_control_9_tcb
>> 5% can_obj_7_Int_3__tcb
>> 0% can_obj_7_0_fault_handler_15_
>> _tcb
>> etc
>>
>> I've tried poking around libsel4bench, but I don't see any obvious way
>> of benchmarking the whole system. From what I can tell, it's mostly
>> designed to get cycle counts from specific code segments. Is that
>> right? What's the best way to go about benchmarking the whole system?
>> It's only for debugging, so I'm willing to make some quick-and-dirty
>> changes to the kernel just to see the results.
>>
>> Thanks,
>> Andrew
>>
>> ___
>> Devel mailing list
>> Devel@sel4.systems
>> https://sel4.systems/lists/listinfo/devel
>>
>>

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

[seL4] seL4 System Utilization / Benchmark

[Andrew Gacek]

Hi,

I'm interested in seeing how much of the CPU is being used by the
various threads in my (camkes) application. I'd like a simple "Task
Manager" style report of the form:

70% idle
25% can_obj_7_0_control_9_tcb
5% can_obj_7_Int_3__tcb
0% can_obj_7_0_fault_handler_15__tcb
etc

I've tried poking around libsel4bench, but I don't see any obvious way
of benchmarking the whole system. From what I can tell, it's mostly
designed to get cycle counts from specific code segments. Is that
right? What's the best way to go about benchmarking the whole system?
It's only for debugging, so I'm willing to make some quick-and-dirty
changes to the kernel just to see the results.

Thanks,
Andrew

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

Re: [seL4] seL4 on Zinq7000 on QEMU

[Andrew Gacek]

Ok thanks. I've created a pull request for this change:

  https://github.com/seL4/seL4_tools/pull/2

-Andrew

On Tue, Dec 6, 2016 at 5:58 PM,  <alexander.k...@data61.csiro.au> wrote:
> Hi Andrew,
>
> Nice find! U-boot obviously performs some initialisation of the UART on
> our behalf, hence we have not had problems when testing on real
> hardware.
>
> The correct place would be here:
> https://github.com/seL4/seL4_tools/blob/2.0.x-compatible/elfloader-tool/src/arch-arm/plat-zynq7000/platform_init.c#L72
>
> But, it should call out to a dedicated init function in sys_fputc.c
>
> The call to platform_init() would also need to occur a few lines
> earlier, before the first printf:
> https://github.com/seL4/seL4_tools/blob/2.0.x-compatible/elfloader-tool/src/arch-arm/boot.c#L81
>
>  - Alex
>
>
> On Tue, 2016-12-06 at 16:35 -0600, Andrew Gacek wrote:
>> I've found the problem. First, the default UART for zynq7000 is the
>> second one, so I need to run qemu like this:
>>
>>   qemu-system-arm -M xilinx-zynq-a9 -kernel
>> images/capdl-loader-experimental-image-arm-zynq7000 -m size=512M
>> -monitor none -nographic -serial /dev/null -serial stdio
>>
>> Second, the Zynq7000 uart needs to be explicitly enabled. This is done
>> by clearing bit 5 and setting bit 4 of the control register. It looks
>> like seL4 and related tools are not doing this. For now I've done this
>> by modifying
>>
>>   tools/elfloader/src/arch-arm/plat-zynq7000/sys_fputc.c
>>
>> to add
>>
>>uint32_t v = *UART_REG(UART_CONTROL);
>> v |= (1 << 4);
>> v &= ~(1 << 5);
>> *UART_REG(UART_CONTROL) = v;
>>
>> to the __fputc function.
>>
>> This clearly isn't the right spot for it. Where should such initial
>> configuration be done?
>>
>> -Andrew
>>
>>
>> On Tue, Dec 6, 2016 at 3:33 PM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>> > If I suspend the execution in QEMU, the program counter is at
>> > 0xe00108ec. In the kernel, that is the  method. So
>> > perhaps the system is running, but I'm just not able to see any output
>> > from the elfloader, kernel, etc.
>> >
>> > -Andrew
>> >
>> > On Tue, Dec 6, 2016 at 2:49 PM, Andrew Gacek <andrew.ga...@gmail.com> 
>> > wrote:
>> >> Thanks Alex. That fixes the crash. Now the system runs but just seems
>> >> to hang without doing anything. I don't get any output at all (whereas
>> >> the kzm version spews out a ton of messages). In 'top' I can see it's
>> >> using about 3% cpu so it's something, though it's not clear what. It's
>> >> hard for me to tell. Perhaps the UART for the console isn't working
>> >> correctly?
>> >>
>> >> -Andrew
>> >>
>> >> On Tue, Dec 6, 2016 at 2:46 PM,  <alexander.k...@data61.csiro.au> wrote:
>> >>> Hi Andrew,
>> >>>
>> >>> It could be because QEMU does not know how much RAM is available.
>> >>> Could you try adding "-m size=512M" to your arguments?
>> >>>
>> >>>  - Alex
>> >>>
>> >>> 
>> >>> From: Devel <devel-bounces@sel4.systems> on behalf of Andrew Gacek 
>> >>> <andrew.ga...@gmail.com>
>> >>> Sent: Wednesday, December 7, 2016 2:23 AM
>> >>> To: devel@sel4.systems
>> >>> Subject: [seL4] seL4 on Zinq7000 on QEMU
>> >>>
>> >>> I'm trying to build and emulate a version of seL4 for the zinq7000
>> >>> platform, but it crashes immediately.
>> >>>
>> >>> I've started by taking the camkes tutorial and building it for zinq7000:
>> >>>
>> >>>   repo init -u https://github.com/seL4/camkes-manifest.git
>> >>>   repo sync
>> >>>   make arm_simple_defconfig
>> >>>   make menuconfig # change seL4 platform to zinq7000
>> >>>   make
>> >>>
>> >>> When I try to emulate it, it crashes right away:
>> >>>
>> >>>   qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel
>> >>> images/capdl-loader-experimental-image-arm-zynq7000
>> >>>
>> >>> qemu: fatal: Trying to execute code outside RAM or ROM at 0x1000
>> >>>
>> >>> R00= R01= R02= R03=
>> >>> R04= R05= R06= R07=
>> >>> R0

Re: [seL4] seL4 on Zinq7000 on QEMU

[Andrew Gacek]

I've found the problem. First, the default UART for zynq7000 is the
second one, so I need to run qemu like this:

  qemu-system-arm -M xilinx-zynq-a9 -kernel
images/capdl-loader-experimental-image-arm-zynq7000 -m size=512M
-monitor none -nographic -serial /dev/null -serial stdio

Second, the Zynq7000 uart needs to be explicitly enabled. This is done
by clearing bit 5 and setting bit 4 of the control register. It looks
like seL4 and related tools are not doing this. For now I've done this
by modifying

  tools/elfloader/src/arch-arm/plat-zynq7000/sys_fputc.c

to add

   uint32_t v = *UART_REG(UART_CONTROL);
v |= (1 << 4);
v &= ~(1 << 5);
*UART_REG(UART_CONTROL) = v;

to the __fputc function.

This clearly isn't the right spot for it. Where should such initial
configuration be done?

-Andrew


On Tue, Dec 6, 2016 at 3:33 PM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
> If I suspend the execution in QEMU, the program counter is at
> 0xe00108ec. In the kernel, that is the  method. So
> perhaps the system is running, but I'm just not able to see any output
> from the elfloader, kernel, etc.
>
> -Andrew
>
> On Tue, Dec 6, 2016 at 2:49 PM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
>> Thanks Alex. That fixes the crash. Now the system runs but just seems
>> to hang without doing anything. I don't get any output at all (whereas
>> the kzm version spews out a ton of messages). In 'top' I can see it's
>> using about 3% cpu so it's something, though it's not clear what. It's
>> hard for me to tell. Perhaps the UART for the console isn't working
>> correctly?
>>
>> -Andrew
>>
>> On Tue, Dec 6, 2016 at 2:46 PM,  <alexander.k...@data61.csiro.au> wrote:
>>> Hi Andrew,
>>>
>>> It could be because QEMU does not know how much RAM is available.
>>> Could you try adding "-m size=512M" to your arguments?
>>>
>>>  - Alex
>>>
>>> 
>>> From: Devel <devel-bounces@sel4.systems> on behalf of Andrew Gacek 
>>> <andrew.ga...@gmail.com>
>>> Sent: Wednesday, December 7, 2016 2:23 AM
>>> To: devel@sel4.systems
>>> Subject: [seL4] seL4 on Zinq7000 on QEMU
>>>
>>> I'm trying to build and emulate a version of seL4 for the zinq7000
>>> platform, but it crashes immediately.
>>>
>>> I've started by taking the camkes tutorial and building it for zinq7000:
>>>
>>>   repo init -u https://github.com/seL4/camkes-manifest.git
>>>   repo sync
>>>   make arm_simple_defconfig
>>>   make menuconfig # change seL4 platform to zinq7000
>>>   make
>>>
>>> When I try to emulate it, it crashes right away:
>>>
>>>   qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel
>>> images/capdl-loader-experimental-image-arm-zynq7000
>>>
>>> qemu: fatal: Trying to execute code outside RAM or ROM at 0x1000
>>>
>>> R00= R01= R02= R03=
>>> R04= R05= R06= R07=
>>> R08= R09= R10= R11=
>>> R12= R13= R14= R15=1000
>>> PSR=41d3 -Z-- A svc32
>>> s00= s01= d00=
>>> s02= s03= d01=
>>> s04= s05= d02=
>>> s06= s07= d03=
>>> s08= s09= d04=
>>> s10= s11= d05=
>>> s12= s13= d06=
>>> s14= s15= d07=
>>> s16= s17= d08=
>>> s18= s19= d09=
>>> s20= s21= d10=
>>> s22= s23= d11=
>>> s24= s25= d12=
>>> s26= s27= d13=
>>> s28= s29= d14=
>>> s30= s31= d15=
>>> s32= s33= d16=
>>> s34= s35= d17=
>>> s36= s37= d18=
>>> s38= s39= d19=
>>> s40= s41= d20=
>>> s42= s43= d21=
>>> s44= s45= d22=
>>> s46= s47= d23=
>>> s48= s49= d24=
>>> 

Re: [seL4] seL4 on Zinq7000 on QEMU

[Andrew Gacek]

If I suspend the execution in QEMU, the program counter is at
0xe00108ec. In the kernel, that is the  method. So
perhaps the system is running, but I'm just not able to see any output
from the elfloader, kernel, etc.

-Andrew

On Tue, Dec 6, 2016 at 2:49 PM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
> Thanks Alex. That fixes the crash. Now the system runs but just seems
> to hang without doing anything. I don't get any output at all (whereas
> the kzm version spews out a ton of messages). In 'top' I can see it's
> using about 3% cpu so it's something, though it's not clear what. It's
> hard for me to tell. Perhaps the UART for the console isn't working
> correctly?
>
> -Andrew
>
> On Tue, Dec 6, 2016 at 2:46 PM,  <alexander.k...@data61.csiro.au> wrote:
>> Hi Andrew,
>>
>> It could be because QEMU does not know how much RAM is available.
>> Could you try adding "-m size=512M" to your arguments?
>>
>>  - Alex
>>
>> ____
>> From: Devel <devel-bounces@sel4.systems> on behalf of Andrew Gacek 
>> <andrew.ga...@gmail.com>
>> Sent: Wednesday, December 7, 2016 2:23 AM
>> To: devel@sel4.systems
>> Subject: [seL4] seL4 on Zinq7000 on QEMU
>>
>> I'm trying to build and emulate a version of seL4 for the zinq7000
>> platform, but it crashes immediately.
>>
>> I've started by taking the camkes tutorial and building it for zinq7000:
>>
>>   repo init -u https://github.com/seL4/camkes-manifest.git
>>   repo sync
>>   make arm_simple_defconfig
>>   make menuconfig # change seL4 platform to zinq7000
>>   make
>>
>> When I try to emulate it, it crashes right away:
>>
>>   qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel
>> images/capdl-loader-experimental-image-arm-zynq7000
>>
>> qemu: fatal: Trying to execute code outside RAM or ROM at 0x1000
>>
>> R00= R01= R02= R03=
>> R04= R05= R06= R07=
>> R08= R09= R10= R11=
>> R12= R13= R14= R15=1000
>> PSR=41d3 -Z-- A svc32
>> s00= s01= d00=
>> s02= s03= d01=
>> s04= s05= d02=
>> s06= s07= d03=
>> s08= s09= d04=
>> s10= s11= d05=
>> s12= s13= d06=
>> s14= s15= d07=
>> s16= s17= d08=
>> s18= s19= d09=
>> s20= s21= d10=
>> s22= s23= d11=
>> s24= s25= d12=
>> s26= s27= d13=
>> s28= s29= d14=
>> s30= s31= d15=
>> s32= s33= d16=
>> s34= s35= d17=
>> s36= s37= d18=
>> s38= s39= d19=
>> s40= s41= d20=
>> s42= s43= d21=
>> s44= s45= d22=
>> s46= s47= d23=
>> s48= s49= d24=
>> s50= s51= d25=
>> s52= s53= d26=
>> s54= s55= d27=
>> s56= s57= d28=
>> s58= s59= d29=
>> s60= s61= d30=
>> s62= s63= d31=
>> FPSCR: 
>> Aborted
>>
>>
>> Is there something I'm doing wrong?
>>
>> Thanks,
>> Andrew
>>
>> ___
>> Devel mailing list
>> Devel@sel4.systems
>> https://sel4.systems/lists/listinfo/devel

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

Re: [seL4] seL4 on Zinq7000 on QEMU

[Andrew Gacek]

Thanks Alex. That fixes the crash. Now the system runs but just seems
to hang without doing anything. I don't get any output at all (whereas
the kzm version spews out a ton of messages). In 'top' I can see it's
using about 3% cpu so it's something, though it's not clear what. It's
hard for me to tell. Perhaps the UART for the console isn't working
correctly?

-Andrew

On Tue, Dec 6, 2016 at 2:46 PM,  <alexander.k...@data61.csiro.au> wrote:
> Hi Andrew,
>
> It could be because QEMU does not know how much RAM is available.
> Could you try adding "-m size=512M" to your arguments?
>
>  - Alex
>
> 
> From: Devel <devel-bounces@sel4.systems> on behalf of Andrew Gacek 
> <andrew.ga...@gmail.com>
> Sent: Wednesday, December 7, 2016 2:23 AM
> To: devel@sel4.systems
> Subject: [seL4] seL4 on Zinq7000 on QEMU
>
> I'm trying to build and emulate a version of seL4 for the zinq7000
> platform, but it crashes immediately.
>
> I've started by taking the camkes tutorial and building it for zinq7000:
>
>   repo init -u https://github.com/seL4/camkes-manifest.git
>   repo sync
>   make arm_simple_defconfig
>   make menuconfig # change seL4 platform to zinq7000
>   make
>
> When I try to emulate it, it crashes right away:
>
>   qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel
> images/capdl-loader-experimental-image-arm-zynq7000
>
> qemu: fatal: Trying to execute code outside RAM or ROM at 0x1000
>
> R00= R01= R02= R03=
> R04= R05= R06= R07=
> R08= R09= R10= R11=
> R12= R13= R14= R15=1000
> PSR=41d3 -Z-- A svc32
> s00= s01= d00=
> s02= s03= d01=
> s04= s05= d02=
> s06= s07= d03=
> s08= s09= d04=
> s10= s11= d05=
> s12= s13= d06=
> s14= s15= d07=
> s16= s17= d08=
> s18= s19= d09=
> s20= s21= d10=
> s22= s23= d11=
> s24= s25= d12=
> s26= s27= d13=
> s28= s29= d14=
> s30= s31= d15=
> s32= s33= d16=
> s34= s35= d17=
> s36= s37= d18=
> s38= s39= d19=
> s40= s41= d20=
> s42= s43= d21=
> s44= s45= d22=
> s46= s47= d23=
> s48= s49= d24=
> s50= s51= d25=
> s52= s53= d26=
> s54= s55= d27=
> s56= s57= d28=
> s58= s59= d29=
> s60= s61= d30=
> s62= s63= d31=
> FPSCR: 
> Aborted
>
>
> Is there something I'm doing wrong?
>
> Thanks,
> Andrew
>
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

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

Re: [seL4] Memory Management

[Andrew Gacek]

Yes, I think the seL4 kernel is mapped into the virtual address space
of all processes. I think the exact separation between user mode space
and kernel space depends on the platform. For example, on the zynq7000
platform we have:

https://github.com/seL4/seL4/blob/master/src/plat/zynq7000/linker.lds

KERNEL_BASE = 0xe000;
PHYS_BASE = 0x;
KERNEL_OFFSET = KERNEL_BASE - PHYS_BASE;

So there is ~3.5GB user mode space, ~500MB kernel space.

-Andrew


On Mon, Nov 21, 2016 at 7:13 PM, Mark Reus  wrote:
> Hi
>
> I have a general case about memory allocation in particular with that of the
> Vspace. I have been reading some documents and trying to compare how it is
> in Linux Kernel. Any program Virtual memory  in a Linux kernel is as shown
> in picture below where all processes have 1GB of virtual memory which is
> mapped to kernel space for faster context switches and system calls.
>
>
>  _
> |  Kernel Space (1GB)  |
> |_|
> | |
> |  User Mode Space |
> |   (3 GB)|
> | |
> |_|
>
>
> I have come across this this link
> http://os.inf.tu-dresden.de/pipermail/l4-hackers/2014/006262.html detailing
> a little about the sel4 memory management. But I haven't been able to
> completely comprehend it . I wanted to know if the seL4 kernel also has a
> similar mapping of kernel space.
>
> Regards
> Mark
>
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
>

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

[seL4] seL4RPC vs seL4RPCCall?

[Andrew Gacek]

What's the difference between seL4RPC and seL4RPCCall in CAmkES? Is
there documentation on the various connectors somewhere?

Thanks,
Andrew

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

Re: [seL4] Send input to seL4 in QEMU

[Andrew Gacek]

I think I have something working now. Here's the steps I took.

1. Create a pipe file in Linux: "mkfifo uart2"

2. In my Client.camkes file I have:


component Client {
control;
uses Simple a;

// Hardware interface
dataport Buf   vaddr;
consumes DataAvailable interrupt;
has semaphore  read_sem;
}

component Uartbase {
hardware;
dataport Buf   mem;
emits DataAvailableirq;
}

assembly {
composition {
// "component Client client" will be defined by the outer camkes file
component Uartbase uartbase;

// UART hardware connection
connection seL4HardwareMMIO uartbase_mem(from client.vaddr, to
uartbase.mem);
connection seL4HardwareInterrupt uartbase_irq(from
uartbase.irq, to client.interrupt);
}

configuration {
// From libplatsupport/plat_include/imx31/platsupport/plat/serial.h
uartbase.mem_attributes = "0x43F94000:0x1000";
uartbase.irq_attributes = 32;
}
}


3. In client.c I have:


#include 
#include 
#include 

#define UART_RX   0x00
#define UART_STAT10x94

#define UART_STAT1_RRDY   BIT(9)

#define REG_PTR(base, offset)  ((volatile uint32_t *)((char*)(base) + (offset)))

int run() {
while (1) {
if (*REG_PTR(vaddr, UART_STAT1) & UART_STAT1_RRDY) {
char c = (char) *REG_PTR(vaddr, UART_RX);
printf("Read: %c (%02x)\n", c, c);
}
}
return 0;
}


4. Compile


5. Attach pipe to second serial port of qemu: "qemu-system-arm -M kzm
-nographic -kernel images/capdl-loader-experimental-image-arm-imx31
-monitor none -serial stdio -serial pipe:uart2"


-Andrew

On Wed, Nov 16, 2016 at 9:56 PM, Andrew Gacek <andrew.ga...@gmail.com> wrote:
> What I'm really wondering is how do I read this information on the
> seL4 side? Are there qemu serial/uart/network drivers available for
> seL4?
>
> I suppose the easiest thing would be if I could open a serial
> connection that I can write to on the host Linux side and somehow read
> from a corresponding serial driver on the seL4 guest side. I've
> started looking through the qemu documentation, but it's been slow
> going. And I think the seL4 side will be the harder part for me to
> figure out.
>
> -Andrew
>
> On Wed, Nov 16, 2016 at 9:40 PM, Tim Newsham <tim.news...@gmail.com> wrote:
>> If by "send information into QEMU" you mean generate packets
>> destined to the VM guest, then yes.  Qemu has various options
>> for configuring the network interface. One option is to hook it up
>> to your host's tunnel interface.  If you do this, you can send
>> packets directly from your host to your guest over the tunnel interface.
>>
>>
>> On Wed, Nov 16, 2016 at 4:59 PM, Andrew Gacek <andrew.ga...@gmail.com>
>> wrote:
>>>
>>> Hi,
>>>
>>> We are developing an seL4 application that will process UDP packets
>>> coming in over a network connection. Eventually, we'll be running this
>>> on real hardware with real drivers, but for now we are using QEMU. We
>>> have a python script that can generate packet payloads. Is there a way
>>> to send this information into QEMU so that we can develop our seL4
>>> application without having the drivers and hardware in place? If it
>>> matters, we are using CAmkES as well.
>>>
>>> Thanks,
>>> Andrew
>>>
>>> ___
>>> Devel mailing list
>>> Devel@sel4.systems
>>> https://sel4.systems/lists/listinfo/devel
>>
>>
>>
>>
>> --
>> Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

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

Re: [seL4] Send input to seL4 in QEMU

[Andrew Gacek]

What I'm really wondering is how do I read this information on the
seL4 side? Are there qemu serial/uart/network drivers available for
seL4?

I suppose the easiest thing would be if I could open a serial
connection that I can write to on the host Linux side and somehow read
from a corresponding serial driver on the seL4 guest side. I've
started looking through the qemu documentation, but it's been slow
going. And I think the seL4 side will be the harder part for me to
figure out.

-Andrew

On Wed, Nov 16, 2016 at 9:40 PM, Tim Newsham <tim.news...@gmail.com> wrote:
> If by "send information into QEMU" you mean generate packets
> destined to the VM guest, then yes.  Qemu has various options
> for configuring the network interface. One option is to hook it up
> to your host's tunnel interface.  If you do this, you can send
> packets directly from your host to your guest over the tunnel interface.
>
>
> On Wed, Nov 16, 2016 at 4:59 PM, Andrew Gacek <andrew.ga...@gmail.com>
> wrote:
>>
>> Hi,
>>
>> We are developing an seL4 application that will process UDP packets
>> coming in over a network connection. Eventually, we'll be running this
>> on real hardware with real drivers, but for now we are using QEMU. We
>> have a python script that can generate packet payloads. Is there a way
>> to send this information into QEMU so that we can develop our seL4
>> application without having the drivers and hardware in place? If it
>> matters, we are using CAmkES as well.
>>
>> Thanks,
>> Andrew
>>
>> ___
>> Devel mailing list
>> Devel@sel4.systems
>> https://sel4.systems/lists/listinfo/devel
>
>
>
>
> --
> Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

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

[seL4] Send input to seL4 in QEMU

[Andrew Gacek]

Hi,

We are developing an seL4 application that will process UDP packets
coming in over a network connection. Eventually, we'll be running this
on real hardware with real drivers, but for now we are using QEMU. We
have a python script that can generate packet payloads. Is there a way
to send this information into QEMU so that we can develop our seL4
application without having the drivers and hardware in place? If it
matters, we are using CAmkES as well.

Thanks,
Andrew

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