- Devel - lists.sel4.systems

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

Does the kernel build support the gold linker?
by Stephen Thomas 30 Jul '14

30 Jul '14

I tried building the kernel for ARCH=ia32 and PLAT=pc99 and I fail with a linker errror. Is there a linker script that supports the gold linker (for linux). Cheers Thomo

2 1

Initial architecture/processor support in seL4
by Peter Howard 26 Jun '14

26 Jun '14

HI, I'm wondering what CPUs the initial source release for seL4 will support. In http://www.nicta.com.au/pub?doc=6930&filename=Elphinstone_Heiser_13.pdf It references Core i7 32-bit, ARM11, and Cortex A9 - covering x86, ARMv6, and ARMv7. What else will be in there? Thanks, -- Peter Howard <pjh(a)northern-ridge.com.au>

2 2