Re: [seL4] seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs)

[Alexander.Kroh]

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 than an seL4 application:

1. In its current form, the elfloader is linked with a CPIO archive that 
contains the user image and seL4. You would need to modify the build system to 
include a third object in this archive.

2. Modify the elfloader code to load this third object:
 https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/common.c#L264

3. You will need to write code to boot the Cortex-R CPUs. This code is not for 
the Ultrascale, but hopefully it will give you a head start:
https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/plat/zynq7000/smp.c#L65

4. Modify seL4 to reserve the physical memory that your server will occupy use:
https://github.com/seL4/seL4/blob/master/include/plat/zynqmp/plat/machine/hardware.h#L58

Since your server will have access to all physical memory, sharing data between 
client and server will be easy. All that remains is a method for notifying 
client and server when data has been updated. While polling shared memory would 
be a good start, you might be able to use software generated IRQs in your final 
solution.


Regards,

  - Alex




From: Devel  on behalf of 
gernot.hei...@data61.csiro.au 
Sent: Wednesday, November 7, 2018 6:53 AM
To: devel@sel4.systems
Subject: Re: [seL4] seL4 on Heterogeneous Processing Architectures (Zynq 
UltraScale+ MPSoCs)
  
On 6 Nov 2018, at 22:27, Blam Kiwi  wrote:



I  wasn't fully appreciating the difference between the MPU and MMU in relation 
to seL4. If the R5's can't be supported then that simplifies the decision space 
somewhat. Guess I'll evaluate the RTOSes before throwing my hands in the air 
and rolling my own design. 
  

You  could run eChronos. It’s an RTOS with a (partial) verification  story that 
supports the  MPU: https://ts.data61.csiro.au/projects/TS/echronos/


Gernot
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Strange behavior when writing to memory mapped to a custom device in the VMM.

[Alexander.Kroh]

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 might be a load with increment (*pArray++). A 
trivial fix might be to rewrite your code as:

 #define idx(i) (i%16)
  for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++){
    mem[idx(i)] = *pArray[i];
  }

Failing that, I recommend using objdump to identify the faulting instruction 
and follow the code path in 
../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357 to see 
how that particular instruction is being decoded and handled.

 - Alex Kroh


From: Devel  on behalf of Dan DaCosta 

Sent: Saturday, September 8, 2018 4:19 AM
To: devel@sel4.systems
Cc: Darren Cofer
Subject: [seL4] Strange behavior when writing to memory mapped to a custom 
device in the VMM.
  

To Whom It May Concern:

I am observing seL4+VM+ARM behavior on the TK1-SOM that I find very
puzzling. Consider the following code:

  #define idx(i) (i%16)
  for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++, pArray++){
    mem[idx(i)] = *pArray;
  }

where 'pArray' is the array representation of 'buf' and 'mem' is a
memory mapped page set that corresponds to a page set of memory that
is managed by a fault handler in the VMM (something I have installed
myself using a 'DEV_CUSTOM' device). This code runs as I would expect.
However, the follow code results in an assertion failure in the VMM:

  #define idx(i) (i%16)
  for(i = 0; i < 16; i++, pArray++){
    mem[idx(i)] = *pArray;
  }

The error report follows:

  32 bit ARM insts not decoded
  
  Pagefault from [Linux]: write fault @ PC: 0xbd7499a8 IPA: 0xe0001000, FSR: 
0x246
  Context:
  r0: 0xb6d2a050
  r1: 0x0
  r2: 0xb6ac76b8
  r3: 0x4c
  r4: 0xb6d2a050
  r5: 0xb6d2a8ec
  r6: 0x1
  r7: 0xb6d2a050
  r8: 0x7fb73000
  r9: 0xad13cfff
  r10: 0xabe31310
  r11: 0x19
  r12: 0xb6d285d8
  pc: 0x7f68f9a8
  r14: 0x7f68f99c
  sp: 0xaf1c3c20
  cpsr: 0x8010
  
  Assertion failed: rt >= 0 
(../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357)
  
Some added information that may be helpful; if the strange modulo
operation I am performing on the index is removed I receive a similar
crash for both code snippets.

Any thoughts on where I might look to get to the bottom of this problem
would be helpful.

Thanks!
Dan DaCosta


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Porting SEL4 on RISCV FPGA

[Alexander.Kroh]

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 in memory.

Alternatively, the destination address range for the memcpy may not be to RAM. 
It might help to draw a diagram of where RAM lies, where the elfloader lies, 
and where the kernel and user images will be copied to.

 - Alex



From: Devel  on behalf of Sathya Narayanan N 

Sent: Friday, August 3, 2018 10:13 PM
To: devel@sel4.systems
Subject: [seL4] Porting SEL4 on RISCV FPGA

Hi,

I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf loader.

The function stuck is memcpy. I have added prints and I am not progressing 
after the last memcpy call in unpack_elf_to_paddr(). All kinds of input 
appreciated.


Function under review:
static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)

/* Parse size/length headers. */
dest_vaddr = elf_getProgramHeaderVaddr(elf, i);
data_size = elf_getProgramHeaderFileSize(elf, i);
data_offset = elf_getProgramHeaderOffset(elf, i);

/* Load data into memory. */

memcpy((char *)dest_vaddr + phys_virt_offset,
   (char *)elf + data_offset, data_size);
printf("loaded data into memory \n"); -> Stuck Here !
 }

}

Can anyone give me a clue on whatsoever to check here ? It worked perfectly in 
spike simulation.

RISCV FPGA configuration - It supports IMAFD. It has already booted linux. 
Kernel is loaded at physical address 80 million.?

--
 regards,
Sathya


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] 1:1 Mapping of Zynqmp devices

[Alexander.Kroh]

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 at a more appropriate 
location by changing their address in the device tree.


 - Alex



From: Devel  on behalf of Chris Guikema 

Sent: Thursday, November 16, 2017 3:27 AM
To: devel@sel4.systems
Subject: [seL4] 1:1 Mapping of Zynqmp devices

Hello,

I am attempting to port the camkes-arm-vm to the zynqmp platform. For the TK1 
and Exynos platforms, the physical address of the hardware devices are well 
below the kernelBase of 0xe000. However, for the zynqmp, these hardware 
devices are greater than the kernel base. This causes the "map_emulated_device" 
function call to fail for the GIC and any other passthrough devices.

sel4utils_reserve_range_at_no_alloc@vspace.c:589 Range not available at 
0xff01, size 0x1000
Assertion failed: res.res 
(/home/chrisguikema/seL4/NAMC/camkes-arm-vm/libs/libsel4arm-vmm/src/devices.c: 
map_device: 160)

Is there a way to 1:1 map these devices, even if they are above the kernelBase?

Thanks,
Chris


___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] loading and booting seL4 on a tegra Tx2

[Alexander.Kroh]

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:
https://github.com/seL4/seL4/blob/master/src/plat/tx1/machine/io.c#L23

 - Alex

On Sat, 2017-11-11 at 11:26 +0530, Muneeswaran Rajendran wrote:
> Hi,
> 
> I am trying to bring up sel4 on tegra Tx2 platform using tegra Tx1 as
> reference.
> 
> I tweaked the important changes of UART,Timer configuration and IRQ
> number and also GIC controller, GIC distributor configuration w.r.t
> Tx2
> 
> after loading and booting the Tx2 board sel4 enter into init kernel
> to initialize the kerenl memory map for GIC and UART devices then
> control transfer to user space. I underdtand from ref manual both Tx1
> and Tx2 using the same clock and baud rate for UART configuration. 
> 
> ## Starting application at 0x8200 ...
> 
> ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3
>   paddr=[8200..827abfff]
>  kernel_phys_start: 0x8000 
>  kernel_phys_end:0x8022fcdf
>  load_elf : image_size 0x23
> ELF-loading image 'kernel'
>   paddr=[8000..8022]
>   vaddr=[ff80..ff800022]
>   virt_entry=ff80
> load_elf : image_size 0x5e9000
> ELF-loading image 'sel4test-driver'
>   paddr=[8023..80818fff]
>   vaddr=[40..9e8fff]
>   virt_entry=41b160
> Enabling MMU and paging
> Jumping to kernel-image entry point...
> 
> Also try to add debug print in the init kernel thread to understand
> the virtual memory set-up but its crashed with synchronous exception.
> 
> It indicates that the UART driver till not available to log the
> messages this was seen in Tx1 and Tx2. Not able to check/debug
> further on this issue.
> 
> Also experimented with various arbitrary address for UARTA_PPTR and
> GIC_PPTR because Tx1 UARTA has 64byte size in case of Tx2 its 1MB.but
> still nothing has improved the state remain same.
> 
> I completely walk through the sel4 boot and arm MMU code.I do not see
> any board specific changes in this code apart from UART,GIC
> configuration and IRQ number. The assembly code of MMU mainly setting
> up TCR ,TTBR , TLB invalidation and pagetable setup for arma-57.
> 
> Please let me know your thought on this issue and how do debug this
> kind of issue.
> 
> Regards,
> Munees
> 
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] loading and booting seL4test on a zynq7000

[Alexander.Kroh]

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:
https://github.com/seL4/seL4/blob/master/include/plat/zynq7000/plat/mac
hine/hardware.h#L57

Note that the kernel will limit usable memory to ~512MB. It is probably
safe to assume that your 128MB memory is in the range 0x to
0x0800.

Additionally, the start address of the elfloader must be changed to a
valid address:
https://github.com/seL4/seL4_tools/blob/master/elfloader-
tool/gen_boot_image.sh#L51

Try 0x0400 or 0x0600.

 - Alex


On Sat, 2017-11-11 at 08:46 +0100, Joel Svensson wrote:
> Thanks again Alex, 
> 
> I'm suspecting something else (to begin with). Since I do get some
> output from elf_loader I went in there 
> and added a few printfs. It seems execution just stops when it has
> entered into the unpack_elf_to_paddr function. 
> It seems to be a memset call in there that just locks up any
> progress. 
> 
> One big difference my platform and the supported one is the amount of
> memory. The board I tried this 
> on has only 128mb. Is it possible that I need to change some memory
> layout-describing files to take this into account. 
> 
> If 128mb is just way too little I have some 512mb variants as well. 
> 
> At least for elf_loader it seems the uart setup is compatible with
> the configuration for the supported board. Maybe 
> this will be a problem again, later in the boot process, but right
> now I suspect the memory difference. 
> 
> Thanks again and have a great weekend. 
> /Joel 
> 
> On Sat, Nov 11, 2017 at 12:42 AM, 
> wrote:
> > Hi Joel,
> > 
> > You could try changing the reported frequency of the UART reference
> > clock:
> > https://github.com/seL4/util_libs/blob/master/libplatsupport/src/ma
> > ch/z
> > ynq/serial.c#L20
> > 
> > Or you could skip the baudrate configuration step altogether:
> > https://github.com/seL4/util_libs/blob/master/libplatsupport/src/ma
> > ch/z
> > ynq/serial.c#L379
> > 
> >  - Alex
> > 
> > 
> > 
> > 
> > On Fri, 2017-11-10 at 07:51 +0100, Joel Svensson wrote:
> > > Hello Alex and thank you. 
> > >
> > > You assumption is correct, I am on a non-supported platform (the
> > > Trenz ZynqBerry). So probably some tweaks will be needed. 
> > > Do you suspect that I will need to make these changes in the sel4
> > > code or will finding and changing some configuration file be
> > enough? 
> > > First, of course, I need to figure out what the important
> > differences
> > > between the ZC706 and the ZynqBerry are. 
> > >
> > > I was using the release build but now switched to debug and tried
> > > that as well. That did not produce any additional output. 
> > > So that UART configuration changes are needed sound very
> > likely.  
> > >
> > > Thanks again and have a great day
> > > /Joel 
> > >
> > > On Fri, Nov 10, 2017 at 12:18 AM,  > >
> > > wrote:
> > > > 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
> > > >
> > > >
> > > >
> > > >
> > > > On Thu, 2017-11-09 at 13:35 +0100, Joel Svensson wrote:
> > > > > Hello, 
> > > > >
> > > > > I want to learn about seL4 so I am trying to get is started
> > on
> > > > the
> > > > > hardware I already have (a zynq 7000). 
> > > > >
> > > > > I have generated the image: sel4test-driver-image-arm-
> > zynq7000
> > > > >
> > > > > Now I try to load that onto the zynq by executing these
> > commands
> > > > in
> > > > > XMD:
> > > > > connect arm hw 
> > > > > rst
> > > > > fpga -f design_1_wrapper.bit
> > > > > source ps7_init.tcl
> > > > > ps7_init
> > > > > ps7_post_config
> > > > > dow sel4test-driver-image-arm-zynq7000
> > > > > run 
> > > > >
> > > > > All of the above seem to be successful. Then, I have a serial
> > > > link
> > > > > hooked up to the board (uart)
> > > > > and there I get the following output (screen /dev/ttyUSB1
> > 115200)
> > > > : 
> > > > > ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0
> > > > >   paddr=[1000..103c881f]
> > > > > ELF-loading image 'kernel'
> > > > >   paddr=[0..2afff]
> > > > >   vaddr=[e000..e002afff]
> > > > >   virt_entry=e000
> > > > >
> > > > > But then nothing more. I am lost what to do from this
> > position in
> > > > > order to continue exploring seL4. 
> > > > > I don't even know if what I see is an indication of a problem
> > or
> > > > > not. 
> > > > > If anyone has experience in running seL4 on zynq and if you
> > sit
> > > > on
> > > > > knowledge you want to share, 
> > > > > 

Re: [seL4] loading and booting seL4test on a zynq7000

[Alexander.Kroh]

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:
https://github.com/seL4/util_libs/blob/master/libplatsupport/src/mach/z
ynq/serial.c#L379

 - Alex




On Fri, 2017-11-10 at 07:51 +0100, Joel Svensson wrote:
> Hello Alex and thank you. 
> 
> You assumption is correct, I am on a non-supported platform (the
> Trenz ZynqBerry). So probably some tweaks will be needed. 
> Do you suspect that I will need to make these changes in the sel4
> code or will finding and changing some configuration file be enough? 
> First, of course, I need to figure out what the important differences
> between the ZC706 and the ZynqBerry are. 
> 
> I was using the release build but now switched to debug and tried
> that as well. That did not produce any additional output. 
> So that UART configuration changes are needed sound very likely.  
> 
> Thanks again and have a great day
> /Joel 
> 
> On Fri, Nov 10, 2017 at 12:18 AM, 
> wrote:
> > 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
> > 
> > 
> > 
> > 
> > On Thu, 2017-11-09 at 13:35 +0100, Joel Svensson wrote:
> > > Hello, 
> > >
> > > I want to learn about seL4 so I am trying to get is started on
> > the
> > > hardware I already have (a zynq 7000). 
> > >
> > > I have generated the image: sel4test-driver-image-arm-zynq7000
> > >
> > > Now I try to load that onto the zynq by executing these commands
> > in
> > > XMD:
> > > connect arm hw 
> > > rst
> > > fpga -f design_1_wrapper.bit
> > > source ps7_init.tcl
> > > ps7_init
> > > ps7_post_config
> > > dow sel4test-driver-image-arm-zynq7000
> > > run 
> > >
> > > All of the above seem to be successful. Then, I have a serial
> > link
> > > hooked up to the board (uart)
> > > and there I get the following output (screen /dev/ttyUSB1 115200)
> > : 
> > > ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0
> > >   paddr=[1000..103c881f]
> > > ELF-loading image 'kernel'
> > >   paddr=[0..2afff]
> > >   vaddr=[e000..e002afff]
> > >   virt_entry=e000
> > >
> > > But then nothing more. I am lost what to do from this position in
> > > order to continue exploring seL4. 
> > > I don't even know if what I see is an indication of a problem or
> > > not. 
> > > If anyone has experience in running seL4 on zynq and if you sit
> > on
> > > knowledge you want to share, 
> > > please fill me in. 
> > >
> > > Thank you
> > >
> > >
> > > ___
> > > Devel mailing list
> > > Devel@sel4.systems
> > > https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] loading and booting seL4test on a zynq7000

[Alexander.Kroh]

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




On Thu, 2017-11-09 at 13:35 +0100, Joel Svensson wrote:
> Hello, 
> 
> I want to learn about seL4 so I am trying to get is started on the
> hardware I already have (a zynq 7000). 
> 
> I have generated the image: sel4test-driver-image-arm-zynq7000
> 
> Now I try to load that onto the zynq by executing these commands in
> XMD:
> connect arm hw 
> rst
> fpga -f design_1_wrapper.bit
> source ps7_init.tcl
> ps7_init
> ps7_post_config
> dow sel4test-driver-image-arm-zynq7000
> run 
> 
> All of the above seem to be successful. Then, I have a serial link
> hooked up to the board (uart)
> and there I get the following output (screen /dev/ttyUSB1 115200) : 
> ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0
>   paddr=[1000..103c881f]
> ELF-loading image 'kernel'
>   paddr=[0..2afff]
>   vaddr=[e000..e002afff]
>   virt_entry=e000
> 
> But then nothing more. I am lost what to do from this position in
> order to continue exploring seL4. 
> I don't even know if what I see is an indication of a problem or
> not. 
> If anyone has experience in running seL4 on zynq and if you sit on
> knowledge you want to share, 
> please fill me in. 
> 
> Thank you
> 
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] PPTR address computation on Sel4 Kernel

[Alexander.Kroh]

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, 2017-11-03 at 18:55 +0530, Muneeswaran Rajendran wrote:
> Hi sel4 development team,
> 
> I understand from the sel4 kernel the paddr and pptr used in the
> kernel framework to compute the page table entry. I found from ref
> manual GICD_PADDR defined as (ARM_PERIPHBASE (0x5004) + 0x1000) 
> 0x50041000 for that GIC_DISTRIBUTOR_PPTR used as 0x3000.
> This details was not able to see in the ref manual and other sel4
> reference. 
> 
> Can someone help to understand the pptr calculation w.r.t sel4?
> 
> Thanks in advance
> Munees
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Questions on seL4's scheduling

[Alexander.Kroh]

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 on the master branch,
> which I'm more familiar, and we can still keep the formally verified
> property :).
> 
> We kind of want to simulate a quick and simple real-time scheduling
> in the master branch.
> Basically, the main thread wants to run a long task but we dont want
> it to hoard all resources. So we split it into a bunch of smaller
> tasks. Then, for a security reason, we want to run each of the
> smaller tasks atomically. One way I can think of is to temporarily
> raise the priority of the main thread when running each task and
> yield once a task is finished.  The goal is to complete the long task
> ASAP while allowing other processes to run if needed. I then want to
> see how much time other processes can use between two tasks.
> 
> Oak
> 
> 
> 
> On Thu, Oct 19, 2017 at 6:06 PM,  wrote:
> > 
> > Recall I stated that the scheduler is basic ;)
> > 
> > The timer ticks on the master kernel are started on boot, then not
> > reset on any thread operation. This means that the actual thread
> > timeslice is just 'X interrupts must come in'. So it's likely to
> > vary by up to the tick ms value, as the yield does not have any
> > relation with a new tick starting.
> > 
> > If you measured the time for many threads (100 or so) to all
> > consumer their timeslice, you should see the error drop off and the
> > average value approach the timeslice.  
> > 
> > I'm curious as to what exactly you are trying to do? the RT kernel
> > may be more suited.
> > 
> > Thanks
> > Anna. 
> > 
> > From: Norrathep Rattanavipanon 
> > Sent: Friday, 20 October 2017 11:52 AM
> > 
> > To: Lyons, Anna (Data61, Kensington NSW)
> > Cc: devel@sel4.systems
> > Subject: Re: [seL4] Questions on seL4's scheduling
> >  
> > Thanks Anna. So I tried to measure timeslice in userspace and it
> > seems like it does not match with the settings. Any idea what
> > happens or what is wrong with my code:
> > I ran it on IMX6-SabreLite, master branch/kernel version 4.0.
> > 
> > main thread:
> > sel4bench_init();
> > seL4_Yield();
> > uint64_t start = sel4bench_get_cycle_count();
> > seL4_Yield();
> > uint64_t end = sel4bench_get_cycle_count();
> > sel4bench_destroy();
> > printf("Takes %llu\n", (end-start));
> > 
> > second thread:
> > while(1);
> > 
> > Both of them have the same priority.
> > 
> > When I set TIMER_TICK_MS=5 and TIME_SLICE=2, it outputs 800,
> > which is around 8msecs.
> > Also, if i set TIMER_TICK_MS=2 and TIME_SLICE=1, I get around
> > 1.6msecs.
> > 
> > Best,
> > 
> > On Thu, Oct 19, 2017 at 5:03 PM, 
> > wrote:
> > > Hi Oak,
> > > 
> > > The timeslice value on the master kernel is only reset on thread
> > > creation and once the thread is depleted, so when a thread drops
> > > its priority the timeslice will not change, so it'll run for 2ms.
> > > 
> > > The timeslice cannot be set to lower than 1 ms, however you could
> > > change the timer driver on your target platform to do so (look at
> > > the initTimer function).
> > > 
> > > Note that the scheduler on the master kernel is fairly basic, the
> > > RT branch is far more fully featured (tickless and you can set
> > > different timeslices per thread). 
> > > 
> > > Cheers
> > > Anna. 
> > > 
> > > From: Norrathep Rattanavipanon 
> > > Sent: Friday, 20 October 2017 10:18 AM
> > > To: Lyons, Anna (Data61, Kensington NSW)
> > > Cc: devel@sel4.systems
> > > Subject: Re: [seL4] Questions on seL4's scheduling
> > >  
> > > Also, is it possible to set timeslice to be less than 1
> > > milliseconds?
> > > 
> > > On Thu, Oct 19, 2017 at 3:08 PM, Norrathep Rattanavipanon  > > n...@uci.edu> wrote:
> > > > Thank you, Anna and Gernot for the answer.
> > > > 
> > > > One more question, so assuming a timeslice is 5ms, a thread
> > > > with the highest priority has run for 3ms, then drops its
> > > > priority to be the same as the other thread.
> > > > Then, the same thread will start running with the fresh
> > > > timeslice and it will run for another 5ms or will it just run
> > > > for 2ms to complete the timeslice?
> > > > 
> > > > Oak
> > > > 
> > > > On Mon, Oct 16, 2017 at 3:09 PM, 
> > > > wrote:
> > > > > Hi Oak,
> > > > > 
> > > > > Assuming your questions are about the master branch of the
> > > > > kernel, as on the RT branch the kernel is tickless.
> > > > > 
> > > > > 1. There are two config paramters
> > > > >     + TIMER_TICK_MS is how many milliseconds per tick
> > > > >     + TIME_SLICE is how many ticks per timeslice. 
> > > > > 
> > > > > 2. Assuming a thread is waiting on a notification object for
> > > > > an irq to arrive, and another thread is 

Re: [seL4] 64 bit ARM ELF image load in Tx1 platform

[Alexander.Kroh]

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 image using menuconfig option and loaded the image
> into 0x00, and used the 'go 0x0'.
> 
> but still kernel crashed with below dump.
> 
> Tegra210 (P2371-2180) # ext4load mmc 1 0x0 sel4test-driver-image-arm-
> tx1.bin 
> 6858320 bytes read in 451 ms (14.5 MiB/s)
> Tegra210 (P2371-2180) # go 0x0
> ## Starting application at 0x ...
> "Synchronous Abort" handler, esr 0x860e
> ELR: 0
> LR:  ff1328d0
> x0 : 0001 x1 : fcc2c238
> x2 : fcc2c238 x3 : 
> x4 : 0030 x5 : 
> x6 : ffd0 x7 : 0044
> x8 : 0210 x9 : 0008
> x10: 000f x11: ff179c20
> x12:  x13: 0040
> x14: 0001 x15: ff12c0e4
> x16: ff12c2f8 x17: 0001
> x18: fcc28df8 x19: fcc2c238
> x20: 0002 x21: 
> x22: fcc2c230 x23: 0002
> x24: ff198b38 x25: 
> x26:  x27: fcc2bff0
> x28:  x29: fcc24a10
> 
> Also verified the elf image header sections for reference the load
> memory address is 0x0
> 
> :~$ aarch64-linux-gnu-objdump -h sel4test-driver-image-arm-tx1
> 
> sel4test-driver-image-arm-tx1:     file format elf64-
> littleaarch64
> 
> Sections:
> Idx Name  Size  VMA   LMA   File
> off  Algn
>   0 .text 700c     
> 0001  2**12
>   CONTENTS, ALLOC, LOAD, READONLY, CODE
>   1 .rodata   0044ef80  7010  7010 
> 00017010  2**3
>   CONTENTS, ALLOC, LOAD, DATA
>   2 .bss  a000  00456000  00456000 
> 00465f90  2**12
>   ALLOC
>   3 .comment  0082     
> 00465f90  2**0
>   CONTENTS, READONLY
> 
> Please suggest if anything is missing.
> 
> Regards,
> Munees
> 
> On Tue, Oct 17, 2017 at 9:11 AM, 
> wrote:
> > 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 the appropriate entry point. From the elf file, the load
> > address
> > and entry point should both be 0x0.
> > 
> > The menuconfig has an option for generating binary files under:
> > Tools -> Build elfloader -> Boot image type
> > 
> >  - Alex
> > 
> > On Mon, 2017-10-16 at 19:31 +0530, Muneeswaran Rajendran wrote:
> > > Hi All,
> > >
> > > I have been trying to load 64bit seL4 (kernel+user space) ELF
> > image
> > > on Tx1 board but it's failed to start the application and crashed
> > > with reason '"Synchronous Abort" handler, esr 0x0200'
> > always. 
> > >
> > > Just walk through the Tx1 u-boot code and found that
> > > 'load_elf_image_phdr(unsigned long addr)' is using 32bit ELF
> > header
> > > structure pointer to load the program header.
> > >
> > > I would like to understand whether 64bit ELF image load handled
> > using
> > > 32bit elf header itself or we need to configure u-boot to load 64
> > bit
> > > ELF image ?
> > >
> > > I have modified the kernel base addr as 0xffc8 and
> > phyadd
> > > as 0x8008 to boot sel4 app image on TX1 board nothing has
> > worked
> > > out. 
> > >
> > > Please share details if someone succeeded to bring sel4 app elf
> > image
> > > on Tx1 platform.
> > >
> > > Regards,
> > > Munees
> > > ___
> > > Devel mailing list
> > > Devel@sel4.systems
> > > https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] 64 bit ARM ELF image load in Tx1 platform

[Alexander.Kroh]

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 the appropriate entry point. From the elf file, the load address
and entry point should both be 0x0.

The menuconfig has an option for generating binary files under:
Tools -> Build elfloader -> Boot image type

 - Alex

On Mon, 2017-10-16 at 19:31 +0530, Muneeswaran Rajendran wrote:
> Hi All,
> 
> I have been trying to load 64bit seL4 (kernel+user space) ELF image
> on Tx1 board but it's failed to start the application and crashed
> with reason '"Synchronous Abort" handler, esr 0x0200' always. 
> 
> Just walk through the Tx1 u-boot code and found that
> 'load_elf_image_phdr(unsigned long addr)' is using 32bit ELF header
> structure pointer to load the program header.
> 
> I would like to understand whether 64bit ELF image load handled using
> 32bit elf header itself or we need to configure u-boot to load 64 bit
> ELF image ?
> 
> I have modified the kernel base addr as 0xffc8 and phyadd
> as 0x8008 to boot sel4 app image on TX1 board nothing has worked
> out. 
> 
> Please share details if someone succeeded to bring sel4 app elf image
> on Tx1 platform.
> 
> Regards,
> Munees
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] sel4Test development Tx1 platform

[Alexander.Kroh]

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 Rajendran wrote:
> Hi Kofi,
> 
> We are trying to bring the sel4 kernel on Tx1 board using SD card.
> The following step used to bring up sel4 kernel.
> 
> 1. flash the kernel.elf as part of Root FS
> 2. stop the u-boot prompt and allow to boot from flashed elf image
> using #ext4load mmc 1 ${loadaddr} ${bootfile}
> 
> but it crashed immediately with below coredump.
> 
> Tegra210 (P2371-2180) # setenv bootfile kernel.elfTegra210 (P2371-
> 2180)
> # ext4load mmc 1 ${loadaddr} ${bootfile}894203 bytes read in 182 ms
> (4.7 MiB/s)Tegra210 (P2371-2180) 
> # bootelf ${loadaddr}#
> # Starting application at 0x ...
> "Synchronous Abort" handler, esr 0x0200ELR: 0LR: 
> ff135194x0 : 0001 x1 : fcc30e28x2 :
> 0006 x3 : 000fx4 :  x5 :
> 001cx6 :  x7 : x8 :
> 0001 x9 : 0008x10: 0a200023 x11:
> 0002x12: 0002 x13: 0040x14:
> 0001 x15: ff12c0d0x16: ff12c3dc x17:
> 0001x18: fcc28df8 x19: 
> 
> Please share the steps followed to bring seL4 kernel on Tx1 board.
> 
> Regards,
> Muneeswaran
>  
> 
> On Wed, Oct 11, 2017 at 10:11 AM, 
> wrote:
> > Hi Muneeswaran,
> > 
> > Well, about here is where we're (quickly) approaching the limits of
> > my usefulness: I have never personally worked with the TX1 board,
> > and I don't know how to flash a u-boot image onto it.
> > 
> > If you're talking though, about trying to get an seL4 kernel image
> > to run on the CPU, then that shouldn't require you to flash
> > anything. Assuming there is already a working, viable u-
> > boot installed on your TX1, you should be able to boot the seL4
> > kernel using fastboot, TFTP, or boot it from an SD card or USB
> > flash drive. I cannot comment on which of these methods is
> > available on your TX1 board, because again: I have no experience
> > with the TX1 platform. But I'm pretty confident that you at least
> > shouldn't have to flash anything to boot seL4 on your board
> > *assuming* you already have u-boot flashed onto it.
> > 
> > -- 
> > Kofi Doku Atuah
> > Kernel engineer
> > DATA61 | CSIRO
> > 
> > 
> > ___
> > Devel mailing list
> > Devel@sel4.systems
> > https://sel4.systems/lists/listinfo/devel
> > 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] sel4test data abort when boot strap test program

[Alexander.Kroh]

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 PL0/user)?

 - AlexK


On Mon, 2017-05-15 at 09:35 +, Joyce Peng(彭美僑) wrote:
> Hi Alex,
> 
> We want to avoid the most of error to access ARM CP15 register in Cortex-A7.
> Is there has any seL4 official github support ARM Cortex-A7 ?
> https://github.com/seL4
> https://github.com/SEL4PROJ
> 
> For example, we found Xilinx zynq7000 support ARM Cortex-A9 in sel4test like 
> below.
> 
> File: sel4test/projects/sel4test/master-configs/zynq7000_release_xml_defconfig
> #
> # seL4 System
> #
> # CONFIG_ARCH_X86 is not set
> CONFIG_ARCH_ARM=y
> CONFIG_ARCH_AARCH32=y
> # CONFIG_ARM1136JF_S is not set
> # CONFIG_ARM_CORTEX_A8 is not set
> CONFIG_ARM_CORTEX_A9=y
> # CONFIG_ARM_CORTEX_A15 is not set
> # CONFIG_PLAT_EXYNOS54XX is not set
> 
> 
> Thanks,
> Joyce Peng
> 
> -Original Message-
> From: alexander.k...@data61.csiro.au [mailto:alexander.k...@data61.csiro.au] 
> Sent: Friday, May 12, 2017 11:40 AM
> To: Joyce Peng(彭美僑)
> Cc: devel@sel4.systems; Jesse-SC Chou (周書正); alexander.k...@data61.csiro.au
> Subject: Re: [seL4] sel4test data abort when boot strap test program
> 
> 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 determines 
> to which level the cache will be flushed:
> https://github.com/seL4/seL4/blob/master/include/arch/arm/arch/32/mode/machine.h#L290
> 
> I think that c10 should be used in place of c11, as has been done for other 
> specific platforms.
> 
>  - AlexK
> 
> 
> 
> On Fri, 2017-05-12 at 03:17 +, Joyce Peng(彭美僑) wrote:
> > Hi Alex,
> > I turning the caches off in configuration. Then it can boot. Thank you.
> > Below is my procedure.
> > $ make menuconfig
> > Navigate through: seL4 Kernel -> Build Options DEBUG_DISABLE_L1_DCACHE 
> > [=y] DEBUG_DISABLE_L1_ICACHE [=y] DEBUG_DISABLE_L2_CACHE [=y]
> > 
> > But how those configurations affect seL4.
> > I confuse what it let the page table of application in seL4 can't access 
> > correctly. 
> > 
> > 
> > Thanks,
> > Joyce Peng
> > -Original Message-
> > From: Joyce Peng(彭美僑)
> > Sent: Friday, May 12, 2017 12:26 AM
> > To: 'alexander.k...@data61.csiro.au'
> > Cc: devel@sel4.systems
> > Subject: RE: [seL4] sel4test data abort when boot strap test program
> > 
> > Hi Alex,
> > 
> > The content of the DFSR is 0x805 and DFAR is 0xDF7FE.
> > And caching is turning off.
> > $make menuconfig
> > DEBUG_DISABLE_L1_DCACHE [=n]
> > DEBUG_DISABLE_L1_ICACHE [=n]
> > DEBUG_DISABLE_L2_CACHE [=n]
> > 
> > Thanks,
> > Joyce.peng
> > 
> > -Original Message-
> > From: alexander.k...@data61.csiro.au 
> > [mailto:alexander.k...@data61.csiro.au]
> > Sent: Thursday, May 11, 2017 11:39 AM
> > To: Joyce Peng(彭美僑)
> > Cc: devel@sel4.systems
> > Subject: Re: [seL4] sel4test data abort when boot strap test program
> > 
> > Hi Joyce,
> > 
> > Can you provide the content of the DFSR? It provides a lot of useful 
> > information about the cause of a data abort. If it is not printed, You can 
> > find it in the context of the fault handler with:
> > 
> > seL4_Word fsr = seL4_GetMR(seL4_VMFault_FSR);
> > 
> > Beware that this message register will be clobbered if you perform a system 
> > call. This may include the use of printf(..).
> > 
> > 
> > You might have a caching problem. You can check this by turning the caches 
> > off via:
> > $ make menuconfig
> > Navigate through: seL4 Kernel -> Build Options
> > 
> > 
> >  - Alex
> > 
> > 
> > 
> > 
> > On Wed, 2017-05-10 at 06:13 +, Joyce Peng(彭美僑) wrote:
> > > Hi Hesham,
> > > 
> > > The board is one of our company's product. 
> > > We want to evaluate capability and performance of seL4 for future product.
> > > So we do some modification of seL4 to let it can run on our board.
> > > Now this board has single ARM Cotex-A7 and 512 MB RAM.
> > > 
> > > First, we try software sel4test that repo from 
> > > https://github.com/seL4/sel4test-manifest.git.
> > > 
> > > And we use QEMU to simulate Zynq-7000 (Xilinx ZC706, ARMv7a, Cortex A9) 
> > > as golden.
> > > $ make zynq_simulation_debug_xml_defconfig
> > > $ make
> > > $ qemu-system-arm -machine xilinx-zynq-a9 -nographic -m 512 -serial 
> > > null -serial mon:stdio -kernel images/
> > > sel4test-driver-image-arm-zynq7000  > simulate-zynq7000-golden
> > > 
> > > So we porting our board from Zynq-7000 and do some relative modification 
> > > in software sel4test.
> > > And we can build it directly. 
> > > 
> > > For example, the modification of loader address for our board
> > > --- 

Re: [seL4] sel4test data abort when boot strap test program

[Alexander.Kroh]

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
determines to which level the cache will be flushed:
https://github.com/seL4/seL4/blob/master/include/arch/arm/arch/32/mode/machine.h#L290

I think that c10 should be used in place of c11, as has been done for
other specific platforms.

 - AlexK



On Fri, 2017-05-12 at 03:17 +, Joyce Peng(彭美僑) wrote:
> Hi Alex,
> I turning the caches off in configuration. Then it can boot. Thank you.
> Below is my procedure.
> $ make menuconfig
> Navigate through: seL4 Kernel -> Build Options
> DEBUG_DISABLE_L1_DCACHE [=y]
> DEBUG_DISABLE_L1_ICACHE [=y]
> DEBUG_DISABLE_L2_CACHE [=y]
> 
> But how those configurations affect seL4.
> I confuse what it let the page table of application in seL4 can't access 
> correctly. 
> 
> 
> Thanks,
> Joyce Peng
> -Original Message-
> From: Joyce Peng(彭美僑) 
> Sent: Friday, May 12, 2017 12:26 AM
> To: 'alexander.k...@data61.csiro.au'
> Cc: devel@sel4.systems
> Subject: RE: [seL4] sel4test data abort when boot strap test program
> 
> Hi Alex,
> 
> The content of the DFSR is 0x805 and DFAR is 0xDF7FE.
> And caching is turning off.
> $make menuconfig
> DEBUG_DISABLE_L1_DCACHE [=n]
> DEBUG_DISABLE_L1_ICACHE [=n]
> DEBUG_DISABLE_L2_CACHE [=n]
> 
> Thanks,
> Joyce.peng
> 
> -Original Message-
> From: alexander.k...@data61.csiro.au [mailto:alexander.k...@data61.csiro.au]
> Sent: Thursday, May 11, 2017 11:39 AM
> To: Joyce Peng(彭美僑)
> Cc: devel@sel4.systems
> Subject: Re: [seL4] sel4test data abort when boot strap test program
> 
> Hi Joyce,
> 
> Can you provide the content of the DFSR? It provides a lot of useful 
> information about the cause of a data abort. If it is not printed, You can 
> find it in the context of the fault handler with:
> 
> seL4_Word fsr = seL4_GetMR(seL4_VMFault_FSR);
> 
> Beware that this message register will be clobbered if you perform a system 
> call. This may include the use of printf(..).
> 
> 
> You might have a caching problem. You can check this by turning the caches 
> off via:
> $ make menuconfig
> Navigate through: seL4 Kernel -> Build Options
> 
> 
>  - Alex
> 
> 
> 
> 
> On Wed, 2017-05-10 at 06:13 +, Joyce Peng(彭美僑) wrote:
> > Hi Hesham,
> > 
> > The board is one of our company's product. 
> > We want to evaluate capability and performance of seL4 for future product.
> > So we do some modification of seL4 to let it can run on our board.
> > Now this board has single ARM Cotex-A7 and 512 MB RAM.
> > 
> > First, we try software sel4test that repo from 
> > https://github.com/seL4/sel4test-manifest.git.
> > 
> > And we use QEMU to simulate Zynq-7000 (Xilinx ZC706, ARMv7a, Cortex A9) as 
> > golden.
> > $ make zynq_simulation_debug_xml_defconfig
> > $ make
> > $ qemu-system-arm -machine xilinx-zynq-a9 -nographic -m 512 -serial 
> > null -serial mon:stdio -kernel images/
> > sel4test-driver-image-arm-zynq7000  > simulate-zynq7000-golden
> > 
> > So we porting our board from Zynq-7000 and do some relative modification in 
> > software sel4test.
> > And we can build it directly. 
> > 
> > For example, the modification of loader address for our board
> > --- a/sel4test/projects/elfloader-tool/gen_boot_image.sh
> > +++ b/sel4test/projects/elfloader-tool/gen_boot_image.sh
> > @@ -49,6 +49,10 @@ case "$PLAT" in
> >  ENTRY_ADDR=0x1000;
> >  FORMAT=elf32-littlearm
> >  ;;
> > + "our_platform")
> > +ENTRY_ADDR=0x2000;
> > +FORMAT=elf32-littlearm
> > +;;
> >  "apq8064")
> >  ENTRY_ADDR=0x82008000;
> >  FORMAT=elf32-littlearm
> > 
> > For example, the Kconfig of kernel
> > --- a/sel4test/kernel/Kconfig
> > +++ b/sel4test/kernel/Kconfig
> > @@ -229,6 +229,15 @@ menu "seL4 System"
> >  help
> >  Support for Xilinx Zynq-7000 platforms.
> > 
> > +config PLAT_OUR_PLATFORM
> > +bool " OUR_PLATFOR (ARMv7a, Cortex A7)"
> > +depends on ARCH_AARCH32
> > +select ARM_CORTEX_A7
> > +select ARCH_ARM_V7A
> > +help
> > +Support for our platforms.
> > +
> > + 
> > 
> > Beside, we found sel4utils_map_page() calls seL4_ARM_Page_Map() and 
> > seL4_ARM_Page_Map() then uses IPC to do page tabe mapping.
> > We want to know the call flow of the VSpace page mapping. By tracing the 
> > detail of VSpace page mapping to see if there's any missing when porting to 
> > our platform.
> > 
> > 
> > Thanks,
> > Joyce Peng
> > 
> > -Original Message-
> > From: hesham.almat...@data61.csiro.au 
> > [mailto:hesham.almat...@data61.csiro.au]
> > Sent: Wednesday, May 10, 2017 9:32 AM
> > To: Joyce Peng(彭美僑); devel@sel4.systems
> > Subject: Re: [seL4] sel4test data abort when boot strap test program

Re: [seL4] Help accessing physical address on zynq7000

[Alexander.Kroh]

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 object manager:
https://github.com/seL4/sel4test/blob/master/apps/sel4test-driver/src/main.c#L83

Initialise an abstract vka interface for allocating objects:
https://github.com/seL4/sel4test/blob/master/apps/sel4test-driver/src/main.c#L89

Initialise a vspace - a user-space virtual memory manager:
https://github.com/seL4/sel4test/blob/master/apps/sel4test-driver/src/main.c#L94


From there, you can initialise an IO mapper for trivially mapping your
physical memory to a virtual address:
https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/include/sel4platsupport/io.h#L32

Last, use this function for mapping the physical memory.
https://github.com/seL4/util_libs/blob/master/libplatsupport/include/platsupport/io.h#L68



 - AlexK


On Mon, 2017-03-20 at 19:31 +, Brandon, Jeffrey - 0553 - MITLL
wrote:
> Hello,
> 
>  
> 
> I’ve been getting started with seL4 on the zynq7000 and I am looking
> for resources on how to read/write physical memory for memory mapped
> io purposes. 
> 
>  
> 
> If there is a relevant tutorial or manual to reference I haven’t come
> across it yet so I wanted to ask here. Any other guidance as to how to
> think about and work with capabilities would be useful at this stage.
> 
>  
> 
> I’m working with a modified version of the sel4test repository.
> Looking at that I found env.simple (simple_t defined
> https://github.com/seL4/seL4_libs/blob/a1c031b0885dec4ddf1ee1f8866bcd23dcca6ac3/libsel4simple/include/simple/simple.h)
>  which seems to contain function pointers for some relevant functions to what 
> I’m trying to do, but I am not entirely sure how to go about using them. What 
> needs to be initialized first and how do I go about that?
> 
>  
> 
> Any guidance greatly appreciated,
> 
>  
> 
> Thanks.
> 
>  
> 
> Jeff Brandon 
> 
> Associate Staff 
> 
> MIT Lincoln Laboratory
> 
> 05-53 Secure Resilient Systems and Technology 
> 
> Ph:   781.981.9233
> 
>  
> 
>  
> 
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] ARM timer driver and interrupts

[Alexander.Kroh]

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 must be written as 1 to clear. If interrupts are edge
triggered, failing to clear this bit (by writing a 1 to it) will stop
interrupts from coming in.
4) Check that your code that clears the interrupt status bit does not
clear the enable bit.

 - Alex Kroh


On Tue, 2017-02-21 at 23:17 +, anna.ly...@data61.csiro.au wrote:
> Hey, 
> 
> First I'd check if the kernel is getting the interrupts in the kernel from 
> this timer - you can put a printf in handleInterrupt in the kernel to see if 
> this is the case and see if the correct interrupt number comes in.
> 
> If so,  then check if those irqs are being sent to the signal handler and not 
> reserved (again by printing / asserting in handle interrupt).
> 
> If not, this points to a problem with your driver.
> 
> Hope this pushes you in the right direction,
> Anna. 
> 
> -Original Message-
> From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Wladislav Wiebe
> Sent: Wednesday, 22 February 2017 10:05 AM
> To: devel@sel4.systems
> Subject: [seL4] ARM timer driver and interrupts
> 
> Hello,
> 
> I wrote a new timer driver for this timer device:
> http://www.ti.com/lit/ug/sprugv5a/sprugv5a.pdf
> 
> I am already able to run the seL4 testsuite successfully, except the 
> interrupt/timer tests.
> It waits forever @ wait_for_timer_interrupt(env);
> 
> I've uploaded the driver temporary to:
> https://github.com/wwladikw/devel/blob/master/timer.c
> 
> Any idea what could be wrong?
> I am able to run the timer periodically or as oneshot.
> The gic_390 interrupt driver in the kernel should also be compatible with the 
> gic_400, for my understanding, right?
> The SoC I am using contains a Coretex A15.
> 
> Thanks a lot in advance!
> Wladislav Wiebe
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] seL4 on Zedboard

[Alexander.Kroh]

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 hardware/bitstream.bit
4. source hardware/ps7_init.tcl
5. ps7_init
6. ps7_post_config
7. dow images/sel4bench-image-arm-zynq7000
8. run
9. exit
-

1-2: Connect to the processor and put it in a known state
3-6: Program the FPGA and perform some early initialisation.
 I am not sure if this is still required for a PS only project.
7: Performs step 2: load the elf sections.
 There is no reason to load the entire elf file into memory first in
this case
8: Performs step 3: jump to the program entry point. The image must be
an ELF file, otherwise the entry point can not be determined by the
tool.

>  
> 
> Also how should I be generating sel4bench-image-arm-zynq7000? 

Replace the argument to the 'dow' command with the location of the image
that you wish to run (probably images/sel4test-image-arm-zynq7000 in
your case).

> 
> Right now I am working from the sel4test repository 
> https://github.com/seL4/sel4test configured to target Zynq-7000.
> 
> When I try the "dow images/sel4bench-image-arm-zynq7000" on images generated 
> using the standard make command and also with make build-binary and make 
> build-uBoot, I get an error: Code 16 Time 1485875053070 Format {Invalid 
> context}.
> 
> Looking at the configuration this seems to be designed for the Xilinx ZC706, 
> ARMv7a, Cortex A9. However the zed board has a ZC702. Would this be the 
> source of my problem or should sel4 work with the ZC702 as well?

Although ZC702 is not a supported platform, the processors are generally
compatible. Actually, the XMD commands that I provided are what I have
been using for my development on the Zedboard.

 - Alex


> 
> Thanks again,
> 
> Jeff
> 
> -Original Message-
> From: alexander.k...@data61.csiro.au [mailto:alexander.k...@data61.csiro.au] 
> Sent: Monday, January 30, 2017 5:40 PM
> To: Brandon, Jeffrey - 0553 - MITLL
> Cc: devel@sel4.systems
> Subject: Re: [seL4] seL4 on Zedboard
> 
> 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 start execution.
> 
> So ${loadaddr} can be anything that you like, as long as it does not 
> overwrite any part of u-boot or occupy the space at which the ELF sections 
> will be copied.
> 
> 
> Loading from SD can be quite awkward during development. I recommend using 
> JTAG via the XMD tool. Here is an example of the required XMD
> commands:
> 
> connect arm hw
> rst
> fpga -f hardware/bitstream.bit
> source hardware/ps7_init.tcl
> ps7_init
> ps7_post_config
> dow images/sel4bench-image-arm-zynq7000
> run
> exit
> -
> 
>  - Alex
> 
> 
> 
> 
> 
> 
> 
> On Mon, 2017-01-30 at 16:04 +, Brandon, Jeffrey - 0553 - MITLL
> wrote:
> > Hi,
> > 
> >  
> > 
> > I’ve been trying to get seL4 running on a Zedboard and I was wondering 
> > if there was any documentation on how to boot sle4 from an SD card.
> > 
> >  
> > 
> > I’ve read
> > 
> > http://sel4.systems/pipermail/devel/2016-December/001160.html
> > 
> > and
> > 
> > https://sel4.systems/Info/Hardware/General/
> > 
> > which mentions using ${loadaddr} but that doesn’t seem to be defined 
> > on the Zedboard’s u-boot.
> > 
> >  
> > 
> > So far I’ve compiled the image targeting the zynq7000 and used the 
> > mkimage command from the general hardware page to try u-boot’s 
> > fastboot, but fastboot doesn’t seem to be available on the zynq 
> > either.
> > 
> >  
> > 
> > I am a bit of a novice here. I worry that the solution may be simple 
> > but I am currently taking shots in the dark. I wanted to ask this list 
> > for any resources you may be aware of for getting sel4 test cases 
> > running on the Zed.
> > 
> >  
> > 
> > Thanks for the help,
> > 
> >  
> > 
> > Jeff Brandon
> > 
> > 05-53 Secure Resilient Systems and Technology
> > 
> >  
> > 
> > 
> > ___
> > Devel mailing list
> > Devel@sel4.systems
> > https://sel4.systems/lists/listinfo/devel
> 

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] seL4 on Zedboard

[Alexander.Kroh]

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 start execution.

So ${loadaddr} can be anything that you like, as long as it does not
overwrite any part of u-boot or occupy the space at which the ELF
sections will be copied.


Loading from SD can be quite awkward during development. I recommend
using JTAG via the XMD tool. Here is an example of the required XMD
commands:

connect arm hw
rst
fpga -f hardware/bitstream.bit
source hardware/ps7_init.tcl
ps7_init
ps7_post_config
dow images/sel4bench-image-arm-zynq7000
run
exit
-

 - Alex







On Mon, 2017-01-30 at 16:04 +, Brandon, Jeffrey - 0553 - MITLL
wrote:
> Hi,
> 
>  
> 
> I’ve been trying to get seL4 running on a Zedboard and I was wondering
> if there was any documentation on how to boot sle4 from an SD card.
> 
>  
> 
> I’ve read 
> 
> http://sel4.systems/pipermail/devel/2016-December/001160.html
> 
> and
> 
> https://sel4.systems/Info/Hardware/General/
> 
> which mentions using ${loadaddr} but that doesn’t seem to be defined
> on the Zedboard’s u-boot.
> 
>  
> 
> So far I’ve compiled the image targeting the zynq7000 and used the
> mkimage command from the general hardware page to try u-boot’s
> fastboot, but fastboot doesn’t seem to be available on the zynq
> either. 
> 
>  
> 
> I am a bit of a novice here. I worry that the solution may be simple
> but I am currently taking shots in the dark. I wanted to ask this list
> for any resources you may be aware of for getting sel4 test cases
> running on the Zed. 
> 
>  
> 
> Thanks for the help,
> 
>  
> 
> Jeff Brandon
> 
> 05-53 Secure Resilient Systems and Technology 
> 
>  
> 
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] arm_data_abort_exception

[Alexander.Kroh]

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 address mapping for that address.

The question is, why is sel4test calling memset on address 0xdf7fefff?
You may need to follow the call stack further to find out.


Another possible problem may be a creative platform-dependent cache
configuration. If the address does have a mapping, perhaps it is not
observable by the translation hardware.
A quick way to rule this problem out is to disable caches. This can be
done via a configuration parameter that can be changed with `make
menuconfig`.

 - Alex Kroh



On Sun, 2017-01-29 at 21:22 +0100, Wladislav Wiebe wrote:
> Hi Alex,
> 
> when configuring the device like:
> devices.h
> #define UART0_PPTR  0xfff01c00
> #define UART0_PADDR 0x0253
> 
> hardware.h
> UART0_PADDR,
> UART0_PPTR,
> 
> io.c
> putDebugChar(unsigned char c)
> {
> if (status_activate_global_pd) {
> while ((*UART_REG(ULSR, (UART0_PPTR)) & ULSR_THRE) == 0);
> *UART_REG(UTHR,(UART0_PPTR)) Wladi= c;
> } else {
> while ((*UART_REG(ULSR, (UART0_PADDR + 0xc00)) & ULSR_THRE) == 0);
> *UART_REG(UTHR,(UART0_PADDR + 0xc00)) = c;
> }
> }
> 
> I can the the kernel successfully booting, but there is pretty early
> an crash in the userspace - memset():
> seL4test/libs/libmuslc/src/string/memset.c:14
>14930:   e5431001strbr1, [r3, #-1]
> 
> So, I am still not sure if the device is correctly configured?
> 
> ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4
>   paddr=[c0008000..c049441f]
> ELF-loading image 'kernel'
>   paddr=[8100..8102efff]
>   vaddr=[e000..e002efff]
>   virt_entry=e000
> ELF-loading image 'sel4test-driver'
>   paddr=[8102f000..81411fff]
>   vaddr=[1..3f2fff]
>   virt_entry=1e8d4
> Enabling MMU and paging
> Jumping to kernel-image entry point...
> 
> Bootstrapping kernel
> 
> Caught cap fault in send phase at address 0x0
> while trying to handle:
> vm fault on data at address 0xdf7fefff with status 0x805
> in thread 0xffdfad00 "sel4test-driver" at address 0x14930
> With stack:
> 0x2f2278: 0x7
> 0x2f227c: 0x1
> 0x2f2280: 0x2f22d0
> 0x2f2284: 0x2f2290
> 0x2f2288: 0x2d9ea4
> 0x2f228c: 0xdf7fe000
> 0x2f2290: 0x1
> 0x2f2294: 0x443
> 0x2f2298: 0x2dda68
> 0x2f229c: 0x5
> 0x2f22a0: 0xc
> 0x2f22a4: 0x0
> 0x2f22a8: 0x2d9ea4
> 0x2f22ac: 0x4f
> 0x2f22b0: 0x0
> 0x2f22b4: 0x1ba40
> 
> 
> Thanks in advance!
> - Wladi
> 
> 
> 2017-01-27 21:52 GMT+01:00  :
> > 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 issue was solved for imx6:
> > https://github.com/seL4/seL4/blob/master/include/plat/imx6/plat/machine/devices.h#L31
> >
> >  - Alex
> >
> >
> >
> > On Fri, 2017-01-27 at 16:40 +0100, Wladislav Wiebe wrote:
> >> Hello,
> >>
> >> I wonder how to map a device to the kernel where the
> >> first 3 bytes are not 0. Like the UART device which is
> >> phyically connected to 0x02530c00.
> >>
> >> The abort handler in pte_pte_small_new() get called
> >> when the first 3 bytes are not 0 (on this SoC are the first 3 bytes
> >> for the UART c00).
> >>
> >> Any advice how to deal with this?
> >>
> >> Thanks in advance!
> >> - Wladi
> >>
> >>
> >>
> >>
> >> 2017-01-25 22:22 GMT+01:00 Wladislav Wiebe :
> >> > Hi Alex,
> >> >
> >> >> A trick that I use to overcome this problem is to introduce a global
> >> >> variable that reflects the status of the PD. The UART driver then
> >> >> switches between the physical and virtual address of the UART as
> >> >> required.
> >> >
> >> > that's it - seems before kernel activates the PD, Kernel might run
> >> > into assertion which wants to print.
> >> > I've changed the UART driver like
> >> > --- a/src/plat/keystone/machine/io.c
> >> > +++ b/src/plat/keystone/machine/io.c
> >> > @@ -18,14 +18,19 @@
> >> >  #define ULSR 0x14 /* UART Line Status Register */
> >> >  #define ULSR_THRE BIT(5) /* Transmit Holding Register Empty */
> >> >
> >> > -#define UART_REG(x) ((volatile uint32_t *)(UART0_PPTR + (x)))
> >> > +#define UART_REG(x,uart_addr) ((volatile uint32_t *)(uart_addr + (x)))
> >> >
> >> >  #if defined(CONFIG_PRINTING) || defined(CONFIG_DEBUG_BUILD)
> >> >  void
> >> >  putDebugChar(unsigned char c)
> >> >  {
> >> > -while ((*UART_REG(ULSR) & ULSR_THRE) == 0);
> >> > -*UART_REG(UTHR) = c;
> >> > +if (status_activate_global_pd) {
> >> > + while ((*UART_REG(ULSR, UART0_PPTR) & ULSR_THRE) == 0);
> >> > + *UART_REG(UTHR,UART0_PPTR) = c;
> >> > +} else {

Re: [seL4] arm_data_abort_exception

[Alexander.Kroh]

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 issue was solved for imx6:
https://github.com/seL4/seL4/blob/master/include/plat/imx6/plat/machine/devices.h#L31

 - Alex



On Fri, 2017-01-27 at 16:40 +0100, Wladislav Wiebe wrote:
> Hello,
> 
> I wonder how to map a device to the kernel where the
> first 3 bytes are not 0. Like the UART device which is
> phyically connected to 0x02530c00.
> 
> The abort handler in pte_pte_small_new() get called
> when the first 3 bytes are not 0 (on this SoC are the first 3 bytes
> for the UART c00).
> 
> Any advice how to deal with this?
> 
> Thanks in advance!
> - Wladi
> 
> 
> 
> 
> 2017-01-25 22:22 GMT+01:00 Wladislav Wiebe :
> > Hi Alex,
> >
> >> A trick that I use to overcome this problem is to introduce a global
> >> variable that reflects the status of the PD. The UART driver then
> >> switches between the physical and virtual address of the UART as
> >> required.
> >
> > that's it - seems before kernel activates the PD, Kernel might run
> > into assertion which wants to print.
> > I've changed the UART driver like
> > --- a/src/plat/keystone/machine/io.c
> > +++ b/src/plat/keystone/machine/io.c
> > @@ -18,14 +18,19 @@
> >  #define ULSR 0x14 /* UART Line Status Register */
> >  #define ULSR_THRE BIT(5) /* Transmit Holding Register Empty */
> >
> > -#define UART_REG(x) ((volatile uint32_t *)(UART0_PPTR + (x)))
> > +#define UART_REG(x,uart_addr) ((volatile uint32_t *)(uart_addr + (x)))
> >
> >  #if defined(CONFIG_PRINTING) || defined(CONFIG_DEBUG_BUILD)
> >  void
> >  putDebugChar(unsigned char c)
> >  {
> > -while ((*UART_REG(ULSR) & ULSR_THRE) == 0);
> > -*UART_REG(UTHR) = c;
> > +if (status_activate_global_pd) {
> > + while ((*UART_REG(ULSR, UART0_PPTR) & ULSR_THRE) == 0);
> > + *UART_REG(UTHR,UART0_PPTR) = c;
> > +} else {
> > + while ((*UART_REG(ULSR, UART0_PADDR) & ULSR_THRE) == 0);
> > + *UART_REG(UTHR,UART0_PADDR) = c;
> > +}
> >  }
> >  #endif
> >
> >
> > When running the machine now,  I am at least able to see the assertion
> > ..
> > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4
> >   paddr=[9000..9048841f]
> > ELF-loading image 'kernel'
> >   paddr=[8000..8002]
> >   vaddr=[e000..e002]
> >   virt_entry=e000
> > ELF-loading image 'sel4test-driver'
> >   paddr=[8003..80411fff]
> >   vaddr=[1..3f1fff]
> >   virt_entry=1e920
> > Enabling MMU and paging
> > Jumping to kernel-image entry point...
> >
> > seL4 failed assertion '(address & ~0xf000ul) == ((0 && (address &
> > (1ul << 31))) ? 0x0 : 0)'
> > at ./arch/object/structures_gen.h:2495 in function pte_pte_small_new
> > halting...
> >
> >
> > Thanks!
> > - Wladi
> >
> >
> >
> > 2017-01-25 1:10 GMT+01:00  :
> >> 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 the peripheral (the elfloader sets up unity mappings for
> >> 0x-0xe000).
> >>
> >> A trick that I use to overcome this problem is to introduce a global
> >> variable that reflects the status of the PD. The UART driver then
> >> switches between the physical and virtual address of the UART as
> >> required.
> >>
> >>  - Alex
> >>
> >> On Tue, 2017-01-24 at 23:55 +0100, Wladislav Wiebe wrote:
> >>> Hi Alex,
> >>>
> >>> thanks for pointing that out - I will double check the device mapping.
> >>>
> >>> - Wladislav Wiebe
> >>>
> >>> 2017-01-24 23:24 GMT+01:00  :
> >>> > 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, no RAM or peripheral is mapped to the physical address)
> >>> >
> >>> > The address of the fault corresponds to a kernel device mapping. My
> >>> > guess is that you are not mapping kernel devices correctly at boot time:
> >>> > https://github.com/seL4/seL4/blob/master/include/plat/exynos5/plat/machine/devices.h#L15
> >>> > https://github.com/seL4/seL4/blob/master/include/plat/exynos5/plat/machine/hardware.h#L26
> >>> > https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/hardware.c#L51
> >>> >
> >>> >
> >>> >  - Alex
> >>> >
> >>> > On Tue, 2017-01-24 at 17:17 +0100, Wladislav Wiebe wrote:
> >>> >> could it be an TLB fault? For my understandig, based on
> >>> >> 

Re: [seL4] arm_data_abort_exception

[Alexander.Kroh]

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 the peripheral (the elfloader sets up unity mappings for
0x-0xe000).

A trick that I use to overcome this problem is to introduce a global
variable that reflects the status of the PD. The UART driver then
switches between the physical and virtual address of the UART as
required.

 - Alex

On Tue, 2017-01-24 at 23:55 +0100, Wladislav Wiebe wrote:
> Hi Alex,
> 
> thanks for pointing that out - I will double check the device mapping.
> 
> - Wladislav Wiebe
> 
> 2017-01-24 23:24 GMT+01:00  :
> > 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, no RAM or peripheral is mapped to the physical address)
> >
> > The address of the fault corresponds to a kernel device mapping. My
> > guess is that you are not mapping kernel devices correctly at boot time:
> > https://github.com/seL4/seL4/blob/master/include/plat/exynos5/plat/machine/devices.h#L15
> > https://github.com/seL4/seL4/blob/master/include/plat/exynos5/plat/machine/hardware.h#L26
> > https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/hardware.c#L51
> >
> >
> >  - Alex
> >
> > On Tue, 2017-01-24 at 17:17 +0100, Wladislav Wiebe wrote:
> >> could it be an TLB fault? For my understandig, based on
> >> http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0438g/BABFFDFD.html
> >> it is the DFSR  = 0x7 -> b00111
> >> Translation fault, 2nd level.
> >>
> >>
> >> Thanks!
> >> - Wladislav Wiebe
> >>
> >> 2017-01-24 15:42 GMT+01:00 Wladislav Wiebe :
> >> > Hello,
> >> >
> >> > has somebody experience with running into arm_data_abort_exception
> >> > after enabling the MMU/paging and jumping to the kernel image:
> >> > ..
> >> > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4
> >> >   paddr=[9000..904b041f]
> >> > ELF-loading image 'kernel'
> >> >   paddr=[8000..80033fff]
> >> >   vaddr=[f000..f0033fff]
> >> >   virt_entry=f000
> >> > ELF-loading image 'sel4test-driver'
> >> >   paddr=[80034000..8042dfff]
> >> >   vaddr=[1..409fff]
> >> >   virt_entry=1e924
> >> > Enabling MMU and paging
> >> > Jumping to kernel-image entry point...
> >> >
> >> > check_data_abort_exception()
> >> > DFAR  = 0xfff01014
> >> > DFSR  = 0x7
> >> > ADFSR = 0x0
> >> > abort() called.
> >> >
> >> > I've dumped the DFAR/DFSR register --
> >> >
> >> > Relevant config parts about the setup:
> >> > CONFIG_ARCH_ARM_V7A=y
> >> > CONFIG_ARCH_ARM=y
> >> > CONFIG_ARCH_AARCH32=y
> >> > CONFIG_ARM_CORTEX_A15=y
> >> > CONFIG_PLAT_KEYSTONE=y
> >> >
> >> >
> >> > Thanks in advance!
> >> > --
> >> > WBR, Wladislav WIebe
> >>
> >>
> >>
> >
> 
> 
> 

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] arm_data_abort_exception

[Alexander.Kroh]

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, no RAM or peripheral is mapped to the physical address)

The address of the fault corresponds to a kernel device mapping. My
guess is that you are not mapping kernel devices correctly at boot time:
https://github.com/seL4/seL4/blob/master/include/plat/exynos5/plat/machine/devices.h#L15
https://github.com/seL4/seL4/blob/master/include/plat/exynos5/plat/machine/hardware.h#L26
https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/hardware.c#L51


 - Alex

On Tue, 2017-01-24 at 17:17 +0100, Wladislav Wiebe wrote:
> could it be an TLB fault? For my understandig, based on
> http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0438g/BABFFDFD.html
> it is the DFSR  = 0x7 -> b00111
> Translation fault, 2nd level.
> 
> 
> Thanks!
> - Wladislav Wiebe
> 
> 2017-01-24 15:42 GMT+01:00 Wladislav Wiebe :
> > Hello,
> >
> > has somebody experience with running into arm_data_abort_exception
> > after enabling the MMU/paging and jumping to the kernel image:
> > ..
> > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4
> >   paddr=[9000..904b041f]
> > ELF-loading image 'kernel'
> >   paddr=[8000..80033fff]
> >   vaddr=[f000..f0033fff]
> >   virt_entry=f000
> > ELF-loading image 'sel4test-driver'
> >   paddr=[80034000..8042dfff]
> >   vaddr=[1..409fff]
> >   virt_entry=1e924
> > Enabling MMU and paging
> > Jumping to kernel-image entry point...
> >
> > check_data_abort_exception()
> > DFAR  = 0xfff01014
> > DFSR  = 0x7
> > ADFSR = 0x0
> > abort() called.
> >
> > I've dumped the DFAR/DFSR register --
> >
> > Relevant config parts about the setup:
> > CONFIG_ARCH_ARM_V7A=y
> > CONFIG_ARCH_ARM=y
> > CONFIG_ARCH_AARCH32=y
> > CONFIG_ARM_CORTEX_A15=y
> > CONFIG_PLAT_KEYSTONE=y
> >
> >
> > Thanks in advance!
> > --
> > WBR, Wladislav WIebe
> 
> 
> 

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] questions about the vgic maintenance for sel4 TK1 ARM VMM

[Alexander.Kroh]

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 have questions about the vgic maintenance for sel4 tk1 ARM VMM.
> When the VM acknowledges an IRQ, an exception is raised and is
> delivered to the VMM. Could someone explain how seL4 intercepts the VM
> ack? How is this exception is raised ? I am confused because the VM is
> supposed to totally control the MMIO of the device and can write any
> thing to the device. How can seL4 be triggered in this case? Which
> part of  source code allows seL4 to intercept the VM ack?
> 
> 
> Thanks
> 
> 
> Peng
> 
> 
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] seL4 on Zinq7000 on QEMU

[Alexander.Kroh]

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:
> 
>   
> https://github.com/seL4/util_libs/blob/master/libplatsupport/src/plat/zynq7000/serial.c#L174
> 
> I've created a pull request to fix that as well.
> 
>   https://github.com/seL4/util_libs/pull/5
> 
> -Andrew
> 
> On Tue, Dec 6, 2016 at 6:46 PM, Andrew Gacek  wrote:
> > Ok thanks. I've created a pull request for this change:
> >
> >   https://github.com/seL4/seL4_tools/pull/2
> >
> > -Andrew
> >
> > On Tue, Dec 6, 2016 at 5:58 PM,   wrote:
> >> Hi Andrew,
> >>
> >> Nice find! U-boot obviously performs some initialisation of the UART on
> >> our behalf, hence we have not had problems when testing on real
> >> hardware.
> >>
> >> The correct place would be here:
> >> https://github.com/seL4/seL4_tools/blob/2.0.x-compatible/elfloader-tool/src/arch-arm/plat-zynq7000/platform_init.c#L72
> >>
> >> But, it should call out to a dedicated init function in sys_fputc.c
> >>
> >> The call to platform_init() would also need to occur a few lines
> >> earlier, before the first printf:
> >> https://github.com/seL4/seL4_tools/blob/2.0.x-compatible/elfloader-tool/src/arch-arm/boot.c#L81
> >>
> >>  - Alex
> >>
> >>
> >> On Tue, 2016-12-06 at 16:35 -0600, Andrew Gacek wrote:
> >>> I've found the problem. First, the default UART for zynq7000 is the
> >>> second one, so I need to run qemu like this:
> >>>
> >>>   qemu-system-arm -M xilinx-zynq-a9 -kernel
> >>> images/capdl-loader-experimental-image-arm-zynq7000 -m size=512M
> >>> -monitor none -nographic -serial /dev/null -serial stdio
> >>>
> >>> Second, the Zynq7000 uart needs to be explicitly enabled. This is done
> >>> by clearing bit 5 and setting bit 4 of the control register. It looks
> >>> like seL4 and related tools are not doing this. For now I've done this
> >>> by modifying
> >>>
> >>>   tools/elfloader/src/arch-arm/plat-zynq7000/sys_fputc.c
> >>>
> >>> to add
> >>>
> >>>uint32_t v = *UART_REG(UART_CONTROL);
> >>> v |= (1 << 4);
> >>> v &= ~(1 << 5);
> >>> *UART_REG(UART_CONTROL) = v;
> >>>
> >>> to the __fputc function.
> >>>
> >>> This clearly isn't the right spot for it. Where should such initial
> >>> configuration be done?
> >>>
> >>> -Andrew
> >>>
> >>>
> >>> On Tue, Dec 6, 2016 at 3:33 PM, Andrew Gacek  
> >>> wrote:
> >>> > If I suspend the execution in QEMU, the program counter is at
> >>> > 0xe00108ec. In the kernel, that is the  method. So
> >>> > perhaps the system is running, but I'm just not able to see any output
> >>> > from the elfloader, kernel, etc.
> >>> >
> >>> > -Andrew
> >>> >
> >>> > On Tue, Dec 6, 2016 at 2:49 PM, Andrew Gacek  
> >>> > wrote:
> >>> >> Thanks Alex. That fixes the crash. Now the system runs but just seems
> >>> >> to hang without doing anything. I don't get any output at all (whereas
> >>> >> the kzm version spews out a ton of messages). In 'top' I can see it's
> >>> >> using about 3% cpu so it's something, though it's not clear what. It's
> >>> >> hard for me to tell. Perhaps the UART for the console isn't working
> >>> >> correctly?
> >>> >>
> >>> >> -Andrew
> >>> >>
> >>> >> On Tue, Dec 6, 2016 at 2:46 PM,   
> >>> >> wrote:
> >>> >>> Hi Andrew,
> >>> >>>
> >>> >>> It could be because QEMU does not know how much RAM is available.
> >>> >>> Could you try adding "-m size=512M" to your arguments?
> >>> >>>
> >>> >>>  - Alex
> >>> >>>
> >>> >>> 
> >>> >>> From: Devel  on behalf of Andrew Gacek 
> >>> >>> 
> >>> >>> Sent: Wednesday, December 7, 2016 2:23 AM
> >>> >>> To: devel@sel4.systems
> >>> >>> Subject: [seL4] seL4 on Zinq7000 on QEMU
> >>> >>>
> >>> >>> I'm trying to build and emulate a version of seL4 for the zinq7000
> >>> >>> platform, but it crashes immediately.
> >>> >>>
> >>> >>> I've started by taking the camkes tutorial and building it for 
> >>> >>> zinq7000:
> >>> >>>
> >>> >>>   repo init -u https://github.com/seL4/camkes-manifest.git
> >>> >>>   repo sync
> >>> >>>   make arm_simple_defconfig
> >>> >>>   make menuconfig # change seL4 platform to zinq7000
> >>> >>>   make
> >>> >>>
> >>> >>> When I try to emulate it, it crashes right away:
> >>> >>>
> >>> >>>   qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel
> >>> >>> images/capdl-loader-experimental-image-arm-zynq7000
> >>> >>>
> >>> >>> qemu: fatal: Trying to execute code outside RAM or ROM at 0x1000
> >>> >>>
> >>> >>> R00= R01= R02= R03=
> >>> >>> R04= R05= R06= R07=
> >>> >>> R08= R09= R10= R11=
> >>> >>> R12= 

Re: [seL4] Syscall errors with musl

[Alexander.Kroh]

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 can be found here:
https://github.com/seL4/util_libs/blob/master/libplatsupport/include/platsupport/timer.h

 - Alex


On Sun, 2016-11-20 at 19:15 +0300, Rinat Dobrokhotov wrote:
> Hi all,
> 
> I have written simple programme which gets system time. I get syscall
> errors when programm is calling gettimeofday function:
> 
> main.c:
> 
> #include 
> #include 
> #include 
> #include 
> 
> int main(int argc, char *argv[]) {
> int iterations = 100;
> 
> struct timeval start, end;
> 
> gettimeofday(, NULL);
> 
> for (int i = 0; i < iterations; i++)
> {
> }
> 
> gettimeofday(, NULL);
> 
> printf("%ld\n", ((end.tv_sec * 100 + end.tv_usec)
> - (start.tv_sec * 100 + start.tv_usec)));
> 
> return 0;
> 
> 
> 
> Errors:
> 
> 
> libsel4muslcsys: Error attempting syscall 263
> libsel4muslcsys: Error attempting syscall 78
> 
> Could you tell me where I mistook?
> 
> 
> -- 
> Best regards,
> Rinat Dobrokhotov
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Unable To Map Physical Frame

[Alexander.Kroh]

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 other timers that you could
use on this platform?

 - Alex


On Sat, 2016-11-12 at 12:59 -0500, Mark Reus wrote:
> Hi
> 
> 
> I want to map the arm global timer which is located at memory
> location 0xF8F00200 .
> 
> 
> However, when I am trying to get the physical frame using :
> 
> 
>   error = simple_get_frame_cap(, (void*)global_timer_paddr, 12,
> _cap_path);
> if (error) {
> ZF_LOGE("Failed to find frame at paddr %p\n",
> global_timer_paddr);
> return error;
> }
> 
> 
> I get the Error Statement on stduout as "main@main.c:209 Failed to
> find frame at paddr 0xf8f00200"
> 
> 
> 
> 
> If i print the bootinfo during bootup, I can see that I have access to
> this region 
> 
> 
> 0xf800 | 0012 | [520 <--> 521 ]
> 
> 
> Can someone help me as why this issue may be caused? I know that this
> global timer is said to be mapped in the private region. But I do not
> what exactly that means and if we cannot do it.
> 
> 
> Regards
> Mark
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] SDHC driver in Sabre Lite

[Alexander.Kroh]

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 eliminate one point of failure as you could allocate a buffer
with malloc isntead.

 - Alex

On Tue, 2016-10-18 at 17:28 -0700, Norrathep Rattanavipanon wrote:
> So I use the following code to create a new buffer for vaddr and
> paddr  :
> void *vaddr = vspace_new_pages(, seL4_AllRights, 1, seL4PageBits);
> 
> seL4_CPtr frame_cap = vsapce_get_cap(, vaddr);
> seL4_ARM_Page_GetAddress_t gaddr = seL4_ARCH_Page_GetAddress(frame_cap);
> 
> uintptr_t paddr = (uintptr_t) gaddr.paddr;
> 
> long read_len = mmc_block_read(*mmc_card, 0x5, 1, vaddr, paddr, NULL, NULL);
> but the code is still stuck in mmc_block_read function. Anything I might be 
> missing here?
> Thanks for the help,
> Oak
> 
> On Fri, Oct 14, 2016 at 11:06 AM, Norrathep Rattanavipanon
>  wrote:
> Ah I see. That might be a problem. I thought that function
> will automatically build a mapping so I can use any vaddr,
> 
> 
> Thanks Alex!
> 
> On Thu, Oct 13, 2016 at 8:38 PM,
>  wrote:
> 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
> 
> 
> 
> 
> On Thu, 2016-10-13 at 17:33 -0700, Norrathep
> Rattanavipanon wrote:
> > Is there any example on how to use sdhc driver in
> >
> 
> (https://github.com/SEL4PROJ/projects_libs/tree/master/libsdhcdrivers)?
> >
> >
> > Currently, I'm struggling to read a block of data
> from micro-sd in
> > seL4.
> > I use the following code (assertions are omitted
> here for readability)
> > to instantiate the driver :
> >
> >
> >
> >
> > ps_io_mapper_t io_mapper = {0};
> > error = sel4platsupport_new_io_mapper(simple,
> vspace, vka,
> > _mapper);
> >
> > ps_dma_man_t dma_man = {0};
> > error = sel4utils_new_page_dma_alloc(, ,
> _man);
> >
> > ps_io_ops_t io_ops = {
> > .io_mapper = io_mapper,
> >  .dma_manager = dma_man
> > };
> >
> > sdio_host_dev_t* dev = (sdio_host_dev_t*)
> malloc(sizeof(*dev));
> > assert(dev != NULL);
> > memset(dev,0, sizeof(*dev));
> >
> >
> > enum sdio_id id = sdio_default_id();
> > error = sdio_init(id, _ops, dev);
> >
> > mmc_card_t* mmc_card = (mmc_card_t*)
> malloc(sizeof(*mmc_card));
> > error = mmc_init(dev, _ops, mmc_card);
> >
> >
> > void* vaddr = (void*) 0x198;
> >
> > uintptr_t paddr = (uintptr_t) 0x119a7000;
> >
> > long read_len = mmc_block_read(*mmc_card, 0, 5,
> vaddr, paddr, NULL,
> > NULL);
> >
> >
> >
> > And the code's stuck in mmc_block_read function
> where interrupt status
> > (BRR and BWR) are never on.
> >
> >
> > Thanks in advance,
> > Oak
> >
> >
> >
> >
> > --
> > Norrathep (Oak) Rattanavipanon
> > M.S. in Computer Science
> > University of California - Irvine
> 
> > ___
> > Devel mailing list
> > Devel@sel4.systems
> > https://sel4.systems/lists/listinfo/devel
> 
> 
> 
> 
> 
> -- 
>

Re: [seL4] SDHC driver in Sabre Lite

[Alexander.Kroh]

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




On Thu, 2016-10-13 at 17:33 -0700, Norrathep Rattanavipanon wrote:
> Is there any example on how to use sdhc driver in
> (https://github.com/SEL4PROJ/projects_libs/tree/master/libsdhcdrivers)?
> 
> 
> Currently, I'm struggling to read a block of data from micro-sd in
> seL4.
> I use the following code (assertions are omitted here for readability)
> to instantiate the driver : 
> 
> 
> 
> 
> ps_io_mapper_t io_mapper = {0};
> error = sel4platsupport_new_io_mapper(simple, vspace, vka,
> _mapper);
>  
> ps_dma_man_t dma_man = {0};
> error = sel4utils_new_page_dma_alloc(, , _man);
>  
> ps_io_ops_t io_ops = {
> .io_mapper = io_mapper,
>  .dma_manager = dma_man
> };
>  
> sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev));
> assert(dev != NULL);
> memset(dev,0, sizeof(*dev));
> 
> 
> enum sdio_id id = sdio_default_id();
> error = sdio_init(id, _ops, dev);
>  
> mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card));
> error = mmc_init(dev, _ops, mmc_card);
> 
> 
> void* vaddr = (void*) 0x198;
> 
> uintptr_t paddr = (uintptr_t) 0x119a7000;
> 
> long read_len = mmc_block_read(*mmc_card, 0, 5, vaddr, paddr, NULL,
> NULL);
> 
> 
> 
> And the code's stuck in mmc_block_read function where interrupt status
> (BRR and BWR) are never on.
> 
> 
> Thanks in advance,
> Oak
> 
> 
> 
> 
> -- 
> Norrathep (Oak) Rattanavipanon
> M.S. in Computer Science
> University of California - Irvine
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel