fix typo; add more links

add Max's contribution
people who contributed to code, design, and docs
2026-03-27 18:39:55 +00:00 · 2014-08-09 13:07:11 +10:00 · 2014-08-08 14:48:02 +10:00 · 2014-08-08 14:45:58 +10:00 · 2014-08-08 13:50:10 +10:00 · 2014-08-08 10:09:56 +10:00
10 changed files with 117 additions and 30 deletions
--- a/CONTRIBUTORS.md
+++ b/CONTRIBUTORS.md
@@ -0,0 +1,54 @@
+Contributors
+------------
+
+People who contributed to the seL4 code, design, or documentation in this
+repository (in alphabetical order).
+
+* June Andronick, NICTA & UNSW
+* Ali Akguel, NICTA
+* Joel Beeren, NICTA
+* Bernard Blackham, NICTA & UNSW
+* Timothy Bourke, NICTA
+* Andrew Boyton, NICTA & UNSW
+* Matthew Brassil, NICTA
+* Aleksander Budzynowski, NICTA & UNSW
+* Manuel Chakravarty, NICTA & UNSW
+* Xi Ma Chen, NICTA
+* Nahida Chowdhury, NICTA
+* Peter Chubb, NICTA
+* David Cock, NICTA & UNSW
+* Adrian Danis, NICTA
+* Matthias Daum, NICTA & UNSW
+* Philip Derrin, NICTA
+* Dhammika Elkaduwe, NICTA & UNSW
+* Kevin Elphinstone, NICTA & UNSW
+* Matthew Fernandez, NICTA & UNSW
+* Peter Gammie, NICTA
+* Xin Gao, NICTA
+* David Greenaway, NICTA & UNSW
+* Matthew Grosvenor, NICTA
+* Lukas Haenel, NICTA
+* Gernot Heiser, NICTA & UNSW
+* Benjamin Kalman, NICTA
+* Justin King-Lacroix, NICTA
+* Gerwin Klein, NICTA & UNSW
+* Rafal Kolanski, NICTA & UNSW
+* Alexander Kroh, NICTA
+* Etienne Le Sueur, NICTA & UNSW
+* Corey Lewis, NICTA
+* Japheth Lim, NICTA
+* Anna Lyons, NICTA & UNSW
+* Stephanie McArthur, NICTA
+* Sam McNally, NICTA
+* Toby Murray, NICTA & UNSW
+* Ameya Palande, NICTA
+* Max R.D. Parmer
+* Sean Peters, NICTA
+* Simon Rodgers, NICTA
+* Sean Seefried, NICTA
+* Thomas Sewell, NICTA & UNSW
+* Michael von Tessin, NICTA & UNSW
+* Adam Walker, NICTA
+* James Wilmot, NICTA
+* Simon Winwood, NICTA
+* Jiawei Xie, NICTA
--- a/14
+++ b/14
@@ -55,13 +55,6 @@ config ARCH_IA32
            help
                Support for ARM1136JF-S

-        config ARM926EJ_S
-            bool "ARM926EJ-S"
-            depends on ARCH_ARM
-            select ARCH_ARM_V5
-            help 
-                Support for ARM926EJ_S
-
        config ARM_CORTEX_A8 
            bool "Cortex A8"
            depends on ARCH_ARM
@@ -97,13 +90,6 @@ config ARCH_IA32
            help
                Support for the KZM platform

-        config PLAT_INTEGRATORCP
-            bool "IntegratorCP Platform"
-            depends on ARCH_ARM
-            depends on ARM926EJ_S
-            help
-                Support for the IntegratorCP platform
-
        config PLAT_OMAP3
            bool "OMAP3 (BeagleBoard)"
            depends on ARCH_ARM
--- a/4
+++ b/4
@@ -17,7 +17,7 @@

 ARCH_LIST:=arm ia32
 CPU_LIST:=arm1136jf-s ixp420 cortex-a8 cortex-a9 cortex-a15
-PLAT_LIST:=imx31 pc99 integratorcp ixp420 omap3 am335x exynos4 exynos5 imx6 apq8064
+PLAT_LIST:=imx31 pc99 ixp420 omap3 am335x exynos4 exynos5 imx6 apq8064
 ARMV_LIST:=armv6 armv7-a

 ifndef SOURCE_ROOT
@@ -147,7 +147,7 @@ default: all
 ### Paths
 ############################################################

-PYTHONPATH = ${SOURCE_ROOT}/tools
+PYTHONPATH := ${PYTHONPATH}:${SOURCE_ROOT}/tools
 export PYTHONPATH

 vpath %.c   ${SOURCE_ROOT}
--- a/README.md
+++ b/README.md
@@ -1,10 +1,10 @@
-<!--  
+<!--
  Copyright 2014, General Dynamics C4 Systems
- 
+
  This software may be distributed and modified according to the terms of
  the GNU General Public License version 2. Note that NO WARRANTY is provided.
  See "LICENSE_GPLv2.txt" for details.
- 
+
  @TAG(GD_GPL)
 -->

@@ -13,25 +13,36 @@ The seL4 Repository

 This repository contains the source code of seL4 microkernel.

+For details about the seL4 microkernel, including details about its formal
+correctness proof, please see the [`sel4.systems`][1] website and associated
+[FAQ][2].
+
+We welcome contributions to seL4. Please see the website for information
+on [how to contribute][3].
+
 This repository is usually not used in isolation, but as part of the build
 system in a larger project.

+  [1]: http://sel4.systems/
+  [2]: http://sel4.systems/FAQ/
+  [3]: http://sel4.systems/Contributing/
+

 Repository Overview
 -------------------

  * `include` and `src`: C and ASM source code of seL4
  * `tools`: build tools
-  * `haskell`: Haskell model of the seL4 kernel, 
+  * `haskell`: Haskell model of the seL4 kernel,
               kept in sync with the C version.
  * `libsel4`: C bindings for the seL4 ABI
-  * `manual`: LaTeX sourced of the seL4 reference manual   
+  * `manual`: LaTeX sources of the seL4 reference manual


 Build Instructions
 ------------------

-tl;dr: 
+tl;dr:

    TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=imx31 ARMV=armv6 CPU=arm1136jf-s \
 	make
@@ -39,10 +50,10 @@ tl;dr:
 The kernel source requires a cross-compiler for the target architecture. To
 build using `make`, follow these instructions:

- * Ensure that the appropriate cross-compiler for your target 
+ * Ensure that the appropriate cross-compiler for your target
   architecture is installed.

- * Set the `TOOLPREFIX` environment variable to your cross-compiler's 
+ * Set the `TOOLPREFIX` environment variable to your cross-compiler's
   prefix. E.g. `arm-none-eabi-`.

 * Set the `ARCH`, `PLAT`, `ARMV` and `CPU` variables for the intended target
@@ -54,9 +65,13 @@ build using `make`, follow these instructions:
    arm  | omap3  | armv7-a | cortex-a8
    arm  | am335x | armv7-a | cortex-a8
    ia32 | pc99   |         |
-                            
+
 * For a debug build, append `DEBUG=y`.

+See the seL4 website for more [comprehensive build instructions][4].
+
+ [4]: http://sel4.systems/Download/
+

 License
 =======
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -1,4 +1,4 @@
-#!/usr/bin/python
+#!/usr/bin/env python
 #
 # Copyright 2014, NICTA
 #
--- a/manual/tools/gen_env.py
+++ b/manual/tools/gen_env.py
@@ -1,4 +1,4 @@
-#!/usr/bin/python
+#!/usr/bin/env python
 #
 # Copyright 2014, NICTA
 #
--- a/src/arch/arm/kernel/boot.c
+++ b/src/arch/arm/kernel/boot.c
@@ -440,6 +440,12 @@ try_init_kernel(
        return false;
    }

+    /* Before creating the initial thread (which also switches to it)
+     * we clean the cache so that any page table information written
+     * as a result of calling create_frames_of_region will be correctly
+     * read by the hardware page table walker */
+    cleanInvalidateL1Caches();
+
    /* create the initial thread */
    if (!create_initial_thread(
                root_cnode_cap,
--- a/src/plat/apq8064/machine/hardware.c
+++ b/src/plat/apq8064/machine/hardware.c
@@ -22,6 +22,7 @@

 /* Available physical memory regions on platform (RAM) */
 /* NOTE: Regions are not allowed to be adjacent! */
+/*       and must be page-aligned                */
 const p_region_t BOOT_RODATA avail_p_regs[] = {
    /* 2 GiB -1 page to prevent uin32_t overflow */
    { /* .start = */ 0x80000000, /* .end = */ 0xfffff000 }
@@ -38,7 +39,10 @@ get_avail_p_reg(unsigned int i)
 {
    return avail_p_regs[i];
 }
-
+/*
+ * We're limited to one page of boot data.
+ * Exclude some devices.
+ */
 const p_region_t BOOT_RODATA dev_p_regs[] = {
    { /* .start */ RPM_PADDR                 , /* .end */ RPM_PADDR                 + (1 << PAGE_BITS) },
    { /* .start */ RPM_TIMERS_PADDR          , /* .end */ RPM_TIMERS_PADDR          + (1 << PAGE_BITS) },
@@ -145,27 +149,49 @@ const p_region_t BOOT_RODATA dev_p_regs[] = {
    { /* .start */ SIC_APU_PADDR             , /* .end */ SIC_APU_PADDR             + (1 << PAGE_BITS) },
    { /* .start */ SIC_NON_SECURE_PADDR      , /* .end */ SIC_NON_SECURE_PADDR      + (1 << PAGE_BITS) },
    { /* .start */ INTCTL0_PADDR             , /* .end */ INTCTL0_PADDR             + (1 << PAGE_BITS) },
+#if (INTCTL1_PADDR & 0xfff) == 0
    { /* .start */ INTCTL1_PADDR             , /* .end */ INTCTL1_PADDR             + (1 << PAGE_BITS) },
+#endif
+#if (INTCTL2_PADDR & 0xfff) == 0
    { /* .start */ INTCTL2_PADDR             , /* .end */ INTCTL2_PADDR             + (1 << PAGE_BITS) },
+#endif
+#if (INTCTL3_PADDR & 0xfff) == 0
    { /* .start */ INTCTL3_PADDR             , /* .end */ INTCTL3_PADDR             + (1 << PAGE_BITS) },
+#endif
+#if (INTCTL4_PADDR & 0xfff) == 0
    { /* .start */ INTCTL4_PADDR             , /* .end */ INTCTL4_PADDR             + (1 << PAGE_BITS) },
+#endif
+#if (INTCTL5_PADDR & 0xfff) == 0
    { /* .start */ INTCTL5_PADDR             , /* .end */ INTCTL5_PADDR             + (1 << PAGE_BITS) },
+#endif
+#if (INTCTL6_PADDR & 0xfff) == 0
    { /* .start */ INTCTL6_PADDR             , /* .end */ INTCTL6_PADDR             + (1 << PAGE_BITS) },
+#endif
+#if (INTCTL7_PADDR & 0xfff) == 0
    { /* .start */ INTCTL7_PADDR             , /* .end */ INTCTL7_PADDR             + (1 << PAGE_BITS) },
+#endif
    { /* .start */ SDC2_PADDR                , /* .end */ SDC2_PADDR                + (1 << PAGE_BITS) },
+#if (SDC2_DML_PADDR & 0xfff) == 0
    { /* .start */ SDC2_DML_PADDR            , /* .end */ SDC2_DML_PADDR            + (1 << PAGE_BITS) },
+#endif
    { /* .start */ SDC2_BAM_PADDR            , /* .end */ SDC2_BAM_PADDR            + (1 << PAGE_BITS) },
    { /* .start */ SDC3_PADDR                , /* .end */ SDC3_PADDR                + (1 << PAGE_BITS) },
+#if (SDC3_DML_PADDR & 0xfff) == 0
    { /* .start */ SDC3_DML_PADDR            , /* .end */ SDC3_DML_PADDR            + (1 << PAGE_BITS) },
+#endif
    { /* .start */ SDC3_BAM_PADDR            , /* .end */ SDC3_BAM_PADDR            + (1 << PAGE_BITS) },
    { /* .start */ SDC4_PADDR                , /* .end */ SDC4_PADDR                + (1 << PAGE_BITS) },
+#if (SDC4_DML_PADDR & 0xfff) == 0
    { /* .start */ SDC4_DML_PADDR            , /* .end */ SDC4_DML_PADDR            + (1 << PAGE_BITS) },
+#endif
    { /* .start */ SDC4_BAM_PADDR            , /* .end */ SDC4_BAM_PADDR            + (1 << PAGE_BITS) },
    { /* .start */ BAM_DMA_PADDR             , /* .end */ BAM_DMA_PADDR             + (1 << PAGE_BITS) },
    { /* .start */ BAM_DMA_BAM_PADDR         , /* .end */ BAM_DMA_BAM_PADDR         + (1 << PAGE_BITS) },
    { /* .start */ BAM_DMA_BAM_XPU_PADDR     , /* .end */ BAM_DMA_BAM_XPU_PADDR     + (1 << PAGE_BITS) },
    { /* .start */ SDC1_PADDR                , /* .end */ SDC1_PADDR                + (1 << PAGE_BITS) },
+#if (SDC1_DML_PADDR & 0xfff) == 0
    { /* .start */ SDC1_DML_PADDR            , /* .end */ SDC1_DML_PADDR            + (1 << PAGE_BITS) },
+#endif
    { /* .start */ SDC1_BAM_PADDR            , /* .end */ SDC1_BAM_PADDR            + (1 << PAGE_BITS) },
    { /* .start */ SPS_GSBI1_PADDR           , /* .end */ SPS_GSBI1_PADDR           + (1 << PAGE_BITS) },
    { /* .start */ SPS_UART1_DM_PADDR        , /* .end */ SPS_UART1_DM_PADDR        + (1 << PAGE_BITS) },
--- a/tools/invocation_header_gen.py
+++ b/tools/invocation_header_gen.py
@@ -1,4 +1,4 @@
-#!/usr/bin/python 
+#!/usr/bin/env python
 #
 # Copyright 2014, NICTA
 #
--- a/tools/syscall_header_gen.py
+++ b/tools/syscall_header_gen.py
@@ -1,4 +1,4 @@
-#!/usr/bin/python 
+#!/usr/bin/env python
 #
 # Copyright 2014, NICTA
 #
Author	SHA1	Message	Date
Gerwin Klein	e88fe4e356	fix typo; add more links	2014-08-09 13:07:11 +10:00
Gerwin Klein	1458c9c191	add Max's contribution	2014-08-08 14:48:02 +10:00
Gerwin Klein	783f0204ab	people who contributed to code, design, and docs (state before release on 29 July 2014)	2014-08-08 14:45:58 +10:00
Peter Chubb	2261557ab3	Fix IFC6410 build The IFC6410 has too many devices to fit into the bootinfo page. What is more, some are aligned on half-page boundaries. Exclude devices on half-page boundaries from the bootinfo device list.	2014-08-08 13:50:10 +10:00
Gerwin Klein	f7611991c3	Remove last bits of unsupported integratorcp platform. Suggested by @jserv on https://github.com/seL4/seL4/issues/1	2014-08-08 10:09:56 +10:00
Adrian Danis	0b64f564e5	arm: Perform additional cache clean to prevent TLB walker loading garbage entries for first user process	2014-08-08 09:30:30 +10:00
Max R.D. Parmer	da5ec79cf9	Use usr/bin/env for all python bangpaths to enable virtualenv use. Very useful with python3 as the default platform.	2014-08-03 18:53:14 -07:00
Gerwin Klein	53941f4beb	remove unsupported platform	2014-07-31 15:05:12 +10:00
Adrian Danis	514256e3ad	Merge pull request #6 from adanis/pythonpath Do not discard user PYTHONPATH when building	2014-07-30 14:41:46 +10:00
Adrian Danis	f5b2a6f9c7	Do not discard user PYTHONPATH when building	2014-07-30 14:21:33 +10:00
David Greenaway	64b43f4447	Add links to "seL4.systems" website to "README.md".	2014-07-29 19:58:26 +10:00