hi.
i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors:
simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented
FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6
FAULT HANDLER: Register dump:
FAULT HANDLER: rip :0x402b7f
,
.
.
so i found …
[View More]that this method not implemented yet so i return 0 in this method and resolved.
for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method.
so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug?
thanks for your attention.
--
This email was Anti Virus checked by Security Gateway.
[View Less]
Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm
trying to run seL4 test suite or simple hello world task from seL4
tutorials on the real hardware. So far I had no problems compiling seL4
test suite and running via QEMU for both x32 and x64 platforms. However,
when I try to run it on the actual hardware following Running on real
hardware tutorial for x86 I end up with no output at all and no error msgs
that can give me a clue on where something went wrong.
After compiling …
[View More]seL4test for x86, I ended up with two images in
sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created
a new GRUB2 entry that looks like this
menuentry “seL4 test suite” --class os {
load video
insmod gzio
insmod part_msdos
insmod ext2
set root=’(hd0,msdos5)’
multiboot /boot/sel4/kernel-ia32-pc99
module /boot/sel4/sel4test-driver-image-ia32-pc99
}
update grub, restart and select the new entry from GRUB menu.
I end up with blinking cursor on the top-left side of the screen. Please
advise.
[View Less]
Hi seL4 Dev team,
Can someone explain the reason (share the reference) to invalidate the
local TLB during kernel vspace activation as part CPU initialisation.
The Tx2 board stuck while performing this operation. As per my
understanding both Tx1 and Tx2 are using same A57 core. so the TLB
initialisation and invalidation remain same for Tx2 and should not stuck
during invalidation.Please correct me if anything wrong here.
I understand from that instruction (tlbi vmalle1) which is invalidating
…
[View More]stage 1 entries associated to the current VMID. Also from arm mmu code the
seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as
16bit and page table setup 4k granular size.
I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the
state of processor but its throwing synchronous exception. Do we have any
other option to dump all the register content to see the state of processor
like we have one in 'sel4debug_dump_registers' which is used in sel4test
code.
Regards,
Muneeswaran R
[View Less]
Hi all
A friendly reminder that the seL4 developer hangout is on again next week:
Wed, Jun 28, 7am (UTC), Topics: (open)
* Sydney: Wed, Jun 28, 5pm
* Central Europe: Wed, Jun 28, 9am
* US Pacific Time: Wed, Jun 28, 12pm (midnight)
Calendar: https://sel4.systems/contact/
Zoom link: https://unsw.zoom.us/j/82640784431
cheers
Birg
---
Dr. Birgit Brecknell
Project Officer
Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au>
seL4 …
[View More]Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems>
0433 880 571
Mon 9am-5pm
Wed 2pm-5pm
Fri 9am-5pm
[View Less]
Hey guys,
I've been attempting to put together some rust bindings for the seL4 fault
handling mechanisms, and I'm afraid the bitfield generator is driving me a
bit up a wall at this point. I'd like to find a concise grammar for the
language so I can better understand how bitfield_gen.py works, but there
doesn't seem to be any explicit BNF for it anywhere.
Is there a paper I should be reading or a reference guide somewhere that
would help?
Thanks!
--
June Tate-Gans
Software Engineer
…
[View More]Techlead, Kata OS / AmbiML, Google
[View Less]
Hi:
I have one question about sel4 kernel preemptionPoint on smp platform such as ARMv8.
Take an example, when kernel takes long time to clear memory when UntypedRetype kernel object on core1, it will check preemptionPoint,
when pending IRQ exists on core1, it will handle this irq, and return to userspace let other syscall or cores such as core2 have chance to run, but irq pending only check current cpu(PerCPU), no all cores of smp system, if core1 execute long …
[View More]seL4_Untyped_Retype syscall, core2 has a pending irq, the pending irq will not be checked in current core1, it will block until the execution of long syscall is completed if we take no account of archtimer irq, This phenomenon looks inconsistent at the system level between signal core and mutil core
I want to know the current design intent about preemptionPoint of archtimer interrupt and other peripheral interrupts on SMP platform, only take current core interrupt as soon as possible or give other core and high priority task a chance to entry kernel and take big kernel lock?
Thanks for your help
[View Less]
Hi all,
was looking around the Rust crates to check what is available to play
around with seL4 from Rust and just found that most interesting ones
(sel4_sys, sel4-start, ...) have documentation pointing doc.robigalia.org
which is a broken link. Looks like the only communication way to Robigalia
is #robigalia IRC channel... (I don't use IRC since 90s, not used to it
anymore...) so I'm publishing this info here as I bet those amazing
developers are in this list too and can read this message: …
[View More]please 🙏 fix
the link at crates.io.
Beside this, I will never get tired of remember the importance of taking
care of the "general public" (that is, common developers not familiarized
with seL4, common companies that are not security nor technical gurus,
etc... that is, the average potential user of seL4 in the future) so it has
an "easy/friendly" approach to seL4 as an early adopter. For that reason,
checking that (healthy) Rust environment is there available for everyone
will be a good starting point. seL4 topic is complex enough with
documentation, so without it becomes simply not usable (for humans... 😅).
Hoping Robigalia amazing guys can read this here, thank you for your work
on Rust, as this is the best interface to seL4 development for people
living on this planet.
Best,
[View Less]
I'm trying to port an old sel4 code base to the latest so I decided to take the sel4test manifest & work through through the following page (https://docs.sel4.systems/projects/sel4/porting.html)
The old code base does not add the new platform the same way since the new code seems to have some new CMake macros that do most of the heavy lifting. Is there a test project that does this with an arbitrary platform that I can use as a reference? My platform defines don't seem to be coming …
[View More]through correctly. Is working through the porting page the best way to do and does it seem current? Thanks.
[View Less]
