Hi Jeff,
Comments inline:
On Tue, 2017-01-31 at 18:25 +, Brandon, Jeffrey - 0553 - MITLL
wrote:
> Thanks Alex,
>
> So in this JTAG example does the run command begin the 3 step boot process
> you outlined?
1. connect arm hw
2. rst # Reset the device
3. fpga -f
Hi Jeff,
The boot process is as follows:
1) u-boot loads the seL4 ELF file into memory at ${loadaddr}
2) u-boot reads the ELF file and copies the appropriate sections to the
correct address for program execution
3) u-boot reads the entry point from the ELF file and jumps to the
address to
Hi Wladi,
seL4test is the foundation of our regression tests. If you have made it
this far in the boot process, the issue is likely to reside in your
platform dependent user space timer or UART driver.
0x805 corresponds with a level 1 translation fault. This means that
there is no virtual
A "Synchronous Data abort" occurs when a virtual memory translation
fails on load/store operations.
A "Prefetch abort" occurs when a virtual memory translation fails when
loading instructions into the CPU pipeline.
An "Asynchronous Data abort" occurs when a physical memory translation
fails (ie,
Hi Wladislav,
If the fault occurs before the activation of the kernel PD, this likely
means that you are trying to printf before the UART is mapped.
If you are using printf for debugging before the PD is activated, you
will need to change your kernel UART driver to use the physical address
of
Hi Wladi,
The addresses must be aligned to the size of the frame to be mapped.
For a small page, it must be aligned to 0x1000. This is a requirement of
the ARM hardware rather than the seL4 kernel.
The simple workaround is to add an additional offset to the mapped
address. You can see how the
Hi Wladi,
If the problem is with your driver, the problem could be in your
management of the INTCTLSTAT register (Chapter 5.10).
1) ARM devices tend to only support 32bit read/write
2) Check that the interrupt enable flag is set before returning from
your timer set up code.
3) The status bits
Hi Oak,
I don't suppose that any of those calls are returning errors?
DMA is optional for the SDHC. It has been a while since I looked at the
code, but I believe that passing 0 as the paddr will prevent the driver
from using DMA. Of course, this is not a solution to your problem, but
it could
Hi Mark,
0xf800 | 0012 | [520 <--> 521 ]
This should cover memory in the range 0xf800-0xf8001fff
Your timer @ 0xF8F00200 is not in this range.
The global/private timers provided by Cortex-A9 CPU's are reserved for
the kernel scheduler.
Which platform are you using? Are there any
Hi Rina,
The seL4 micro-kernel does not provide any typical OS services,
instead, these should be provided by user space drivers and processes.
Unfortunately, we do not yet provide any user space services for
acquiring the time of day, however, we do provide timer drivers.
The timer driver API
Hi Oak,
Your code looks fine, but where do these numbers come from?
void* vaddr = (void*) 0x198;
uintptr_t paddr = (uintptr_t) 0x119a7000;
vaddr should be the virtual address of a buffer to which the block
should be read, and paddr should be the physical address of this buffer.
- Alex
Hi Andrew,
Thanks for your contributions. We will add Zynq simulation to our
regression tests.
- Alex
On Tue, 2016-12-06 at 19:56 -0600, Andrew Gacek wrote:
> It looks like the libplatsupport drivers do this enabling as well.
> Though it appears there's a typo in the transmit enable:
>
>
Hi Peng,
ARM provides hardware support for virtual interrupts. When the VM writes
to the acknowledge register of the virtual interrupt controller, an IRQ
exception is triggered and delivered to PL2 (hypervisor mode).
- Alex Kroh
On Sun, 2017-01-08 at 17:22 -0500, PX wrote:
> Hi, all
> I
Hi Brandon,
The seL4test project has some example code for setting up these
frameworks.
Initialise 'simple' - and abstraction for the boot information that seL4
provides to the initial thread:
https://github.com/seL4/sel4test/blob/master/apps/sel4test-driver/src/main.c#L479
Configure a kernel
Hi Joyce Peng,
The ARM has a hardware page table walker, but the walker and CPU don't
have the same view of memory. Once the CPU has written to the page
table, it must clean the cache line before it is visible to the walker.
My hunch is that you will need to modify the following code which
Hi Joyce,
Sorry for the delay. I see that your question about Cortex-A7 support
has already been answered:
http://sel4.systems/pipermail/devel/2017-May/001410.html
Which CP15 registers are you having trouble accessing, and from which
CPU mode are you trying to access them (PL1/kernel or
Hi Munees,
Apologies for the bum steer. I have now heard that the "bootelf"
command does not work on the tx1, obviously this information comes too
late.
The alternative is to convert the elf format file into a binary file,
load it to the correct location in memory, and use the "go" command
with
Hi Muneeswaran,
The steps that you are using are correct, but it looks like you are
trying to boot the kernel without a user space image.
Try booting a complete image file from the ./images/ directory of the
project that you are using.
- Alex
On Wed, 2017-10-11 at 13:22 +0530, Muneeswaran
Hi Munees,
I am afraid that this is the limit of my TX1 knowledge. Sorry I can't
be more help.
- Alex
On Tue, 2017-10-17 at 11:03 +0530, Muneeswaran Rajendran wrote:
> Hi Alex,
>
> Thanks for confirmation. As you suggested to use binary file to load
> at address is 0x0.
>
> Build the binary
Hi Joel,
The serial driver in the elfloader and kernel are very limited. It
doesn't perform any baud rate configuration and hence won't be affected
by frequency variations between platforms. Only the user space drivers
are affected.
Memory is defined in the kernel here:
Hi Munees,
I am afraid I can't be much help, but I can offer some tips for debug
printing.
The elfloader boots the kernel with unity mappings. If you would like
to use debug printing before the kernel maps the serial port, try
changing UARTA_PPTR to UARTA_PADDR in the UART driver:
Hi Joel,
You could try changing the reported frequency of the UART reference
clock:
https://github.com/seL4/util_libs/blob/master/libplatsupport/src/mach/z
ynq/serial.c#L20
Or you could skip the baudrate configuration step altogether:
Hi Chris,
I am afraid not. For a hyp kernel, we reserve an entry in the first level page
directory to store its associated ASID. If we were able to store this
elsewhere, the application would have full use of the virtual address space.
You might be able to convince Linux that the devices are
Hi Munees,
The GIC_DISTRIBUTOR_PPTR is the virtual address at which the kernel
can access the physical address range of the distributor. The address
is somewhat arbitrary. We start at 0xf..f and bump this pointer for
each kernel-accessible device (GIC/TIMER/UART/etc).
- Alex
On Fri,
Hi Joel,
Which Zynq-7000 platform are you using?
The supported platform is the ZC706. Other platforms might need some
trivial changes, particularly for UART baudrate configuration.
Are you using the debug or release config?
The debug build should show additional messages during boot.
- Alex
Hi Oak,
What frequency are you running the CPU at? The default is 800MHz.
800 / 800MHz = 10ms
- Alex
On Thu, 2017-10-19 at 21:41 -0700, Norrathep Rattanavipanon wrote:
> Yes, ideally we would want to run our experiments on the RT branch.
> But given the close deadline, i'd rather do it
Hi Sathya,
I'm familiar with the use of the elfloader on ARM platforms, but not so
familiar with the RISC-V port.
My bet is that the memcpy is overwriting some part of the elfloader code, data
or stack sections.
To resolve this, you could try to load/execute the elfloader from a higher
address
Hi Dan,
It is likely that the instruction that is causing the fault is not being
decoded by hardware or software. ARM has done a reasonable job in providing
hardware support for decoding faulting instructions, but only a subset of the
ISA is supported.
The instruction causing the fault
Hi Robbie,
You could run seL4 on the Cortex-A and eChronos on the Cortex-R. If you intend
to run a single single-threaded application on the Cortex-R, you could run the
server without an OS.
I recommend that you load and start the server OS (or bare metal server) using
the elfloader rather
29 matches
Mail list logo
