November 2019 - Devel - lists.sel4.systems

compile camkes_arm_vm project(tx1 vm_minimal), The file format is not correct
by yadong.li 22 Nov '19

22 Nov '19

Hi I compile camkes_arm_vm with tx1 vm_minimal Command: ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 Buf output file is not elf # aarch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized see appendix for the log Thank you very much Log: 1、配置环境 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 loading initial cache file /home/yadong.li/seL4/camkes_arm_vm/projects/vm/settings.cmake correct_platform_strings: Based on toolchain, setting KernelSel4Arch: aarch64 -- Found seL4: /home/yadong.li/seL4/camkes_arm_vm/kernel …………. -- Found camkes-arm-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/vm -- Found camkes-tool: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-tool -- Found global-components: /home/yadong.li/seL4/camkes_arm_vm/projects/global-components -- Found camkes-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm -- Found camkes-vm-images: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm-images -- Found sel4_projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_projects_libs -- Found elfloader-tool: /home/yadong.li/seL4/camkes_arm_vm/tools/seL4/elfloader-tool -- Found musllibc: /home/yadong.li/seL4/camkes_arm_vm/projects/musllibc -- Found util_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/util_libs -- Found seL4_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_libs -- Found projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/projects_libs -- Found capdl: /home/yadong.li/seL4/camkes_arm_vm/projects/capdl -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found sel4runtime: /home/yadong.li/seL4/camkes_arm_vm/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/ast.pickle is out of date. Regenerating... -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/camkes-gen.cmake is out of date. Regenerating... -- Configuring done -- Generating done -- Build files have been written to: /home/yadong.li/seL4/camkes_arm_vm/build_temp 2、编译 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ninja [41/320] Performing CAmkES generation for 15 files [58/320] Generating capDL-tool/parse-capDL stack build --fast Building all executables for `capDL-tool' once. After a successful build of all of them, only specified executables will be rebuilt. capDL-tool-1.0.0.1: configure (exe) Configuring capDL-tool-1.0.0.1... capDL-tool-1.0.0.1: build (exe) Preprocessing executable 'parse-capDL' for capDL-tool-1.0.0.1... [ 1 of 16] Compiling CapDL.Model ( CapDL/Model.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Model.o ) [ 2 of 16] Compiling CapDL.State ( CapDL/State.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/State.o ) [ 3 of 16] Compiling CapDL.PrintUtils ( CapDL/PrintUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintUtils.o ) [ 4 of 16] Compiling CapDL.PrintC ( CapDL/PrintC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintC.o ) [ 5 of 16] Compiling CapDL.PrintDot ( CapDL/PrintDot.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintDot.o ) [ 6 of 16] Compiling CapDL.PrintIsabelle ( CapDL/PrintIsabelle.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintIsabelle.o ) [ 7 of 16] Compiling CapDL.PrintModel ( CapDL/PrintModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintModel.o ) [ 8 of 16] Compiling CapDL.PrintXml ( CapDL/PrintXml.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintXml.o ) [ 9 of 16] Compiling CapDL.Matrix ( CapDL/Matrix.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Matrix.o ) [10 of 16] Compiling CapDL.STCC ( CapDL/STCC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/STCC.o ) [11 of 16] Compiling CapDL.AST ( CapDL/AST.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/AST.o ) [12 of 16] Compiling CapDL.MakeModel ( CapDL/MakeModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/MakeModel.o ) [13 of 16] Compiling CapDL.ParserUtils ( CapDL/ParserUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/ParserUtils.o ) [14 of 16] Compiling CapDL.DumpParser ( CapDL/DumpParser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/DumpParser.o ) [15 of 16] Compiling CapDL.Parser ( CapDL/Parser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Parser.o ) [16 of 16] Compiling Main ( Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/Main.o ) Linking .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL ... capDL-tool-1.0.0.1: copy/register Installing executable(s) in /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin stack install Copying from /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin/parse-capDL to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/parse-capDL Copied executables to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool: - parse-capDL Warning: Installation path /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool not found on the PATH environment variable. [68/320] Building C object CMakeFiles/vm0.instance.bin.dir/components/VM/src/main.c.obj ………………….. musllibc/build-temp/stage/include/inttypes.h:133:27: note: format string is defined here #define PRIuPTR __PRIPTR "u" [320/320] Generating images/capdl-loader-image-arm-tx1 #file images/capdl-loader-image-arm-tx1 images/capdl-loader-image-arm-tx1: data #arch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized

2 1

Camkes and GPIO
by Parvaneh Ahgajani 21 Nov '19

21 Nov '19

Hello all, I am trying to implement a simple demo on sel4 using camkes. I need to add some external hardware like sensors to my demo. For this purpose I need GPIO programming. Could you please point me to some example GPIO components? Should I add hardware component? or just use <platsupport.GPIO.h> to write signal on pins on source files? Thank you for your time and consideration, Parveneh.

2 5

releasing confidentiality
by Michael Neises 15 Nov '19

15 Nov '19

Hi, I know that seL4 provides confidentiality, which is described as a property that "means that data cannot be read without permission." Given this wording, I wonder if it is not possible to revoke those permissions in certain cases. In particular, I would like for one camkes component to be able to perform runtime measurements, such as heap analysis, on another component. Or even better, I would like for a component to be able to perform runtime measurements on a program running within the camkes linux vm. Is such a feat possible? Best, Michael Neises

3 2

Fwd: camkes vm question
by Michael Neises 15 Nov '19

15 Nov '19

Hello, In my system, sel4 is loaded by u-boot from an sd card that contains only an ELF image. I would like to store some sensitive data in plaintext for use in a non-vm component, but I worry that it can be read from the ELF image. Can this sd card data be accessed from within a linux vm instance? Or otherwise, is it certain that the vm cannot access this data? Best, Michael Neises

2 2

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Re: [seL4] RISC-V port
by Zhuang, Siwei (Data61, Kensington NSW) 14 Nov '19

14 Nov '19

It looks like either you're using the libarchive in python2 or the package is outdated. Try something like, pip3 install libarchive --upgrade You may need to remove the libarchive from python2, although seL4test requires both python2 and 3. Regards, Siwei On Wed, 2019-11-13 at 20:26 -0800, Jacob Yu wrote: > Thanks, Siwei. > > After I have done a clean build (by removing previous installation in > "/opt/riscv"), I am able to enable "multilib" when building > "riscv-gnu-toolchain" successfully. I also found out that I needed to > build Newlib. > > I can now run " ../init-build.sh -DPLATFORM=spike -DRISCV64=TRUE > -DSIMULATION=1" in the build directory under seL4Test but still failed in > ninja: > > [1/20] Generating gen_headers/image_start_addr.h > FAILED: elfloader/gen_headers/image_start_addr.h > cd /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader && sh -c > "/home/webuser/Dev/l4/l4dev/seL4test/tools/seL4/elfloader-tool/../cmake- > tool/helpers/shoehorn.py > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/kernel/gen_headers/plat/machine/p > latform_gen.yaml > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader/archive.o > > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader/gen_headers//image_star > t_addr.h" > Traceback (most recent call last): > File > "/home/webuser/Dev/l4/l4dev/seL4test/tools/seL4/elfloader-tool/../cmake- > tool/helpers/shoehorn.py", > line 81, in <module> > def get_bytes(entry: libarchive.entry.ArchiveEntry) -> io.BytesIO: > AttributeError: module 'libarchive' has no attribute 'entry' > ninja: build stopped: subcommand failed. > > Thank again for all the help. > > Regards, > > > Jacob > > On Tue, Nov 12, 2019 at 4:37 PM Zhuang, Siwei (Data61, Kensington NSW) < > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > Hi Jacob, > > > > Never had this problem before, so just a blind guess. > > > > As you can build "riscv-pk", you must be using the cross compiler from > > your > > previous build(with multilib disabled). Try removing the previous > > installation in "/opt/riscv", and also do "make clean" to remove all the > > previous build directories. > > > > I noticed that the log you attached says "Checking whether the C compiler > > works ... no", have a look at "config.log" to see if there's any useful > > info. > > > > Also make sure you have enough disk space, my build takes 21GB. > > > > Regards, > > Siwei > > > > On Tue, 2019-11-12 at 11:31 -0800, Jacob Yu wrote: > > > Hi > > > > > > I am able to install & build "riscv-pk" and "riscv-isa-sim", and then > > > try > > > out Spike. Many thank! > > > > > > > ./configure --prefix=/opt/riscv --enable-multilib > > > > sudo make linux > > > Otherwise, I also tried to enable "multilib" when building > > > "riscv-gnu-toolchain" but with no luck. It complained: > > > > > > > ... > > > > configure: error: in > > > `/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/riscv64-unknown-linux-gnu/lib32/ilp32/libgomp': > > > > configure: error: C compiler cannot create executables > > > > > > And make failed with: > > > > > > > Makefile:13703: recipe for target 'configure-target-libgomp' failed > > > > make[2]: *** [configure-target-libgomp] Error 1 > > > > > > Again, any suggestions? > > > > > > Regards, > > > > > > > > > Jacob > > > ============================================================ > > > ... > > > checking for riscv64-unknown-linux-gnu-gcc... > > > /home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/./gcc/xgcc > > > > > -B/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > stage2/./gcc/ > > > -B/opt/riscv/riscv64-unknown-linux-gnu/bin/ > > > -B/opt/riscv/riscv64-unknown-linux-gnu/lib/ -isystem > > > /opt/riscv/riscv64-unknown-linux-gnu/include -isystem > > > /opt/riscv/riscv64-unknown-linux-gnu/sys-include -march=rv32imac > > > -mabi=ilp32 > > > > > > > > > > > > *checking whether the C compiler works... noconfigure: error: in > > > `/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/riscv64-unknown-linux-gnu/lib32/ilp32/libgomp':configure: > > > error: C compiler cannot create executablesSee `config.log' for more > > > details* > > > > > > *Makefile:13703: recipe for target 'configure-target-libgomp' > > > failedmake[2]: *** [configure-target-libgomp] Error 1* > > > make[2]: Leaving directory > > > '/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux-stage2' > > > Makefile:951: recipe for target 'all' failed > > > make[1]: *** [all] Error 2 > > > make[1]: Leaving directory > > > '/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux-stage2' > > > Makefile:304: recipe for target 'stamps/build-gcc-linux-stage2' failed > > > make: *** [stamps/build-gcc-linux-stage2] Error 2 > > > > > > On Mon, Nov 11, 2019 at 5:52 PM Zhuang, Siwei (Data61, Kensington NSW) < > > > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > > > > > No, building riscv-isa-sim alone is sufficient if you only need Spike. > > > > > > > > seL4 also generates a script called "simulate" in the your build > > > > directory. > > > > The script invokes qemu for simulation. > > > > > > > > Regards, > > > > Siwei > > > > > > > > On Mon, 2019-11-11 at 17:20 -0800, Jacob Yu wrote: > > > > > Thanks, Siwei for the info. I'll give it a try. > > > > > > > > > > > Running seL4 no longer requires RISC-V tools. In case you want to > > use > > > > > Spike, > > > > > > I'd suggest building the riscv-isa-sim separately to get the > > > > > > latest > > > > code. > > > > > Does this require RISC-V tools to build? > > > > > > > > > > Best, > > > > > > > > > > > > > > > Jacob > > > > > > > > > > On Sun, Nov 10, 2019 at 10:58 PM Zhuang, Siwei (Data61, Kensington > > NSW) > > > > > < > > > > > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > > > > > > > > > Hi Jacob, > > > > > > > > > > > > You need to enable multilib when building "riscv-gnu-toolchain". > > > > > > > > > > > > ./configure --prefix=/path-to-install-toolchain > > --enable-multilib > > > > > > then > > > > > > make or make linux > > > > > > > > > > > > Running seL4 no longer requires RISC-V tools. In case you want to > > use > > > > > > Spike, > > > > > > I'd suggest building the riscv-isa-sim separately to get the > > > > > > latest > > > > code. > > > > > > Regards, > > > > > > Siwei > > > > > > > > > > > > On Sun, 2019-11-10 at 15:50 -0800, Jacob Yu wrote: > > > > > > > Hi > > > > > > > > > > > > > > I am trying to build "seL4 tests" for "Spike" platform (the > > RISC-V > > > > > > > simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit > > system. > > > > > > > First of all, I was able to build RISC-V tools with "build.sh" > > after > > > > > > > manually installing "riscv-gnu-toolchain" from GitHub as well as > > > > > > additional > > > > > > > python modules (future, ply, protobuf). I then kicked of > > > > > > "../init-build.sh > > > > > > > -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build > > > > > > directory. > > > > > > > After that, however, "ninja" command complained about "undefined > > > > > > reference > > > > > > > to `__nedf2'". I understand there is no FPU support in "Spike" > > > > platform > > > > > > so > > > > > > > a need for "soft-float" module. Where should I specify > > "-lsoft-fp"? > > > > > > > Any suggestions? > > > > > > > > > > > > > > Thanks, > > > > > > > > > > > > > > > > > > > > > Jacob > > > > > > > _______________________________________________ > > > > > > > Devel mailing list > > > > > > > Devel(a)sel4.systems > > > > > > > https://sel4.systems/lists/listinfo/devel

2 1

RISC-V port
by Jacob Yu 13 Nov '19

13 Nov '19

Hi I am trying to build "seL4 tests" for "Spike" platform (the RISC-V simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit system. First of all, I was able to build RISC-V tools with "build.sh" after manually installing "riscv-gnu-toolchain" from GitHub as well as additional python modules (future, ply, protobuf). I then kicked of "../init-build.sh -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build directory. After that, however, "ninja" command complained about "undefined reference to `__nedf2'". I understand there is no FPU support in "Spike" platform so a need for "soft-float" module. Where should I specify "-lsoft-fp"? Any suggestions? Thanks, Jacob

2 5

Re: [seL4] RISC-V port
by Jesse Millwood 12 Nov '19

12 Nov '19

I do believe you can use SiFive's toolchain: https://static.dev.sifive.com/dev-tools/riscv64-unknown-elf-gcc-8.3.0-2019.… Then you don't have to compile it. There is also Data61's Docker https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles If you look at the make file there are some targets for including the RISC-V toolchain. Jesse On 2019-11-11 1:58 a.m., Zhuang, Siwei (Data61, Kensington NSW) wrote: > Hi Jacob, > > You need to enable multilib when building "riscv-gnu-toolchain". > > ./configure --prefix=/path-to-install-toolchain --enable-multilib > then > make or make linux > > Running seL4 no longer requires RISC-V tools. In case you want to use Spike, > I'd suggest building the riscv-isa-sim separately to get the latest code. > > Regards, > Siwei > > On Sun, 2019-11-10 at 15:50 -0800, Jacob Yu wrote: >> Hi >> >> I am trying to build "seL4 tests" for "Spike" platform (the RISC-V >> simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit system. >> >> First of all, I was able to build RISC-V tools with "build.sh" after >> manually installing "riscv-gnu-toolchain" from GitHub as well as additional >> python modules (future, ply, protobuf). I then kicked of "../init-build.sh >> -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build directory. >> >> After that, however, "ninja" command complained about "undefined reference >> to `__nedf2'". I understand there is no FPU support in "Spike" platform so >> a need for "soft-float" module. Where should I specify "-lsoft-fp"? >> >> Any suggestions? >> >> Thanks, >> >> >> Jacob >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

Rust ports on Genode/seL4
by guo minskey 11 Nov '19

11 Nov '19

Hi, guys, I am trying to build genode/sel4 on x86_64 platform and expect to get a GUI working. And so I enable this option in my build.conf : REPOSITORIES += $(GENODE_DIR)/repos/libports. Seems that rust support is broken (because rustc version ??). Which version of rustc should I use to build rust ports on genode ? Or how can I disable rust ports in build.conf configuration or somewhere else ? thanks, -Minskey

3 3

a letter for seeking help about sel4
by 李庚 08 Nov '19

08 Nov '19

Dear Sir or Madam, Very Sorry to brother you. We have get into trouble after compiling sel4 following the https://docs.sel4.systems/Docker.html,may I seek some advice from you? First,I attmpt to follow the https://docs.sel4.systems/Hardware/VMware/,however,error "Failed to allocate object of size xxxx" ara discovered in serial_output.txt . Second,we wanna to make a sel4 startup disk for x86_64,is there any useful Document ? Sorry again for this sudden interruption and I would be very grateful if receive your reply. Yours Sinerely, Andrew

2 1