- Devel - lists.sel4.systems

raspberry pi 4
by Sachin More 04 Nov '20

04 Nov '20

Hi: Thanks to Nick and Peter. I have made some progress: 1. For the kernel code, used origin/rpi4 branch from https://github.com/nspin/seL4.git 2. Used https://github.com/seL4/camkes.git for the build and replaced the kernel with the one in step 1. 3. There is no bcm2711.dts in origin/rpi4, so got one one from linux. The final version, called rpi4.dts is listed at the end this email. 4. Made changes to add rpi4 as a new platform. However, I am stumped trying to reconcile rpi4.dts and overlay-rpi4.dts. The latter contains a reference to a node /soc/gic400@40041000. The equivalent node in rpi4.dts is /sic/gicv2. But I am getting the following error from init-build.sh when it is trying to create kernel.dtb: /host/VPI/camkes-project/build/kernel/kernel.dtb: ERROR (path_references): /chosen: Reference to non-existent node or label "/soc/gicv2" Any ideas? thanks, Sachin -------------------- rpi4.dts ----------------------------- /dts-v1/; /memreserve/ 0x00000000 0x00001000; / { compatible = "brcm,bcm2835"; model = "BCM2835"; #address-cells = <1>; #size-cells = <1>; aliases { serial0 = &uart0; serial1 = &uart1; }; chosen { stdout-path = "serial0:115200n8"; }; rmem: reserved-memory { #address-cells = <1>; #size-cells = <1>; ranges; cma: linux,cma { compatible = "shared-dma-pool"; size = <0x4000000>; reusable; linux,cma-default; }; }; thermal-zones { cpu_thermal: cpu-thermal { polling-delay-passive = <0>; polling-delay = <1000>; trips { cpu-crit { temperature = <90000>; hysteresis = <0>; type = "critical"; }; }; cooling-maps { }; }; }; soc { compatible = "simple-bus"; #address-cells = <1>; #size-cells = <1>; system_timer: timer@7e003000 { compatible = "brcm,bcm2835-system-timer"; reg = <0x7e003000 0x1000>; interrupts = <1 0>, <1 1>, <1 2>, <1 3>; clock-frequency = <1000000>; }; txp: txp@7e004000 { compatible = "brcm,bcm2835-txp"; reg = <0x7e004000 0x20>; interrupts = <1 11>; }; clocks: cprman@7e101000 { compatible = "brcm,bcm2835-cprman"; #clock-cells = <1>; reg = <0x7e101000 0x2000>; clocks = <&clk_osc>, <&dsi0 0>, <&dsi0 1>, <&dsi0 2>, <&dsi1 0>, <&dsi1 1>, <&dsi1 2>; }; mailbox: mailbox@7e00b880 { compatible = "brcm,bcm2835-mbox"; reg = <0x7e00b880 0x40>; interrupts = <0 1>; #mbox-cells = <0>; }; gpio: gpio@7e200000 { compatible = "brcm,bcm2835-gpio"; reg = <0x7e200000 0xb4>; interrupts = <2 17>, <2 18>, <2 19>, <2 20>; gpio-controller; #gpio-cells = <2>; interrupt-controller; #interrupt-cells = <2>; dpi_gpio0: dpi_gpio0 { brcm,pins = <0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27>; brcm,function = <6>; }; emmc_gpio22: emmc_gpio22 { brcm,pins = <22 23 24 25 26 27>; brcm,function = <7>; }; emmc_gpio34: emmc_gpio34 { brcm,pins = <34 35 36 37 38 39>; brcm,function = <7>; brcm,pull = <0 2 2 2 2 2>; }; emmc_gpio48: emmc_gpio48 { brcm,pins = <48 49 50 51 52 53>; brcm,function = <7>; }; gpclk0_gpio4: gpclk0_gpio4 { brcm,pins = <4>; brcm,function = <4>; }; gpclk1_gpio5: gpclk1_gpio5 { brcm,pins = <5>; brcm,function = <4>; }; gpclk1_gpio42: gpclk1_gpio42 { brcm,pins = <42>; brcm,function = <4>; }; gpclk1_gpio44: gpclk1_gpio44 { brcm,pins = <44>; brcm,function = <4>; }; gpclk2_gpio6: gpclk2_gpio6 { brcm,pins = <6>; brcm,function = <4>; }; gpclk2_gpio43: gpclk2_gpio43 { brcm,pins = <43>; brcm,function = <4>; brcm,pull = <0>; }; i2c0_gpio0: i2c0_gpio0 { brcm,pins = <0 1>; brcm,function = <4>; }; i2c0_gpio28: i2c0_gpio28 { brcm,pins = <28 29>; brcm,function = <4>; }; i2c0_gpio44: i2c0_gpio44 { brcm,pins = <44 45>; brcm,function = <5>; }; i2c1_gpio2: i2c1_gpio2 { brcm,pins = <2 3>; brcm,function = <4>; }; i2c1_gpio44: i2c1_gpio44 { brcm,pins = <44 45>; brcm,function = <6>; }; jtag_gpio22: jtag_gpio22 { brcm,pins = <22 23 24 25 26 27>; brcm,function = <3>; }; pcm_gpio18: pcm_gpio18 { brcm,pins = <18 19 20 21>; brcm,function = <4>; }; pcm_gpio28: pcm_gpio28 { brcm,pins = <28 29 30 31>; brcm,function = <6>; }; sdhost_gpio48: sdhost_gpio48 { brcm,pins = <48 49 50 51 52 53>; brcm,function = <4>; }; spi0_gpio7: spi0_gpio7 { brcm,pins = <7 8 9 10 11>; brcm,function = <4>; }; spi0_gpio35: spi0_gpio35 { brcm,pins = <35 36 37 38 39>; brcm,function = <4>; }; spi1_gpio16: spi1_gpio16 { brcm,pins = <16 17 18 19 20 21>; brcm,function = <3>; }; spi2_gpio40: spi2_gpio40 { brcm,pins = <40 41 42 43 44 45>; brcm,function = <3>; }; uart0_gpio14: uart0_gpio14 { brcm,pins = <14 15>; brcm,function = <4>; }; uart0_ctsrts_gpio16: uart0_ctsrts_gpio16 { brcm,pins = <16 17>; brcm,function = <7>; }; uart0_ctsrts_gpio30: uart0_ctsrts_gpio30 { brcm,pins = <30 31>; brcm,function = <7>; brcm,pull = <2 0>; }; uart0_gpio32: uart0_gpio32 { brcm,pins = <32 33>; brcm,function = <7>; brcm,pull = <0 2>; }; uart0_gpio36: uart0_gpio36 { brcm,pins = <36 37>; brcm,function = <6>; }; uart0_ctsrts_gpio38: uart0_ctsrts_gpio38 { brcm,pins = <38 39>; brcm,function = <6>; }; uart1_gpio14: uart1_gpio14 { brcm,pins = <14 15>; brcm,function = <2>; }; uart1_ctsrts_gpio16: uart1_ctsrts_gpio16 { brcm,pins = <16 17>; brcm,function = <2>; }; uart1_gpio32: uart1_gpio32 { brcm,pins = <32 33>; brcm,function = <2>; }; uart1_ctsrts_gpio30: uart1_ctsrts_gpio30 { brcm,pins = <30 31>; brcm,function = <2>; }; uart1_gpio40: uart1_gpio40 { brcm,pins = <40 41>; brcm,function = <2>; }; uart1_ctsrts_gpio42: uart1_ctsrts_gpio42 { brcm,pins = <42 43>; brcm,function = <2>; }; }; uart0: serial@7e201000 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201000 0x200>; interrupts = <2 25>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; }; sdhost: mmc@7e202000 { compatible = "brcm,bcm2835-sdhost"; reg = <0x7e202000 0x100>; interrupts = <2 24>; clocks = <&clocks 20>; status = "disabled"; }; i2s: i2s@7e203000 { compatible = "brcm,bcm2835-i2s"; reg = <0x7e203000 0x24>; clocks = <&clocks 31>; status = "disabled"; }; spi: spi@7e204000 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204000 0x200>; interrupts = <2 22>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c0: i2c@7e205000 { compatible = "brcm,bcm2835-i2c"; reg = <0x7e205000 0x200>; interrupts = <2 21>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; dpi: dpi@7e208000 { compatible = "brcm,bcm2835-dpi"; reg = <0x7e208000 0x8c>; clocks = <&clocks 20>, <&clocks 44>; clock-names = "core", "pixel"; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; dsi0: dsi@7e209000 { compatible = "brcm,bcm2835-dsi0"; reg = <0x7e209000 0x78>; interrupts = <2 4>; #address-cells = <1>; #size-cells = <0>; #clock-cells = <1>; clocks = <&clocks 32>, <&clocks 47>, <&clocks 49>; clock-names = "phy", "escape", "pixel"; clock-output-names = "dsi0_byte", "dsi0_ddr2", "dsi0_ddr"; status = "disabled"; }; aux: aux@7e215000 { compatible = "brcm,bcm2835-aux"; #clock-cells = <1>; reg = <0x7e215000 0x8>; clocks = <&clocks 20>; }; uart1: serial@7e215040 { compatible = "brcm,bcm2835-aux-uart"; reg = <0x7e215040 0x40>; interrupts = <1 29>; clocks = <&aux 0>; status = "disabled"; }; spi1: spi@7e215080 { compatible = "brcm,bcm2835-aux-spi"; reg = <0x7e215080 0x40>; interrupts = <1 29>; clocks = <&aux 1>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi2: spi@7e2150c0 { compatible = "brcm,bcm2835-aux-spi"; reg = <0x7e2150c0 0x40>; interrupts = <1 29>; clocks = <&aux 2>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; pwm: pwm@7e20c000 { compatible = "brcm,bcm2835-pwm"; reg = <0x7e20c000 0x28>; clocks = <&clocks 30>; assigned-clocks = <&clocks 30>; assigned-clock-rates = <10000000>; #pwm-cells = <2>; status = "disabled"; }; sdhci: sdhci@7e300000 { compatible = "brcm,bcm2835-sdhci"; reg = <0x7e300000 0x100>; interrupts = <2 30>; clocks = <&clocks 28>; status = "disabled"; }; hvs@7e400000 { compatible = "brcm,bcm2835-hvs"; reg = <0x7e400000 0x6000>; interrupts = <2 1>; }; dsi1: dsi@7e700000 { compatible = "brcm,bcm2835-dsi1"; reg = <0x7e700000 0x8c>; interrupts = <2 12>; #address-cells = <1>; #size-cells = <0>; #clock-cells = <1>; clocks = <&clocks 35>, <&clocks 48>, <&clocks 50>; clock-names = "phy", "escape", "pixel"; clock-output-names = "dsi1_byte", "dsi1_ddr2", "dsi1_ddr"; status = "disabled"; }; i2c1: i2c@7e804000 { compatible = "brcm,bcm2835-i2c"; reg = <0x7e804000 0x1000>; interrupts = <2 21>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; vec: vec@7e806000 { compatible = "brcm,bcm2835-vec"; reg = <0x7e806000 0x1000>; clocks = <&clocks 24>; interrupts = <2 27>; status = "disabled"; }; usb: usb@7e980000 { compatible = "brcm,bcm2835-usb"; reg = <0x7e980000 0x10000>; interrupts = <1 9>; #address-cells = <1>; #size-cells = <0>; clocks = <&clk_usb>; clock-names = "otg"; phys = <&usbphy>; phy-names = "usb2-phy"; }; }; clocks { clk_osc: clk-osc { compatible = "fixed-clock"; #clock-cells = <0>; clock-output-names = "osc"; clock-frequency = <19200000>; }; clk_usb: clk-usb { compatible = "fixed-clock"; #clock-cells = <0>; clock-output-names = "otg"; clock-frequency = <480000000>; }; }; usbphy: phy { compatible = "usb-nop-xceiv"; #phy-cells = <0>; }; }; / { compatible = "brcm,bcm2711"; #address-cells = <2>; #size-cells = <1>; interrupt-parent = <&gicv2>; vc4: gpu { compatible = "brcm,bcm2711-vc5"; status = "disabled"; }; clk_27MHz: clk-27M { #clock-cells = <0>; compatible = "fixed-clock"; clock-frequency = <27000000>; clock-output-names = "27MHz-clock"; }; clk_108MHz: clk-108M { #clock-cells = <0>; compatible = "fixed-clock"; clock-frequency = <108000000>; clock-output-names = "108MHz-clock"; }; soc { ranges = <0x7e000000 0x0 0xfe000000 0x01800000>, <0x7c000000 0x0 0xfc000000 0x02000000>, <0x40000000 0x0 0xff800000 0x00800000>; dma-ranges = <0xc0000000 0x0 0x00000000 0x40000000>; local_intc: local_intc@40000000 { compatible = "brcm,bcm2836-l1-intc"; reg = <0x40000000 0x100>; }; gicv2: interrupt-controller@40041000 { interrupt-controller; #interrupt-cells = <3>; compatible = "arm,gic-400"; reg = <0x40041000 0x1000>, <0x40042000 0x2000>, <0x40044000 0x2000>, <0x40046000 0x2000>; interrupts = <1 9 ((((1 << (4)) - 1) << 8) | 4)>; }; avs_monitor: avs-monitor@7d5d2000 { compatible = "brcm,bcm2711-avs-monitor", "syscon", "simple-mfd"; reg = <0x7d5d2000 0xf00>; thermal: thermal { compatible = "brcm,bcm2711-thermal"; #thermal-sensor-cells = <0>; }; }; dma: dma@7e007000 { compatible = "brcm,bcm2835-dma"; reg = <0x7e007000 0xb00>; interrupts = <0 80 4>, <0 81 4>, <0 82 4>, <0 83 4>, <0 84 4>, <0 85 4>, <0 86 4>, <0 87 4>, <0 87 4>, <0 88 4>, <0 88 4>; interrupt-names = "dma0", "dma1", "dma2", "dma3", "dma4", "dma5", "dma6", "dma7", "dma8", "dma9", "dma10"; #dma-cells = <1>; brcm,dma-channel-mask = <0x07f5>; }; pm: watchdog@7e100000 { compatible = "brcm,bcm2835-pm", "brcm,bcm2835-pm-wdt"; #power-domain-cells = <1>; #reset-cells = <1>; reg = <0x7e100000 0x114>, <0x7e00a000 0x24>, <0x7ec11000 0x20>; clocks = <&clocks 21>, <&clocks 29>, <&clocks 23>, <&clocks 22>; clock-names = "v3d", "peri_image", "h264", "isp"; system-power-controller; }; rng@7e104000 { compatible = "brcm,bcm2711-rng200"; reg = <0x7e104000 0x28>; }; uart2: serial@7e201400 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201400 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; uart3: serial@7e201600 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201600 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; uart4: serial@7e201800 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201800 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; uart5: serial@7e201a00 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201a00 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; spi3: spi@7e204600 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204600 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi4: spi@7e204800 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204800 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi5: spi@7e204a00 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204a00 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi6: spi@7e204c00 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204c00 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c3: i2c@7e205600 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205600 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c4: i2c@7e205800 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205800 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c5: i2c@7e205a00 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205a00 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c6: i2c@7e205c00 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205c00 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; pixelvalve0: pixelvalve@7e206000 { compatible = "brcm,bcm2711-pixelvalve0"; reg = <0x7e206000 0x100>; interrupts = <0 109 4>; status = "disabled"; }; pixelvalve1: pixelvalve@7e207000 { compatible = "brcm,bcm2711-pixelvalve1"; reg = <0x7e207000 0x100>; interrupts = <0 110 4>; status = "disabled"; }; pixelvalve2: pixelvalve@7e20a000 { compatible = "brcm,bcm2711-pixelvalve2"; reg = <0x7e20a000 0x100>; interrupts = <0 101 4>; status = "disabled"; }; pwm1: pwm@7e20c800 { compatible = "brcm,bcm2835-pwm"; reg = <0x7e20c800 0x28>; clocks = <&clocks 30>; assigned-clocks = <&clocks 30>; assigned-clock-rates = <10000000>; #pwm-cells = <2>; status = "disabled"; }; pixelvalve4: pixelvalve@7e216000 { compatible = "brcm,bcm2711-pixelvalve4"; reg = <0x7e216000 0x100>; interrupts = <0 110 4>; status = "disabled"; }; hvs: hvs@7e400000 { compatible = "brcm,bcm2711-hvs"; interrupts = <0 97 4>; }; pixelvalve3: pixelvalve@7ec12000 { compatible = "brcm,bcm2711-pixelvalve3"; reg = <0x7ec12000 0x100>; interrupts = <0 106 4>; status = "disabled"; }; dvp: clock@7ef00000 { compatible = "brcm,brcm2711-dvp"; reg = <0x7ef00000 0x10>; clocks = <&clk_108MHz>; #clock-cells = <1>; #reset-cells = <1>; }; hdmi0: hdmi@7ef00700 { compatible = "brcm,bcm2711-hdmi0"; reg = <0x7ef00700 0x300>, <0x7ef00300 0x200>, <0x7ef00f00 0x80>, <0x7ef00f80 0x80>, <0x7ef01b00 0x200>, <0x7ef01f00 0x400>, <0x7ef00200 0x80>, <0x7ef04300 0x100>, <0x7ef20000 0x100>; reg-names = "hdmi", "dvp", "phy", "rm", "packet", "metadata", "csc", "cec", "hd"; clock-names = "hdmi", "bvb", "audio", "cec"; resets = <&dvp 0>; ddc = <&ddc0>; dmas = <&dma 10>; dma-names = "audio-rx"; status = "disabled"; }; ddc0: i2c@7ef04500 { compatible = "brcm,bcm2711-hdmi-i2c"; reg = <0x7ef04500 0x100>, <0x7ef00b00 0x300>; reg-names = "bsc", "auto-i2c"; clock-frequency = <97500>; status = "disabled"; }; hdmi1: hdmi@7ef05700 { compatible = "brcm,bcm2711-hdmi1"; reg = <0x7ef05700 0x300>, <0x7ef05300 0x200>, <0x7ef05f00 0x80>, <0x7ef05f80 0x80>, <0x7ef06b00 0x200>, <0x7ef06f00 0x400>, <0x7ef00280 0x80>, <0x7ef09300 0x100>, <0x7ef20000 0x100>; reg-names = "hdmi", "dvp", "phy", "rm", "packet", "metadata", "csc", "cec", "hd"; ddc = <&ddc1>; clock-names = "hdmi", "bvb", "audio", "cec"; resets = <&dvp 1>; dmas = <&dma 17>; dma-names = "audio-rx"; status = "disabled"; }; ddc1: i2c@7ef09500 { compatible = "brcm,bcm2711-hdmi-i2c"; reg = <0x7ef09500 0x100>, <0x7ef05b00 0x300>; reg-names = "bsc", "auto-i2c"; clock-frequency = <97500>; status = "disabled"; }; }; emmc2bus: emmc2bus { compatible = "simple-bus"; #address-cells = <2>; #size-cells = <1>; ranges = <0x0 0x7e000000 0x0 0xfe000000 0x01800000>; dma-ranges = <0x0 0xc0000000 0x0 0x00000000 0x40000000>; emmc2: emmc2@7e340000 { compatible = "brcm,bcm2711-emmc2"; reg = <0x0 0x7e340000 0x100>; interrupts = <0 126 4>; clocks = <&clocks 51>; status = "disabled"; }; }; arm-pmu { compatible = "arm,cortex-a72-pmu", "arm,armv8-pmuv3"; interrupts = <0 16 4>, <0 17 4>, <0 18 4>, <0 19 4>; interrupt-affinity = <&cpu0>, <&cpu1>, <&cpu2>, <&cpu3>; }; timer { compatible = "arm,armv8-timer"; interrupts = <1 13 ((((1 << (4)) - 1) << 8) | 8)>, <1 14 ((((1 << (4)) - 1) << 8) | 8)>, <1 11 ((((1 << (4)) - 1) << 8) | 8)>, <1 10 ((((1 << (4)) - 1) << 8) | 8)>; arm,cpu-registers-not-fw-configured; }; cpus: cpus { #address-cells = <1>; #size-cells = <0>; enable-method = "brcm,bcm2836-smp"; cpu0: cpu@0 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <0>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000d8>; }; cpu1: cpu@1 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <1>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000e0>; }; cpu2: cpu@2 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <2>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000e8>; }; cpu3: cpu@3 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <3>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000f0>; }; }; scb { compatible = "simple-bus"; #address-cells = <2>; #size-cells = <1>; ranges = <0x0 0x7c000000 0x0 0xfc000000 0x03800000>, <0x6 0x00000000 0x6 0x00000000 0x40000000>; pcie0: pcie@7d500000 { compatible = "brcm,bcm2711-pcie"; reg = <0x0 0x7d500000 0x9310>; device_type = "pci"; #address-cells = <3>; #interrupt-cells = <1>; #size-cells = <2>; interrupts = <0 148 4>, <0 148 4>; interrupt-names = "pcie", "msi"; interrupt-map-mask = <0x0 0x0 0x0 0x7>; interrupt-map = <0 0 0 1 &gicv2 0 143 4>; msi-controller; msi-parent = <&pcie0>; ranges = <0x02000000 0x0 0xf8000000 0x6 0x00000000 0x0 0x04000000>; dma-ranges = <0x02000000 0x0 0x00000000 0x0 0x00000000 0x0 0xc0000000>; brcm,enable-ssc; }; genet: ethernet@7d580000 { compatible = "brcm,bcm2711-genet-v5"; reg = <0x0 0x7d580000 0x10000>; #address-cells = <0x1>; #size-cells = <0x1>; interrupts = <0 157 4>, <0 158 4>; status = "disabled"; genet_mdio: mdio@e14 { compatible = "brcm,genet-mdio-v5"; reg = <0xe14 0x8>; reg-names = "mdio"; #address-cells = <0x0>; #size-cells = <0x1>; }; }; }; }; &clk_osc { clock-frequency = <54000000>; }; &clocks { compatible = "brcm,bcm2711-cprman"; }; &cpu_thermal { coefficients = <(-487) 410040>; thermal-sensors = <&thermal>; }; &dsi0 { interrupts = <0 100 4>; }; &dsi1 { interrupts = <0 108 4>; }; &gpio { compatible = "brcm,bcm2711-gpio"; interrupts = <0 113 4>, <0 114 4>, <0 115 4>, <0 116 4>; gpclk0_gpio49: gpclk0_gpio49 { pin-gpclk { pins = "gpio49"; function = "alt1"; bias-disable; }; }; gpclk1_gpio50: gpclk1_gpio50 { pin-gpclk { pins = "gpio50"; function = "alt1"; bias-disable; }; }; gpclk2_gpio51: gpclk2_gpio51 { pin-gpclk { pins = "gpio51"; function = "alt1"; bias-disable; }; }; i2c0_gpio46: i2c0_gpio46 { pin-sda { function = "alt0"; pins = "gpio46"; bias-pull-up; }; pin-scl { function = "alt0"; pins = "gpio47"; bias-disable; }; }; i2c1_gpio46: i2c1_gpio46 { pin-sda { function = "alt1"; pins = "gpio46"; bias-pull-up; }; pin-scl { function = "alt1"; pins = "gpio47"; bias-disable; }; }; i2c3_gpio2: i2c3_gpio2 { pin-sda { function = "alt5"; pins = "gpio2"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio3"; bias-disable; }; }; i2c3_gpio4: i2c3_gpio4 { pin-sda { function = "alt5"; pins = "gpio4"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio5"; bias-disable; }; }; i2c4_gpio6: i2c4_gpio6 { pin-sda { function = "alt5"; pins = "gpio6"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio7"; bias-disable; }; }; i2c4_gpio8: i2c4_gpio8 { pin-sda { function = "alt5"; pins = "gpio8"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio9"; bias-disable; }; }; i2c5_gpio10: i2c5_gpio10 { pin-sda { function = "alt5"; pins = "gpio10"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio11"; bias-disable; }; }; i2c5_gpio12: i2c5_gpio12 { pin-sda { function = "alt5"; pins = "gpio12"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio13"; bias-disable; }; }; i2c6_gpio0: i2c6_gpio0 { pin-sda { function = "alt5"; pins = "gpio0"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio1"; bias-disable; }; }; i2c6_gpio22: i2c6_gpio22 { pin-sda { function = "alt5"; pins = "gpio22"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio23"; bias-disable; }; }; i2c_slave_gpio8: i2c_slave_gpio8 { pins-i2c-slave { pins = "gpio8", "gpio9", "gpio10", "gpio11"; function = "alt3"; }; }; jtag_gpio48: jtag_gpio48 { pins-jtag { pins = "gpio48", "gpio49", "gpio50", "gpio51", "gpio52", "gpio53"; function = "alt4"; }; }; mii_gpio28: mii_gpio28 { pins-mii { pins = "gpio28", "gpio29", "gpio30", "gpio31"; function = "alt4"; }; }; mii_gpio36: mii_gpio36 { pins-mii { pins = "gpio36", "gpio37", "gpio38", "gpio39"; function = "alt5"; }; }; pcm_gpio50: pcm_gpio50 { pins-pcm { pins = "gpio50", "gpio51", "gpio52", "gpio53"; function = "alt2"; }; }; pwm0_0_gpio12: pwm0_0_gpio12 { pin-pwm { pins = "gpio12"; function = "alt0"; bias-disable; }; }; pwm0_0_gpio18: pwm0_0_gpio18 { pin-pwm { pins = "gpio18"; function = "alt5"; bias-disable; }; }; pwm1_0_gpio40: pwm1_0_gpio40 { pin-pwm { pins = "gpio40"; function = "alt0"; bias-disable; }; }; pwm0_1_gpio13: pwm0_1_gpio13 { pin-pwm { pins = "gpio13"; function = "alt0"; bias-disable; }; }; pwm0_1_gpio19: pwm0_1_gpio19 { pin-pwm { pins = "gpio19"; function = "alt5"; bias-disable; }; }; pwm1_1_gpio41: pwm1_1_gpio41 { pin-pwm { pins = "gpio41"; function = "alt0"; bias-disable; }; }; pwm0_1_gpio45: pwm0_1_gpio45 { pin-pwm { pins = "gpio45"; function = "alt0"; bias-disable; }; }; pwm0_0_gpio52: pwm0_0_gpio52 { pin-pwm { pins = "gpio52"; function = "alt1"; bias-disable; }; }; pwm0_1_gpio53: pwm0_1_gpio53 { pin-pwm { pins = "gpio53"; function = "alt1"; bias-disable; }; }; rgmii_gpio35: rgmii_gpio35 { pin-start-stop { pins = "gpio35"; function = "alt4"; }; pin-rx-ok { pins = "gpio36"; function = "alt4"; }; }; rgmii_irq_gpio34: rgmii_irq_gpio34 { pin-irq { pins = "gpio34"; function = "alt5"; }; }; rgmii_irq_gpio39: rgmii_irq_gpio39 { pin-irq { pins = "gpio39"; function = "alt4"; }; }; rgmii_mdio_gpio28: rgmii_mdio_gpio28 { pins-mdio { pins = "gpio28", "gpio29"; function = "alt5"; }; }; rgmii_mdio_gpio37: rgmii_mdio_gpio37 { pins-mdio { pins = "gpio37", "gpio38"; function = "alt4"; }; }; spi0_gpio46: spi0_gpio46 { pins-spi { pins = "gpio46", "gpio47", "gpio48", "gpio49"; function = "alt2"; }; }; spi2_gpio46: spi2_gpio46 { pins-spi { pins = "gpio46", "gpio47", "gpio48", "gpio49", "gpio50"; function = "alt5"; }; }; spi3_gpio0: spi3_gpio0 { pins-spi { pins = "gpio0", "gpio1", "gpio2", "gpio3"; function = "alt3"; }; }; spi4_gpio4: spi4_gpio4 { pins-spi { pins = "gpio4", "gpio5", "gpio6", "gpio7"; function = "alt3"; }; }; spi5_gpio12: spi5_gpio12 { pins-spi { pins = "gpio12", "gpio13", "gpio14", "gpio15"; function = "alt3"; }; }; spi6_gpio18: spi6_gpio18 { pins-spi { pins = "gpio18", "gpio19", "gpio20", "gpio21"; function = "alt3"; }; }; uart2_gpio0: uart2_gpio0 { pin-tx { pins = "gpio0"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio1"; function = "alt4"; bias-pull-up; }; }; uart2_ctsrts_gpio2: uart2_ctsrts_gpio2 { pin-cts { pins = "gpio2"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio3"; function = "alt4"; bias-disable; }; }; uart3_gpio4: uart3_gpio4 { pin-tx { pins = "gpio4"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio5"; function = "alt4"; bias-pull-up; }; }; uart3_ctsrts_gpio6: uart3_ctsrts_gpio6 { pin-cts { pins = "gpio6"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio7"; function = "alt4"; bias-disable; }; }; uart4_gpio8: uart4_gpio8 { pin-tx { pins = "gpio8"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio9"; function = "alt4"; bias-pull-up; }; }; uart4_ctsrts_gpio10: uart4_ctsrts_gpio10 { pin-cts { pins = "gpio10"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio11"; function = "alt4"; bias-disable; }; }; uart5_gpio12: uart5_gpio12 { pin-tx { pins = "gpio12"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio13"; function = "alt4"; bias-pull-up; }; }; uart5_ctsrts_gpio14: uart5_ctsrts_gpio14 { pin-cts { pins = "gpio14"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio15"; function = "alt4"; bias-disable; }; }; }; &rmem { #address-cells = <2>; }; &cma { alloc-ranges = <0x0 0x00000000 0x40000000>; }; &i2c0 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; interrupts = <0 117 4>; }; &i2c1 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; interrupts = <0 117 4>; }; &mailbox { interrupts = <0 33 4>; }; &sdhci { interrupts = <0 126 4>; }; &sdhost { interrupts = <0 120 4>; }; &spi { interrupts = <0 118 4>; }; &spi1 { interrupts = <0 93 4>; }; &spi2 { interrupts = <0 93 4>; }; &system_timer { interrupts = <0 64 4>, <0 65 4>, <0 66 4>, <0 67 4>; }; &txp { interrupts = <0 75 4>; }; &uart0 { interrupts = <0 121 4>; }; &uart1 { interrupts = <0 93 4>; }; &usb { interrupts = <0 73 4>; }; &vec { interrupts = <0 123 4>; }; / { leds { compatible = "gpio-leds"; act { label = "ACT"; default-state = "keep"; linux,default-trigger = "heartbeat"; }; }; soc { firmware: firmware { compatible = "raspberrypi,bcm2835-firmware", "simple-mfd"; #address-cells = <1>; #size-cells = <1>; mboxes = <&mailbox>; dma-ranges; }; power: power { compatible = "raspberrypi,bcm2835-power"; firmware = <&firmware>; #power-domain-cells = <1>; }; vchiq: mailbox@7e00b840 { compatible = "brcm,bcm2835-vchiq"; reg = <0x7e00b840 0x3c>; interrupts = <0 2>; }; }; }; &gpio { pinctrl-names = "default"; gpioout: gpioout { brcm,pins = <6>; brcm,function = <1>; }; alt0: alt0 { brcm,pins = <4 5 7 8 9 10 11>; brcm,function = <4>; }; }; &i2c0 { pinctrl-names = "default"; pinctrl-0 = <&i2c0_gpio0>; status = "okay"; clock-frequency = <100000>; }; &i2c1 { pinctrl-names = "default"; pinctrl-0 = <&i2c1_gpio2>; status = "okay"; clock-frequency = <100000>; }; &usb { power-domains = <&power 6>; }; &vec { power-domains = <&power 7>; status = "okay"; }; &dsi0 { power-domains = <&power 17>; }; &dsi1 { power-domains = <&power 18>; }; &usb { dr_mode = "peripheral"; g-rx-fifo-size = <256>; g-np-tx-fifo-size = <32>; g-tx-fifo-size = <256 256 512 512 512 768 768>; }; / { compatible = "raspberrypi,4-model-b", "brcm,bcm2711"; model = "Raspberry Pi 4 Model B"; chosen { stdout-path = "serial1:115200n8"; }; memory@0 { device_type = "memory"; reg = <0 0 0>; }; aliases { emmc2bus = &emmc2bus; ethernet0 = &genet; pcie0 = &pcie0; }; leds { act { gpios = <&gpio 42 0>; }; pwr { label = "PWR"; gpios = <&expgpio 2 1>; default-state = "keep"; linux,default-trigger = "default-on"; }; }; wifi_pwrseq: wifi-pwrseq { compatible = "mmc-pwrseq-simple"; reset-gpios = <&expgpio 1 1>; }; sd_io_1v8_reg: sd_io_1v8_reg { compatible = "regulator-gpio"; regulator-name = "vdd-sd-io"; regulator-min-microvolt = <1800000>; regulator-max-microvolt = <3300000>; regulator-boot-on; regulator-always-on; regulator-settling-time-us = <5000>; gpios = <&expgpio 4 0>; states = <1800000 0x1 3300000 0x0>; status = "okay"; }; sd_vcc_reg: sd_vcc_reg { compatible = "regulator-fixed"; regulator-name = "vcc-sd"; regulator-min-microvolt = <3300000>; regulator-max-microvolt = <3300000>; regulator-boot-on; enable-active-high; gpio = <&expgpio 6 0>; }; }; &ddc0 { status = "okay"; }; &ddc1 { status = "okay"; }; &firmware { firmware_clocks: clocks { compatible = "raspberrypi,firmware-clocks"; #clock-cells = <1>; }; expgpio: gpio { compatible = "raspberrypi,firmware-gpio"; gpio-controller; #gpio-cells = <2>; gpio-line-names = "BT_ON", "WL_ON", "PWR_LED_OFF", "GLOBAL_RESET", "VDD_SD_IO_SEL", "CAM_GPIO", "SD_PWR_ON", ""; status = "okay"; }; reset: reset { compatible = "raspberrypi,firmware-reset"; #reset-cells = <1>; }; }; &gpio { gpio-line-names = "ID_SDA", "ID_SCL", "SDA1", "SCL1", "GPIO_GCLK", "GPIO5", "GPIO6", "SPI_CE1_N", "SPI_CE0_N", "SPI_MISO", "SPI_MOSI", "SPI_SCLK", "GPIO12", "GPIO13", "TXD1", "RXD1", "GPIO16", "GPIO17", "GPIO18", "GPIO19", "GPIO20", "GPIO21", "GPIO22", "GPIO23", "GPIO24", "GPIO25", "GPIO26", "GPIO27", "RGMII_MDIO", "RGMIO_MDC", "CTS0", "RTS0", "TXD0", "RXD0", "SD1_CLK", "SD1_CMD", "SD1_DATA0", "SD1_DATA1", "SD1_DATA2", "SD1_DATA3", "PWM0_MISO", "PWM1_MOSI", "STATUS_LED_G_CLK", "SPIFLASH_CE_N", "SDA0", "SCL0", "RGMII_RXCLK", "RGMII_RXCTL", "RGMII_RXD0", "RGMII_RXD1", "RGMII_RXD2", "RGMII_RXD3", "RGMII_TXCLK", "RGMII_TXCTL", "RGMII_TXD0", "RGMII_TXD1", "RGMII_TXD2", "RGMII_TXD3"; }; &hdmi0 { clocks = <&firmware_clocks 13>, <&firmware_clocks 14>, <&dvp 0>, <&clk_27MHz>; clock-names = "hdmi", "bvb", "audio", "cec"; status = "okay"; }; &hdmi1 { clocks = <&firmware_clocks 13>, <&firmware_clocks 14>, <&dvp 1>, <&clk_27MHz>; clock-names = "hdmi", "bvb", "audio", "cec"; status = "okay"; }; &hvs { clocks = <&firmware_clocks 4>; }; &pixelvalve0 { status = "okay"; }; &pixelvalve1 { status = "okay"; }; &pixelvalve2 { status = "okay"; }; &pixelvalve4 { status = "okay"; }; &pwm1 { pinctrl-names = "default"; pinctrl-0 = <&pwm1_0_gpio40 &pwm1_1_gpio41>; status = "okay"; }; &sdhci { #address-cells = <1>; #size-cells = <0>; pinctrl-names = "default"; pinctrl-0 = <&emmc_gpio34>; bus-width = <4>; non-removable; mmc-pwrseq = <&wifi_pwrseq>; status = "okay"; brcmf: wifi@1 { reg = <1>; compatible = "brcm,bcm4329-fmac"; }; }; &emmc2 { vqmmc-supply = <&sd_io_1v8_reg>; vmmc-supply = <&sd_vcc_reg>; broken-cd; status = "okay"; }; &genet { phy-handle = <&phy1>; phy-mode = "rgmii-rxid"; status = "okay"; }; &genet_mdio { phy1: ethernet-phy@1 { reg = <0x1>; }; }; &pcie0 { pci@1,0 { #address-cells = <3>; #size-cells = <2>; ranges; reg = <0 0 0 0 0>; usb@1,0 { reg = <0x10000 0 0 0 0>; resets = <&reset 0>; }; }; }; &uart0 { pinctrl-names = "default"; pinctrl-0 = <&uart0_ctsrts_gpio30 &uart0_gpio32>; uart-has-rtscts; status = "okay"; bluetooth { compatible = "brcm,bcm43438-bt"; max-speed = <2000000>; shutdown-gpios = <&expgpio 0 0>; }; }; &uart1 { pinctrl-names = "default"; pinctrl-0 = <&uart1_gpio14>; status = "okay"; }; &vchiq { interrupts = <0 34 4>; }; &vc4 { status = "okay"; }; &vec { status = "disabled"; };

3 5

Odroid-C2 help
by ogosinkem＠gmail.com 03 Nov '20

03 Nov '20

Hi, I was wondering if there were any verbose guides that explain how to setup an odroid c2 board to run sel4. As a side note, are there any tools that i could use to simulate this board if need be? Thanks, Nkem Ogosi

1 0

Simple hello for RISC-V/spike
by Porter, Jeremy 03 Nov '20

03 Nov '20

I'm trying to build a simple hello world project for RISC-V/spike. I've been through the tutorials and through the sel4test for RISC-V/spike. That project is too large for what I need. I tried following this: https://github.com/manu88/SeL4_101 and modified the CMakeLists.txt to configure as required: ### SeL4_101 CMakeLists.txt ### cmake_minimum_required(VERSION 3.7.2) #message(STATUS "Femur print " ${KernelX86Sel4Arch_all_strings}) #if (${PLATFORM} IN_LIST KernelRiscVSel4Arch_all_strings) if (${PLATFORM} IN_LIST KernelRiscVPlatform_all_strings) #if (${PLATFORM} IN_LIST ${KernelX86Sel4Arch_all_strings} ${KernelARMPlatform_all_strings} ${KernelRiscVPlatform_all_strings}) set(KernelArch riscv CACHE STRING "" FORCE) set(KernelRiscVSel4Arch riscv64 CACHE STRING "" FORCE) endif() include(tools/cmake-tool/default-CMakeLists.txt) if(SIMULATION) ApplyCommonSimulationSettings("riscv64") else() if(KernelArchX86) set(KernelIOMMU ON CACHE BOOL "" FORCE) endif() endif() # We must build the debug kernel because the tutorials rely on seL4_DebugPutChar # and they don't initialize a platsupport driver. ApplyCommonReleaseVerificationSettings(FALSE FALSE) GenerateSimulateScript() ############################################################################## When I build, I get the following error: user@user-KVM:/mnt/data/femur/build$ ninja [55/90] Building C object projects/util_libs/libplatsupport/CMakeFiles/platsupport.dir/src/plat/spike/serial.c.obj ../projects/util_libs/libplatsupport/src/plat/spike/serial.c:18:28: warning: 'struct dev_defn' declared inside parameter list will not be visible outside of this definition or declaration int uart_init(const struct dev_defn* defn, ^~~~~~~~ [73/90] Linking C executable projects/hello/hello FAILED: projects/hello/hello : && ccache /mnt/data/rocket-tools/bin/riscv64-unknown-elf-gcc --sysroot=/mnt/data/femur/build -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -g -D__KERNEL_64__ -static -nostdlib -z max-page-size=0x1000 -u _sel4_start -e _sel4_start -T /mnt/data/femur/tools/cmake-tool/tls_rootserver.lds /mnt/data/femur/build/lib/crt1.o /mnt/data/femur/build/lib/crti.o /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/rv64imac/lp64/crtbegin.o projects/hello/CMakeFiles/hello.dir/src/main.c.obj -lgcc projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/util_libs/libelf/libelf.a projects/musllibc/build-temp/lib/libc.a -lgcc projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/util_libs/libelf/libelf.a projects/musllibc/build-temp/lib/libc.a /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/rv64imac/lp64/crtend.o /mnt/data/femur/build/lib/crtn.o -o projects/hello/hello && : /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/../../../../riscv64-unknown-elf/bin/ld: projects/seL4_libs/libsel4platsupport/libsel4platsupport.a(common.c.obj): in function `vspace_map_pages': /mnt/data/femur/build/../projects/seL4_libs/libsel4vspace/include/vspace/vspace.h:492: undefined reference to `__ctzdi2' /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/../../../../riscv64-unknown-elf/bin/ld: projects/seL4_libs/libsel4platsupport/libsel4platsupport.a(common.c.obj): in function `platsupport_alloc_device_vaddr': /mnt/data/femur/build/../projects/seL4_libs/libsel4platsupport/src/common.c:83: undefined reference to `__ctzdi2' collect2: error: ld returned 1 exit status ninja: build stopped: subcommand failed. The missing symbol is in fact in the build, it shows up in kernel_all_pp.c etc. user@user-KVM:/mnt/data/femur/build$ grep -r ctzdi2 kernel/kernel_all_pp.c:uint32_t __ctzdi2(uint64_t x); kernel/kernel_all_pp.c:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all_copy.c:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all.i:uint32_t __ctzdi2(uint64_t x); kernel/kernel_all.i:uint32_t __ctzdi2(uint64_t x) Binary file kernel/kernel.elf matches kernel/kernel_all_pp_prune_wrapper_temp.c:uint32_t __ctzdi2(uint64_t x) kernel/CMakeFiles/kernel_i_wrapper_temp_lib.dir/kernel_all_copy.c.obj:uint32_t __ctzdi2(uint64_t x); kernel/CMakeFiles/kernel_i_wrapper_temp_lib.dir/kernel_all_copy.c.obj:uint32_t __ctzdi2(uint64_t x) Binary file kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj matches kernel/CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj:uint32_t __ctzdi2(uint64_t x); kernel/CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all.c:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all_pp_prune.c:uint32_t __ctzdi2(uint64_t x); kernel/kernel_all_pp_prune.c:uint32_t __ctzdi2(uint64_t x) Binary file projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/irq_server/irq_server.c.obj matches Binary file projects/seL4_libs/libsel4utils/libsel4utils.a matches Binary file projects/seL4_libs/libsel4platsupport/libsel4platsupport.a matches Binary file projects/seL4_libs/libsel4platsupport/CMakeFiles/sel4platsupport.dir/src/common.c.obj matches What am I missing here?

1 0

Docker / gnat
by dave＠synergy.org 02 Nov '20

02 Nov '20

Hello, I converted over from my old development environment to the docker-based version this weekend. Everything worked fine, except for one thing. I was using the gnat-6-aarch64-linux-gnu and gnat-6-arm-linux-gnueabihf packages to compile Ada code. Ada is not installed by default in the docker container. I can install it, but it goes away when the container terminates. I am brand new to docker. Can I make these changes permanent myself or does it require the container provider to do so? Thanks! Dave

2 2

raspberry pi 4
by Sachin More 31 Oct '20

31 Oct '20

Hi: Has anyone tried to use seL4 on a raspberry pi 4? thanks, Sachin

4 7

Re: [seL4] Devel Digest, Vol 77, Issue 11
by Chris Koziarz 30 Oct '20

30 Oct '20

Thanks Damon for your help! I've added the required "simple" attribute to the assembly configuration: assembly { composition { [...] component Client client; } configuration { [....] client.simple = true; } } But the usage generates: implicit declaration of function ‘camkes_make_simple’ and I don't know what header(s) I should include and/or any library I should link to get ‘camkes_make_simple’ decl/def. camkes_make_simple() function does not exist in any of simple camkes tutorials to figure out the required headers, while your example has too many headers to figure out what headers are really needed. Further help with it is greatly appreciated. Thanks. Chris On Thu, Oct 29, 2020 at 4:36 PM <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. seL4_BootInfo in Camkes environment (Chris Koziarz) > 2. Re: seL4_BootInfo in Camkes environment > (Lee, Damon (Data61, Kensington NSW)) > 3. Re: raspberry pi 4 (Jose A. Pascual) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Thu, 29 Oct 2020 13:39:12 +1100 > From: Chris Koziarz <chris(a)breakawayconsulting.com.au> > To: devel(a)sel4.systems > Subject: [seL4] seL4_BootInfo in Camkes environment > Message-ID: > <CAMuEnL6VH8xYxK9SR64Sc65onK7By= > 66XkiPHhgMzu4rjDgnRg(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > In a regular seL4 PD, I always have seL4_BootInfo available > via platsupport_get_bootinfo(), and all goodies that I can learn from > therein are available. > > But it appears that the camkes components (probably we should talk about > "client components", i.e. the ones with "control;" attribute and an entry > point: int run(void)), > are started as a typical root task, with a call: > void __sel4_start_root(seL4_BootInfo *boot_info) > however boot_info is passed herein as NULL. > At least boot_info appears NULL for me on ARM64. > So, is the access to seL4_BootInfo disallowed in camkes env? Or how can I > access seL4_BootInfo in camkes? > > Chris > > > ------------------------------ > > Message: 2 > Date: Thu, 29 Oct 2020 04:28:56 +0000 > From: "Lee, Damon (Data61, Kensington NSW)" > <Damon.Lee(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] seL4_BootInfo in Camkes environment > Message-ID: <tfbft5x4pve.fsf(a)coopers.keg.data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi Chris, > > > In a regular seL4 PD, I always have seL4_BootInfo available > > via platsupport_get_bootinfo(), and all goodies that I can learn > > from > > therein are available. > > > > But it appears that the camkes components (probably we should > > talk about > > "client components", i.e. the ones with "control;" attribute and > > an entry > > point: int run(void)), > > are started as a typical root task, with a call: > > void __sel4_start_root(seL4_BootInfo *boot_info) > > however boot_info is passed herein as NULL. > > At least boot_info appears NULL for me on ARM64. > > So, is the access to seL4_BootInfo disallowed in camkes env? Or > > how can I > > access seL4_BootInfo in camkes? > > The bootinfo isn't disallowed in a CAmkES environment but parts of > it > is gutted out (untyped information, IRQ control cap etc.) > depending on > the configuration of the CAmkES application. To access the > bootinfo, > you could append this configuration option for a specific > component in > the "configuration" block in the ".camkes" file of your > application: > > <component_name>.simple = true; > > The simple_t interface which abstracts the bootinfo can then be > grabbed via the 'camkes_make_simple()' function. > > There are examples of the bootinfo usage in our CAmkES VM > repositories > that you can checkout here: > > https://github.com/seL4/camkes-vm/blob/master/components/VM_Arm/src/main.c#… > > Regards, > Damon > > > ------------------------------ > > Message: 3 > Date: Thu, 29 Oct 2020 06:45:16 +0100 > From: "Jose A. Pascual" <joseantonio.pascual(a)ehu.eus> > To: Nick Spinale <Nick.Spinale(a)arm.com> > Cc: Sachin More <sachinsureshmore(a)gmail.com>, "devel(a)sel4.systems" > <devel(a)sel4.systems> > Subject: Re: [seL4] raspberry pi 4 > Message-ID: > <CAK8ti4+QiFTDnBKRfZYWQ-XXAT_= > MnTr_+jHJRfmwZQ-w6W6NA(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Hi, > We are also running seL4 on the RPI4 and we managed to run "sel4test" > passing all the tests. > Basically, you can build the sel4test project and execute all the tests > without errors as in the Rpi3. > We are using it in an OS course to build a very simple OS on top of seL4. > I'll try to open a PR in the following days. > Nick, if you don't mind, I'll compare our patch with yours to check if we > are doing everything the same way. > I'll keep you informed. > > Jose (& Mikel) > > > On Thu, Oct 29, 2020 at 1:29 AM Nick Spinale <Nick.Spinale(a)arm.com> wrote: > > > > Can I prepare, say seL4 11.0 and then apply your patches and then > > compile using seL4's build system (or your build system if it is in > public > > domain)? > > > > At the moment, I?m unable to share the rest of the code for this > > particular project. I have, however, published our Raspberry Pi 4-related > > patches to public branches of 'seL4' [1] and ?seL4_tools' [2]. These > > patches, which are the extent of our Raspberry Pi 4-related patches for > > upstream seL4 repositories, only encompasses the bootloader (?elfloader?) > > and the seL4 kernel itself. The projects that you might use for getting > > started, such as ?sel4test? [3], depend on platform support for userland > > libraries such as those found in ?seL4_libs? [4]. > > > > If you decide to add Raspberry Pi 4 support to those userland libraries, > > I?d be happy to help out with that. > > > > > > [1] https://github.com/nspin/seL4/tree/rpi4 > > [2] https://github.com/nspin/seL4_tools/tree/rpi4 > > [3] https://github.com/seL4/sel4test-manifest > > [4] https://github.com/seL4/seL4_libs > > > > > > - - - - > > Nick Spinale (nickspinale.com) > > Arm Research, Cambridge UK > > - - - - > > > > IMPORTANT NOTICE: The contents of this email and any attachments are > > confidential and may also be privileged. If you are not the intended > > recipient, please notify the sender immediately and do not disclose the > > contents to any other person, use it for any purpose, or store or copy > the > > information in any medium. Thank you. > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 77, Issue 11 > ************************************* >

2 2

seL4_BootInfo in Camkes environment
by Chris Koziarz 29 Oct '20

29 Oct '20

In a regular seL4 PD, I always have seL4_BootInfo available via platsupport_get_bootinfo(), and all goodies that I can learn from therein are available. But it appears that the camkes components (probably we should talk about "client components", i.e. the ones with "control;" attribute and an entry point: int run(void)), are started as a typical root task, with a call: void __sel4_start_root(seL4_BootInfo *boot_info) however boot_info is passed herein as NULL. At least boot_info appears NULL for me on ARM64. So, is the access to seL4_BootInfo disallowed in camkes env? Or how can I access seL4_BootInfo in camkes? Chris

2 1

seL4 on gem5
by Bodun Hu 28 Oct '20

28 Oct '20

Hello, I'm currently trying to set up seL4 inside the gem5 simulator to get some benchmark results. Are there any tutorials or instructions regarding how to set it up? Any tip will be appreciated! *Edward Hu* The University of Texas at Austin | Computer Science | Homepage: https:// <http://goog_1605193962>bodunhu.com

2 1

Adding a library to the camkes project
by Chris Koziarz 28 Oct '20

28 Oct '20

Camkes CMakefiles are quite different to the non-camkes ones that I've learned recently. For starters, I cannot figure out a simple step of adding an include path & a static library to a camkes project. For example, I want to expand projects/camkes/apps to include an extra file that calls functions from libsel4vka. Adding a source file is easy: just expand SOURCES list, e.g.: DeclareCAmkESComponent(Driver SOURCES components/Driver/src/driver.c components/Driver/src/sel4vka-caller.c) But sel4vka-caller.c needs the include paths to seL4_libs/libsel4vka/include. And the libsel4vka.a needs to be built and linked to the executable. I don't know how I can achieve it. The CMakefile original (trivial) content is: project(uart C) DeclareCAmkESComponent(Client SOURCES components/Client/src/client.c) DeclareCAmkESComponent(Driver SOURCES components/Driver/src/driver.c) DeclareCAmkESRootserver(uart.camkes) I try to add the libsel4vka.a to the linker via appending to it: target_link_libraries( uart PUBLIC sel4vka ) But I get: /usr/bin/cmake -S/home/chris/camkes_brkwy/projects/camkes -B/home/chris/camkes_brkwy/uart_tqma8xqp-build ninja: error: rebuilding 'build.ninja': subcommand failed chris@ubuntu:~/camkes_brkwy/uart_tqma8xqp-build$ ninja CMake Error at apps/uart/CMakeLists.txt:35 (target_link_libraries): Cannot specify link libraries for target "uart" which is not built by this project. I don't understand why "uart" is not a target, given the statement: project(uart C) So given target_link_libraries() fails me here, what am I doing wrong? what's the proper way of including -I paths and *.a files in Camkes-type CMakefile? Thanks for your help! Chris

2 1

3rd seL4 Summit - Tutorial
by Cedric MAIRE 24 Oct '20

24 Oct '20

Dear seL4 developers, I would be happy to get more information about the presented tutorial during the 3rd seL4 summit. What will it be about? Is this tutorial already available on the website or exclusive to the summit attendees? I looked through the given PDF (https://na.eventscloud.com/file_uploads/a236a51b4b76609e82fcc316992b73f4_20…) but didn't find any information regarding the tutorial. Best regards, Cedric Maire <html xmlns="http://www.w3.org/1999/xhtml"> <head> <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> <STYLE type="text/css">  </STYLE> </head> <body> <hr style="color: #000000;background-color: #000000;height: 1px;"/> <p>The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: <a href="http://www.icrc.org">www.icrc.org</a><p> <p>This e-mail is intended for the named recipient(s) only.<br> Its contents are confidential and may only be retained by the named recipient(s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. </p> <hr style="color: #000000;background-color: #000000;height: 1px;"/> </body> </html>

1 0