Hello together,
I was wondering how you do get the execution time in seL4 if you are using
multiple threads.
In the initial thread I can use the timer as it is shown in the tutorial
about timers since I do have the bootinfo, vka, allocman and so on.
But how do I use the timer to measure the execution time of the other
threads without stopping their execution to "pull" the time from the
initial thread? Is it possible to share the timer or create new ones in the
other threads? Or is there another way to measure the execution time?
Some background information:
The threads have different VSpace's and CSpace's.
Used tutorials: seL4-tutorial 4, seL4-tutorial timer.
The other threads do not have a bootinfo in their environment.
Kind regards,
Chris
Hello.
I'm a poor person looking for an advice.
I know this is the right place since all of you have huge expertise in
formal verification.
I'm not a smart person (maybe I'm stupid), but I'm interested in open
source contribution using C language.
Is there any solution to write C code free from undefined behavior and
vulnerability without paying for any tools?
Dear Sir/Lady,
This is a student from china, I am very interested in the sel4, works on
the camkes, When I first compile the project camkes, I met a problem:
camkes.c:502: undefined reference to `component_control_main'
I know this means it not implemented this function, but this function seems
produced by a auto method, so could you tell how to solve this problem?
I follow the command:
https://docs.sel4.systems/CAmkES/
to compile the :
repo init -u https://github.com/seL4/camkes-manifest.git
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 there for testing, or something else?
Elinor Holm
Software Engineer
781-410-5221
This message and/or attachments may include information subject to GDC4S S.P. 1.8.6 and GD Corporate Policy 07-105 and are intended to be accessed only by authorized recipients. Use, storage and transmission are governed by General Dynamics and its policies. Contractual restrictions apply to third parties. Recipients should refer to the policies or contract to determine proper handling. Unauthorized review, use, disclosure or distribution is prohibited. If you are not an intended recipient, please contact the sender and destroy all copies of the original message.
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
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
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.
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
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
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