Loading...
Searching...
No Matches
vcpu.h
Go to the documentation of this file.
/*
* (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
* economic rights: Technische Universität Dresden (Germany)
*
* License: see LICENSE.spdx (in this directory or the directories above)
*/
#pragma once
#include <l4/sys/vcpu.h>
#include <l4/sys/utcb.h>
__BEGIN_DECLS
typedef void (*l4vcpu_event_hndl_t)(l4_vcpu_state_t *vcpu);
typedef void (*l4vcpu_setup_ipc_t)(l4_utcb_t *utcb);
L4_CV L4_INLINE
void
l4vcpu_irq_disable(l4_vcpu_state_t *vcpu) L4_NOTHROW;
L4_CV L4_INLINE
unsigned
l4vcpu_irq_disable_save(l4_vcpu_state_t *vcpu) L4_NOTHROW;
L4_CV L4_INLINE
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;
L4_CV L4_INLINE
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;
L4_CV L4_INLINE
void
l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
l4_timeout_t to,
l4vcpu_event_hndl_t do_event_work_cb,
l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
L4_CV L4_INLINE
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;
L4_CV void
l4vcpu_print_state(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
L4_CV void
l4vcpu_print_state_arch(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
L4_CV L4_INLINE
int
l4vcpu_is_irq_entry(l4_vcpu_state_t const *vcpu) L4_NOTHROW;
L4_CV L4_INLINE
int
l4vcpu_is_page_fault_entry(l4_vcpu_state_t const *vcpu) L4_NOTHROW;
L4_CV 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;
/* ===================================================================== */
/* Implementations */
#include <l4/sys/ipc.h>
#include <l4/vcpu/vcpu_arch.h>
L4_CV L4_INLINE
void
l4vcpu_irq_disable(l4_vcpu_state_t *vcpu) L4_NOTHROW
{
vcpu->state &= ~L4_VCPU_F_IRQ;
l4_barrier();
}
L4_CV L4_INLINE
unsigned
l4vcpu_irq_disable_save(l4_vcpu_state_t *vcpu) L4_NOTHROW
{
unsigned s = vcpu->state;
l4vcpu_irq_disable(vcpu);
return s;
}
L4_CV L4_INLINE
void
l4vcpu_wait(l4_vcpu_state_t *vcpu, l4_utcb_t *utcb,
l4_timeout_t to,
l4vcpu_event_hndl_t do_event_work_cb,
l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW
{
l4vcpu_irq_disable(vcpu);
setup_ipc(utcb);
vcpu->i.tag = l4_ipc_wait(utcb, &vcpu->i.label, to);
if (L4_LIKELY(!l4_msgtag_has_error(vcpu->i.tag)))
do_event_work_cb(vcpu);
}
L4_CV L4_INLINE
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
{
if (!(vcpu->state & L4_VCPU_F_IRQ))
{
setup_ipc(utcb);
l4_barrier();
}
while (1)
{
vcpu->state |= L4_VCPU_F_IRQ;
l4_barrier();
if (L4_LIKELY(!(vcpu->sticky_flags & L4_VCPU_SF_IRQ_PENDING)))
break;
l4vcpu_wait(vcpu, utcb, L4_IPC_BOTH_TIMEOUT_0,
do_event_work_cb, setup_ipc);
}
}
L4_CV L4_INLINE
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
{
if (s & L4_VCPU_F_IRQ)
l4vcpu_irq_enable(vcpu, utcb, do_event_work_cb, setup_ipc);
else if (vcpu->state & L4_VCPU_F_IRQ)
l4vcpu_irq_disable(vcpu);
}
L4_CV L4_INLINE
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
{
l4vcpu_wait(vcpu, utcb, L4_IPC_NEVER, do_event_work_cb, setup_ipc);
}
__END_DECLS
l4vcpu_ext_alloc
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.
l4vcpu_is_irq_entry
int l4vcpu_is_irq_entry(l4_vcpu_state_t const *vcpu) L4_NOTHROW
Return whether the entry reason was an IRQ/IPC message.
l4vcpu_irq_enable
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
l4vcpu_irq_restore
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
l4vcpu_irq_disable_save
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
l4vcpu_is_page_fault_entry
int l4vcpu_is_page_fault_entry(l4_vcpu_state_t const *vcpu) L4_NOTHROW
Return whether the entry reason was a page fault.
l4vcpu_irq_disable
void l4vcpu_irq_disable(l4_vcpu_state_t *vcpu) L4_NOTHROW
Disable a vCPU for event delivery.
Definition vcpu.h:201
l4vcpu_print_state
void l4vcpu_print_state(const l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW
Print the state of a vCPU.
l4vcpu_wait_for_event
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
l4_addr_t
unsigned long l4_addr_t
Address type.
Definition l4int.h:34
l4_cap_idx_t
unsigned long l4_cap_idx_t
Capability selector type.
Definition types.h:336
l4_ipc_wait
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
l4_msgtag_has_error
unsigned l4_msgtag_has_error(l4_msgtag_t t) L4_NOTHROW
Test for error indicator flag.
Definition types.h:440
L4_IPC_BOTH_TIMEOUT_0
#define L4_IPC_BOTH_TIMEOUT_0
0 receive and send timeout
Definition __timeout.h:79
L4_IPC_NEVER
#define L4_IPC_NEVER
never timeout
Definition __timeout.h:76
l4_utcb_t
struct l4_utcb_t l4_utcb_t
Opaque type for the UTCB.
Definition utcb.h:56
L4_VCPU_SF_IRQ_PENDING
@ 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
@ L4_VCPU_F_IRQ
Receiving of IRQs and IPC enabled.
Definition vcpu.h:114
L4_CV
#define L4_CV
Define calling convention.
Definition linkage.h:33
L4_NOTHROW
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition compiler.h:161
L4_INLINE
#define L4_INLINE
L4 Inline function attribute.
Definition compiler.h:51
l4_barrier
void l4_barrier(void)
Memory barrier.
Definition compiler.h:332
L4_LIKELY
#define L4_LIKELY(x)
Expression is likely to execute.
Definition compiler.h:283
ipc.h
Common IPC interface.
utcb.h
UTCB definitions.
l4_vcpu_state_t
State of a vCPU.
Definition vcpu.h:76
vcpu.h
vCPU API
l4_timeout_t
Timeout pair.
Definition __timeout.h:53