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)
 *
 * 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
 
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