- Devel - lists.sel4.systems

CAmkES 3.5.0 Build Error
by Amit Goyal 27 Jul '18

27 Jul '18

Hi, I am running CAmkES 3.5.0 on Ubuntu 16.04, 64 Bit, i5 machine, CMake 3.11.4. I am getting the following error on running ../init --plat pc99 --tut hello-camkes-1 --solution (although seL4 10.0.0 works perfectly fine). ------------------------------------------------------------------------------------------------------------------------------- Traceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 58, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python2.7/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL=hello-camkes-1 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- The C compiler identification is GNU 5.3.1 -- The CXX compiler identification is GNU 5.3.1 -- 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 -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FA... (295 more, please see e.stdout) STDERR: CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) CMake Error at tools/camkes/camkes.cmake:581 (message): Failed to generate camkes-gen.cmake: Traceback (most recent call last): File "/usr/lib/python2.7/runpy.py", line 174, in _run_module_as_main "__main__", fname, loader, pkg_name) File "/usr/lib/python2.7/runpy.py", line 72, in _run_code exec code in run_globals File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/tools/camkes/camkes/runner/__main__.py", lin... (614 more, please see e.stderr) -------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a way around? -- Thanks and Regards, Amit Goyal

2 2

Question about wrapper files
by Holm, Elinor M 26 Jul '18

26 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are they for testing, or something else? Elinor Holm

1 0

Image lies outside of usable physical memory v2
by Jeremy Fields 26 Jul '18

26 Jul '18

http://sel4.systems/pipermail/devel/2016-July/000918.html I'm running into the same issue, with likely the same cause. I wanted to see if there is any further insight that can be given on this? I'm guessing there hasn't been any updates to seL4's memory allocation in this aspect. (I'm using seL4 9.0.1) My naive attempt of commenting out that particular check in seL4 just results in the machine hard resetting when it runs (if only it were that easy). >Unfortunately I cannot say that we will get around to fixing this in a particularly timely manner. (2016) Any chance this is on a roadmap? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Implementing a Filesystem on CAmkES
by Grant Jurgensen 25 Jul '18

25 Jul '18

Hello all, I was hoping to get some advice on how to implement a filesystem on my CAmkES project. For now I'm targeting FAT32, but that is flexible. So far, my plan is to port the libsdhcdriver to my platform (which shouldn't be too bad. I'm targeting exynos5, and I see exynos4 is already supported). After that, I assume I'm on my own when it comes to creating a filesystem interface. Perhaps there is an existing library for this that can hook into any standard SD controller implementation? Finally, is there an easy way to integrate said filesystem into musllibc such that one could use the standard open/read/write/close functions? Does this sound like the best way to go, or am I missing a simpler solution? Thanks, Grant

3 2

Re: [seL4] Understanding how SEL4 recognises UART on board
by Sathya Narayanan N 19 Jul '18

19 Jul '18

Hi Experts, I am curious to know how SEL4 recognises the existence of UART on the board and mapped to a particular memory address. I see there is no DTB/ DTS files read from memory. could someone help me understand the concept here ? Or is it something hardcoded in the kernel ? -- regards, Sathya

2 1

RISC-V - sel4test and sel4bench running on SiFive's Unleashed Platform
by Hesham Almatary 18 Jul '18

18 Jul '18

Hi everyone, I pushed my local seL4/RISC-V work to GitHub which contains the following new features: * A new option to run seL4 in machine mode. * A port of seL4 to QEMU's SiFiveU and virt platforms. * DTB parsing in seL4 to read and use UARTs when available. * Ported seL4 to run on VC707 FPGA Freedom Unleashed platform. * Initial Benchmarking support in seL4. * Initial sel4bench port that can measure IPC and trap timing. Link for more details: http://heshamelmatary.blogspot.com/2018/07/new-sel4test-and-sel4bench-relea… -- Hesham

1 0

Porting sel4 on RISCV architecture
by Sathya Narayanan N 16 Jul '18

16 Jul '18

Hi Experts, This is Sathya from IIT Madras. We are working on porting SEL4 on RISCV architecture running on FPGA. We have ported linux on the FPGA. I have some doubts regarding OS porting. I am stuck at the end. Before my actual query, let me tell my platform. Hardware - 64 bit RISCV design running on FPGA. It doesn't support compressed instn and multiarch. Operating system - SEL4, repo synced from latest official repository. Tools - Latest synched from RISCV official repo. Query - I simulated sel4test on spike and then I am trying to port it on FPGA. We have UART to be mapped to 0x11400 address location. I set scan->reg to this value. I understood, incase of simulation, the DTB argument passed to init_first_hart function comes from spike simulator (file - sim.cc). Now, for FPGA I want to pass the DTB value to the init_first_hart() function. I am planning to write a DTS file and somehow read the data from DTS file here. I am trying to know, what is the right method to do for SEL4 ? Can you please let me understand, how you went ahead for SEL4 ? Is there any changes, I have to do in the repo code ? any readings would you suggest to proceed ahead ? -- regards, Sathya

3 4

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 13 Jul '18

13 Jul '18

Thanks again for the reply. I was looking for the foolproof way to write safe C code, but seems like the best way to go forward is to carefully design and code. Your advice is helpful to me. On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > >> Clang does have a static analyzer builtin that can be help in some > cases. That being said, the best way forward is for you as a developer to > understand the types of code that can lead to problems and not rely > entirely on a static analyzer. > > >>> >>> >

1 0

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 13 Jul '18

13 Jul '18

Thanks a lot for the reply. What is your opinion on static checking tool and safe subset of C? Does that help? On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > Hello Wean, > > It is certainly possible to learn how to program in C without spending any > money; all it requires is a basic toolchain and a willingness to learn. > don't sell yourself short by hinting that you might be "stupid" (you almost > certainly aren't). > > In order to get started with C I suggest setting up an environment to > experiment in; for that look into installing LLVM/Clang ( > http://releases.llvm.org/) there are pre-built binaries for most major > operating systems. Once that is done all you need is a text editor (Notepad > on Windows or one of the other many free options) and some patience. As for > tutorials and resources, some options are: > > - Searching on Google for "c tutorial"; one result that looks interesting > is http://www.learn-c.org/. > - Finding an open source project that interests you and trying to > understand the code then implement a change. > - While not free, may people swear by the K&R book as a great resource to > start. > > In terms of writing code that is free of undefined behaviour and > vulnerabilities your best bet is to learn what code constructs cause those > to occur and how to avoid them. A great book for this is The Art of > Software Security Assessment by Mark Dowd, there is a PDF of Chapter 6 (C > Language Issues) available at https://trailofbits.github.io/ > ctf/vulnerabilities/references/Dowd_ch06.pdf. > > Learning about C, undefined behaviour, and vulnerabilities doesn't happen > overnight so be patient and enjoy the journey. > > --Dean > > > >

1 0

Help ! Simulating SEL4 with Zero testcases running
by Sathya Narayanan N 13 Jul '18

13 Jul '18

Hi Experts, I am running sel4 simulation on spike. I want to disable test cases from running. I tried setting default value "" from ".*" in Kconfig file. Is this enough ? Or is something else to be done ? -- regards, Sathya

2 2