[seL4] Re: shoehorn & fudge factor

Do what's easiest for you. On Sun, Mar 12, 2023 at 8:05 PM Kent Mcleod wrote: > On Fri, Feb 3, 2023 at 10:29 AM Sam Leffler wrote: > > > > On Thu, Feb 2, 2023 at 1:56 PM Kent Mcleod > wrote: > >> > >> On Fri, Feb 3, 2023 at 8:26 AM Sam Leffler via Deve

[seL4] Re: memory zero'ing

RISC-V (32-bit), no L2 cache. All of user-space shares 1 ASID. On Fri, Mar 10, 2023 at 4:23 PM Indan Zupancic wrote: > Hello, > > On 2023-03-11 10:56, Sam Leffler via Devel wrote: > > I've got a stress test that forces lots of memory recycling by > > creating,

[seL4] Re: memory zero'ing

On Fri, Mar 10, 2023 at 3:55 PM Gerwin Klein wrote: > > > On 11 Mar 2023, at 09:19, Sam Leffler via Devel > wrote: > > I'm chasing an issue that looks like retype'd memory has nonsense data. If > I read the kernel code correctly it looks like the object ret

[seL4] Re: memory zero'ing

On Fri, Mar 10, 2023 at 3:28 PM Kent Mcleod wrote: > > > On Sat, 11 Mar 2023, 09:40 Sam Leffler via Devel, > wrote: > >> I'm chasing an issue that looks like retype'd memory has nonsense data. If >> I read the kernel code correctly it looks like the objec

[seL4] memory zero'ing

I'm chasing an issue that looks like retype'd memory has nonsense data. If I read the kernel code correctly it looks like the object returned by an seL4_UntypeRetype syscall should be zero'd (looks to happen when an untyped memory object is reset here

[seL4] Re: shoehorn & fudge factor

On Thu, Feb 2, 2023 at 1:56 PM Kent Mcleod wrote: > On Fri, Feb 3, 2023 at 8:26 AM Sam Leffler via Devel > wrote: > > > > I have a target platform with only 4M of memory. When the system image is > > generated and the shoehorn helper script is used to find a place in

[seL4] shoehorn & fudge factor

I have a target platform with only 4M of memory. When the system image is generated and the shoehorn helper script is used to find a place in memory to load the build artifacts it tacks on an extra 4M of memory use (aka fudge_factor). The comment in the code

[seL4] Re: kernel builds w/ different memory configurations

Yes, that was a better approach. Thank you! On Mon, Jan 23, 2023 at 2:37 PM Axel Heider wrote: > Sam, > > > I have a target platform w/ 2 pre-defined memory configs. I've > > created separate .dts files w/ the different memory sizes and > > then in src/plat/sparrow/config.cmake do:> if(Kerne

[seL4] kernel builds w/ different memory configurations

I have a target platform w/ 2 pre-defined memory configs. I've created separate .dts files w/ the different memory sizes and then in src/plat/sparrow/config.cmake do: if(KernelDebugBuild) list(APPEND KernelDTSList "tools/dts/sparrow-debug.dts") else() list(APPEND KernelDTSL

[seL4] Re: sel4test:nested timeout fault test flaky?

e: > https://github.com/seL4/ci-actions/pull/233. > > Ivan > > On 6/01/2023, at 5:13 AM, Sam Leffler via Devel > wrote: > > We run sel4test regularly for a 64-bit raspi target under qemu and > occasionally see failures like this: > > Starting test 129: TIMEOUTFAULT0003

[seL4] sel4test:nested timeout fault test flaky?

We run sel4test regularly for a 64-bit raspi target under qemu and occasionally see failures like this: Starting test 129: TIMEOUTFAULT0003 > Running test TIMEOUTFAULT0003 (Nested timeout fault) > Error: Check badge(3) == expected_badge(2) failed. at line 9 This is a stock sel4test

[seL4] tool to report per-component memory / resource use from system.cdl

I'm looking for a script/tool that can break down memory by component given a system.cdl file. I've been doing this by hand (sorta) but figured I should ask before doing something more organized. -Sam ___ Devel mailing list -- devel@sel4.systems To unsub

[seL4] Re: Project Sparrow / KataOS Initial Open Source Release

[elaborating] On Mon, Aug 22, 2022 at 9:21 AM June Tate-Gans (ジューン) wrote: > Ah, no, actually. That's just our simple heap memory allocator we needed > for Rust TCBs. > The kata-os-allocator crate supports per-component heap allocation

[seL4] Re: section type mismatch on aarch64

A clean upstream checkout fails to build w/ gcc 11.2 because of the section mismatch. On Mon, Aug 1, 2022 at 3:57 PM Sam Leffler wrote: > On Mon, Aug 1, 2022 at 2:53 PM Axel Heider wrote: > >> Sam, >> >> > >> /usr/local/google/home/sleffler/camkes-aarch64-rootserver/kernel/include/arch/arm/arch

[seL4] Re: section type mismatch on aarch64

On Mon, Aug 1, 2022 at 2:53 PM Axel Heider wrote: > Sam, > > > > /usr/local/google/home/sleffler/camkes-aarch64-rootserver/kernel/include/arch/arm/arch/64/mode/kernel/vspace.h:55:36: > > error: ‘mode_reserved_region’ causes a section type conflict with > > ‘avail_p_regs’ > >55 | static const

[seL4] section type mismatch on aarch64

I'm building for aarch64 and hitting: /usr/local/google/home/sleffler/camkes-aarch64-rootserver/kernel/include/arch/arm/arch/64/mode/kernel/vspace.h:55:36: error: ‘mode_reserved_region’ causes a section type conflict with ‘avail_p_regs’ 55 | static const region_t BOOT_RODATA *mode_reserved_regi

[seL4] Re: seL4 kernel memory footprint

140KB was high (not sure where I got it as a debug build is 160KB): $ readelf -lS kernel.elf There are 15 section headers, starting at offset 0x1a158: Section Headers: [Nr] Name TypeAddr OffSize ES Flg Lk Inf Al [ 0] NULL00

[seL4] Re: seL4 kernel memory footprint

Oh, and thanks again Kent, as always you've been very helpful! On Tue, Jul 12, 2022 at 4:02 PM Sam Leffler wrote: > On Tue, Jul 12, 2022 at 3:40 PM Kent Mcleod > wrote: > >> On Wed, Jul 13, 2022 at 7:36 AM Sam Leffler via Devel >> wrote: >> > >> >

[seL4] Re: seL4 kernel memory footprint

On Tue, Jul 12, 2022 at 3:40 PM Kent Mcleod wrote: > On Wed, Jul 13, 2022 at 7:36 AM Sam Leffler via Devel > wrote: > > > > On Mon, Jul 11, 2022 at 1:24 PM Axel Heider wrote: > > > > > Sam > > > > > > > Aha, thank you (that's very hid

[seL4] Re: seL4 kernel memory footprint

On Mon, Jul 11, 2022 at 1:24 PM Axel Heider wrote: > Sam > > > Aha, thank you (that's very hidden)! I do see the 2MB reserve in the > > generated DTS (gen_headers/plat/machine/devices_gen.h). And we don't > > have/use SBI. Any reason why this PR has yet to be merged? > > > Basically lack of time

[seL4] Re: seL4 kernel memory footprint

On Sun, Jul 10, 2022 at 5:33 PM Kent Mcleod wrote: > > >> > > > >> > I'm trying to figure out the physical memory used by the kernel. > This is > > >> > for riscv if it matters. > > >> > > Starting from the ram region defined by the device tree, I recall the > following happens for RISC-V: > - So

[seL4] Re: seL4 kernel memory footprint

On Sun, Jul 10, 2022 at 3:04 PM Sam Leffler wrote: > On Fri, Jul 8, 2022 at 6:38 PM Gernot Heiser wrote: > >> On 9 Jul 2022, at 05:15, Sam Leffler via Devel >> wrote: >> > >> > I'm trying to figure out the physical memory used by the kernel. This is &

[seL4] Re: seL4 kernel memory footprint

On Fri, Jul 8, 2022 at 6:38 PM Gernot Heiser wrote: > On 9 Jul 2022, at 05:15, Sam Leffler via Devel wrote: > > > > I'm trying to figure out the physical memory used by the kernel. This is > > for riscv if it matters. > > Hi Sam, > > The RAM usage of

[seL4] seL4 kernel memory footprint

I'm trying to figure out the physical memory used by the kernel. This is for riscv if it matters. -Sam ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

[seL4] seL4 gdb + renode support

As I mentioned on yesterday's zoom call Antmicro has released support for debugging seL4 applications (esp CAmkES). https://antmicro.com/blog/2022/06/sel4-userspace-debugging-with-gdb-extensions-in-renode/ I've used it extensively and find it very useful. -Sam ___

[seL4] Re: camkes q's

On Tue, May 10, 2022 at 1:42 AM Kent Mcleod wrote: > On Mon, May 9, 2022 at 8:07 AM Sam Leffler via Devel > wrote: > > > > 1. I need multiple VSpace "holes" to map page frames. This is the > > equivalent of what capdl_loader_app sets up in init_copy_frame. To

[seL4] camkes q's

1. I need multiple VSpace "holes" to map page frames. This is the equivalent of what capdl_loader_app sets up in init_copy_frame. To do this I setup named static arrays and unmap the frame caps in camkes.c:post_main. This works but using a per-component attribute to enable this was awkward so I end

[seL4] RTReply and cap xfer

The kernel supports attaching a capability to an RTReply xfer. sel4test even checks this WAI. But capdl doesn't seem to support it as I see no way to express the set of rights associated with a capability to an RTReply object. I added capdl support so I can mark the Grant right and verified cap xfe

[seL4] Re: capDL-tool fix for empty CNode slots

My change is just wrong; discard. On Wed, Apr 6, 2022 at 11:07 AM Sam Leffler wrote: > Actually, I sent this prematurely. It appears to mess up something in the > VSpace construction. Please ignore for now. > > On Wed, Apr 6, 2022 at 10:36 AM Axel Heider wrote: > >> Sam, >> >> > If you generate

[seL4] Re: capDL-tool fix for empty CNode slots

Actually, I sent this prematurely. It appears to mess up something in the VSpace construction. Please ignore for now. On Wed, Apr 6, 2022 at 10:36 AM Axel Heider wrote: > Sam, > > > If you generate capdl for a CNode with empty slots, capDL-tool > incorrectly > > calculates CDL_CapMap::num becaus

[seL4] capDL-tool fix for empty CNode slots

If you generate capdl for a CNode with empty slots, capDL-tool incorrectly calculates CDL_CapMap::num because it uses Map.size which doesn't include empty slots. The right way to calculate "num" is by taking the max of the key values +1. diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/P

[seL4] Re: propagating initial thread's capabilities

[Thanks again for your timeley responses, more inline] On Sun, Mar 27, 2022 at 6:11 PM Kent Mcleod wrote: > On Mon, Mar 28, 2022 at 11:04 AM Sam Leffler wrote: > > > > On Sun, Mar 27, 2022 at 3:43 PM Kent Mcleod > wrote: > >> > >> On Mon, Mar 28, 2

[seL4] Re: propagating initial thread's capabilities

On Sun, Mar 27, 2022 at 3:43 PM Kent Mcleod wrote: > On Mon, Mar 28, 2022 at 6:29 AM Sam Leffler via Devel > wrote: > > > > The rootserver gets various caps setup for it by the kernel (see Table > 9.1 > > in the manual). This includes the gobal ASID, IRQ, Domain, a

[seL4] propagating initial thread's capabilities

The rootserver gets various caps setup for it by the kernel (see Table 9.1 in the manual). This includes the gobal ASID, IRQ, Domain, and Sched controllers. I need these caps in a process created by the rootserver. This is within a CAmkES environment. So far I've created CAmkES component attributes

[seL4] Re: sel4-sys support

On Wed, Dec 15, 2021 at 5:14 PM Kent Mcleod wrote: > On Thu, Dec 16, 2021 at 11:36 AM Sam Leffler wrote: > > > > [Karol is working with me on this so hopefully it's ok to interject] > > > > On Wed, Dec 15, 2021 at 3:40 PM Kent Mcleod > wrote: > >> > >> On Thu, Dec 16, 2021 at 1:20 AM wrote: >

[seL4] Re: sel4-sys support

[Karol is working with me on this so hopefully it's ok to interject] On Wed, Dec 15, 2021 at 3:40 PM Kent Mcleod wrote: > On Thu, Dec 16, 2021 at 1:20 AM wrote: > > > > Hi All, > > > > We’ve been working on reviving the sel4-sys Rust crate and getting it > usable again. Currently, we have it wo

[seL4] Re: capdl-loader questions

[thanks for the extensive answers] On Mon, Dec 6, 2021 at 10:13 PM Kent Mcleod wrote: > On Wed, Dec 1, 2021 at 9:59 AM Sam Leffler via Devel > wrote: > > > > Some updates inline. Especially interested in answers for #5 and #8. > > > > On Wed, Nov 24, 2021

[seL4] Re: capdl-loader questions

Some updates inline. Especially interested in answers for #5 and #8. On Wed, Nov 24, 2021 at 9:12 PM Sam Leffler wrote: > I've been investigating how capd-loader works and have some questions. My > apologies if these were previously discussed. > > 1. CDL_Model is mutable. The capDL specification

[seL4] capdl-loader questions

I've been investigating how capd-loader works and have some questions. My apologies if these were previously discussed. 1. CDL_Model is mutable. The capDL specification looks like a perfect candidate for being in .rodata but it's stored+treated as mutable. Why? I see capdl-loader uses the mutabili