Hi All,

As per the suggestion, I tried running the seL4bench (https://github.com/seL4/sel4bench) but it did not work. I tried to run it as a separate project using the following commands on x86 system, ubuntu 16.04 on qemu:

mkdir sel4bench
cd sel4bench
repo init -u https://github.com/seL4/sel4bench-manifest.git
repo sync
mkdir build
cd build


Cases are
i) ../init-build.sh -DPLATFORM=sabre -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE

It produces Error1.txt

ii) ../init-build.sh -DPLATFORM=sabre -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE (*successful*)

ninja

It produces Error2.txt

iii) ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE (*successful*)

ninja

It produces the following error.

cpio: unrecognized option '--reproducible'
Try `cpio --help' or `cpio --usage' for more information.
ninja: build stopped: subcommand failed.

Can you please suggest a possible way out for running it?

--
Thanks and Regards,
Amit Goyal

On 2018-07-11 06:06, anna.ly...@data61.csiro.au wrote:
Hi Amit,

Yes, it's possible to share vka, allocman etc (if they are in the
same address space you can make them global and use them - although
beware, these libraries are not thread safe). Between processes you
can set up new allocators, I recommend you take a look at the
sel4bench project [1] which passes the timer to each new benchmark
process.

However, it depends on what you want. If you just want to be able to
read the time and get timeouts, you don't want to share the timer
itself (its a device) but expose a timer service either through a
library, or RPC if it is between processes. I'll note this down as an
example we should build into future tutorials, but you can start by
using the timer manager [2].

Good luck!

Anna.

[1] https://github.com/seL4/sel4bench

[2]https://github.com/seL4/util_libs/blob/9784983ec4038236ba53dd090c57e27ee499dfb9/libplatsupport/include/platsupport/time_manager.h
________________________________________
From: Amit Goyal <amitgo...@cse.iitb.ac.in>
Sent: Wednesday, 11 July 2018 12:31 AM
To: Lyons, Anna (Data61, Kensington NSW)
Cc: devel@sel4.systems; chrisdennebe...@gmail.com
Subject: Re: [seL4] seL4 - getting the execution time of different threads

Hi Anna,

Thanks for your reply. I was going through this email chain. I
understand the 3 techniques that you told. I was wondering about this
particular question of Chris: "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. Is it possible to share the timer or
create new ones in the other threads?"

Can you please suggest is it possible to share or create a new timer in the other thread? Creating a timer in the other thread will require vka,
allocman etc. This boils down to, if it is possible to share vka,
allocman etc. with the other thread or create new ones in the other
thread. If yes, how can we do that?

--
Thanks and Regards,
Amit Goyal


On 2018-07-10 06:55, anna.ly...@data61.csiro.au wrote:
Hi Chris,


It depends on your use case. If you are looking to monitor the
execution times of threads for debugging and/or benchmarking
purposes,
you can use our kernel benchmarking support, detailed here [1].


Otherwise, you could consider using the mcs branch of the kernel,
which allows you to obtain the execution time of a thread via the
seL4_SchedContext_Consumed invocation [2].


If you need to use the master branch of the kernel, then you would
need to intercept the scheduler on thread switch, by running a high
priority thread which enables other threads.


Cheers

Anna.


[1] https://docs.sel4.systems/BenchmarkingGuide.html#cpu-utilisation

[2] https://github.com/seL4/seL4/releases/tag/9.0.0-mcs?

________________________________
From: Devel <devel-bounces@sel4.systems> on behalf of Mr. Peace
<chrisdennebe...@gmail.com>
Sent: Monday, 9 July 2018 3:34 AM
To: devel@sel4.systems
Subject: [seL4] seL4 - getting the execution time of different
threads

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

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
-- The C compiler identification is unknown
-- The CXX compiler identification is unknown
CMake Error in CMakeLists.txt:
 The CMAKE_C_COMPILER:

   arm-linux-gnueabi-gcc

 is not a full path and was not found in the PATH.

 Tell CMake where to find the compiler by setting either the environment
 variable "CC" or the CMake cache entry CMAKE_C_COMPILER to the full path to
 the compiler, or to the compiler name if it is in the PATH.


CMake Error in CMakeLists.txt:
 The CMAKE_CXX_COMPILER:

   arm-linux-gnueabi-g++

 is not a full path and was not found in the PATH.

 Tell CMake where to find the compiler by setting either the environment
 variable "CXX" or the CMake cache entry CMAKE_CXX_COMPILER to the full path
 to the compiler, or to the compiler name if it is in the PATH.


-- Configuring incomplete, errors occurred!
See also "/home/usds/Documents/sel4bench/build/CMakeFiles/CMakeOutput.log".
See also "/home/usds/Documents/sel4bench/build/CMakeFiles/CMakeError.log"

[1/255] Generate invocation header gen_headers/arch/api/invocation.h
[2/255] Generate invocation header gen_headers/arch/api/sel4_invocation.h
[3/255] Generate invocation header gen_headers/api/invocation.h
[4/255] Generate syscall invocations
[5/255] Generate dummy headers for prune compilation
[6/255] Concatenating C files
[7/255] Generating linker.lds_pp
FAILED: cd /home/usds/Documents/sel4bench/build/elfloader-tool && /usr/bin/gcc 
-march=armv7-a -marm -D__KERNEL_32__ 
-I/home/usds/Documents/sel4bench/build/autoconf 
-I/home/usds/Documents/sel4bench/build/kernel/gen_config 
-I/home/usds/Documents/sel4bench/build/elfloader-tool/gen_config 
-I/home/usds/Documents/sel4bench/build/libsel4/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/projects_libs/libusbdrivers/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4vka/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4utils/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4platsupport/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4serialserver/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4debug/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4test/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4muslcsys/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/seL4_libs/libsel4vmm/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/fault/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/hardware/gen_config
 -I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/ipc/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/irq/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/irquser/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/page_mapping/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/scheduler/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/signal/gen_config
 -I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/smp/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/sync/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/sel4bench/apps/sel4bench/gen_config
 -I/home/usds/Documents/sel4bench/build/projects/util_libs/libutils/gen_config 
-I/home/usds/Documents/sel4bench/build/projects/util_libs/libplatsupport/gen_config
 
-I/home/usds/Documents/sel4bench/build/projects/util_libs/libethdrivers/gen_config
 -P -E -o linker.lds_pp -x c 
/home/usds/Documents/sel4bench/tools/seL4/elfloader-tool/src/arch-arm/linker.lds
gcc: error: unrecognized command line option ‘-marm’
ninja: build stopped: subcommand failed.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to