Merge pull request #423 in SEL4/sel4 from ~HALMATARY/sel4:benchmarkRe…

…fine to master * commit 'e3f764a65be484d89e29ebc22ea406f1438ae3d3': Benchmark: move arch-dependent benchmark.c from api/ to new benchmark/ directory Benchmark: Pack arch-independent benchmark-related files into separate directories
seL4 · Oct 20, 2016 · 423f3ea · 423f3ea
2 parents 59f50c7 + e3f764a
commit 423f3ea
Show file tree

Hide file tree

Showing 35 changed files with 95 additions and 37 deletions.
diff --git a/include/api/debug.h b/include/api/debug.h
@@ -14,7 +14,7 @@
 #ifndef __API_DEBUG_H
 #define __API_DEBUG_H
 
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 #include <arch/api/syscall.h>
 #include <model/statedata.h>
 

diff --git a/include/arch/arm/arch/fastpath/fastpath.h b/include/arch/arm/arch/fastpath/fastpath.h
@@ -13,7 +13,7 @@
 
 #include <arch/linker.h>
 #include <mode/fastpath/fastpath.h>
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 #include <mode/machine/debug.h>
 
 void slowpath(syscall_t syscall) NORETURN;

diff --git a/include/arch/x86/arch/32/mode/fastpath/fastpath.h b/include/arch/x86/arch/32/mode/fastpath/fastpath.h
@@ -16,7 +16,7 @@
 #include <arch/machine/debug.h>
 #include <api/types.h>
 #include <api/syscall.h>
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 #include <mode/stack.h>
 
 static inline void

diff --git a/include/benchmark/Makefile b/include/benchmark/Makefile
@@ -0,0 +1,13 @@
+#
+# Copyright 2016, Data61
+# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+# ABN 41 687 119 230.
+#
+# This software may be distributed and modified according to the terms of
+# the GNU General Public License version 2. Note that NO WARRANTY is provided.
+# See "LICENSE_GPLv2.txt" for details.
+#
+# @TAG(D61_GPL)
+#
+
+DIRECTORIES += benchmark
diff --git a/include/benchmark.h → include/benchmark/benchmark.h b/include/benchmark.h → include/benchmark/benchmark.h
@@ -15,7 +15,7 @@
 #include <machine/io.h>
 #include <arch/api/constants.h>
 #include <arch/machine/hardware.h>
-#include <benchmark_tracepoints_types.h>
+#include <benchmark/benchmark_tracepoints_types.h>
 
 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 typedef struct {

diff --git a/include/benchmark/benchmark_tracepoints_types.h b/include/benchmark/benchmark_tracepoints_types.h
@@ -0,0 +1 @@
+../../libsel4/include/sel4/benchmark_tracepoints_types.h
diff --git a/include/benchmark_track.h → include/benchmark/benchmark_track.h b/include/benchmark_track.h → include/benchmark/benchmark_track.h
@@ -13,7 +13,7 @@
 
 #include <config.h>
 #include <arch/benchmark.h>
-#include <benchmark_track_types.h>
+#include <benchmark/benchmark_track_types.h>
 #include <arch/api/constants.h>
 #include <machine/io.h>
 #include <kernel/cspace.h>

diff --git a/include/benchmark/benchmark_track_types.h b/include/benchmark/benchmark_track_types.h
@@ -0,0 +1 @@
+../../libsel4/include/sel4/benchmark_track_types.h
diff --git a/include/benchmark_utilisation.h → include/benchmark/benchmark_utilisation.h b/include/benchmark_utilisation.h → include/benchmark/benchmark_utilisation.h
@@ -13,7 +13,7 @@
 
 #include <config.h>
 #include <arch/benchmark.h>
-#include <benchmark_utilisation_types.h>
+#include <benchmark/benchmark_utilisation_types.h>
 #include <arch/api/constants.h>
 #include <model/statedata.h>
 

diff --git a/include/benchmark/benchmark_utilisation_types.h b/include/benchmark/benchmark_utilisation_types.h
@@ -0,0 +1 @@
+../../libsel4/include/sel4/benchmark_utilisation_types.h
diff --git a/include/benchmark_tracepoints_types.h b/include/benchmark_tracepoints_types.h
diff --git a/include/benchmark_track_types.h b/include/benchmark_track_types.h
diff --git a/include/benchmark_utilisation_types.h b/include/benchmark_utilisation_types.h
diff --git a/include/object/structures.h b/include/object/structures.h
@@ -16,7 +16,7 @@
 #include <stdint.h>
 #include <arch/object/structures_gen.h>
 #include <arch/api/constants.h>
-#include <benchmark.h>
+#include <benchmark/benchmark.h>
 
 enum irq_state {
     IRQInactive  = 0,

diff --git a/src/Makefile b/src/Makefile
@@ -14,11 +14,9 @@ include ${SOURCE_ROOT}/src/kernel/Makefile
 include ${SOURCE_ROOT}/src/object/Makefile
 include ${SOURCE_ROOT}/src/model/Makefile
 include ${SOURCE_ROOT}/src/machine/Makefile
+include ${SOURCE_ROOT}/src/benchmark/Makefile
 
 C_SOURCES += src/inlines.c \
              src/assert.c \
              src/util.c \
-             src/string.c \
-             src/benchmark_track.c \
-             src/benchmark_utilisation.c
-
+             src/string.c
diff --git a/src/api/syscall.c b/src/api/syscall.c
@@ -9,10 +9,10 @@
  */
 
 #include <types.h>
-#include <benchmark.h>
+#include <benchmark/benchmark.h>
 #include <arch/benchmark.h>
-#include <benchmark_track.h>
-#include <benchmark_utilisation.h>
+#include <benchmark/benchmark_track.h>
+#include <benchmark/benchmark_utilisation.h>
 #include <api/syscall.h>
 #include <api/failures.h>
 #include <api/faults.h>

diff --git a/src/arch/arm/32/c_traps.c b/src/arch/arm/32/c_traps.c
@@ -15,8 +15,8 @@
 #include <api/syscall.h>
 #include <arch/linker.h>
 
-#include <benchmark_track.h>
-#include <benchmark_utilisation.h>
+#include <benchmark/benchmark_track.h>
+#include <benchmark/benchmark_utilisation.h>
 
 /** DONT_TRANSLATE */
 static inline void FORCE_INLINE NORETURN restore_user_context(void)

diff --git a/src/arch/arm/32/kernel/vspace.c b/src/arch/arm/32/kernel/vspace.c
@@ -10,7 +10,7 @@
 
 #include <config.h>
 #include <types.h>
-#include <benchmark.h>
+#include <benchmark/benchmark.h>
 #include <api/failures.h>
 #include <api/syscall.h>
 #include <kernel/boot.h>
@@ -32,7 +32,7 @@
 #include <arch/object/vcpu.h>
 
 #ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 #endif
 
 /* ARM uses multiple identical mappings in a page table / page directory to construct

diff --git a/src/arch/arm/Makefile b/src/arch/arm/Makefile
@@ -15,6 +15,7 @@ include ${SOURCE_ROOT}/src/arch/arm/object/Makefile
 include ${SOURCE_ROOT}/src/arch/arm/kernel/Makefile
 include ${SOURCE_ROOT}/src/arch/arm/model/Makefile
 include ${SOURCE_ROOT}/src/arch/arm/machine/Makefile
+include ${SOURCE_ROOT}/src/arch/arm/benchmark/Makefile
 include ${SOURCE_ROOT}/src/arch/arm/armv/$(ARMV)/Makefile
 
 ARCH_C_SOURCES += c_traps.c

diff --git a/src/arch/arm/api/Makefile b/src/arch/arm/api/Makefile
@@ -10,4 +10,4 @@
 
 DIRECTORIES += src/arch/arm/api
 
-ARCH_C_SOURCES += api/faults.c api/benchmark.c
+ARCH_C_SOURCES += api/faults.c
diff --git a/src/arch/arm/benchmark/Makefile b/src/arch/arm/benchmark/Makefile
@@ -0,0 +1,14 @@
+# Copyright 2016, Data61
+# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+# ABN 41 687 119 230.
+#
+# This software may be distributed and modified according to the terms of
+# the GNU General Public License version 2. Note that NO WARRANTY is provided.
+# See "LICENSE_GPLv2.txt" for details.
+#
+# @TAG(D61_GPL)
+#
+
+DIRECTORIES += src/arch/arm/benchmark
+
+ARCH_C_SOURCES += benchmark/benchmark.c
diff --git a/src/arch/arm/api/benchmark.c → src/arch/arm/benchmark/benchmark.c b/src/arch/arm/api/benchmark.c → src/arch/arm/benchmark/benchmark.c
@@ -10,7 +10,7 @@
 
 #if CONFIG_MAX_NUM_TRACE_POINTS > 0
 
-#include <benchmark.h>
+#include <benchmark/benchmark.h>
 #include <arch/benchmark.h>
 
 timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];

diff --git a/src/arch/arm/c_traps.c b/src/arch/arm/c_traps.c
@@ -14,9 +14,9 @@
 #include <arch/machine/registerset.h>
 #include <api/syscall.h>
 
-#include <benchmark_track_types.h>
-#include <benchmark_track.h>
-#include <benchmark_utilisation.h>
+#include <benchmark/benchmark_track_types.h>
+#include <benchmark/benchmark_track.h>
+#include <benchmark/benchmark_utilisation.h>
 
 /** DONT_TRANSLATE */
 void VISIBLE NORETURN

diff --git a/src/arch/x86/32/c_traps.c b/src/arch/x86/32/c_traps.c
@@ -13,7 +13,7 @@
 #include <arch/machine/fpu.h>
 #include <arch/fastpath/fastpath.h>
 #include <arch/machine/debug.h>
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 #include <mode/stack.h>
 
 #include <api/syscall.h>

diff --git a/src/arch/x86/32/kernel/vspace.c b/src/arch/x86/32/kernel/vspace.c
@@ -16,7 +16,7 @@
 #include <arch/kernel/vspace.h>
 #include <arch/kernel/boot.h>
 #include <arch/api/invocation.h>
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 
 /* 'gdt_idt_ptr' is declared globally because of a C-subset restriction.
  * It is only used in init_drts(), which therefore is non-reentrant.

diff --git a/src/arch/x86/Makefile b/src/arch/x86/Makefile
@@ -13,6 +13,7 @@ include ${SOURCE_ROOT}/src/arch/$(ARCH)/object/Makefile
 include ${SOURCE_ROOT}/src/arch/$(ARCH)/kernel/Makefile
 include ${SOURCE_ROOT}/src/arch/$(ARCH)/model/Makefile
 include ${SOURCE_ROOT}/src/arch/$(ARCH)/machine/Makefile
+include ${SOURCE_ROOT}/src/arch/$(ARCH)/benchmark/Makefile
 
 ifeq ($(__X86_32__),y)
 include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/Makefile

diff --git a/src/arch/x86/api/Makefile b/src/arch/x86/api/Makefile
@@ -10,4 +10,4 @@
 
 DIRECTORIES += src/arch/$(ARCH)/api
 
-ARCH_C_SOURCES += api/faults.c api/benchmark.c
+ARCH_C_SOURCES += api/faults.c
diff --git a/src/arch/x86/benchmark/Makefile b/src/arch/x86/benchmark/Makefile
@@ -0,0 +1,15 @@
+#
+# Copyright 2016, Data61
+# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+# ABN 41 687 119 230.
+#
+# This software may be distributed and modified according to the terms of
+# the GNU General Public License version 2. Note that NO WARRANTY is provided.
+# See "LICENSE_GPLv2.txt" for details.
+#
+# @TAG(D61_GPL)
+#
+
+DIRECTORIES += src/arch/$(ARCH)/benchmark
+
+ARCH_C_SOURCES += benchmark/benchmark.c
diff --git a/src/arch/x86/api/benchmark.c → src/arch/x86/benchmark/benchmark.c b/src/arch/x86/api/benchmark.c → src/arch/x86/benchmark/benchmark.c
@@ -10,7 +10,7 @@
 
 #if CONFIG_MAX_NUM_TRACE_POINTS > 0
 
-#include <benchmark.h>
+#include <benchmark/benchmark.h>
 #include <arch/benchmark.h>
 #include <arch/machine/hardware.h>
 

diff --git a/src/arch/x86/c_traps.c b/src/arch/x86/c_traps.c
@@ -16,8 +16,8 @@
 #include <machine/debug.h>
 #include <api/syscall.h>
 
-#include <benchmark_track.h>
-#include <benchmark_utilisation.h>
+#include <benchmark/benchmark_track.h>
+#include <benchmark/benchmark_utilisation.h>
 
 /** DONT_TRANSLATE */
 void VISIBLE

diff --git a/src/benchmark/Makefile b/src/benchmark/Makefile
@@ -0,0 +1,16 @@
+#
+# Copyright 2016, Data61
+# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+# ABN 41 687 119 230.
+#
+# This software may be distributed and modified according to the terms of
+# the GNU General Public License version 2. Note that NO WARRANTY is provided.
+# See "LICENSE_GPLv2.txt" for details.
+#
+# @TAG(D61_GPL)
+#
+
+DIRECTORIES += src/benchmark
+
+C_SOURCES += src/benchmark/benchmark_track.c
+C_SOURCES += src/benchmark/benchmark_utilisation.c
diff --git a/src/benchmark_track.c → src/benchmark/benchmark_track.c b/src/benchmark_track.c → src/benchmark/benchmark_track.c
@@ -9,7 +9,7 @@
  */
 
 #include <config.h>
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 #include <model/statedata.h>
 
 #ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES

diff --git a/src/benchmark_utilisation.c → src/benchmark/benchmark_utilisation.c b/src/benchmark_utilisation.c → src/benchmark/benchmark_utilisation.c
@@ -9,7 +9,7 @@
  */
 
 #include <config.h>
-#include <benchmark_utilisation.h>
+#include <benchmark/benchmark_utilisation.h>
 
 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 

diff --git a/src/fastpath/fastpath.c b/src/fastpath/fastpath.c
@@ -12,9 +12,9 @@
 #include <fastpath/fastpath.h>
 
 #ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 #endif
-#include <benchmark_utilisation.h>
+#include <benchmark/benchmark_utilisation.h>
 
 void
 #ifdef ARCH_X86

diff --git a/src/model/statedata.c b/src/model/statedata.c
@@ -15,7 +15,7 @@
 #include <model/statedata.h>
 #include <object/structures.h>
 #include <object/tcb.h>
-#include <benchmark_track.h>
+#include <benchmark/benchmark_track.h>
 
 /* Collective cpu states, including both pre core architecture dependant and independent data */
 SMP_STATE_DEFINE(smpStatedata_t, ksSMP[CONFIG_MAX_NUM_NODES] ALIGN(CONFIG_CACHE_LN_SZ));