L4Re - L4 Runtime Environment
vcpu.h
1 /*
2  * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
3  * economic rights: Technische Universit├Ąt Dresden (Germany)
4  *
5  * This file is part of TUD:OS and distributed under the terms of the
6  * GNU General Public License 2.
7  * Please see the COPYING-GPL-2 file for details.
8  *
9  * As a special exception, you may use this file as part of a free software
10  * library without restriction. Specifically, if other files instantiate
11  * templates or use macros or inline functions from this file, or you compile
12  * this file and link it with other files to produce an executable, this
13  * file does not by itself cause the resulting executable to be covered by
14  * the GNU General Public License. This exception does not however
15  * invalidate any other reasons why the executable file might be covered by
16  * the GNU General Public License.
17  */
18 #pragma once
19 
20 #include <l4/sys/vcpu.h>
21 #include <l4/sys/utcb.h>
22 
23 __BEGIN_DECLS
24 
40 typedef void (*l4vcpu_event_hndl_t)(l4_vcpu_state_t *vcpu);
41 typedef void (*l4vcpu_setup_ipc_t)(l4_utcb_t *utcb);
42 
49 L4_CV L4_INLINE
50 void
52 
61 L4_CV L4_INLINE
62 unsigned
64 
77 L4_CV L4_INLINE
78 void
80  l4vcpu_event_hndl_t do_event_work_cb,
81  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
82 
97 L4_CV L4_INLINE
98 void
99 l4vcpu_irq_restore(l4_vcpu_state_t *vcpu, unsigned s,
100  l4_utcb_t *utcb,
101  l4vcpu_event_hndl_t do_event_work_cb,
102  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
103 
117 L4_CV L4_INLINE
118 void
119 l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
120  l4_timeout_t to,
121  l4vcpu_event_hndl_t do_event_work_cb,
122  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
123 
137 L4_CV L4_INLINE
138 void
140  l4vcpu_event_hndl_t do_event_work_cb,
141  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
142 
143 
151 L4_CV void
152 l4vcpu_print_state(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
153 
157 L4_CV void
158 l4vcpu_print_state_arch(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
159 
160 
169 L4_CV L4_INLINE
170 int
172 
181 L4_CV L4_INLINE
182 int
184 
196 L4_CV int
197 l4vcpu_ext_alloc(l4_vcpu_state_t **vcpu, l4_addr_t *ext_state,
198  l4_cap_idx_t task, l4_cap_idx_t regmgr) L4_NOTHROW;
199 
200 /* ===================================================================== */
201 /* Implementations */
202 
203 #include <l4/sys/ipc.h>
204 #include <l4/vcpu/vcpu_arch.h>
205 
206 L4_CV L4_INLINE
207 void
209 {
210  vcpu->state &= ~L4_VCPU_F_IRQ;
211  l4_barrier();
212 }
213 
214 L4_CV L4_INLINE
215 unsigned
217 {
218  unsigned s = vcpu->state;
219  l4vcpu_irq_disable(vcpu);
220  return s;
221 }
222 
223 L4_CV L4_INLINE
224 void
225 l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
226  l4_timeout_t to,
227  l4vcpu_event_hndl_t do_event_work_cb,
228  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
229 {
230  l4vcpu_irq_disable(vcpu);
231  setup_ipc(utcb);
232  vcpu->i.tag = l4_ipc_wait(utcb, &vcpu->i.label, to);
233  if (L4_LIKELY(!l4_msgtag_has_error(vcpu->i.tag)))
234  do_event_work_cb(vcpu);
235 }
236 
237 L4_CV L4_INLINE
238 void
240  l4vcpu_event_hndl_t do_event_work_cb,
241  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
242 {
243  if (!(vcpu->state & L4_VCPU_F_IRQ))
244  {
245  setup_ipc(utcb);
246  l4_barrier();
247  }
248 
249  while (1)
250  {
251  vcpu->state |= L4_VCPU_F_IRQ;
252  l4_barrier();
253 
255  break;
256 
257  l4vcpu_wait(vcpu, utcb, L4_IPC_BOTH_TIMEOUT_0,
258  do_event_work_cb, setup_ipc);
259  }
260 }
261 
262 L4_CV L4_INLINE
263 void
265  l4_utcb_t *utcb,
266  l4vcpu_event_hndl_t do_event_work_cb,
267  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
268 {
269  if (s & L4_VCPU_F_IRQ)
270  l4vcpu_irq_enable(vcpu, utcb, do_event_work_cb, setup_ipc);
271  else if (vcpu->state & L4_VCPU_F_IRQ)
272  l4vcpu_irq_disable(vcpu);
273 }
274 
275 L4_CV L4_INLINE
276 void
278  l4vcpu_event_hndl_t do_event_work_cb,
279  l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
280 {
281  l4vcpu_wait(vcpu, utcb, L4_IPC_NEVER, do_event_work_cb, setup_ipc);
282 }
283 
State of a vCPU.
Definition: vcpu.h:34
int l4vcpu_ext_alloc(l4_vcpu_state_t **vcpu, l4_addr_t *ext_state, l4_cap_idx_t task, l4_cap_idx_t regmgr) L4_NOTHROW
Allocate state area for an extended vCPU.
unsigned l4_msgtag_has_error(l4_msgtag_t t) L4_NOTHROW
Test for error indicator flag.
Definition: types.h:436
l4_vcpu_ipc_regs_t i
IPC state.
Definition: vcpu.h:39
void l4vcpu_print_state(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW
Print the state of a vCPU.
unsigned long l4_cap_idx_t
L4 Capability selector Type.
Definition: types.h:342
#define __END_DECLS
End section with C types and functions.
Definition: compiler.h:193
struct l4_utcb_t l4_utcb_t
Opaque type for the UTCB.
Definition: utcb.h:67
#define L4_IPC_NEVER
never timeout
Definition: __timeout.h:80
Timeout pair.
Definition: __timeout.h:57
void l4vcpu_irq_disable(l4_vcpu_state_t *vcpu) L4_NOTHROW
Disable a vCPU for event delivery.
Definition: vcpu.h:208
int l4vcpu_is_irq_entry(l4_vcpu_state_t const *vcpu) L4_NOTHROW
Return whether the entry reason was an IRQ/IPC message.
void l4vcpu_irq_enable(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb, l4vcpu_event_hndl_t do_event_work_cb, l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
Enable a vCPU for event delivery.
Definition: vcpu.h:239
l4_uint16_t state
Current vCPU state.
Definition: vcpu.h:41
An event (e.g. IRQ) is pending.
Definition: vcpu.h:74
#define L4_CV
Define calling convention.
Definition: linkage.h:44
void l4vcpu_irq_restore(l4_vcpu_state_t *vcpu, unsigned s, l4_utcb_t *utcb, l4vcpu_event_hndl_t do_event_work_cb, l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
Restore a previously saved IRQ/event state.
Definition: vcpu.h:264
#define L4_LIKELY(x)
Expression is likely to execute.
Definition: compiler.h:233
void l4vcpu_wait_for_event(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb, l4vcpu_event_hndl_t do_event_work_cb, l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
Wait for event.
Definition: vcpu.h:277
void l4_barrier(void)
Memory barrier.
Definition: compiler.h:269
l4_msgtag_t l4_ipc_wait(l4_utcb_t *utcb, l4_umword_t *label, l4_timeout_t timeout) L4_NOTHROW
Wait for an incoming message from any possible sender.
Definition: ipc.h:478
IRQs (events) enabled.
Definition: vcpu.h:60
unsigned long l4_addr_t
Address type.
Definition: l4int.h:45
unsigned l4vcpu_irq_disable_save(l4_vcpu_state_t *vcpu) L4_NOTHROW
Disable a vCPU for event delivery and return previous state.
Definition: vcpu.h:216
int l4vcpu_is_page_fault_entry(l4_vcpu_state_t const *vcpu) L4_NOTHROW
Return whether the entry reason was a page fault.
l4_uint16_t sticky_flags
Pending flags.
Definition: vcpu.h:43
#define L4_IPC_BOTH_TIMEOUT_0
0 receive and send timeout
Definition: __timeout.h:83
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition: compiler.h:185