FOC/L4RE: Upstream revision 40

l4/pkg/libvcpu/Control

@@ -0,0 +1,3 @@
+provides: libvcpu
+requires: l4re-util libc
+maintainer: adam@os.inf.tu-dresden.de

l4/pkg/libvcpu/Makefile

@@ -0,0 +1,4 @@
+PKGDIR		= .
+L4DIR		?= $(PKGDIR)/../..
+
+include $(L4DIR)/mk/subdir.mk

l4/pkg/libvcpu/doc/files.cfg

@@ -0,0 +1 @@
+INPUT += l4/vcpu

l4/pkg/libvcpu/include/ARCH-amd64/vcpu_arch.h

@@ -0,0 +1,32 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+#pragma once
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_irq_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return vcpu->r.trapno == 0xfe;
+}
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_page_fault_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return vcpu->r.trapno == 0xe;
+}

l4/pkg/libvcpu/include/ARCH-arm/vcpu_arch.h

@@ -0,0 +1,32 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+#pragma once
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_irq_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return vcpu->r.err == 0x00600000;
+}
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_page_fault_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return vcpu->r.err & 0x00010000;
+}

l4/pkg/libvcpu/include/ARCH-ppc32/vcpu_arch.h

@@ -0,0 +1,36 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+#pragma once
+
+#warning This file needs to be implemented.
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_irq_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  (void)vcpu;
+  return 0; // TBD
+}
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_page_fault_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  (void)vcpu;
+  return 0; // TBD
+}

l4/pkg/libvcpu/include/ARCH-sparc/vcpu_arch.h

@@ -0,0 +1,32 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+#pragma once
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_irq_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return 0; // tbd
+}
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_page_fault_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return 0; // tbd
+}

l4/pkg/libvcpu/include/ARCH-x86/vcpu_arch.h

@@ -0,0 +1,32 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+#pragma once
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_irq_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return vcpu->r.trapno == 0xfe;
+}
+
+L4_CV L4_INLINE
+int
+l4vcpu_is_page_fault_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  return vcpu->r.trapno == 0xe;
+}

l4/pkg/libvcpu/include/Makefile

@@ -0,0 +1,7 @@
+PKGDIR        =	..
+L4DIR        ?=	$(PKGDIR)/../..
+
+PKGNAME       = vcpu
+EXTRA_TARGET += vcpu
+
+include $(L4DIR)/mk/include.mk

l4/pkg/libvcpu/include/vcpu

@@ -0,0 +1,271 @@
+// vi:se ft=cpp:
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+
+#pragma once
+
+#include <l4/re/env>
+#include <l4/vcpu/vcpu.h>
+
+namespace L4vcpu {
+
+/**
+ * \brief C++ implementation of state word in the vCPU area
+ * \ingroup api_libvcpu
+ */
+class State
+{
+public:
+  State() {}
+
+  /**
+   * \brief Initialize state.
+   *
+   * \param v Initial state.
+   */
+  explicit State(l4vcpu_state_t v) : _s(v) {}
+
+  /**
+   * \brief Add flags.
+   *
+   * \param bits Bits to add to the word.
+   */
+  void add(unsigned bits) throw()    { _s |= bits; }
+
+  /**
+   * \brief Clear flags.
+   *
+   * \param bits Bits to clear in the word.
+   */
+  void clear(unsigned bits) throw()  { _s &= ~bits; }
+
+  /**
+   * \brief Set flags.
+   *
+   * \param v Set the word to the value of v.
+   */
+  void set(l4vcpu_state_t v) throw() { _s = v; }
+
+private:
+  l4vcpu_state_t _s;
+};
+
+/**
+ * \brief C++ implementation of the vCPU save state area
+ * \ingroup api_libvcpu
+ */
+class Vcpu : private l4_vcpu_state_t
+{
+public:
+  /**
+   * \brief IRQ status type.
+   */
+  typedef l4vcpu_irq_state_t Irq_state;
+
+  /**
+   * \brief Disable the vCPU for event delivery.
+   */
+  void irq_disable() throw()
+  { l4vcpu_irq_disable(this); }
+
+  /**
+   * \brief Disable the vCPU for event delivery and return previous state.
+   * \return IRQ state before disabling IRQs.
+   */
+  Irq_state irq_disable_save() throw()
+  { return l4vcpu_irq_disable_save(this); }
+
+  /**
+   * \brief Get state word
+   * \return Pointer to state word in the vCPU
+   */
+  State *state() throw()
+  { return reinterpret_cast<State *>(&(l4_vcpu_state_t::state)); }
+
+  /**
+   * \brief Get state word
+   * \return Pointer to state word in the vCPU
+   */
+  State state() const throw()
+  { return static_cast<State>(l4_vcpu_state_t::state); }
+
+  /**
+   * \brief Get saved_state word
+   * \return Pointer to saved_state word in the vCPU
+   */
+  State *saved_state() throw()
+  { return reinterpret_cast<State *>(&(l4_vcpu_state_t::saved_state)); }
+
+  /**
+   * \brief Get saved_state word
+   * \return Pointer to saved_state word in the vCPU
+   */
+  State saved_state() const throw()
+  { return static_cast<State>(l4_vcpu_state_t::saved_state); }
+
+  /**
+   * \brief Enable the vCPU for event delivery.
+   *
+   * \param utcb             The UTCB to use.
+   * \param do_event_work_cb Call-back function that is called in case an
+   *                         event (such as an interrupt) is pending.
+   * \param setup_ipc        Call-back function that is called before an
+   *                         IPC operation is called.
+   */
+  void irq_enable(l4_utcb_t *utcb, l4vcpu_event_hndl_t do_event_work_cb,
+                  l4vcpu_setup_ipc_t setup_ipc) throw()
+  { l4vcpu_irq_enable(this, utcb, do_event_work_cb, setup_ipc); }
+
+  /**
+   * \brief Restore a previously saved IRQ/event state.
+   *
+   * \param s                IRQ state to be restored.
+   * \param utcb             The UTCB to use.
+   * \param do_event_work_cb Call-back function that is called in case an
+   *                         event (such as an interrupt) is pending.
+   * \param setup_ipc        Call-back function that is called before an
+   *                         IPC operation is called.
+   */
+  void irq_restore(Irq_state s, l4_utcb_t *utcb,
+                   l4vcpu_event_hndl_t do_event_work_cb,
+                   l4vcpu_setup_ipc_t setup_ipc) throw()
+  { l4vcpu_irq_restore(this, s, utcb, do_event_work_cb, setup_ipc); }
+
+  /**
+   * \brief Halt/block the vCPU.
+   *
+   * \param utcb             The UTCB to use.
+   * \param do_event_work_cb Call-back function that is called in case an
+   *                         event (such as an interrupt) is pending.
+   * \param setup_ipc        Call-back function that is called before an
+   *                         IPC operation is called.
+   */
+  void halt(l4_utcb_t *utcb, l4vcpu_event_hndl_t do_event_work_cb,
+            l4vcpu_setup_ipc_t setup_ipc) throw()
+  { l4vcpu_halt(this, utcb, do_event_work_cb, setup_ipc); }
+
+  /**
+   * \brief Set the task of the vCPU.
+   * \param task Task to set, defaults to invalid task.
+   */
+  void task(L4::Cap<L4::Task> const task = L4::Cap<L4::Task>::Invalid) throw()
+  { user_task = task.cap(); }
+
+  /**
+   * \brief Return whether the entry reason was a page fault.
+   * return 0 if not, !=0 otherwise.
+   */
+  int is_page_fault_entry()
+  { return l4vcpu_is_page_fault_entry(this); }
+
+  /**
+   * \brief Return whether the entry reason was an IRQ/IPC message.
+   * return 0 if not, !=0 otherwise.
+   */
+  int is_irq_entry()
+  { return l4vcpu_is_irq_entry(this); }
+
+  /**
+   * \brief Return pointer to register state.
+   * \return Pointer to register state.
+   */
+  l4_vcpu_regs_t *r() throw()
+  { return &(l4_vcpu_state_t::r); }
+
+  /**
+   * \brief Return pointer to register state.
+   * \return Pointer to register state.
+   */
+  l4_vcpu_regs_t const *r() const throw()
+  { return &(l4_vcpu_state_t::r); }
+
+  /**
+   * \brief Return pointer to IPC state.
+   * \return Pointer to IPC state.
+   */
+  l4_vcpu_ipc_regs_t *i() throw()
+  { return &(l4_vcpu_state_t::i); }
+
+  /**
+   * \brief Return pointer to IPC state.
+   * \return Pointer to IPC state.
+   */
+  l4_vcpu_ipc_regs_t const *i() const throw()
+  { return &(l4_vcpu_state_t::i); }
+
+  /**
+   * \brief Set vCPU entry stack pointer.
+   * \param sp  Stack pointer address to set.
+   *
+   * \note The value is only used when entering from a user-task.
+   */
+  void entry_sp(l4_umword_t sp)
+  { l4_vcpu_state_t::entry_sp = sp; }
+
+  /**
+   * \brief Set vCPU entry instruction pointer.
+   * \param ip  Instruction pointer address to set.
+   */
+  void entry_ip(l4_umword_t ip)
+  { l4_vcpu_state_t::entry_ip = ip; }
+
+  /**
+   * \brief Allocate state area for an extented vCPU.
+   *
+   * \retval vcpu      Allocated vcpu-state area.
+   * \retval ext_state Allocated extended vcpu-state area.
+   * \param  task      Task to use for allocation, defaults to own task.
+   * \param  rm        Region manager to use for allocation defaults to standard region manager.
+   *
+   * \return 0 for success, error code otherwise
+   */
+  L4_CV static int
+  ext_alloc(Vcpu **vcpu,
+            l4_addr_t *ext_state,
+            L4::Cap<L4::Task> task = L4Re::Env::env()->task(),
+            L4::Cap<L4Re::Rm> rm = L4Re::Env::env()->rm()) throw();
+
+  /**
+   * \brief Cast a void ponter to a class pointer.
+   *
+   * \param x Pointer.
+   *
+   * \return Pointer to Vcpu class.
+   */
+  static inline Vcpu *cast(void *x) throw()
+  { return reinterpret_cast<Vcpu *>(x); }
+
+  /**
+   * \brief Cast an address to a class pointer.
+   *
+   * \param x Pointer.
+   *
+   * \return Pointer to Vcpu class.
+   */
+  static inline Vcpu *cast(l4_addr_t x) throw()
+  { return reinterpret_cast<Vcpu *>(x); }
+
+  /**
+   * \brief Print the state of the vCPU.
+   */
+  void print_state(const char *prefix = "") throw()
+  { l4vcpu_print_state(this, prefix); }
+};
+
+
+}

l4/pkg/libvcpu/include/vcpu.h

@@ -0,0 +1,301 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+#pragma once
+
+#include <l4/sys/vcpu.h>
+#include <l4/sys/utcb.h>
+
+__BEGIN_DECLS
+
+/**
+ * \defgroup api_libvcpu vCPU Support Library
+ * \brief vCPU handling functionality.
+ *
+ * This library provides convenience functionality on top of the l4sys vCPU
+ * interface to ease programming. It wraps commonly used code and abstracts
+ * architecture depends parts as far as reasonable.
+ */
+
+/**
+ * \defgroup api_libvcpu_ext Extended vCPU support
+ * \ingroup api_libvcpu
+ * \brief extended vCPU handling functionality.
+ */
+
+/**
+ * \brief IRQ/Event enable and disable flags.
+ * \ingroup api_libvcpu
+ */
+typedef enum l4vcpu_irq_state_t
+{
+  L4VCPU_IRQ_STATE_DISABLED = 0,             ///< IRQ/Event delivery disabled
+  L4VCPU_IRQ_STATE_ENABLED  = L4_VCPU_F_IRQ, ///< IRQ/Event delivery enabled
+} l4vcpu_irq_state_t;
+
+typedef l4_umword_t l4vcpu_state_t;
+typedef void (*l4vcpu_event_hndl_t)(l4_vcpu_state_t *vcpu);
+typedef void (*l4vcpu_setup_ipc_t)(l4_utcb_t *utcb);
+
+/**
+ * \brief Return the state flags of a vCPU.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu  Pointer to vCPU area.
+ */
+L4_CV L4_INLINE
+l4vcpu_state_t
+l4vcpu_state(l4_vcpu_state_t const *vcpu) L4_NOTHROW;
+
+/**
+ * \brief Disable a vCPU for event delivery.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu  Pointer to vCPU area.
+ */
+L4_CV L4_INLINE
+void
+l4vcpu_irq_disable(l4_vcpu_state_t *vcpu) L4_NOTHROW;
+
+/**
+ * \brief Disable a vCPU for event delivery and return previous state.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu  Pointer to vCPU area.
+ *
+ * \return IRQ state before disabling IRQs.
+ */
+L4_CV L4_INLINE
+l4vcpu_irq_state_t
+l4vcpu_irq_disable_save(l4_vcpu_state_t *vcpu) L4_NOTHROW;
+
+/**
+ * \brief Enable a vCPU for event delivery.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu             Pointer to vCPU area.
+ * \param utcb             Utcb pointer of the calling vCPU.
+ * \param do_event_work_cb Call-back function that is called in case an
+ *                         event (such as an interrupt) is pending.
+ * \param setup_ipc        Function call-back that is called right before
+ *                         any IPC operation.
+ */
+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;
+
+/**
+ * \brief Restore a previously saved IRQ/event state.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu             Pointer to vCPU area.
+ * \param s                IRQ state to be restored.
+ * \param utcb             Utcb pointer of the calling vCPU.
+ * \param do_event_work_cb Call-back function that is called in case an
+ *                         event (such as an interrupt) is pending after
+ *                         enabling.
+ * \param setup_ipc        Function call-back that is called right before
+ *                         any IPC operation.
+ */
+L4_CV L4_INLINE
+void
+l4vcpu_irq_restore(l4_vcpu_state_t *vcpu, l4vcpu_irq_state_t s,
+                   l4_utcb_t *utcb,
+                   l4vcpu_event_hndl_t do_event_work_cb,
+                   l4vcpu_setup_ipc_t setup_ipc) L4_NOTHROW;
+
+/**
+ * \internal
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu             Pointer to vCPU area.
+ * \param utcb             Utcb pointer of the calling vCPU.
+ * \param to               Timeout to do IPC operation with.
+ * \param do_event_work_cb Call-back function that is called in case an
+ *                         event (such as an interrupt) is pending after
+ *                         enabling.
+ * \param setup_ipc        Function call-back that is called right before
+ *                         any IPC operation.
+ */
+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;
+
+/**
+ * \brief Halt the vCPU (sleep).
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu             Pointer to vCPU area.
+ * \param utcb             Utcb pointer of the calling vCPU.
+ * \param do_event_work_cb Call-back function that is called when the vCPU
+ *                         awakes and needs to handle an event/IRQ.
+ * \param setup_ipc        Function call-back that is called right before
+ *                         any IPC operation.
+ */
+L4_CV L4_INLINE
+void
+l4vcpu_halt(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;
+
+
+/**
+ * \brief Print the state of a vCPU.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu   Pointer to vCPU area.
+ * \param prefix A prefix for each line printed.
+ */
+L4_CV void
+l4vcpu_print_state(l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
+
+/**
+ * \internal
+ */
+L4_CV void
+l4vcpu_print_state_arch(l4_vcpu_state_t *vcpu, const char *prefix) L4_NOTHROW;
+
+
+/**
+ * \brief Return whether the entry reason was an IRQ/IPC message.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu Pointer to vCPU area.
+ *
+ * return 0 if not, !=0 otherwise.
+ */
+L4_CV L4_INLINE
+int
+l4vcpu_is_irq_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW;
+
+/**
+ * \brief Return whether the entry reason was a page fault.
+ * \ingroup api_libvcpu
+ *
+ * \param vcpu Pointer to vCPU area.
+ *
+ * return 0 if not, !=0 otherwise.
+ */
+L4_CV L4_INLINE
+int
+l4vcpu_is_page_fault_entry(l4_vcpu_state_t *vcpu) L4_NOTHROW;
+
+/**
+ * \brief Allocate state area for an extented vCPU.
+ * \ingroup api_libvcpu_ext
+ *
+ * \retval vcpu      Allocated vcpu-state area.
+ * \retval ext_state Allocated extended vcpu-state area.
+ * \param  task      Task to use for allocation.
+ * \param  regmgr    Region manager to use for allocation.
+ *
+ * \return 0 for success, error code otherwise
+ */
+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
+l4vcpu_state_t
+l4vcpu_state(l4_vcpu_state_t const *vcpu) L4_NOTHROW
+{
+  return vcpu->state;
+}
+
+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
+l4vcpu_irq_state_t
+l4vcpu_irq_disable_save(l4_vcpu_state_t *vcpu) L4_NOTHROW
+{
+  l4vcpu_irq_state_t s = (l4vcpu_irq_state_t)l4vcpu_state(vcpu);
+  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 (EXPECT_TRUE(!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
+{
+  while (1)
+    {
+      vcpu->state |= L4_VCPU_F_IRQ;
+      l4_barrier();
+
+      if (EXPECT_TRUE(!(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, l4vcpu_irq_state_t 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);
+}
+
+L4_CV L4_INLINE
+void
+l4vcpu_halt(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);
+  l4vcpu_irq_enable(vcpu, utcb, do_event_work_cb, setup_ipc);
+}
+
+__END_DECLS

l4/pkg/libvcpu/lib/Makefile

@@ -0,0 +1,4 @@
+PKGDIR		= ..
+L4DIR		?= $(PKGDIR)/../..
+
+include $(L4DIR)/mk/subdir.mk

l4/pkg/libvcpu/lib/src/ARCH-amd64/arch.cc

@@ -0,0 +1,32 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+
+#include <l4/vcpu/vcpu.h>
+#include <stdio.h>
+
+void l4vcpu_print_state_arch(l4_vcpu_state_t *vcpu,
+                             const char *prefix) L4_NOTHROW
+{
+  printf("%svcpu=%p ip=%08lx sp=%08lx trapno=%08lx label=%lx\n",
+         prefix, vcpu, vcpu->r.ip, vcpu->r.sp, vcpu->r.trapno, vcpu->i.label);
+  printf("%sax=%08lx dx=%08lx bx=%08lx cx=%08lx\n",
+         prefix, vcpu->r.ax, vcpu->r.dx, vcpu->r.bx, vcpu->r.cx);
+  printf("%ssi=%08lx di=%08lx bp=%08lx flags=%08lx\n",
+         prefix, vcpu->r.si, vcpu->r.di, vcpu->r.bp, vcpu->r.flags);
+}
+

l4/pkg/libvcpu/lib/src/ARCH-arm/arch.cc

@@ -0,0 +1,36 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+
+#include <l4/vcpu/vcpu.h>
+
+#include <stdio.h>
+
+void l4vcpu_print_state_arch(l4_vcpu_state_t *vcpu,
+                             const char *prefix) L4_NOTHROW
+{
+  printf("%svcpu=%p ip=%08lx  sp=%08lx err=%08lx label=%08lx\n",
+         prefix, vcpu, vcpu->r.ip, vcpu->r.sp, vcpu->r.err, vcpu->i.label);
+  printf("%s r0=%08lx  r1=%08lx  r2=%08lx  r3=%08lx\n",
+         prefix, vcpu->r.r[0], vcpu->r.r[1], vcpu->r.r[2], vcpu->r.r[3]);
+  printf("%s r4=%08lx  r5=%08lx  r6=%08lx  r7=%08lx\n",
+         prefix, vcpu->r.r[4], vcpu->r.r[5], vcpu->r.r[6], vcpu->r.r[7]);
+  printf("%s r8=%08lx  r9=%08lx r10=%08lx r11=%08lx\n",
+         prefix, vcpu->r.r[8], vcpu->r.r[9], vcpu->r.r[10], vcpu->r.r[11]);
+  printf("%sr12=%08lx  lr=%08lx flags=%08lx\n",
+         prefix, vcpu->r.r[12], vcpu->r.lr, vcpu->r.flags);
+}

l4/pkg/libvcpu/lib/src/ARCH-ppc32/arch.cc

@@ -0,0 +1,28 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+#include <l4/vcpu/vcpu.h>
+
+#include <stdio.h>
+
+void l4vcpu_print_state_arch(l4_vcpu_state_t *vcpu,
+                             const char *prefix) L4_NOTHROW
+{
+  (void)vcpu;
+  printf("%sTBD\n", prefix);
+}
+

l4/pkg/libvcpu/lib/src/ARCH-sparc/arch.cc

@@ -0,0 +1,36 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+
+#include <l4/vcpu/vcpu.h>
+
+#include <stdio.h>
+
+void l4vcpu_print_state_arch(l4_vcpu_state_t *vcpu,
+                             const char *prefix) L4_NOTHROW
+{
+  printf("%svcpu=%p ip=%08lx  sp=%08lx err=%08lx label=%08lx\n",
+         prefix, vcpu, vcpu->r.ip, vcpu->r.sp, vcpu->r.err, vcpu->i.label);
+  printf("%s r0=%08lx  r1=%08lx  r2=%08lx  r3=%08lx\n",
+         prefix, vcpu->r.r[0], vcpu->r.r[1], vcpu->r.r[2], vcpu->r.r[3]);
+  printf("%s r4=%08lx  r5=%08lx  r6=%08lx  r7=%08lx\n",
+         prefix, vcpu->r.r[4], vcpu->r.r[5], vcpu->r.r[6], vcpu->r.r[7]);
+  printf("%s r8=%08lx  r9=%08lx r10=%08lx r11=%08lx\n",
+         prefix, vcpu->r.r[8], vcpu->r.r[9], vcpu->r.r[10], vcpu->r.r[11]);
+  printf("%sr12=%08lx  lr=%08lx flags=%08lx\n",
+         prefix, vcpu->r.r[12], vcpu->r.lr, vcpu->r.flags);
+}

l4/pkg/libvcpu/lib/src/ARCH-x86/arch.cc

@@ -0,0 +1,34 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+
+#include <l4/vcpu/vcpu.h>
+#include <stdio.h>
+
+void l4vcpu_print_state_arch(l4_vcpu_state_t *vcpu,
+                             const char *prefix) L4_NOTHROW
+{
+  printf("%sip=%08lx sp=%08lx trapno=%08lx\n",
+         prefix, vcpu->r.ip, vcpu->r.sp, vcpu->r.trapno);
+  printf("%sax=%08lx dx=%08lx bx=%08lx cx=%08lx\n",
+         prefix, vcpu->r.ax, vcpu->r.dx, vcpu->r.bx, vcpu->r.cx);
+  printf("%ssi=%08lx di=%08lx bp=%08lx flags=%08lx\n",
+         prefix, vcpu->r.si, vcpu->r.di, vcpu->r.bp, vcpu->r.flags);
+  printf("%sds=%08lx es=%08lx gs=%08lx fs=%08lx\n",
+         prefix, vcpu->r.ds, vcpu->r.es, vcpu->r.gs, vcpu->r.fs);
+}
+

l4/pkg/libvcpu/lib/src/Makefile

@@ -0,0 +1,8 @@
+PKGDIR  ?= ../..
+L4DIR   ?= $(PKGDIR)/../..
+
+PC_FILENAME   = libvcpu
+TARGET        = libvcpu.a libvcpu.so
+SRC_CC        = vcpu.cc ARCH-$(ARCH)/arch.cc
+
+include $(L4DIR)/mk/lib.mk

l4/pkg/libvcpu/lib/src/vcpu.cc

@@ -0,0 +1,72 @@
+/*
+ * (c) 2010 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
+ *     economic rights: Technische Universität Dresden (Germany)
+ *
+ * This file is part of TUD:OS and distributed under the terms of the
+ * GNU General Public License 2.
+ * Please see the COPYING-GPL-2 file for details.
+ *
+ * As a special exception, you may use this file as part of a free software
+ * library without restriction.  Specifically, if other files instantiate
+ * templates or use macros or inline functions from this file, or you compile
+ * this file and link it with other files to produce an executable, this
+ * file does not by itself cause the resulting executable to be covered by
+ * the GNU General Public License.  This exception does not however
+ * invalidate any other reasons why the executable file might be covered by
+ * the GNU General Public License.
+ */
+
+#include <l4/vcpu/vcpu>
+#include <l4/re/util/kumem_alloc>
+#include <cstdio>
+#include <cstring>
+
+L4_CV void
+l4vcpu_print_state(l4_vcpu_state_t *vcpu,
+                   const char *prefix) L4_NOTHROW
+{
+  printf("%svcpu=%p state=%x savedstate=%x label=%lx\n",
+         prefix, vcpu, vcpu->state, vcpu->saved_state, vcpu->i.label);
+  printf("%ssticky=%x user_task=%lx\n",
+         prefix, vcpu->sticky_flags, vcpu->user_task << L4_CAP_SHIFT);
+  printf("%sentry_sp=%lx entry_ip=%lx\n",
+         prefix, vcpu->entry_sp, vcpu->entry_ip);
+  l4vcpu_print_state_arch(vcpu, prefix);
+}
+
+static int
+do_l4vcpu_ext_alloc(L4vcpu::Vcpu **vcpu,
+                    l4_addr_t *ext_state,
+                    L4::Cap<L4::Task> task,
+                    L4::Cap<L4Re::Rm> rm) L4_NOTHROW
+{
+  int r;
+  l4_addr_t v;
+
+  if ((r = L4Re::Util::kumem_alloc(&v, 0, task, rm)))
+    return r;
+
+  *vcpu      = L4vcpu::Vcpu::cast(v);
+  *ext_state = v + L4_VCPU_OFFSET_EXT_STATE;
+
+  return 0;
+}
+
+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
+{
+  L4::Cap<L4::Task> t(task);
+  L4::Cap<L4Re::Rm> r(regmgr);
+  L4vcpu::Vcpu **v = reinterpret_cast<L4vcpu::Vcpu **>(vcpu);
+  return do_l4vcpu_ext_alloc(v, ext_state, t, r);
+}
+
+L4_CV int
+L4vcpu::Vcpu::ext_alloc(Vcpu **vcpu,
+                        l4_addr_t *ext_state,
+                        L4::Cap<L4::Task> task,
+                        L4::Cap<L4Re::Rm> rm) throw()
+{
+  return do_l4vcpu_ext_alloc(vcpu, ext_state, task, rm);
+}