Hello,
On 04.12.2017 18:15, Edward Sandberg wrote:
> I modified the demo.run file to use fb_boot_drv and built the uefi
> image. I tested it on an UP board, a Minnowboard Turbot, a Dell M3800
> laptop, and a Dell Precision 5810 desktop. I was unable to get
> graphical output on any of them. I have pasted the logs for all (except
> the laptop which has no serial port) below.
> * UP BOARD ********************************
> WARNING: no console will be available to OS
> …
[View More]Bender: Hello World.
> framebuffer at [80000000+808ca000) 1920x1200@32
> framebuffer at [80000000+808ca000) 1920x1200@32
good
> [init -> fb_boot_drv] Framebuffer with 1920x1200x32 @ 0x80000000 type=1 pitch=7680
> [init] child "report_rom" announces service "Report"
> [init -> fb_boot_drv] resource_request: ram_quota=4612096
If you see such a message, the driver or component in general will not
continue.
The specified memory for the driver seems to be too low, try to increase
it. It should be something above 9.2M (7680 Byte * 1200 = 9.2 M + some
memory for the driver). Maybe 10-11M should suffice.
> * MinnowBoard ***********************************
> framebuffer at [80000000+808ca000) 1920x1200@32
> framebuffer at [80000000+808ca000) 1920x1200@32
good
> [init -> fb_boot_drv] Framebuffer with 1920x1200x32 @ 0x80000000 type=1 pitch=7680
> [init -> fb_boot_drv] resource_request: ram_quota=4612096
Same here, try increase the memory for the framebuffer.
> * Dell Precision 5810 **************************************
> Bender: Hello World.
> framebuffer at [f1000000+f1300000) 1024x768@32
> framebuffer at [f1000000+f1300000) 1024x768@32
good
>
> Boot config: parsing cmdline 'sel4 disable_iommu'
> Boot config: console_port = 0x3f8
> Boot config: debug_port = 0x3f8
> Boot config: disable_iommu = true
> module #0: start=0xf9b8000 end=0xffff228 size=0x647228 name='image.elf'
> Physical Memory Region from 0 size a0000 type 1
> Physical Memory Region from 100000 size 997ae000 type 1
> Adding physical memory region 0x100000-0x1f800000
> Physical Memory Region from 998ae000 size 9ac000 type 2
> Physical Memory Region from 9a25a000 size 49000 type 3
> Physical Memory Region from 9a2a3000 size c71000 type 4
> Physical Memory Region from 9af14000 size 492000 type 2
> Physical Memory Region from 9b3a6000 size 65000 type 20
> Physical Memory Region from 9b40b000 size 1000 type 1
> Physical Memory Region from 9b40c000 size e000 type 2
> Physical Memory Region from 9b41a000 size 1be6000 type 1
> Physical Memory Region from a0000000 size 10000000 type 2
> Physical Memory Region from fed1c000 size 4000 type 2
> Physical Memory Region from ff000000 size 1000000 type 2
> Physical Memory Region from 1000000000 size 1760000000 type 1
> Physical memory region not addressable
> Adding physical memory region 0x0-0x1f800000
> seL4 failed assertion '!p_region_overlaps(reg)' at /home/esandberg/projects/embedded/genode-17.11/genode-17.11/contrib/sel4-097171f475bff21223783e130445b9be6b3d1bb4/src/kernel/sel4/src/arn
> halting...
This is a assertion in the seL4 kernel. Probably it complains about that
region overlap due to following lines
> Adding physical memory region 0x100000-0x1f800000
> Adding physical memory region 0x0-0x1f800000
I'm not sure, whether here the Multiboot 2 information is incorrect or
the parsing by the kernel is too strict. Here one would require some
more investigation in the Multiboot 2 spec (overlapping regions are
valid or not?) and on the target machine in grub2/uefi, potentially
bender and the sel4 kernel.
Thanks for testing and the infos.
--
Alexander Boettcher
Genode Labs
http://www.genode-labs.com - http://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
[View Less]
Hi,
I would like to bring up seL4 on inmate cell of Tx1. The jailhouse is
running successfully on Tx1 board. I have created root cell and not root
cell configuration on jailhouse.
I able to load seL4 image successfully on inmate cell then during execution
its stuck in the while extracting the program header.
I checked with jailhouse forum they suggested some one might have ported
seL4 or L4 kernel on jailhouse.also informed that seL4 kernel need to
rebuild with some patches.
Somehow I do …
[View More]not find the patches for seL4 or Fiasco.OC kernel to bring up
on jailhouse.Please share links if you any.
Also experimented by changing the PHY_ADDR higher then 2G (0x80000000)
configuration ie(0x90000000 to 0xF0000000) and (0x100000000 to 0x170000000)
while booting from the u-boot I observed KERNEL DATA abort after boot
strapping the kernel. It means that this address cannot accessible in the
seL4 kernel.
Case 1: 0x90000000 to 0xF0000000
sample logs:
-------------------
Bootstrapping kernel
KERNEL DATA ABORT!
Faulting instruction: 0x1ca9c
FAR: 0x90000000 ESR (DFSR): 0x96000044
halting...
Kernel entry via Interrupt, irq 0
case 2: 0x100000000 to 0x170000000
It's throwing synchronous data abort during program header extraction.
sample logs:
------------------
binaries/elf64: elf64_getNumProgramHeaders
"Synchronous Abort" handler, esr 0x96000044
ELR: 82002c8c
LR: 820031f4
x0 : 0000000100000000 x1 : 0000000000000000
x2 : 000000000022fc10 x3 : 00000000827a5d40
x4 : 0000000000000000 x5 : 00000000000db8ab
x6 : 0000000082007948 x7 : 0000000082008578
x8 : 0000000082008570 x9 : 0000000000000008
x10: 000000000000000f x11: 00000000fed87118
x12: 0000000000000047 x13: 0000000000000040
x14: 0000000000000001 x15: 00000000fed33114
x16: 0000000000000000 x17: 0000000000000000
x18: 00000000fc82ede0 x19: 00000000827a5ff0
x20: 0000000000000002 x21: 0000000082000000
x22: 00000000fc832800 x23: 0000000000000002
x24: 00000000fedaa7fc x25: 0000000000000000
x26: 0000000000000000 x27: 00000000fc8322f0
x28: 0000000000000000 x29: 00000000827a5e80
someone can give suggestion or pointers how we can bring seL4 on Jailhouse.
Regards,
Munees
[View Less]
Hi everyone,
Greetings,
I'm just started with seL4.
Current Progress: - I have built an application on top of seL4 as learning from tutorials, so this is my current design
[seL4,My main_APP,App2,App1,App3]
Here My main_App is my main application build on seL4 and App1, App2 and App3 are sub components link with My main_App.( Just like in Tutorial 4 of seL4).
When i build and run , this is working fine, no issue with it.
when i run make command first i build kernel then …
[View More]libraries, then App1 , App2, App3, then My main_app and in the end it generate a single image file to execute.
My Question :- Can i dynamic load my sub components(App1, App2, App3) which is required by My_main_App in run time ? Can we do that in seL4 is yes then how ? i dont want my App1, App2 and App3 part of final image, I want to load them and run them separately using My_main _App?
Thank you in Advance,
Please Help.
Regards,
Aslam ALVI
#
" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system."
#
[View Less]
Can camkes be used with ARM AARCH64?
I am attempting to build a linux virtual machine on top of the zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project as my reference point.
When the build system attempts to generate camkes-gen.mk, it fails - displaying an error indicating that aarch64 is not a valid architecture specification for camkes. I see that valid arm options are aarch32 or arm_hyp.
Is arm_hyp what I am looking for here?
What would I need to do in order to strip the …
[View More]camkes dependencies out of the tk1 vmm project?
Thanks,
Mike D
Computer Security Engineer - Intelligent Automation, Inc.
(301)294-5263
________________________________
This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
[View Less]
Is there a plan to add UEFI support in seL4 for x86 hardware in the near
future? Newer x86 boards are frequently UEFI only. It is possible to
get around the lack of UEFI support, as I have done with the UP board:
https://up-community.org/wiki/Hardware_Specification
but I am hitting problems which I will detail below.
When I compile using ia32_debug_xml_defconfig and boot using the
resulting images the board fails to find the RSDP location. To fix this
I had to modify the source code a bit:…
[View More]
* seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h
+ #define UPBOARD_RSDP 0x5B161000
* seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c
- acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP,
strlen(ACPI_SIG_RSDP),
- (void *) BIOS_PADDR_START, (void *)
BIOS_PADDR_END);
+ acpi->rsdp = (void *)UPBOARD_RSDP;
* seL4test/kernel/src/plat/pc99/machine/acpi.c
- for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END;
addr += 16) {
+ for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) {
It would be handy to have this as a kernel parameter to cover cases
where it is not successfully discovered automatically. With these
changes I can boot the board and several tests pass but then I get stuck
on INTERRUPT0001 (Test interrupts with timer). I don't get a test
failure or an error the board just sits and makes no more progress.
Someone had that test fail in this post:
https://sel4.systems/pipermail/devel/2017-February/001328.html
and the first recommendation was to check if the irq of the timer was
correctly found. I booted the board into linux to find the correct irq
which was listed as 0 in /proc/interupts. I added a printf to
handleInterrupt in the kernel source, recompiled and when I booted seL4
I found that the irq reported to handleInterrupt is 125 (which sel4
reports as the max interrupt value) every time that function is called.
Adding this printf also showed me that when the test hangs the board
hasn't crashed or locked up as calls to handleInterrupt are made
continuously.
At this point I noticed that before any tests started to run several
ACPI tables are not recognized:
Parsing ACPI tables
Skipping table FPDTD, unknown
Skipping table FIDT<9c>, unknown
Skipping table UEFIB, unknown
Skipping table TPM24, unknown
Skipping table LPIT^D^A, unknown
Skipping table BCFG9^A, unknown
Skipping table PRAM0, unknown
Skipping table CSRTL^A, unknown
Skipping table BCFG9^A, unknown
Skipping table OEM0<84>, unknown
Skipping table OEM1@, unknown
Skipping table PIDVÜ, unknown
Skipping table RSCI,, unknown
Skipping table WDAT^D^A, unknown
Warning: skipping table ACPI XSDT
Maybe one or more of those tables needs to be loaded to handle
interrupts properly. The LPIT table is conspicuous in the case of the
timer test but I think other tests are likely to depend on the other tables.
Any suggestions about porting this type of hardware?
--
Edward Sandberg
Adventium Labs
111 3rd Avenue S. Suite #100
Minneapolis, MN 55401
ed.sandberg(a)adventiumlabs.com
[View Less]
Hi everyone,
I have built a very simple application that loads another process, which
is very similar to the tutorials. For testing I wanted to send from the
second process to the first one using seL4_Send and observe that the
second process never continues after the seL4_Send blocked, despite the
receiver called seL4_Recv and got the message. If I call seL4_Call and
the receiver does seL4_Recv + seL4_ReplyRecv it works without any other
changes to the code. I am wondering if I am …
[View More]understanding something
fundamentally wrong and/or what the best strategy to debug this behavior
is.
Thanks for your help!
Cheers,
Stefan
[View Less]
We have a multi component camkes application with each component using a
few common services and then having application interfaces to a small
number of other components.All these components are imported into a top
level system description camkes file.
Examining the generated camkes I see that all the generated header and
source files have exactly the same make prerequisites meaning a change to
logically unrelated components causes them all to be regenerated and
recompiled.
Now I have …
[View More]discovered the camkes cache this is less of an issue but is
there a better way we can structure our application to reduce the
edit-compile-go cycle ?
Regards
Gordon
[View Less]
We have a security requirement on our ARM based product using CAmkES 2.2.x
to ensure all sensitive data declared in specific seL4SharedData regions
are erased on detection of a power failure. We achieve this by overwriting
the data with a known pattern that we read back from a separate component
before declaring the device as secured. This is working fine. But we need
to guarantee that the overwrite data is actually written to DDR and we
aren't just using cached values. This means flushing the …
[View More]L1 and L2 data
caches specific regions.
We could use seL4HardwareMMIO regions and declare our data in the memory
map and use these regions as un-cached. Or use the _hardware_cached
attribute and call the provided flush method when necessary. Our main issue
with doing this, except the fiddle of mapping multiple different sized
regions into the memory map, is we could potentially expose the physical
locations of the sensitive data rather than having it wrapped in the
virtual address space of a component.
Having a flush method on seL4SharedData would be the ideal solution.
We are not in a position to upgrade our CAmkES version on this product at
the moment.
Any thoughts?
Zippy
[View Less]
Hi,
The PPTR address range between UART and GIC distributor was 12k
(kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1
reference sheet the length was specified as 64byte for UART,4k for GIC
distributor and 8k for interrupt controller.
can you please point out the reference or reason to choose this address for
Tx1 board?
/* These devices are used by the seL4 kernel. */
#define UARTA_PPTR 0xffffffffffff0000
#define GIC_DISTRIBUTOR_PPTR …
[View More]0xffffffffffff3000
#define GIC_CONTROLLER_PPTR 0xffffffffffff4000
These addresses are used during kernel device map to access in the
userspace
map_kernel_devices : kernel_devices[i].paddr :0x50042000
kernel_devices[i].pptr 0xffffffffffff4000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]:
0xffffff800002b000 vaddr :0x1f4
map_kernel_devices : kernel_devices[i].paddr :0x50041000
kernel_devices[i].pptr 0xffffffffffff3000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]:
0xffffff800002b000 vaddr :0x1f3
map_kernel_devices : kernel_devices[i].paddr :0x70006000
kernel_devices[i].pptr 0xffffffffffff0000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]:
0xffffff800002b000 vaddr :0x1f0
Regards,
Munees
[View Less]
Hi seL4 Dev Team,
I am bringing up the sel4 kernel on tx2 board with ref of Tx1. I
encountered the TLB invalidation hang issue after kernel map window setup.
I do not know the exact reason for hang so just disable that piece of code
to look further execution of sel4 kernel. After that it dropped into the
usersapce and throwing the cap fault or vm fault issue.
Does anyone has come across this type of issue and how it debugged?.
Please share your thought or pointers to debug this issue. I …
[View More]shared the
full log details here.
## Starting application at 0x82000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3
paddr=[82000000..827abfff]
kernel_phys_start: 0xffffffff80000000
kernel_phys_end:0xffffffff8022fcdf
load_elf : image_size 0x230000
ELF-loading image 'kernel'
paddr=[80000000..8022ffff]
vaddr=[ffffff8000000000..ffffff800022ffff]
virt_entry=ffffff8000000000
load_elf : image_size 0x5e9000
ELF-loading image 'sel4test-driver'
paddr=[80230000..80818fff]
vaddr=[400000..9e8fff]
virt_entry=41b160
Enabling MMU and paging
Jumping to kernel-image entry point...
kernel_info.virt_entry : 0x0
user_info.phys_region_start : 0xffffffff80230000
user_info.phys_region_end:0xffffffff80819000
user_info.virt_region_start:0x400000
user_info.virt_region_end:0x9e9000
user_info.phys_virt_offset:0x7fe30000 user_info.virt_entry:0x41b160
Bootstrapping kernel
Booting all finished, dropped to user space
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on code at address 0x41b160 with status 0x82000010
in thread 0xffffff8027ef4200 "rootserver" at address 0x41b160
With stack:
halting...
Kernel entry via VM Fault, fault type: 4305248
Thanks in advance
Muneeswaran R
[View Less]
