Hi all,
I'm trying to port camkes-arm-vm to a different platform, that supports
gic-v3
In the process, I hit a compilation error:
Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/
kernel_all_pp_prune_wrapper_temp.c.obj
FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c
In file included from /home/chris/camkes-tqma8xqp-
vm/kernel/src/arch/arm/object/vcpu.c:15:
/home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23:
error: "IRQ_MASK" redefined [-Werror]
23 #define IRQ_MASK MASK(10u)
In file included from kernel/gen_headers/plat/platform_gen.h:23,
from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/
default/plat/machine.h:8,
from /home/chris/camkes-tqma8xqp-
vm/kernel/include/machine.h:9,
from /home/chris/camkes-tqma8xqp-
vm/kernel/include/api/syscall.h:10,
from /home/chris/camkes-tqma8xqp-
vm/kernel/src/api/faults.c:10:
/home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30:
note: this is the location of the previous definition
30 #define IRQ_MASK MASK(16u)
which is an indicative that both gic_v3.h & gic_v2.h headers have been
included, which is an error because said headers are not compatible:
kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u)
kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u)
So my question is: how can I configure the build to avoid such a conflict?
I can grepp the relevant configuration option in CMakeCache.txt:
build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h
but cannot see it in ccmake gui because it's "INTERNAL"
What is the solution?
- replace this option somehow to use gic_v2 and have my HW use gic v.2, or
- change compilation options to use gic_v3 everywhere
Thanks for any help,
Chris.
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 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.
I'm trying to build a low memory footprint of RISC-V based seL4. I'm using QEMU/spike for now.
In seL4 12.0 I can modify spike.dts to 8.5 MB of memory 0x00880000.
42 memory@80000000 {
43 device_type = "memory";
44 reg = <0x00000000 0x80000000 0x00000000 0x00880000>;
45 };
This is the smallest value that builds, lower than this I get the error:
[0/1] Re-running CMake...
-- Found GCC with prefix riscv64-unknown-linux-gnu-
STATUS,KernelDTSList: tools/dts/spike.dts
-- /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating...
STATUS,platform_yaml: /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml
-- Detecting cached version of: musllibc
-- Found valid cache entry for musllibc
-- Configuring done
-- Generating done
-- Build files have been written to: /mnt/data/femur_12.0/build
[18/36] Generating gen_headers/image_start_addr.h
FAILED: elfloader-tool/gen_headers/image_start_addr.h
cd /mnt/data/femur_12.0/build/elfloader-tool && sh -c "/mnt/data/femur_12.0/tools/elfloader-tool/../cmake-tool/helpers/shoehorn.py /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml /mnt/data/femur_12.0/build/elfloader-tool/archive.o > /mnt/data/femur_12.0/build/elfloader-tool/gen_headers//image_start_addr.h"
shoehorn: fatal error: ELF-loader image "/mnt/data/femur_12.0/build/elfloader-tool/archive.o" of size 0x107548 does not fit within any memory region described in "{'devices': [{'end': 2147483648, 'start': 0}, {'end': 549755809792, 'start': 2155872256}], 'memory': [{'end': 2155872256, 'start': 2149580800}]}"
ninja: build stopped: subcommand failed.
What do I need to modify to get to < 2 MB?
Thanks!
Dear seL4 community,
As some of you have already noticed, we now have a YouTube channel run by the seL4 Foundation: https://www.youtube.com/channel/UCIqVY1XFPOPIZ1z2A9TrmMA/about. It presently has two playlists, one with the recordings of the seL4 material from this year’s UNSW Advanced Operating Systems course, and one with seL4 Summit talks from Trustworthy Systems.
More to come, enjoy
Gernot
I'm building a simple "hello, world" project and running into some bugs.
The code works, but the after execution there is an exception. It appears to be in restore_user_context or nearby. Can anyone point out what the problem could be here?
user@user-KVM:/mnt/data/sel4hello_manifest/build$ qemu-system-riscv64 --machine spike --nographic --serial mon:stdio --m size=4095M --bios images/hello-image-riscv-spike
bbl loader
ELF-loader started on (HART 0) (NODES 1)
paddr=[80200000..80312d0f]
Looking for DTB in CPIO archive...found at 802e5910.
Loaded DTB from 802e5910.
paddr=[8401e000..8401efff]
ELF-loading image 'kernel'
paddr=[84000000..8401dfff]
vaddr=[ffffffff84000000..ffffffff8401dfff]
virt_entry=ffffffff84000000
ELF-loading image 'hello'
paddr=[8401f000..84157fff]
vaddr=[10000..148fff]
virt_entry=14aa4
Jumping to kernel-image entry point...
Init local IRQ
Initialing PLIC...
Booting all finished, dropped to user space
hello, world!
Warning: using printf before serial is set up. This only works as your
printf is backed by seL4_Debug_PutChar()
hrintf is bac
Caught cap fault in send phase at address 0
while trying to handle:
vm fault on code at address 0 with status 0x1
in thread 0xffffffc17fee8200 "rootserver" at address 0
With stack:
0x143ea0: 0x143ec0
0x143ea8: 0x101ea
0x143eb0: 0x143f00
0x143eb8: 0x14b90
0x143ec0: 0x0
0x143ec8: 0x143f30
0x143ed0: 0x143f20
0x143ed8: 0x143f10
0x143ee0: 0x1
0x143ee8: 0x101d6
0x143ef0: 0x144000
0x143ef8: 0x14cbc
0x143f00: 0x0
0x143f08: 0x14a000
0x143f10: 0x20110
0x143f18: 0x0
Hi there,
I'm working on USB Storage in Sel4 on I.MX7,
when I read/write some block of data from/to USB Driver , sometimes USB Driver fails with this output by this output:
ehci_wait_for_completion@async.c:594 Timeout
this error happened in ehci_schedule_xact function that waiting for transaction completion.
I port USB Driver on I.MX7 but because of above bug, it isn't Stable.
Can anyone help me how to fix this bug?
regards,
Mohamad
--
This email was Anti Virus checked by Security Gateway.
Hello all,
I wonder if it is possible for a component to directly access some specific
part of memory with an address or access the whole component (not some
dataports) using Camkes.
I can see how to set up the permissions (R/W) for each dataport in the
tutorial #port_privileges part,
but I wonder if one component can read some specific memory region with
starting and ending addresses, or read the whole memory where another
component is located.
Thanks for your help!
Best regards,
Seoyeon
Microkernel Devroom at FOSDEM 2021
CALL FOR PARTICIPATION
On-line version of this CfP: http://fosdem.microkernel.info/
The developers and users of several free and open source
microkernel-based operating systems will meet on-line as part of
FOSDEM 2021 [1] and will share a developer room. The devroom is
currently looking for content in the form of talks and activities
related to the area of microkernel-based, unikernel-based,
component-based operating systems and similar topics.
The devroom has been preliminarily scheduled to Saturday February 6th
2021. The devroom will take place during European day hours.
Possible topics of the devroom include, but are not limited to:
* introduction of a specific OS or framework
* design of subsystems and the general architecture of an OS
* used languages, tools and toolchains
* enabling support for hardware (architectures, device drivers)
* enabling support for programming languages
* development processes, debugging
* maintenance, testing and release engineering
* security and robustness
* trends and challenges
* community and governance
* use cases, experiences and status updates
* best practices, lessons learned and demos
This is a call for your participation. We kindly ask you to submit
your proposals no later than on December 26th 2020. Please use the
Pentabarf website [2] to submit your proposals. If you already have
a user account in Pentabarf, please do not create a new one.
Please make sure to select the Microkernel devroom as the track when
submitting your talk and include at least the following information
in your proposal:
* title of your talk
* your full name
* short abstract of your talk (one or two paragraphs)
* duration of your talk (at least 20 minutes and no longer than 50
minutes), excluding a Q&A part
* your short bio
* your photo
The talks will be pre-recorded in advance in January and streamed
during the event. This means that you will need to complete and
submit your talk by around mid January. However, each speaker should
be also present on-line just after the streaming of the talk for
a live Q&A. You can specify your prefered time slot of your talk.
The communication language of the devroom is English.
The official devroom schedule (along with the accepted talks) will be
announced on December 31st 2020 on the devroom's mailing list [3] and
the speakers will be notified via e-mail. The schedule will also be
published on the FOSDEM website.
You are also invited to send any other suggestions for what you want
to see or do at the devroom to the mailing list.
About the Devroom
Since the first Microkernel devroom at FOSDEM 2012 [4], this devroom
has been part of each following FOSDEM. The focus gradually widened
to include component-based and unikernel-based operating systems. By
now it has become a somewhat institutionalized tradition for the
community to meet there. To this date, over a dozen projects have
participated in one way or another. Each of the projects face similar
challenges but come up with partially different solutions. Therefore,
the goal of the devroom is to bring the various projects together,
let them exchange ideas, cross-pollinate and socialize.
Extraordinary Circumstances in 2021
Due to the extraordinary mode of organization of FOSDEM 2021 (being
an on-line event for the first time), many practical aspects of the
devroom are still in the process of determination. For example, the
devroom talks will be required to be pre-recorded in January and
streamed during the event (with a live Q&A), but the technical
details are still sketchy at this moment.
The talk videos will be published under Creative Commons license by
FOSDEM. By submitting a recorded talk, the speaker agrees to have it
made available publicly indefinitively. For organizational purposes,
we also need contact information of the speakers of accepted talks.
Please check the official CfP page [5] of our devroom regularly. We
will keep updating it as new guidelines will be determined by the
FOSDEM organizers.
Sadly, it will not be possible to arrange our traditional microkernel
dinner and other in-person social gatherings in Brussels this time.
However, we plan to organize an on-line replacement. The details will
be announced later in January.
On the other hand, the on-line nature of the devroom allows us to
"overflow" to a second day in case we receive a substatial number of
quality proposals.
About FOSDEM
FOSDEM [6] is a two-day event organised by volunteers to promote the
widespread use of free and open source software. FOSDEM is widely
recognised as one of the best such conferences worldwide. FOSDEM
covers a wide spectrum of free and open source software and hardware
projects and offers a platform for people to collaborate.
To this end, FOSDEM has set up developer rooms (devrooms) where teams
can meet and showcase their projects. Devrooms are a place for teams
to discuss, hack and publicly present latest directions, lightning
talks, news and proposals. Besides developer rooms, FOSDEM also
offers main tracks, lightning talks, and in the past instances
certification exams and project stands.
In recent years, FOSDEM has been hosting more than 5000 developers at
the ULB Solbosch campus. Due to the circumstances, FOSDEM 2021 will
be organized as an on-line event. Despite this, the participation in
FOSDEM is still totally free, although the organisers gratefully
accept donations and sponsorship. No registration is necessary, but
attendees are expected to follow the FOSDEM's code of conduct [7].
Important Dates Recap
* 2020-12-26: Deadline for talk proposal submission
* 2020-12-31: Schedule published and speakers notified of acceptance
* mid January 2021: Time frame for talk pre-recoding
* 2021-02-06: Devroom taking place on-line
Contact
In case of any questions, comments and suggestions, please do not
hesitate to contact the devroom organizers via the devroom's mailing
list [3].
The primary organizers of the devroom in 2021 are:
* Martin Decky
* Jakub Jermar
Links
[1] https://fosdem.org/2021/
[2] https://penta.fosdem.org/submission/FOSDEM21/
[3] https://lists.fosdem.org/listinfo/microkernel-devroom
[4]
https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html
[5] http://fosdem.microkernel.info/
[6] https://fosdem.org/
[7] https://fosdem.org/2021/practical/conduct/
Am I correct to assume that support for running 32-bit code on a
64-bit kernel using compatibility mode rather than virtualization and
support for (presumably limited) direct system calls from VMs,
bypassing any user-mode VMM (using something like Xen's trampoline
page) wouldn't be accepted into seL4?
These are yet more things that I am going to want at some point and
can't think of any other way to do them (besides adding them to the
kernel) without significant penalties to hardware compatibility (in
the case of the 32-bit support; while UX/RT will mostly be focused on
64-bit systems, it will support 32-bit Linux programs in its
compatibility layer) or performance (in the case of direct kernel
traps from VMs; I am planning to write a dynamic general-purpose
hypervisor to go with UX/RT eventually, and adding an extra trap into
the VMM on every IPC would likely add a fair bit of overhead).
Hi,
I have two questions about whether seL4 support C++:
1. When we create a component, whether the src file of component can be c++ style file like **.cxx, or **.cpp ?
I found it will print “camkes.environment.c : undefined reference to run” error when compile
2. If our app code write by c++, how can I use it in seL4 environment as native component?Is there some example ?
Thank you very much.