Re: [seL4] Questions about Memory Management in seL4

Hi Daniel, From: Devel on behalf of Daniel Wang Sent: Thursday, September 22, 2016 6:51 AM To: devel@sel4.systems Subject: [seL4] Questions about Memory Management in seL4 Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can

Re: [seL4] endpoint.c

Hi Vasily, The test is basically doing the following: 1- test_ep_recycle() creates a badged ep. 2- The call_func() thread invoke seL4_Call(), (the second invocation). At this point, call_func() thread blocks waiting for a reply (on the same ep). 3- test_ep_recycle() recycles all badged ep caps (i

Re: [seL4] Using the seL4 Benchmark Tool

Hi Chris, Thanks for reporting this. Looks like some new changes to the kernel introduced circular dependencies that prevented the header that defines benchmark_util_t from getting included. Should be fixed now (530852b). Cheers, Hesham From: Devel on behal

Re: [seL4] seL4 System Utilization / Benchmark

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 ___

Re: [seL4] seL4 System Utilization / Benchmark

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 Sent: Thursday, January 19, 2017 9:18 AM To: Almatary, Hesh

Re: [seL4] sel4 kernel boot problem on i.mx6q board

Hi Shijun, The load physical address of the kernel does not seem to be right. May I ask which kernel revision are you using? How did you get the repo and how do you run it? Regards, Hesham On 20/03/17 20:15, shijun zhao wrote: > Hi everyone, > > I am running sel4 on i.mx6q sabre board. I use th

Re: [seL4] sel4 kernel boot problem on i.mx6q board

Hi Shijun, It's the physical address of the "kernel" that's the problem, not the whole image. The elfloader reads the LMA of the kernel elf file to load it to memory. For imx6, currently the kernel assumes the physical load address to be 0x1000. Have a look at the linker file at "./src/plat

Re: [seL4] Confusion with various memory address

Hi Daniel, The convention is: - paddr_t is used for physical addresses. - pptr_t is a virtual address "in the kernel window" that refers to a kernel object (e.g. page directory or endpoint). Users don't have access to any pptr_t addresses (but might have a capability to do operations on it, via

Re: [seL4] sel4test data abort when boot strap test program

Hi Joyce, On 09/05/17 17:15, Joyce Peng(彭美僑) wrote: > > Hi all, > > I tried to run seL4 test suite on my ARM Cortex-A7 target board. > What is the name of the board you have? How do you build and run sel4test? > > There is no error message when boot up seL4 kernel and boot strap test > program o

Re: [seL4] sel4test data abort when boot strap test program

Hi Joyce, The work to add a new platform requires some work on: 1) seL4, mainly you've to look at all plat/ directories and modify them to fit with your platform, specifically, physical memory range and virtual memory/device drivers mapping. 2) sel4libs, again have a look at plat/ directories t

Re: [seL4] The path where the kernel jumps to apps

Hi Shijun, _sel4_start sets up the stack (for the root task) as libmusl expects, and then jumps to _start (from libmuscl) and *NOT* the one at sel4platsupport/crt0.S. The _start function you're after (called by _sel4_start) exists in libmuslc for each arch e.g. libmuslc/arch/arm/crt_arch.h.

Re: [seL4] camkes-manifest project make failed for arm

Hi Talos, This might be because of this change [1] to the kernel. Since this change has passed on our local machines, I'd be interested to know which toolchain version are you using (specifically binutils)? [1] https://github.com/seL4/seL4/commit/1930cf2e44908cb8faa5b315651bdb1958102f8f Ch

Re: [seL4] camkes-manifest project make failed for arm

Hi Talos, Thanks for reporting this. It seems like it’s an issue with KZM (ARMv6) targets which I assume you’re using? I submitted a fix, should be public on GitHub soon. Meanwhile, you can use the following patch to get around this error. diff --git a/include/util.h b/include/util.h index d6af

Re: [seL4] 回复： camkes-manifest project make failed for arm

1:42 PM To: Almatary, Hesham (Data61, Kensington NSW) Subject: 回复： [seL4] camkes-manifest project make failed for arm Hi Hesham, How could I get which targets I used? Thanks for your patient! -- 原始邮件 -- 发件人: "Hesham.Almatary";; 发送时间: 2017年6月2日(星期五) 中午11:11

Re: [seL4] Questions about TK1-SOM Memory Management

Hi Daniel, On 21/06/17 08:26, Daniel Wang wrote: > Hi Adrian, > > Thank you very much for your explain. I might have some > misunderstanding about the source code. First may I ask what the > kernel window means? Does it means the virtual memory space kernel can > access (through pptr_t)? > Yes >

Re: [seL4] drivers in seL4

Hi Jeremy, A conventional device driver needs: 1) IRQ, 2) IO mapped registers and 3) DMA memory. You can get more details on those by: 1) Reading the seL4 manual [1], Chapter 8: Hardware I/O. 2) Follow sel4 tutorials [2], specifically hello-timer, to learn about how to use our seL4 libraries to

Re: [seL4] Questions about TK1-SOM Memory Management

Hi Daniel, On 22/06/17 06:44, Daniel Wang wrote: > Thank you very much Hesham! A follow up question: > > I know that ARM Linux uses TTBR0 only to for different process’s virtual > memory. The TTBR0 is stored in process TCB and when context switch is needed > the TTBR0 register is replaced with

Re: [seL4] elfloader-tool

Hi Yevgeny, The elfloader tool is part of seL4_tools, and is only relevant for ARM-based seL4 projects (not x86). A seL4 project (that includes the seL4 microkernel, libraries and build system and tools), uses the elfloader as the seL4-tools first piece of code that runs on the hardware, which lo

Re: [seL4] SMP on Zynq7000 zc702

Hi Jesse On 09/08/17 06:45, Jesse Millwood wrote: > > Hello, > > I realize that the only officially supported SMP platform is the i.mx6 > but I did see some code on 6.0 to master for SMP and the zynq7000 so I > am trying to test out some SMP functionality on my zc702 board. > > I am wondering if

Re: [seL4] SMP on Zynq7000 zc702

Hi Jesse, On sel4test/SMP, TEST_FPU0002 test relies on platform-dependent timer driver to implement sleep()/timestamp(). In the case of zynq7000, TTC timers are being used. We have recently added this functionality (basically ltimer/gettime()). From top-level sel4test; it's at projects/util_li

Re: [seL4] does seL4 support NVIDIA Jetson Tx2 board ?

Hi all, On 06/10/17 03:00, Muneeswaran Rajendran wrote: > Hi Mike, > > Thanks for your input. But I observed in the latest SEL4 kernel it has > option to choose TX1 in the platform list to build. can you please let > me know if any development happened on TX1 platform. > TX1 is supported by seL4

Re: [seL4] Booting seL4 in bbb (beaglebone black)

Hi Sathish, Thanks for the log. The steps look fine to me. I also tried to re-produce it, but did not get this error. Could you please let us know: * How did you configure/build sel4test (i.e. which *_defconfig file have you used)? * What toolchain do you use? * Which sel4(test) release do y