Devel

devel@sel4.systems

8 participants
1389 discussions

am335x - configs and refos
by Tim Newsham 04 Mar '15

04 Mar '15

Attached are some patches for am335x support. I've started to play with refos, and can build it for am335x and run some of the startup (with release mode) but it hangs at some point.. still a work in progress. Also there's a few minor proofread tweaks on the refos doc. By the way, sel4test runs pretty well now in debug and release modes. Instructions are pretty straightforward: - build the project using the debug or release config - use objcopy to extract a raw binary from the ELF image - load the binary with uboot (I use "tftp", it defaults to the proper load address) - run it in uboot with "go 82000000" Tim

2 1

Joint a formally verified C compiler with seL4?
by Grissiom 02 Mar '15

02 Mar '15

Hi all, I've heard a formally verified optimizing C compiler: CompCert recently: http://www.absint.com/compcert/ HN: https://news.ycombinator.com/item?id=9130934 . So what benefit will there be if some one use CompCert as the compiler for seL4? -- Cheers, Grissiom

3 2

Re: [seL4] How are capabilities assigned
by Sebastian Lau 02 Mar '15

02 Mar '15

Hi, sorry if this sounds stupid but are address spaces and threads directly managed by the kernel as in are they allocated and identified by the kernel or is there another that helps the kernel?

2 2

ifc6410 loading instructions
by Joel Nider 26 Feb '15

26 Feb '15

Hi, I'm trying to follow the instructions for loading the test image for ifc6410 on this page: http://sel4.systems/Hardware/IFC6410/ I'm not clear about the second instruction "> ramdisk". It looks to me like this is a redirection with some missing parts. Can you please help me fill in the blanks? Thanks, Joel

2 2

question about repo
by Tim Newsham 21 Feb '15

21 Feb '15

This is slightly tangential to sel4.. but.. sel4 uses "repo" to tie together projects that span multiple github repos. I'm really unclear on the proper workflow for using repo. I would like to keep my local patches (and be able to pull down updates from the master repositories), and I would like to pick patches to contribute back. What would the normal flow for these be? Should I be forking each github project that I work with and then fork a master "repo" project to reference my versions, somehow? Is there a good online guide that covers this? Tim

2 1

[PATCH] - fix am335x spurious interrupt issue
by Tim Newsham 21 Feb '15

21 Feb '15

patch for seL4 kernel attached.

1 0

How are capabilities assigned
by Sebastian Lau 17 Feb '15

17 Feb '15

I have a question, how are capabilities assigned or given to processes? Is it through the kernel or can the root process (like init etc.) assign capabilities as well? Also is IPC managed by calls to the kernel? I have in mind to base something off of seL4 in the future but I'm not quite ready to start though and just want to get an understanding of how things work.

2 3

am335x patches
by Tim Newsham 17 Feb '15

17 Feb '15

This set of fixes pushes AM335x support closer to working. With these patches and the previously submitted bootloader fix (https://github.com/seL4/elfloader-tool/issues/2) sel4 can boot and the sel4test project can run through some of the test cases. There are still some notable ommissions like missing timer and uart features and lack of uart IRQ support. - sel4 kernel - fix up sel4 kernel support for the am335x timer - note: this still receives lots of spurious interrupts - libplatsupport - bring code into line with conventions used by other ports - bring the uart code to life. PIO only for now - support multiple timers - libsel4platsupport - bring code into line with conventions used by other ports -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

2 2

am335x test PREEMPT_REVOKE hanging
by Tim Newsham 16 Feb '15

16 Feb '15

while running the am335x port through the sel4 test suite I'm getting a hang in the PREEMPT_REVOKE test. It appears the revoke_thread is getting created but it is never getting executed and hence the wait_for_helper on the revoke thread is hanging indefinitely.. Any idea what would cause this behavior? Tim

2 1

am335x and question
by Tim Newsham 14 Feb '15

14 Feb '15

I'm playing around with the am335x code now and have the sel4 test building but not working properly. If anyone else is interested in playing with this, let me know. I have a question about the boot loader, I'm seeing: if (UART_PPTR < kernel_info.virt_region_start) { printf("Jumping to kernel-image entry point...\n\n"); } else { /* Our serial port is no longer accessible */ } is this necessary? It looks like init_boot_pd established a 1:1 mapping for all addresses lower than the kernel vaddr (which for me is 0xf0000000). Shouldnt the UART be accesible here? I'm seeing the bootloader run up to mmu is turned on but nothing after that and trying to track down where the failure is happening. printf's after arm_enable_mmu are not working for me, and I don't understand if this is due to mmu bringup problems or something else. By the way, I started a "#seL4" channel on freenode IRC. -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

2 2

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel