00001
00007
00008
00009
00010
00011
00012 #ifndef __L4UTIL__INCLUDE__ARCH_X86__THREAD_TIME_H__
00013 #define __L4UTIL__INCLUDE__ARCH_X86__THREAD_TIME_H__
00014
00015 #include <l4/sys/compiler.h>
00016 #include <l4/sys/kernel.h>
00017 #include <l4/sys/types.h>
00018
00019 #include <l4/util/rdtsc.h>
00020
00021 EXTERN_C_BEGIN
00022
00031 L4_INLINE l4_cpu_time_t l4util_thread_time(const l4_kernel_info_t * kinfo);
00032 L4_INLINE l4_cpu_time_t l4util_thread_time(const l4_kernel_info_t * kinfo)
00033 {
00034 l4_cpu_time_t switch_time, thread_time, now;
00035
00036 do
00037 {
00038 now = l4_rdtsc();
00039
00040 thread_time = kinfo->thread_time;
00041 switch_time = kinfo->switch_time;
00042 }
00043 while (now < switch_time);
00044
00045 return now - switch_time + thread_time;
00046 }
00047
00048 EXTERN_C_END
00049
00050
00051 #endif