L4Re Operating System Framework
Interface and Usage Documentation
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 * License: see LICENSE.spdx (in this directory or the directories above)
6 */
11#pragma once
12
13#include <l4/sys/vcpu.h>
14#include <l4/sys/utcb.h>
15
17
33typedef void (*l4vcpu_event_hndl_t)(l4_vcpu_state_t *vcpu);
34typedef void (*l4vcpu_setup_ipc_t)(l4_utcb_t *utcb);
35
43void
45
55unsigned
57
71void
73 l4vcpu_event_hndl_t do_event_work_cb,
74 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
75
91void
92l4vcpu_irq_restore(l4_vcpu_state_t *vcpu, unsigned s,
93 l4_utcb_t *utcb,
94 l4vcpu_event_hndl_t do_event_work_cb,
95 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
96
111void
112l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
113 l4_timeout_t to,
114 l4vcpu_event_hndl_t do_event_work_cb,
115 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
116
131void
133 l4vcpu_event_hndl_t do_event_work_cb,
134 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
135
136
144L4_CV void
145l4vcpu_print_state(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
146
150L4_CV void
151l4vcpu_print_state_arch(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
152
153
163int
165
175int
177
189L4_CV int
192
193/* ===================================================================== */
194/* Implementations */
195
196#include <l4/sys/ipc.h>
197#include <l4/vcpu/vcpu_arch.h>
198
200void
202{
203 vcpu->state &= ~L4_VCPU_F_IRQ;
204 l4_barrier();
205}
206
208unsigned
210{
211 unsigned s = vcpu->state;
212 l4vcpu_irq_disable(vcpu);
213 return s;
214}
215
217void
218l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
219 l4_timeout_t to,
220 l4vcpu_event_hndl_t do_event_work_cb,
221 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
222{
223 l4vcpu_irq_disable(vcpu);
224 setup_ipc(utcb);
225 vcpu->i.tag = l4_ipc_wait(utcb, &vcpu->i.label, to);
226 if (L4_LIKELY(!l4_msgtag_has_error(vcpu->i.tag)))
227 do_event_work_cb(vcpu);
228}
229
231void
233 l4vcpu_event_hndl_t do_event_work_cb,
234 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
235{
236 if (!(vcpu->state & L4_VCPU_F_IRQ))
237 {
238 setup_ipc(utcb);
239 l4_barrier();
240 }
241
242 while (1)
243 {
244 vcpu->state |= L4_VCPU_F_IRQ;
245 l4_barrier();
246
247 if (L4_LIKELY(!(vcpu->sticky_flags & L4_VCPU_SF_IRQ_PENDING)))
248 break;
249
250 l4vcpu_wait(vcpu, utcb, L4_IPC_BOTH_TIMEOUT_0,
251 do_event_work_cb, setup_ipc);
252 }
253}
254
256void
258 l4_utcb_t *utcb,
259 l4vcpu_event_hndl_t do_event_work_cb,
260 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
261{
262 if (s & L4_VCPU_F_IRQ)
263 l4vcpu_irq_enable(vcpu, utcb, do_event_work_cb, setup_ipc);
264 else if (vcpu->state & L4_VCPU_F_IRQ)
265 l4vcpu_irq_disable(vcpu);
266}
267
269void
271 l4vcpu_event_hndl_t do_event_work_cb,
272 l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
273{
274 l4vcpu_wait(vcpu, utcb, L4_IPC_NEVER, do_event_work_cb, setup_ipc);
275}
276
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:232
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:257
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:209
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:201
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:270
unsigned long l4_addr_t
Address type.
Definition l4int.h:34
unsigned long l4_cap_idx_t
Capability selector type.
Definition types.h:335
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:593
unsigned l4_msgtag_has_error(l4_msgtag_t t) L4_NOTHROW
Test for error indicator flag.
Definition types.h:439
#define L4_IPC_BOTH_TIMEOUT_0
0 receive and send timeout
Definition __timeout.h:79
#define L4_IPC_NEVER
never timeout
Definition __timeout.h:76
struct l4_utcb_t l4_utcb_t
Opaque type for the UTCB.
Definition utcb.h:56
@ 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:171
@ L4_VCPU_F_IRQ
Receiving of IRQs and IPC enabled.
Definition vcpu.h:114
#define __END_DECLS
End section with C types and functions.
Definition compiler.h:167
#define L4_CV
Define calling convention.
Definition linkage.h:33
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition compiler.h:159
#define L4_INLINE
L4 Inline function attribute.
Definition compiler.h:51
void l4_barrier(void)
Memory barrier.
Definition compiler.h:323
#define __BEGIN_DECLS
Start section with C types and functions.
Definition compiler.h:164
#define L4_LIKELY(x)
Expression is likely to execute.
Definition compiler.h:274
State of a vCPU.
Definition vcpu.h:76
vCPU API
Timeout pair.
Definition __timeout.h:53