1 |
|
/* space.h - Architecture dependent part of public interface to L4 threads. |
2 |
|
Copyright (C) 2003 Free Software Foundation, Inc. |
3 |
|
Written by Marcus Brinkmann <marcus@gnu.org>. |
4 |
|
|
5 |
|
This file is part of the GNU L4 library. |
6 |
|
|
7 |
|
The GNU L4 library is free software; you can redistribute it and/or |
8 |
|
modify it under the terms of the GNU Lesser General Public License |
9 |
|
as published by the Free Software Foundation; either version 2.1 of |
10 |
|
the License, or (at your option) any later version. |
11 |
|
|
12 |
|
The GNU L4 library is distributed in the hope that it will be |
13 |
|
useful, but WITHOUT ANY WARRANTY; without even the implied warranty |
14 |
|
of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
15 |
|
GNU Lesser General Public License for more details. |
16 |
|
|
17 |
|
You should have received a copy of the GNU Lesser General Public |
18 |
|
License along with the GNU L4 library; if not, write to the Free |
19 |
|
Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA |
20 |
|
02111-1307, USA. */ |
21 |
|
|
22 |
#ifndef _L4_SPACE_H |
#ifndef _L4_SPACE_H |
23 |
# error "Never use <l4/bits/space.h> directly; include <l4/space.h> instead." |
# error "Never use <l4/bits/space.h> directly; include <l4/space.h> instead." |
24 |
#endif |
#endif |
25 |
|
|
|
#ifndef _L4_EXTERN_INLINE |
|
|
#define _L4_EXTERN_INLINE extern __inline |
|
|
#endif |
|
|
|
|
26 |
|
|
27 |
/* IO Fpages. */ |
/* IO Fpages. */ |
28 |
|
|
37 |
_L4_BITFIELD_32_64 (base, 16, 48)); |
_L4_BITFIELD_32_64 (base, 16, 48)); |
38 |
})) l4_io_fpage_t; |
})) l4_io_fpage_t; |
39 |
|
|
40 |
_L4_EXTERN_INLINE l4_fpage_t |
|
41 |
|
static inline l4_fpage_t |
42 |
|
__attribute__((__always_inline__)) |
43 |
l4_io_fpage (l4_word_t base_address, int size) |
l4_io_fpage (l4_word_t base_address, int size) |
44 |
{ |
{ |
45 |
l4_fpage_t fpage; |
l4_fpage_t fpage; |
55 |
} |
} |
56 |
|
|
57 |
|
|
58 |
_L4_EXTERN_INLINE l4_fpage_t |
static inline l4_fpage_t |
59 |
|
__attribute__((__always_inline__)) |
60 |
l4_io_fpage_log2 (l4_word_t base_address, int log2_size) |
l4_io_fpage_log2 (l4_word_t base_address, int log2_size) |
61 |
{ |
{ |
62 |
l4_fpage_t fpage; |
l4_fpage_t fpage; |
76 |
#define L4_LARGE_SPACE 0 |
#define L4_LARGE_SPACE 0 |
77 |
#define L4_SMALL_SPACE (1 << 31) |
#define L4_SMALL_SPACE (1 << 31) |
78 |
|
|
79 |
|
|
80 |
/* LOC and SIZE are in MB. */ |
/* LOC and SIZE are in MB. */ |
81 |
_L4_EXTERN_INLINE l4_word_t |
static inline l4_word_t |
82 |
|
__attribute__((__always_inline__)) |
83 |
l4_small_space (l4_word_t loc, l4_word_t size) |
l4_small_space (l4_word_t loc, l4_word_t size) |
84 |
{ |
{ |
85 |
l4_word_t small_space = loc >> 1; /* Divide by 2 (MB). */ |
l4_word_t small_space = loc >> 1; /* Divide by 2 (MB). */ |