- Devel - lists.sel4.systems

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 11 Nov '19

11 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

Building seL4test x86_64 on Debian with the Docker image
by Jacob Yu 05 Nov '19

05 Nov '19

Hi I am building "seL4test" using the Docker image on Ubuntu 18.04.3 LTS, a 64-bit system. After entering "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" in a build directory within Docker it complained "Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE)". I wonder should I manually download and install protocol buffer compiler, protoc? Please advise. Thank for your help. Jacob =============================================== loading initial cache file /host/projects/sel4test/settings.cmake correct_platform_strings: Attempting to correct PLATFORM: x86_64 to new valid KernelPlatform: pc99 KernelSel4Arch: x86_64 -- Found seL4: /host/kernel -- The C compiler identification is GNU 6.5.0 -- The CXX compiler identification is GNU 6.5.0 -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /host/tools/seL4/elfloader-tool -- Found musllibc: /host/projects/musllibc -- Found util_libs: /host/projects/util_libs -- Found seL4_libs: /host/projects/seL4_libs -- Found sel4_projects_libs: /host/projects/sel4_projects_libs -- Found sel4runtime: /host/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- Found PythonInterp: /usr/bin/python (found version "2.7.15") -- Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE) -- CPIO test cpio_reproducible_flag PASSED -- Configuring done -- Generating done -- Build files have been written to: /host/build-x86

2 2

Re: [seL4] Devel Digest, Vol 65, Issue 24
by Mcleod, Kent (Data61, Kensington NSW) 04 Nov '19

04 Nov '19

> abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world > loading initial cache file ../settings.cmake > CMake Error: Error: generator : Ninja > Does not match the generator used previously: Unix Makefiles > Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. These errors indicate that CMake already believes a project has been created in the target directory and that this project was a Makefile based project. Is there any CMakeCache.txt files located anywhere in the project structure that may be causing CMake to get confused? Otherwise you could reinitialise the tutorial project and try initialising hello-world again and that would also fix your problem.

1 0

Re: [seL4] Devel Digest, Vol 65, Issue 24
by abdi mahmud haji 31 Oct '19

31 Oct '19

i am working on sel4-tutorials for the first time .i setup my machine accordingly and then when i trying to generate the tutorials like this "./init --tut hello-world" i keep getting an error message and dont know what to do or how to fix it . the error was like bellowing =================================================== abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world loading initial cache file ../settings.cmake CMake Error: Error: generator : Ninja Does not match the generator used previously: Unix Makefiles Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /home/abdi/.local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world82varrcf -C ../settings.cmake .. STDOUT: STDERR: ====================================================================== is there someone who suggests what i should do please. thanks On Sun, Oct 27, 2019 at 4:00 AM <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. Re: releasing confidentiality > (Heiser, Gernot (Data61, Kensington NSW)) > 2. Fwd: port sel4 to RK3308(quad cortex-a35) (Yun Zhou) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 26 Oct 2019 03:07:23 +0000 > From: "Heiser, Gernot (Data61, Kensington NSW)" > <Gernot.Heiser(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] releasing confidentiality > Message-ID: <5FEA58C5-9011-49B7-9790-28B4B54849EF(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > On 26 Oct 2019, at 08:00, Michael Neises <neisesmichael(a)gmail.com> wrote: > > > > 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? > > Hi Michael > > seL4’s confidentiality (and other security) enforcement means that the > kernel guarantees that you can only access objects to which you have been > given explicit permission (in the form of a capability). How those > permissions are allocated is a matter of policy, the kernel doesn’t care, > it only enforces. > > In particular, it is totally possible in seL4 to give one component access > to another component’s address space, that’s for the user-level policy > framework to decide. > > Whether the present CAmkES framework supports this is a different > question, which I’ll leave to someone who’s more up to date with CAmkES > details. > > Gernot > > > ------------------------------ > > Message: 2 > Date: Sat, 26 Oct 2019 10:35:50 +0800 > From: Yun Zhou <shiny725829(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Fwd: port sel4 to RK3308(quad cortex-a35) > Message-ID: > <CAHNKqcxb7ws3MD=- > nwJka6HKEcA4hXZipJv0vdsStetJjxP-yg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > ---------- Forwarded message --------- > 发件人： Yun Zhou <shiny725829(a)gmail.com> > Date: 2019年10月25日周五下午9:52 > Subject: port sel4 to RK3308(quad cortex-a35) > To: <devel-owner(a)sel4.systems> > > > Dear sel4 Experts > How are you > I found some information about sel4, and sel4 is great microkernel OS, i > want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal > processing. Form the Tutorials I found sel4 just support cortex-a53, I > would like to ask does sel4 support cortex-a35 SMP mode. and because our > application is real time audio processing so system delay must lower than > 3ms and hard real-time determinism. > Will sel4 support real-time signal processing? > Looking forward to your reply > > Thanks &Kind regards > Yun >

1 0

The seL4 Foundation is coming!
by Heiser, Gernot (Data61, Kensington NSW) 25 Oct '19

25 Oct '19

Re-post from announce(a)sel4.systems<mailto:announce@sel4.systems> regarding the seL4 Foundation. We’ll start recruiting members soon. Gernot Begin forwarded message: From: Announcements about seL4 -- low volume list <announce(a)sel4.systems<mailto:announce@sel4.systems>> Subject: [seL4 Announce] The seL4 Foundation is coming! Date: 25 October 2019 at 17:09:30 AEDT To: "announce(a)sel4.systems<mailto:announce@sel4.systems>" <announce(a)sel4.systems<mailto:announce@sel4.systems>> Reply-To: <announce(a)sel4.systems<mailto:announce@sel4.systems>> Dear seL4 community, With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. This was originally announced at the seL4 Summit in the US last month. I apologise for the delay in this posting (side-tracked with various issues). Gernot on behalf of the Trustworthy Systems team _______________________________________________ Announce mailing list Announce(a)sel4.systems<mailto:Announce@sel4.systems> https://sel4.systems/lists/listinfo/announce

1 0