L4Re Operating System Framework
Interface and Usage Documentation
Loading...
Searching...
No Matches
vcpu.h
Go to the documentation of this file.
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 */
22#pragma once
23
24#include <l4/sys/vcpu.h>
25#include <l4/sys/utcb.h>
26
28
44typedef void (*l4vcpu_event_hndl_t)(l4_vcpu_state_t *vcpu);
45typedef void (*l4vcpu_setup_ipc_t)(l4_utcb_t *utcb);
46
54void
56
66unsigned
68
82void
84 l4vcpu_event_hndl_t do_event_work_cb,
85 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
86
102void
103l4vcpu_irq_restore(l4_vcpu_state_t *vcpu, unsigned s,
104 l4_utcb_t *utcb,
105 l4vcpu_event_hndl_t do_event_work_cb,
106 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
107
122void
123l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
124 l4_timeout_t to,
125 l4vcpu_event_hndl_t do_event_work_cb,
126 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
127
142void
144 l4vcpu_event_hndl_t do_event_work_cb,
145 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
146
147
155L4_CV void
156l4vcpu_print_state(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
157
161L4_CV void
162l4vcpu_print_state_arch(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
163
164
174int
176
186int
188
200L4_CV int
203
204/* ===================================================================== */
205/* Implementations */
206
207#include <l4/sys/ipc.h>
208#include <l4/vcpu/vcpu_arch.h>
209
211void
213{
214 vcpu->state &= ~L4_VCPU_F_IRQ;
215 l4_barrier();
216}
217
219unsigned
221{
222 unsigned s = vcpu->state;
223 l4vcpu_irq_disable(vcpu);
224 return s;
225}
226
228void
229l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
230 l4_timeout_t to,
231 l4vcpu_event_hndl_t do_event_work_cb,
232 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
233{
234 l4vcpu_irq_disable(vcpu);
235 setup_ipc(utcb);
236 vcpu->i.tag = l4_ipc_wait(utcb, &vcpu->i.label, to);
237 if (L4_LIKELY(!l4_msgtag_has_error(vcpu->i.tag)))
238 do_event_work_cb(vcpu);
239}
240
242void
244 l4vcpu_event_hndl_t do_event_work_cb,
245 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
246{
247 if (!(vcpu->state & L4_VCPU_F_IRQ))
248 {
249 setup_ipc(utcb);
250 l4_barrier();
251 }
252
253 while (1)
254 {
255 vcpu->state |= L4_VCPU_F_IRQ;
256 l4_barrier();
257
258 if (L4_LIKELY(!(vcpu->sticky_flags & L4_VCPU_SF_IRQ_PENDING)))
259 break;
260
261 l4vcpu_wait(vcpu, utcb, L4_IPC_BOTH_TIMEOUT_0,
262 do_event_work_cb, setup_ipc);
263 }
264}
265
267void
269 l4_utcb_t *utcb,
270 l4vcpu_event_hndl_t do_event_work_cb,
271 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
272{
273 if (s & L4_VCPU_F_IRQ)
274 l4vcpu_irq_enable(vcpu, utcb, do_event_work_cb, setup_ipc);
275 else if (vcpu->state & L4_VCPU_F_IRQ)
276 l4vcpu_irq_disable(vcpu);
277}
278
280void
282 l4vcpu_event_hndl_t do_event_work_cb,
283 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
284{
285 l4vcpu_wait(vcpu, utcb, L4_IPC_NEVER, do_event_work_cb, setup_ipc);
286}
287
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.
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:243
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:268
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:220
int l4vcpu_is_page_fault_entry(l4_vcpu_state_t const *vcpu) L4_NOTHROW
Return whether the entry reason was a page fault.
void l4vcpu_irq_disable(l4_vcpu_state_t *vcpu) L4_NOTHROW
Disable a vCPU for event delivery.
Definition vcpu.h:212
void l4vcpu_print_state(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW
Print the state of a vCPU.
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:281
unsigned long l4_addr_t
Address type.
Definition l4int.h:45
unsigned long l4_cap_idx_t
Capability selector type.
Definition types.h:359
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:604
unsigned l4_msgtag_has_error(l4_msgtag_t t) L4_NOTHROW
Test for error indicator flag.
Definition types.h:457
#define L4_IPC_BOTH_TIMEOUT_0
0 receive and send timeout
Definition __timeout.h:87
#define L4_IPC_NEVER
never timeout
Definition __timeout.h:84
struct l4_utcb_t l4_utcb_t
Opaque type for the UTCB.
Definition utcb.h:67
@ L4_VCPU_SF_IRQ_PENDING
An event is pending: Either an IRQ or another thread attempts to send an IPC to this vCPU thread.
Definition vcpu.h:182
@ L4_VCPU_F_IRQ
Receiving of IRQs and IPC enabled.
Definition vcpu.h:125
#define __END_DECLS
End section with C types and functions.
Definition compiler.h:199
#define L4_CV
Define calling convention.
Definition linkage.h:44
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition compiler.h:188
#define L4_INLINE
L4 Inline function attribute.
Definition compiler.h:62
void l4_barrier(void)
Memory barrier.
Definition compiler.h:344
#define __BEGIN_DECLS
Start section with C types and functions.
Definition compiler.h:196
#define L4_LIKELY(x)
Expression is likely to execute.
Definition compiler.h:295
State of a vCPU.
Definition vcpu.h:87
vCPU API
Timeout pair.
Definition __timeout.h:61