#include "tpl_os_kernel.h"          /* tpl_schedule */
#include "tpl_os_timeobj_kernel.h"  /* tpl_counter_tick */
#include "tpl_machine_interface.h"  /* tpl_switch_context_from_it */

#define OS_START_SEC_CODE
#include "tpl_memmap.h"
FUNC(tpl_bool, OS_CODE) tpl_call_counter_tick()
{
%
foreach counter in HARDWARECOUNTERS do
%  tpl_counter_tick(&% !counter::NAME %_counter_desc);
%
end foreach
if OS::NUMBER_OF_CORES == 1 then
%
  if (tpl_kern.need_schedule)
  {
    tpl_schedule_from_running();
    LOCAL_SWITCH_CONTEXT(0)
  }
%
else
%
  GET_CURRENT_CORE_ID(core_id)
  tpl_multi_schedule();
  tpl_dispatch_context_switch();
  LOCAL_SWITCH_CONTEXT(core_id)
%
end if
%
  return TRUE;
}

#define OS_STOP_SEC_CODE
#include "tpl_memmap.h"