Re: [seL4] speed up sel4

Hi Sreenadh, This is sel4test trying to allocate huge amounts of memory. To change it, you can change this line: https://github.com/seL4/sel4test/blob/master/apps/sel4test-driver/src/main.c#L162 to use a smaller size_bits value to start looking at. Cheers Anna.

Re: [seL4] some questions about camkes-manifest

Hi, 1. You can find the library in https://github.com/SEL4PROJ/projects_libs? 2. Sorry, we do not have any public demos that use this library. It has mainly been used in experimental contexts. Cheers Anna. ___ Devel mailing list Devel@sel4.systems

Re: [seL4] port SeL4 to renesas rcar-H3 development board

Hi Diego, Cool! We're currently in the process of making arm board ports much easier, and when that's done we'll write up a concrete tutorial on adding new platform support for ARM boards. For now though... Which cores are you looking to run seL4 on? And in which mode (aarch64 or aarch32?) W

Re: [seL4] Multiboot and extra modules

Hi all, Just to confirm what has already been stated: while it would be possible for seL4 to load multiple images, however this is incongruent with L4 philosophy. We want to keep the kernel as small as possible to minimise the trusted computing base and maximise policy freedom. The root task c

Re: [seL4] sel4bench config problem

Hi, Can you please send all of the commands you have used to configure the build directory? It should look something like this: mkdir build cd build ../init-build.sh -DPLATFORM=sabre -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE ? Cheers, Anna. From: Dev

Re: [seL4] seL4 10.1.0 and camkes-3.6.0

Great! I'll take a look. Cheers Anna. From: Devel on behalf of jonas...@protonmail.com Sent: Thursday, 15 November 2018 9:51 PM To: devel@sel4.systems Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 Hi, Today I created a few pull-requests on seL4 rep

[seL4] seL4 stack overflow

Hi everyone, I've created a proposal for an seL4 stack overflow, which will complement the mailing list. Please support it! https://area51.stackexchange.com/proposals/120611/sel4?referrer=oNjnX5y9POxoX0Q4ck0dRg2? Cheers, Anna. ___ Devel mailing

Re: [seL4] sel4bench IPC questions

Hi, > 1. Making seL4_IPCBuffer and mapping into the thread is necessary? > I think that sending short messages don't need seL4_IPCBuffer, is it right? Correct. There is a constant defined for each architecture in libsel4 (`seL4_FastMessageRegisters`) which specifies the size of message that ca

Re: [seL4] Scheduling of vCPUs on x86

Hi Alexander, > Following patch seems to fix the issue. Can you please have a look and > verify that it is correct ? Or should it be solved on another place in > the kernel differently. Yes, the patch is correct and definitely fixes a bug. Thanks! Would you like me to apply this directly or wil

Re: [seL4] Support for QNX-like booting from an XIP filesystem image

Hi Andrew, I had a quick look and the changes seem ok on brief inspection, although if you were to put up a pull request for merging we'd need to do a lot more testing. As an aside, I encourage you to consider listing your project on our Community Projects [1] page. We want to provide visibili

Re: [seL4] Non CAmkES VM on x86

Hi Chris, > Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar > to > how the old ARM VMM worked? If so, is that something that could be > released? We spent a bit of time looking, but although the initial development did involve such a thing, it no longer exists (if

Re: [seL4] Support for QNX-like booting from an XIP filesystem image

Hi Andrew, Sorry for the late reply on this one! The boot code of seL4 is currently unverified, but we do have ambitions for verification in the future. As such, we'd want to keep a minimal, static boot environment. That said, we'd be more than happy to take a look at any patches you have in

Re: [seL4] seL4 IPC and SMP question.

Hi, > 2. Can you explain the difference when thread state is "ThreadState_Running" > and "ThreadState_Restart"? This indicates if the thread is returning from a system call (therefore the instruction pointer needs to be updated) or a preemption. See the function activateThread which does the u

Re: [seL4] seL4 IPC fastpath question

Hi, > 1. IPC fastpath can apply in seL4_Call and seL4_Reply_Recv, is it right? > seL4_Send, seL4_Recv can't apply IPC fastpath. Yes. We could add fastpaths for other paths if required but they do not currently exist. > 2. IPC_fastpath can only send message that message's length is 0, is it ri

Re: [seL4] Does seL4 provide an initrd with a shell?

Hi Baptiste, Aside from running a Linux guest, we do not currently have a native shell. The x86 VM should work though. Cheers Anna. From: Devel on behalf of Baptiste Lepers Sent: Thursday, 27 September 2018 2:28 PM To: devel@sel4.systems Subject: [seL4] D

Re: [seL4] x86 seL4 kernel bug - kernel page faults on seL4_VMEnter

Hi Alex, Yes, this is indeed a bug and no, the x86_64 VM code is not currently verified. The following snippet should fix it, and give the misbehaving thread an 'unknown syscall' fault. diff --git a/src/arch/x86/c_traps.c b/src/arch/x86/c_traps.c index f17e5473..857896dd 100644 --- a/src/arch/x

Re: [seL4] CAmkES VMM platform support

Hi Grant, Yes, this is possible. We mostly use 64-bit hosts on x64, with 32-bit guests. Cheers Anna. From: Grant Jurgensen Sent: Friday, 7 September 2018 10:50 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] CAmkES VMM p

Re: [seL4] CAmkES VMM platform support

?Hi Grant, Yes, currently seL4 only supports 32-bit guests. This is something we are working on ameliorating in the future, keep an eye on our upcoming releases. I have an odroid-xu4 on my desk at the moment, as it will soon become a supported platform, but I haven't started the port yet. How

Re: [seL4] seL4 benchmark configure

Hi, Please see our docs on configuring cmake projects [1]. You can change KernelMaxNumNodes for the number of CPUs. There are some options to turn on and off caches too, depending on the platform. If the option you want is not there you will need to implement it yourself. Cheers. Anna. ?[

Re: [seL4] Demo build

Hi Chris, For the first issue - just making sure you initialised a new build directory for building ia32? The second issue - our HPET driver is very bare and doesn't support the full gamut of features. If you want to continue with this platform you'll need to improve the driver. Thanks,

Re: [seL4] sel4test driver can not load big elf file

Hi Dong, Are you using ia32 or x64? x64 has a lot more memory available than ia32 due to the way untyped memory management works. How big is the image you are trying to load? Can you please provide the full sel4test output so I can help diagnose the issue. Cheers, Anna. ___

Re: [seL4] create process in seL4

Hi Leonid, I don't understand your first question, which untyped are you wanting to adjust the size of? As for the second question, you can take a look at the sel4bench project, where all created processes use the same function to get a working allocator through the libsel4benchsupport libra

Re: [seL4] Demo build

Hi Chris, That's strange, the build system definitely should not hang. However I need more information to help at all. Which OS version are you using (host and seL4)? Which gcc version and cmake version? Is there any output from the init-build script at all? Also, have you used a clean build

Re: [seL4] seL4 benchmark cache unable.

Hi, It's unclear which cache you are talking about. There are debug features which allow you to turn off L2 and branch predictor etc for certain platforms, but it really depends on the platform itself as to what is supported. Use the cmake configuration ui (cd build && ccmake ..) to see the

Re: [seL4] compile error aarch64 platform hikey

Hi Thad, zynqmp is now a supported cmake platform as of: https://github.com/seL4/seL4/commit/9bd2b784c176ebc91e0d5e0c46d05c8fec2e3853 We've tested that it compiles, but we don't have an actual board to test that it runs, but the parameters match what was used by Kbuild. Cheers, Anna. ___

Re: [seL4] Paging in SEL4

Hi Sathya, For details on virtual memory in seL4, please see chapter 7 of the manual: http://sel4.systems/Info/Docs/seL4-manual-latest.pdf Thanks Anna. From: Devel on behalf of Sathya Narayanan N Sent: Thursday, 9 August 2018 10:34 PM To: devel@sel4.system

Re: [seL4] Questions about sel4bench IPC statistic in the website

Hi Zihan, The numbers on the benchmark are one fastpath, one slowpath (the details show that the length of the IPC is 10, and any messages > 4 go to the slowpath as they will not fit in registers). I'm going to look at getting these numbers updated with more details for reproducability - is t

Re: [seL4] compile error aarch64 platform hikey

Hi Thad, zyncmp hasn't been ported to cmake yet, I'll see if we can fix that this week. For the build error: you need to use a version of aarch64-linux-gnu-gcc > 5. $ aarch64-linux-gnu-gcc --version aarch64-linux-gnu-gcc (Ubuntu/Linaro 5.4.0-6ubuntu1~16.04.9) 5.4.0 20160609 Cheers, Anna.

Re: [seL4] Combined Ada and C project with Kbuild

Hi, The Kbuild system is deprecated for CMake, and is in the process of being removed, so if you want to continue using it you will need to fork the project. If you want to continue with make I recommend looking at the GNU make docs. If you want to transition to CMake, we have provided docs f

Re: [seL4] sel4 thread creation problem

Hi Leonid, It looks like you haven't set the cspace guard correctly in the new tcb, which means that cptr look ups will fail. This should fix it: - error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page); + seL4_Wor

Re: [seL4] camkes-project error

Hi, Sorry, the docs at https://sel4.systems/Info/CAmkES/GettingStarted.pml? ?are completely out of date. I'll look into getting them removed. The second set of docs ( https://docs.sel4.systems/CAmkES/)? are correct. I just reproduced building correctly on

Re: [seL4] about compile error

?Hi, I've updated the Camkes docs for our new build system on how to run a sample application. Can you try again with the new instructions on 'building a sample application'? https://docs.sel4.systems/CAmkES/ Cheers Anna. From: Devel on behalf of wong xu

Re: [seL4] Question about wrapper files

Hi all, As part of the kernel build process several intermediate files are created, for several reasons: mainly because our verification toolchain currently requires the kernel as 1 C file, and to support the bitfield generator, which generates the minimal code and proofs for various data stru

Re: [seL4] Image lies outside of usable physical memory v2

Hi Jeremy, This is currently not on our roadmap and hasn't been fixed. However, if you can put up a pull request with what you have done we'd be more than happy to take a look. Cheers, Anna. From: Devel on behalf of Jeremy Fields Sent: Wednesday, 18 July

Re: [seL4] Implementing a Filesystem on CAmkES

Hi Grant, I can answer the "is there an easy way to integrate said filesystem into musllibc such that one could use the standard open/read/write/close functions"? The answer is yes ;). Take a look at libsel4camkes [1] which already binds some of the common C library functions. You could exten

Re: [seL4] seL4 - getting the execution time of different threads

Hi Amit, Yes, it's possible to share vka, allocman etc (if they are in the same address space you can make them global and use them - although beware, these libraries are not thread safe). Between processes you can set up new allocators, I recommend you take a look at the sel4bench project [1]

Re: [seL4] ARM Vchan Error

Hi Daniel, Sorry for the late reply. We do not currently support vchans on ARM. We are working internally on guest-to-guest communication support, and will post about it when it is available. Thanks, Anna. From: Devel on behalf of Daniel Wang Sent: Wedne

Re: [seL4] reading thread registers

Hi Michael, In seL4, all memory is managed by user level. In order to access any memory it must be mapped in to the current address space, at which point you can access that memory at will, as long as you have the correct capabilities. Capabilities to all untyped memory in the system are passe

Re: [seL4] seL4 - getting the execution time of different threads

Hi Chris, It depends on your use case. If you are looking to monitor the execution times of threads for debugging and/or benchmarking purposes, you can use our kernel benchmarking support, detailed here [1]. Otherwise, you could consider using the mcs branch of the kernel, which allows you t

Re: [seL4] Future plans w.r.t. Cortex-R

Hi Piotr, For platforms without MMUs, take a look at eChronos[1], which is a small RTOS that does support MPUs. seL4 only targest systems with MMUs. Thanks Anna. [1] https://ts.data61.csiro.au/projects/TS/echronos/ From: Devel on behalf of pi...@skrzyp

Re: [seL4] Memory Region overlap error

Hi Jeremy, Could you please provide more details about your setup? What version of seL4 are you using? And which platform / configuration? Thanks Anna. From: Devel on behalf of Jeremy Fields Sent: Wednesday, 4 July 2018 10:34 PM To: devel@sel4.systems Sub

Re: [seL4] IPC

You could start by looking at [1] and follow the references from there. Cheers. Anna. [1] http://sigops.org/sosp/sosp13/papers/p133-elphinstone.pdf From: Devel on behalf of tj5527 Sent: Thursday, 22 February 2018 10:46 AM To: devel@sel4.systems Subject:

Re: [seL4] Automatic testing using qemu

Hi Paolo, For our internal continuous integration, we use the python pexpect[1] package to detect output/timeouts and then terminate the test. It's not perfect, but it works most of the time. Cheers, Anna. [1] https://pexpect.readthedocs.io/en/stable/

Re: [seL4] Announcing seL4 9.0.1: with RISC-V support

Hi Arun, 32-bit RISC-V is not scheduled on our roadmap currently, unless it's required for another project. Code for 32-bit RISC-V is there for the kernel and user-level, and currently compiles. But the kernel doesn't successfully boot and needs investigation. A community contribution is we

Re: [seL4] camkes tutorial build compilation error

Hi Thad, In the current build system used by the tutorials you need to `make clean` if you are switching architectures. Our upcoming build system addresses this problem, but we're still applying the finishing touches. Cheers, Anna. ​ From: Devel on behal

Re: [seL4] split.c bootstrap.c failure?

Hi Richard, Usually this error occurs when the allocator has been told a capability is free when it actually isn't. This is usually due to a capability being duplicated and only one copy being deleted. The error you are seeing is the allocator attempting to use a slot that it thinks is free bu

Re: [seL4] Questions on seL4's scheduling

Hi Oak, We have code here to set the clock on the sabre to 1Ghz: https://github.com/seL4/sel4bench/blob/master/apps/sel4bench/src/plat/imx6/plat.c#L20 Anna. From: Norrathep Rattanavipanon Sent: Saturday, 21 October 2017 6:00 AM To: Kroh, Alexander (Data61,

Re: [seL4] Questions on seL4's scheduling

Recall I stated that the scheduler is basic ;) The timer ticks on the master kernel are started on boot, then not reset on any thread operation. This means that the actual thread timeslice is just 'X interrupts must come in'. So it's likely to vary by up to the tick ms value, as the yield does

Re: [seL4] Questions on seL4's scheduling

Hi Oak, The timeslice value on the master kernel is only reset on thread creation and once the thread is depleted, so when a thread drops its priority the timeslice will not change, so it'll run for 2ms. The timeslice cannot be set to lower than 1 ms, however you could change the timer drive

Re: [seL4] Questions on seL4's scheduling

Hi Oak, Assuming your questions are about the master branch of the kernel, as on the RT branch the kernel is tickless. 1. There are two config paramters + TIMER_TICK_MS is how many milliseconds per tick + TIME_SLICE is how many ticks per timeslice. 2. Assuming a thread is waiting o

Re: [seL4] Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1"

Hi, I think your stack version might need updating. Can you try s'tack upgrade --git'? Cheers, Anna. From: Devel on behalf of tj5527 Sent: Thursday, 6 July 2017 6:43 AM To: devel@sel4.systems Subject: [seL4] Invalid package ID: "array-0.5.1.1 base-4.9.0.0

Re: [seL4] malloc & errno

Hi Fabrizio, Our port of muslc to seL4 is very minimal and does not implement errno - when it's accessed by a thread that thread will fault. If you are in debug mode and that thread does not have a fault handler, you'll see a double fault, where seL4 will print out the details of the fault. Th

[seL4] Pre-release of mixed criticality seL4 extensions

= seL4-5.2.0-mcs = The first round of mixed-criticality extensions for seL4 are now available for your perusal and usage. This is a prerelease of features that are currently our candidate for verification. They are *not* verified and most likely contain bugs. If you encounter any, please repor

Re: [seL4] vmm documentation

Hi Mike, We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more: https://wiki.sel4.systems/CAmkESVM We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare

Re: [seL4] CapDL & RT

Hi Richard, The support for the RT kernel is indeed for the latest RT version which isn’t pushed out yet. What particular features were you after? I can push a branch out for you if so. But yes, it’s still WIP, I’ll be pushing out some real branches with documentation etc in the next few month

Re: [seL4] ARM timer driver and interrupts

Hey, First I'd check if the kernel is getting the interrupts in the kernel from this timer - you can put a printf in handleInterrupt in the kernel to see if this is the case and see if the correct interrupt number comes in. If so, then check if those irqs are being sent to the signal handler

Re: [seL4] RT and domains

Hi, For the first release of the RT kernel (which is a pre-release) we excluded the domain scheduler to make development easier. The final version of the RT kernel will probably include the domain scheduler. However, it should be noted that if using RT + domain scheduler the max deadline miss

Re: [seL4] Exposing ticks to the rt API

Hi Corey, I'm back from leave, but Adrian mostly answered the question. I will reiterate the most important points: * Currently the PIT is only used to calibrate the tsc if the processor isn't known to support the platform info MSR to read the frequency from. This code is currently only writte

Re: [seL4] SDHC driver in Sabre Lite

Hi Oak, You can also try setting the 3rd argument of vspace_new_pages to 0 instead of 1. Currently it will map the pages in cached, and unless the driver is flushing the caches itself (which it can't, as it doesn't have the caps passed into it) the changes won't get past the caches. 0 tells th

Re: [seL4] General Questions

Hi Mark, To answer your questions: i)Processes can be spawned and created from any task that has the caps to do so. ii) ZF_LOG* is only currently used at user level, it would be nice in the kernel. You can use printf in the kernel. iii) S

Re: [seL4] syscall.c

Hi Vasily, The point of the syscall.c tests is to check that registers are not being corrupted by our syscalls (i.e that the kernel ABI + stubs follows the calling convention of the architecture). For arm, this just means checking any registers that are not caller saved are preserved across the

Re: [seL4] Why send-only IPC doesn't and shouldn't return a success indicator

Hi Richard, This is a common misunderstanding: seL4_Call doesn’t generate a cap to the ep, but a cap to the thread that the seL4_Call went through (called the ‘reply cap’). seL4_Reply(Wait) sends directly to this thread via that capability, so the IPC is guaranteed to go to the caller. If you