Devel

devel@sel4.systems

20 participants
1384 discussions

[PATCH] Use usr/bin/env for all python bangpaths to enable virtualenv
by Max R.D. Parmer 05 Aug '14

05 Aug '14

This patch targets the core "seL4" repo. I idly submitted a PR on github before reading anything at all really (beyond checking to see if the issue was made more consistent in subsequent commits). Apologies if this is/was inconvenient. I saw some prior github discussion on whether "python2" or "python" is best'; IMHO, "python" is best as virtualenv allows the desired binary to be specified at env creation time. CLA forthcoming, I'm quite a long way from printers/scanners and all those sorts of things. -- @maximus_freeman 0x7D964D3361142ACF

3 2

seL4 boot issue
by Jorge Ventura 05 Aug '14

05 Aug '14

I am trying to boot seL4 on beaglebone white. I have an initial code just to configure the DDR2 memory at range 0x80000000-0xbfffffff. As we can see below, the start address is the virtual address 0xf0000000 but at this point I have no MMU configured. I was thinking that the segment .boot should be the code to prepare all details about MMU/D-CACHE/I-CACHE but it's not what gdb is understanding based in the elf header. Someone could explain to me how is the kernel boot; what do I have to consider. I guess that beaglebone is not supported but this is exactly my goal, to make seL4 boot on beaglebone. Any help or suggestion is very welcome. Sincerely, Jorge Ventura (gdb) load kernel.elf > Loading section .boot, size 0x10000 lma 0x80000000 > Loading section .text, size 0xf1ec lma 0x80010000 > Loading section .text.unlikely, size 0xd98 lma 0x8001f1ec > Loading section .rodata, size 0x4170 lma 0x8001ff84 > Loading section .data, size 0x8 lma 0x800240f4 > Start address 0xf0000000, load size 147708 > Transfer rate: 319 KB/sec, 3787 bytes/write. > (gdb) monitor poll background polling: on TAP: am335x.dap (enabled) target state: halted target halted in ARM state due to debug-request, current mode: System cpsr: 0x6000019f pc: 0xf0000000 MMU: disabled, D-Cache: disabled, I-Cache: disabled

1 1

active development and verification
by Tim Newsham 05 Aug '14

05 Aug '14

A question I had about how the sel4 project is run internally: What is your process of developing ongoing changes and how does verification fit into it? Do you maintain the proofs with kernel modifications on an ongoing basis? On a semi-regular basis? Is the "experimental" branch verified? When time slices are no longer global, will those changes be verified? etc... Tim

2 2

ArchLinux/Manjaro development
by stercor 03 Aug '14

03 Aug '14

Has there been any seL4 development effort for the ArchLinux or Manjaro platforms? -- GPG/PGP public key: B07F9AAE

2 1

signing git commits
by HW42 01 Aug '14

01 Aug '14

Hi, I really like to see big formally verified software. But it seems your provide no way to verify the downloads from your repositories. I think you should use signed git tags and also ensure that repo verify those. HW42

2 1

run_tests needs mlton-compiler gcc-arm-none-eabi
by Harry Butterworth 01 Aug '14

01 Aug '14

On Ubuntu 14.04, after attempting to follow the instructions, I found I needed to add two extra packages. I needed mlton-complier for CParserTools and gcc-arm-none-eabi for CBaseRefine. gcc-arm-linux-gnueabi is a documented dependency for 14.04 and was already installed when the CBaseRefine test was failing. After installing those two packages and the documented latex extras all 31 regression tests passed.

2 1

AM335X (BeagleBone) support?
by Tim Newsham 31 Jul '14

31 Jul '14

What is the state of "AM335X (BeagleBone)" support in the main and experimental branches? Tim

2 1

Running seL4 on a Raspberry Pi?
by Quigley, Joseph 31 Jul '14

31 Jul '14

Hello! My name is Joe Quigley, I found out about the project recently and want to start experimenting with it on a Rasberry Pi I have floating around. Because it uses a very similar ARMv6 CPU as the KZM-ARM11-01, am I correct in assuming it will work with that kernel? -- --Joe Quigley

2 1

(simple?) build error?
by Tim Newsham 31 Jul '14

31 Jul '14

I'm getting an error when building from Ubuntu. I'm building from: repo init -u https://github.com/seL4/sel4test-manifest.git I've configured with: make ia32_simulation_release_xml_defconfig and done "make menuconfig" accepting the defaults. Finally I run make and get errors: [KERNEL] [CC] kernel_final.s src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c: In function ‘init_boot_pd’: src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c:58:23: error: array subscript is above array bounds [-Werror=array-bounds] cc1: all warnings being treated as errors make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Error 2 Attached is the output of "make V=2" (for verbosity). Tim

3 2

virtualization and linux?
by Tim Newsham 31 Jul '14

31 Jul '14

Is there any documentation on using the VMM support for x86 seL4? Also, when can we hear more about "Served by Apache on Linux on seL4."? Tim

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel