src/include/kernel/types.h


1
2
3
4
5
6
7
8
9
10
11
12
13

#ifndef __KERNEL_TYPES_H
#define __KNERLE_TYPES_H

#include <stdint.h>

typedef uint16_t 	tid_t;	// This is 16-bit for the VMM mapping of 
				// stacks.  See VmmManager.
struct task_t;

typedef uint64_t	cpuid_t;
struct cpu_t;

#endif