portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge branch 'feature/tk1' into feature/arm_hyp_tk1

Browse source
This commit is contained in:
Yanyan Shen 2016-03-14 16:45:28 +11:00
commit 6b2c9ade2a
72 changed files with 2247 additions and 322 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
Kconfig
View file

@ -70,6 +70,13 @@ config ARM_HYPERVISOR_SUPPORT
help
Support for ARM1136JF-S
config ARM_CORTEX_A7
bool "Cortex A7"
depends on ARCH_ARM
select ARCH_ARM_V7A
help
Support for Cortex A7 processor
config ARM_CORTEX_A8
bool "Cortex A8"
depends on ARCH_ARM
@ -106,6 +113,12 @@ config ARM_HYPERVISOR_SUPPORT
Common flag for SabreLight and Wandboard Quad
config PLAT_IMX7
bool
default n
help
Common flag for iMX7 SoC
choice
prompt "Platform Type"
help
@ -185,6 +198,14 @@ config ARM_HYPERVISOR_SUPPORT
help
Support for iMX6 platform (Wandboard Quad).
config PLAT_IMX7_SABRE
bool "iMX7 (Sabre)"
depends on ARCH_ARM
depends on ARM_CORTEX_A7
select PLAT_IMX7
help
Support for iMX7 Sabre Dual.
config PLAT_ZYNQ7000
bool "Zynq-7000 (Xilinx ZC706)"
depends on ARCH_ARM
@ -204,6 +225,14 @@ config ARM_HYPERVISOR_SUPPORT
depends on ARM_CORTEX_A15
help
Support for ALLWINNERA20 platform (CUBIETRUCK).
config PLAT_TK1
bool "Jetson (Tegra K1)"
depends on ARCH_ARM
depends on ARM_CORTEX_A15
help
Support for Tegra K1 platform
endchoice
source "$KERNEL_PATH/src/arch/arm/Kconfig"

19
Makefile
View file

@ -17,8 +17,8 @@
SEL4_ARCH_LIST:=aarch32 ia32
ARCH_LIST:=arm x86
CPU_LIST:=arm1136jf-s ixp420 cortex-a8 cortex-a9 cortex-a15
PLAT_LIST:=imx31 pc99 ixp420 omap3 am335x exynos4 exynos5 imx6 apq8064 zynq7000 allwinnerA20
CPU_LIST:=arm1136jf-s ixp420 cortex-a7 cortex-a8 cortex-a9 cortex-a15
PLAT_LIST:=imx31 pc99 ixp420 omap3 am335x exynos4 exynos5 imx6 imx7 apq8064 zynq7000 allwinnerA20 tk1
ARMV_LIST:=armv6 armv7-a
ifndef SOURCE_ROOT
@ -297,6 +297,9 @@ DEFINES += -DARCH_ARM
ifeq (${SEL4_ARCH}, aarch32)
DEFINES += -D__KERNEL_32__ -DAARCH32
export __ARM_32__ = y
ifeq (${CPU},cortex-a7)
DEFINES += -DARM_CORTEX_A7
endif
ifeq (${CPU},cortex-a8)
DEFINES += -DARM_CORTEX_A8
endif
@ -309,6 +312,9 @@ endif
ifeq ($(PLAT),imx6)
DEFINES += -DIMX6
endif
ifeq ($(PLAT),imx7)
DEFINES += -DIMX7
endif
ifeq ($(PLAT),imx31)
DEFINES += -DIMX31
endif
@ -342,7 +348,7 @@ endif
endif # SEL4_ARCH=aarch32
endif # ARCH=arm
ifeq (${ARCH}, x86)
CFLAGS += -m32 -mno-mmx -mno-sse
CFLAGS += -m32
ASFLAGS += -Wa,--32
DEFINES += -DARCH_IA32 -DARCH_X86 -DX86_32 -D__KERNEL_32__
LDFLAGS += -Wl,-m,elf_i386
@ -409,6 +415,13 @@ ifeq (${CONFIG_WHOLE_PROGRAM_OPTIMISATIONS_KERNEL}, y)
CFLAGS += -fwhole-program
endif
# Set kernel build specific flags for the different x86 variants
# These are set here and not by the common build system as they
# only apply to building the kernel, and nothing else
ifeq (${ARCH}, x86)
CFLAGS += -mno-mmx -mno-sse -mno-sse2 -mno-3dnow
endif
# Allow overriding of the CFLAGS. Use with caution.
ifdef CONFIG_KERNEL_CFLAGS
ifneq (${CONFIG_KERNEL_CFLAGS},)

2
VERSION
View file

@ -1 +1 @@
2.1.0
3.0.0-dev

35
haskell/src/SEL4/Kernel/Thread.lhs
View file

@ -148,8 +148,8 @@ If either of the buffers is missing, then the message will be truncated to inclu
> doIPCTransfer ::
> PPtr TCB -> Maybe (PPtr Endpoint) -> Word -> Bool ->
> PPtr TCB -> Bool -> Kernel ()
> doIPCTransfer sender endpoint badge grant receiver diminish = do
> PPtr TCB -> Kernel ()
> doIPCTransfer sender endpoint badge grant receiver = do
> receiveBuffer <- lookupIPCBuffer True receiver
> fault <- threadGet tcbFault sender
@ -161,14 +161,14 @@ For normal IPC messages, the message registers are transferred.
> sendBuffer <- lookupIPCBuffer False sender
> doNormalTransfer
> sender sendBuffer endpoint badge grant
> receiver receiveBuffer diminish
> receiver receiveBuffer
If the sent message is a fault IPC, the stored fault is transferred.
> Just _ -> do
> doFaultTransfer badge sender receiver receiveBuffer
Replies sent by the "Reply" and "ReplyRecv" system calls can either be normal IPC replies, or fault replies. In the former case, the transfer is the same as for an IPC send, but there is never a fault, capability grants are always allowed, the badge is always 0, and capabilities are never received with diminished rights.
Replies sent by the "Reply" and "ReplyRecv" system calls can either be normal IPC replies, or fault replies. In the former case, the transfer is the same as for an IPC send, but there is never a fault, capability grants are always allowed, the badge is always 0, and capabilities are never received with diminished rights (diminished rights are now removed).
> doReplyTransfer :: PPtr TCB -> PPtr TCB -> PPtr CTE -> Kernel ()
> doReplyTransfer sender receiver slot = do
@ -185,7 +185,7 @@ Replies sent by the "Reply" and "ReplyRecv" system calls can either be normal IP
> fault <- threadGet tcbFault receiver
> case fault of
> Nothing -> do
> doIPCTransfer sender Nothing 0 True receiver False
> doIPCTransfer sender Nothing 0 True receiver
> cteDeleteOne slot
> setThreadState Running receiver
> attemptSwitchTo receiver
@ -208,9 +208,9 @@ Ordinary IPC simply transfers all message registers. It requires pointers to the
> doNormalTransfer ::
> PPtr TCB -> Maybe (PPtr Word) -> Maybe (PPtr Endpoint) -> Word -> Bool ->
> PPtr TCB -> Maybe (PPtr Word) -> Bool -> Kernel ()
> PPtr TCB -> Maybe (PPtr Word) -> Kernel ()
> doNormalTransfer sender sendBuffer endpoint badge canGrant
> receiver receiveBuffer diminish = do
> receiver receiveBuffer = do
> tag <- getMessageInfo sender
> caps <- if canGrant
> then lookupExtraCaps sender sendBuffer tag
@ -218,7 +218,7 @@ Ordinary IPC simply transfers all message registers. It requires pointers to the
> else return []
> msgTransferred <- copyMRs sender sendBuffer receiver receiveBuffer $
> msgLength tag
> tag' <- transferCaps tag caps endpoint receiver receiveBuffer diminish
> tag' <- transferCaps tag caps endpoint receiver receiveBuffer
> let tag'' = tag' { msgLength = msgTransferred }
> setMessageInfo receiver tag''
> asUser receiver $ setRegister badgeRegister badge
@ -251,23 +251,23 @@ The recipient's argument registers are filled in with various information about
This function is called when an IPC message includes a capability to transfer. It attempts to perform the transfer, and returns an adjusted messageInfo containing the number of caps transferred and the bitmask of which caps were unwrapped.
> transferCaps :: MessageInfo -> [(Capability, PPtr CTE)] ->
> Maybe (PPtr Endpoint) -> PPtr TCB -> Maybe (PPtr Word) -> Bool ->
> Maybe (PPtr Endpoint) -> PPtr TCB -> Maybe (PPtr Word) ->
> Kernel MessageInfo
> transferCaps info caps endpoint receiver receiveBuffer diminish = do
> transferCaps info caps endpoint receiver receiveBuffer = do
> destSlots <- getReceiveSlots receiver receiveBuffer
> let info' = info { msgExtraCaps = 0, msgCapsUnwrapped = 0 }
> case receiveBuffer of
> Nothing -> return info'
> Just rcvBuffer -> do
> transferCapsToSlots endpoint diminish rcvBuffer 0
> transferCapsToSlots endpoint rcvBuffer 0
> caps destSlots info'
> transferCapsToSlots :: Maybe (PPtr Endpoint) -> Bool -> PPtr Word -> Int ->
> transferCapsToSlots :: Maybe (PPtr Endpoint) -> PPtr Word -> Int ->
> [(Capability, PPtr CTE)] -> [PPtr CTE] -> MessageInfo ->
> Kernel MessageInfo
> transferCapsToSlots _ _ _ n [] _ mi =
> transferCapsToSlots _ _ n [] _ mi =
> return $ mi { msgExtraCaps = fromIntegral n }
> transferCapsToSlots ep diminish rcvBuffer n (arg:caps) slots mi =
> transferCapsToSlots ep rcvBuffer n (arg:caps) slots mi =
> constOnFailure (mi { msgExtraCaps = fromIntegral n }) $ do
> case (cap, ep, slots) of
> (EndpointCap { capEPPtr = p1 }, Just p2, _) | p1 == p2 -> do
@ -275,16 +275,13 @@ This function is called when an IPC message includes a capability to transfer. I
> setExtraBadge rcvBuffer (capEPBadge cap) n
> withoutFailure $ transferAgain slots miCapUnfolded
> (_, _, destSlot:slots') -> do
> cap' <- unifyFailure $ deriveCap srcSlot $ if diminish
> then allRights { capAllowWrite = False }
> `maskCapRights` cap
> else cap
> cap' <- unifyFailure $ deriveCap srcSlot $ cap
> when (isNullCap cap') $ throw undefined
> withoutFailure $ cteInsert cap' srcSlot destSlot
> withoutFailure $ transferAgain slots' mi
> _ -> return $ mi { msgExtraCaps = fromIntegral n }
> where
> transferAgain = transferCapsToSlots ep diminish rcvBuffer (n + 1) caps
> transferAgain = transferCapsToSlots ep rcvBuffer (n + 1) caps
> miCapUnfolded = mi { msgCapsUnwrapped = msgCapsUnwrapped mi .|. bit n}
> (cap, srcSlot) = arg

16
haskell/src/SEL4/Object/Endpoint.lhs
View file

@ -84,9 +84,8 @@ If the endpoint is receiving, then a thread is removed from its queue, and an IP
> recvState <- getThreadState dest
> assert (isReceive recvState)
> "TCB in receive endpoint queue must be blocked on send"
> let diminish = blockingIPCDiminishCaps recvState
> doIPCTransfer thread (Just epptr) badge canGrant
> dest diminish
> dest
The receiving thread has now completed its blocking operation and can run. If the receiving thread has higher priority than the current thread, the scheduler is instructed to switch to it immediately.
@ -96,7 +95,7 @@ The receiving thread has now completed its blocking operation and can run. If th
If the sender is performing a call or has faulted, set up the reply capability.
> fault <- threadGet tcbFault thread
> case (call, fault, canGrant && not diminish) of
> case (call, fault, canGrant) of
> (False, Nothing, _) -> return ()
> (_, _, True) -> setupCallerCap thread dest
> _ -> setThreadState Inactive thread
@ -117,7 +116,6 @@ The IPC receive operation is essentially the same as the send operation, but wit
> receiveIPC thread cap@(EndpointCap {}) isBlocking = do
> let epptr = capEPPtr cap
> ep <- getEndpoint epptr
> let diminish = not $ capEPCanSend cap
> -- check if anything is waiting on bound ntfn
> ntfnPtr <- getBoundNotification thread
> ntfn <- maybe (return $ NTFN IdleNtfn Nothing) (getNotification) ntfnPtr
@ -127,15 +125,13 @@ The IPC receive operation is essentially the same as the send operation, but wit
> IdleEP -> case isBlocking of
> True -> do
> setThreadState (BlockedOnReceive {
> blockingObject = epptr,
> blockingIPCDiminishCaps = diminish }) thread
> blockingObject = epptr }) thread
> setEndpoint epptr $ RecvEP [thread]
> False -> doNBRecvFailedTransfer thread
> RecvEP queue -> case isBlocking of
> True -> do
> setThreadState (BlockedOnReceive {
> blockingObject = epptr,
> blockingIPCDiminishCaps = diminish }) thread
> blockingObject = epptr }) thread
> setEndpoint epptr $ RecvEP $ queue ++ [thread]
> False -> doNBRecvFailedTransfer thread
> SendEP (sender:queue) -> do
@ -148,10 +144,10 @@ The IPC receive operation is essentially the same as the send operation, but wit
> let badge = blockingIPCBadge senderState
> let canGrant = blockingIPCCanGrant senderState
> doIPCTransfer sender (Just epptr) badge canGrant
> thread diminish
> thread
> let call = blockingIPCIsCall senderState
> fault <- threadGet tcbFault sender
> case (call, fault, canGrant && not diminish) of
> case (call, fault, canGrant) of
> (False, Nothing, _) -> do
> setThreadState Running sender
> switchIfRequiredTo sender

2
haskell/src/SEL4/Object/Notification.lhs
View file

@ -38,7 +38,7 @@ This module specifies the behavior of notification objects.
> -- helper function
> receiveBlocked :: ThreadState -> Bool
> receiveBlocked st = case st of
> BlockedOnReceive _ _ -> True
> BlockedOnReceive _ -> True
> _ -> False
This function performs an signal operation, given a capability to a notification object, and a single machine word of message data (the badge). This operation will never block the signalling thread.

5
haskell/src/SEL4/Object/Structures.lhs
View file

@ -333,8 +333,7 @@ A user thread may be in the following states:
\item blocked on a synchronous IPC send or receive (which require the presence of additional data about the operation);
> = BlockedOnReceive {
> blockingObject :: PPtr Endpoint,
> blockingIPCDiminishCaps :: Bool }
> blockingObject :: PPtr Endpoint }
\item blocked waiting for a reply to a previously sent message;
@ -439,7 +438,7 @@ Convenience functions dealing with properties of the machine word:
> _ -> error "Unknown word size"
> isReceive :: ThreadState -> Bool
> isReceive (BlockedOnReceive _ _) = True
> isReceive (BlockedOnReceive _) = True
> isReceive _ = False
> isSend :: ThreadState -> Bool

1
include/api/bootinfo_types.h Symbolic link
View file

@ -0,0 +1 @@
../../libsel4/include/sel4/bootinfo_types.h

1
include/api/types.h
View file

@ -23,7 +23,6 @@
/* cap_rights_t defined in api/types.bf */
typedef word_t prio_t;
typedef word_t dom_t;
enum domainConstants {
minDom = 0,

6
include/arch/arm/arch/32/mode/fastpath/fastpath.h
View file

@ -51,12 +51,6 @@ switchToThread_fp(tcb_t *thread, pde_t *cap_pd, pde_t stored_hw_asid)
clearExMonitor_fp();
}
static inline void
thread_state_ptr_set_blockingIPCDiminish_np(thread_state_t *ts_ptr, word_t dim)
{
ts_ptr->words[2] = dim;
}
static inline void
mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged(
mdb_node_t *node_ptr, word_t mdbNext,

4
include/arch/arm/arch/32/mode/machine.h
View file

@ -227,6 +227,10 @@ static inline void cleanByVA_PoU(vptr_t vaddr, paddr_t paddr)
#elif defined(PLAT_EXYNOS5)
/* Flush to coherency for table walks... Why? */
asm volatile("mcr p15, 0, %0, c7, c10, 1" : : "r"(vaddr));
#elif defined(PLAT_IMX7)
asm volatile("mcr p15, 0, %0, c7, c10, 1" : : "r"(vaddr));
#elif defined(PLAT_TK1)
asm volatile("mcr p15, 0, %0, c7, c10, 1" : : "r"(vaddr));
#else
asm volatile("mcr p15, 0, %0, c7, c11, 1" : : "r"(vaddr));
#endif

3
include/arch/arm/arch/32/mode/machine/hardware.h
View file

@ -34,6 +34,9 @@
#elif defined(ARM_CORTEX_A9)
#define L1_CACHE_LINE_SIZE_BITS 5 /* 32 bytes */
#elif defined(ARM_CORTEX_A7)
#define L1_CACHE_LINE_SIZE_BITS 6 /* 64 bytes */
#elif defined(ARM_CORTEX_A15)
#define L1_CACHE_LINE_SIZE_BITS 6 /* 64 bytes */
#endif

5
include/arch/arm/arch/types.h
View file

@ -22,6 +22,7 @@ typedef word_t paddr_t;
typedef word_t pptr_t;
typedef word_t cptr_t;
typedef word_t node_id_t;
typedef word_t dom_t;
typedef uint8_t hw_asid_t;
@ -34,5 +35,9 @@ enum hwASIDConstants {
typedef word_t seL4_Word;
typedef cptr_t seL4_CPtr;
typedef uint32_t seL4_Uint32;
typedef uint8_t seL4_Uint8;
typedef node_id_t seL4_NodeId;
typedef dom_t seL4_Domain;
typedef paddr_t seL4_PAddr;
#endif

7
include/arch/x86/arch/32/mode/fastpath/fastpath.h
View file

@ -39,13 +39,6 @@ switchToThread_fp(tcb_t *thread, pde_t *pd, pde_t stored_hw_asid)
ksCurThread = thread;
}
static inline void
thread_state_ptr_set_blockingIPCDiminish_np(thread_state_t *ts_ptr, word_t dim)
{
ts_ptr->words[2] &= BIT(0);
ts_ptr->words[1] = dim;
}
static inline void
mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged(
mdb_node_t *node_ptr, word_t mdbNext,

6
include/arch/x86/arch/types.h
View file

@ -24,10 +24,14 @@ typedef word_t cptr_t;
typedef word_t dev_id_t;
typedef word_t cpu_id_t;
typedef word_t node_id_t;
typedef word_t dom_t;
/* for libsel4 headers that the kernel shares */
typedef word_t seL4_Word;
typedef cptr_t seL4_CPtr;
typedef uint32_t seL4_Uint32;
typedef uint8_t seL4_Uint8;
typedef node_id_t seL4_NodeId;
typedef paddr_t seL4_PAddr;
typedef dom_t seL4_Domain;
#endif

59
include/bootinfo.h
View file

@ -13,65 +13,14 @@
#include <config.h>
#include <types.h>
#include <api/bootinfo_types.h>
#define BI_PTR(r) ((bi_t*)(r))
#define BI_PTR(r) ((seL4_BootInfo*)(r))
#define BI_REF(p) ((word_t)(p))
/* bootinfo data structures (directly corresponding to abstract specification) */
#define BI_FRAME_SIZE_BITS PAGE_BITS
/* fixed cap positions in root CNode */
#define BI_CAP_NULL 0 /* null cap */
#define BI_CAP_IT_TCB 1 /* initial thread's TCB cap */
#define BI_CAP_IT_CNODE 2 /* initial thread's root CNode cap */
#define BI_CAP_IT_VSPACE 3 /* initial thread's vspace root cap */
#define BI_CAP_IRQ_CTRL 4 /* global IRQ controller cap */
#define BI_CAP_ASID_CTRL 5 /* global ASID controller cap */
#define BI_CAP_IT_ASID_POOL 6 /* initial thread's ASID pool cap */
#define BI_CAP_IO_PORT 7 /* global IO port cap (null cap if not supported) */
#define BI_CAP_IO_SPACE 8 /* global IO space cap (null cap if no IOMMU support) */
#define BI_CAP_BI_FRAME 9 /* bootinfo frame cap */
#define BI_CAP_IT_IPCBUF 10 /* initial thread's IPC buffer frame cap */
#define BI_CAP_DOM 11 /* domain cap */
#define BI_CAP_DYN_START 12 /* slot where dynamically allocated caps start */
/* type definitions */
typedef word_t slot_pos_t;
typedef struct slot_region {
slot_pos_t start;
slot_pos_t end;
} slot_region_t;
#define S_REG_EMPTY (slot_region_t){ .start = 0, .end = 0 }
typedef struct bi_dev_reg {
paddr_t base_paddr; /* base physical address of device region */
uint32_t frame_size_bits; /* size (2^n bytes) of a device-region frame */
slot_region_t frame_caps; /* device-region frame caps */
} bi_dev_reg_t;
typedef struct bi {
node_id_t node_id;
uint32_t num_nodes;
uint32_t num_iopt_levels; /* number of IOMMU PT levels (0 if no IOMMU support) */
vptr_t ipcbuf_vptr; /* vptr to initial thread's IPC buffer */
slot_region_t null_caps; /* null caps (empty slots) */
slot_region_t sh_frame_caps; /* shared-frame caps */
slot_region_t ui_frame_caps; /* userland-image frame caps */
slot_region_t ui_paging_caps; /* userland-image paging structure caps */
slot_region_t ut_obj_caps; /* untyped-object caps (UT caps) */
paddr_t ut_obj_paddr_list [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each UT cap */
uint8_t ut_obj_size_bits_list[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each UT cap */
uint8_t it_cnode_size_bits; /* initial thread's root CNode size (2^n slots) */
uint32_t num_dev_regs; /* number of device regions */
bi_dev_reg_t dev_reg_list[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
dom_t it_domain; /* initial thread's domain ID */
} bi_t;
#define S_REG_EMPTY (seL4_SlotRegion){ .start = 0, .end = 0 }
/* adjust constants in config.h if this assert fails */
compile_assert(bi_size, sizeof(bi_t) <= BIT(BI_FRAME_SIZE_BITS))
compile_assert(bi_size, sizeof(seL4_BootInfo) <= BIT(BI_FRAME_SIZE_BITS))
#endif

8
include/kernel/boot.h
View file

@ -32,9 +32,9 @@ typedef cte_t* slot_ptr_t;
typedef struct ndks_boot {
region_t freemem[MAX_NUM_FREEMEM_REG];
bi_t* bi_frame;
slot_pos_t slot_pos_cur;
slot_pos_t slot_pos_max;
seL4_BootInfo* bi_frame;
seL4_SlotPos slot_pos_cur;
seL4_SlotPos slot_pos_max;
} ndks_boot_t;
extern ndks_boot_t ndks_boot;
@ -67,7 +67,7 @@ pptr_t allocate_bi_frame(node_id_t node_id, word_t num_nodes, vptr_t ipcbuf_vptr
void create_bi_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, pptr_t pptr, vptr_t vptr);
typedef struct create_frames_of_region_ret {
slot_region_t region;
seL4_SlotRegion region;
bool_t success;
} create_frames_of_region_ret_t;

5
include/kernel/thread.h
View file

@ -44,12 +44,11 @@ void activateThread(void) VISIBLE;
void suspend(tcb_t *target);
void restart(tcb_t *target);
void doIPCTransfer(tcb_t *sender, endpoint_t *endpoint,
word_t badge, bool_t grant, tcb_t *receiver,
bool_t diminish);
word_t badge, bool_t grant, tcb_t *receiver);
void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot);
void doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint,
word_t badge, bool_t canGrant, tcb_t *receiver,
word_t *receiveBuffer, bool_t diminish);
word_t *receiveBuffer);
void doFaultTransfer(word_t badge, tcb_t *sender, tcb_t *receiver,
word_t *receiverIPCBuffer);
void doNBRecvFailedTransfer(tcb_t *thread);

8
include/object/structures_32.bf
View file

@ -161,7 +161,6 @@ block mdb_node {
-- * Restart
-- * Inactive
-- * BlockedOnReceive
-- - DiminishCaps
-- - Endpoint
-- * BlockedOnSend
-- - Endpoint
@ -262,16 +261,15 @@ block user_exception {
-- Thread state: size = 12 bytes
block thread_state(blockingIPCBadge, blockingIPCCanGrant, blockingIPCIsCall,
tcbQueued, blockingIPCDiminishCaps, blockingObject,
tcbQueued, blockingObject,
tsType) {
field blockingIPCBadge 28
field blockingIPCCanGrant 1
field blockingIPCIsCall 1
padding 1
field blockingIPCDiminishCaps 1
padding 2
-- this is fastpath-specific. it is useful to be able to write
-- tsType and blockingIPCDiminishCaps without changing tcbQueued
-- tsType and without changing tcbQueued
padding 31
field tcbQueued 1

89
include/plat/imx7/autoconf.h Normal file
View file

@ -0,0 +1,89 @@
/*
* Automatically generated C config: don't edit
* Project Configuration
* Mon Nov 9 14:36:38 2015
*/
#define AUTOCONF_INCLUDED
#define CONFIG_LIB_SEL4_SIMPLE 1
#define CONFIG_ARM_CORTEX_A9 1
#define CONFIG_HAVE_CACHE 1
#define CONFIG_LIB_SEL4_DEBUG 1
#define CONFIG_LIB_ELF 1
#define CONFIG_USER_DEBUG_BUILD 1
#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1
#define CONFIG_HAVE_LIB_SEL4 1
#define CONFIG_LIB_SEL4_VKA 1
#define CONFIG_HAVE_CRT 1
#define CONFIG_TIMER_TICK_MS 2
#define CONFIG_ARM_ERRATA_764369 1
#define CONFIG_KERNEL_CFLAGS ""
#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1
#define CONFIG_HAVE_LIBC 1
#define CONFIG_PRINT_XML 1
#define CONFIG_USER_COMPILER ""
#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1
#define CONFIG_WORD_SIZE 32
#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199
#define CONFIG_APP_TESTS 1
#define CONFIG_MAX_NUM_TRACE_POINTS 0
#define CONFIG_SEL4UTILS_STACK_SIZE 65536
#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1
#define CONFIG_FASTPATH 1
#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0
#define CONFIG_HAVE_TIMER 1
#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17
#define CONFIG_DOMAIN_SCHEDULE ""
#define CONFIG_BUFFER_OUTPUT 1
#define CONFIG_LIB_SEL4 1
#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
#define CONFIG_LIB_SEL4_UTILS 1
#define CONFIG_RELEASE_BUILD 1
#define CONFIG_LIB_SEL4_VSPACE 1
#define CONFIG_LIB_PLATSUPPORT 1
#define CONFIG_LIB_SEL4_ALLOCMAN 1
#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
#define CONFIG_LIB_SEL4_TEST 1
#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1
#define CONFIG_LIB_ELFLOADER 1
#define CONFIG_HAVE_LIB_SEL4_VSPACE 1
#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166
#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0
#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-"
#define CONFIG_LIB_SEL4_MUSLC_SYS 1
#define CONFIG_HAVE_LIB_SEL4_TEST 1
#define CONFIG_LIB_MUSL_C 1
#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100
#define CONFIG_ARCH_ARM_V7A 1
#define CONFIG_USER_CFLAGS ""
#define CONFIG_HAVE_LIB_SEL4_DEBUG 1
#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1
#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1
#define CONFIG_LIB_UTILS 1
#define CONFIG_OPTIMISATION_O2 1
#define CONFIG_HAVE_LIB_CPIO 1
#define CONFIG_PLAT_IMX6 1
#define CONFIG_HAVE_LIB_SEL4_VKA 1
#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1
#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1
#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700"
#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
#define CONFIG_ARCH_ARM 1
#define CONFIG_HAVE_LIB_ELF 1
#define CONFIG_HAVE_LIB_PLATSUPPORT 1
#define CONFIG_NUM_DOMAINS 16
#define CONFIG_HAVE_LIB_UTILS 1
#define CONFIG_USER_OPTIMISATION_O2 1
#define CONFIG_LIB_CPIO 1
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
#define CONFIG_ROOT_CNODE_SIZE_BITS 12
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_TESTPRINTER_REGEX ".*"
#define CONFIG_APP_SEL4TEST 1
#define CONFIG_HAVE_LIB_SEL4_UTILS 1
#define CONFIG_KERNEL_COMPILER ""
#define CONFIG_TIME_SLICE 5
#define CONFIG_KERNEL_EXTRA_CPPFLAGS ""
#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128
#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1
#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576
#define CONFIG_BUILDSYS_USE_CCACHE 1

11
include/plat/imx7/plat/Makefile Normal file
View file

@ -0,0 +1,11 @@
#
# Copyright 2014, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile

89
include/plat/imx7/plat/machine.h Normal file
View file

@ -0,0 +1,89 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_H
#define __PLAT_MACHINE_H
#include <arch/machine/gic_pl390.h>
#define N_INTERRUPTS 160
/* pull some device interrupts from Linux device tree, need to
* confirm them when the offcial manual is available.
*/
enum IRQConstants {
// INTERRUPT_RESERVED = 0,
// INTERRUPT_RESERVED = 1,
// INTERRUPT_RESERVED = 2,
// INTERRUPT_RESERVED = 3,
// INTERRUPT_RESERVED = 4,
// INTERRUPT_RESERVED = 5,
// INTERRUPT_RESERVED = 6,
// INTERRUPT_RESERVED = 7,
// INTERRUPT_RESERVED = 8,
// INTERRUPT_RESERVED = 9,
// INTERRUPT_RESERVED = 10,
// INTERRUPT_RESERVED = 11,
// INTERRUPT_RESERVED = 12,
// INTERRUPT_RESERVED = 13,
// INTERRUPT_RESERVED = 14,
// INTERRUPT_RESERVED = 15,
// INTERRUPT_RESERVED = 16,
// INTERRUPT_RESERVED = 17,
// INTERRUPT_RESERVED = 18,
// INTERRUPT_RESERVED = 19,
// INTERRUPT_RESERVED = 20,
// INTERRUPT_RESERVED = 21,
// INTERRUPT_RESERVED = 22,
// INTERRUPT_RESERVED = 23,
// INTERRUPT_RESERVED = 24,
// INTERRUPT_RESERVED = 25,
// INTERRUPT_RESERVED = 26,
// INTERRUPT_RESERVED = 27,
// INTERRUPT_RESERVED = 28,
INTERRUPT_PRIV_TIMER = 29,
// INTERRUPT_RESERVED = 30,
// INTERRUPT_RESERVED = 31,
INTERRUPT_IOMUXC = 32,
INTERRUPT_GPIO0_15_0 = 96,
INTERRUPT_GPIO0_31_16 = 97,
INTERRUPT_GPIO1_15_0 = 98,
INTERRUPT_GPIO1_31_16 = 99,
INTERRUPT_GPIO2_15_0 = 100,
INTERRUPT_GPIO2_31_16 = 101,
INTERRUPT_GPIO3_15_0 = 102,
INTERRUPT_GPIO3_31_16 = 103,
INTERRUPT_GPIO4_15_0 = 104,
INTERRUPT_GPIO4_31_16 = 105,
INTERRUPT_GPIO5_15_0 = 106,
INTERRUPT_GPIO5_31_16 = 107,
INTERRUPT_GPIO6_15_0 = 108,
INTERRUPT_GPIO6_31_16 = 109,
INTERRUPT_WDOG0 = 110,
INTERRUPT_WDOG1 = 111,
INTERRUPT_WDOG2 = 42,
INTERRUPT_WDOG3 = 141,
INTERRUPT_GPT0 = 87,
INTERRUPT_GPT1 = 86,
INTERRUPT_GPT2 = 85,
INTERRUPT_GPT3 = 84,
INTERRUPT_ANATOP_0 = 81,
INTERRUPT_ANATOP_1 = 83,
maxIRQ = 159
} platform_interrupt_t;
#define KERNEL_TIMER_IRQ INTERRUPT_PRIV_TIMER
enum irqNumbers {
irqInvalid = (irq_t) - 1
};
#endif /* !__PLAT_MACHINE_H */

13
include/plat/imx7/plat/machine/Makefile Normal file
View file

@ -0,0 +1,13 @@
#
# Copyright 2014, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
DIRECTORIES += plat/machine
BF_SOURCES += plat/machine/hardware.bf

17
include/plat/imx7/plat/machine/debug_helpers.h Normal file
View file

@ -0,0 +1,17 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_DEBUG_HELPERS_H
#define __PLAT_MACHINE_DEBUG_HELPERS_H
#include <plat/machine/io.h>
#endif /* ! __PLAT_MACHINE_DEBUG_HELPERS_H */

85
include/plat/imx7/plat/machine/devices.h Normal file
View file

@ -0,0 +1,85 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_DEVICES_H
#define __PLAT_MACHINE_DEVICES_H
/* These devices are used by the seL4 kernel. */
#define UART_PADDR UART0_PADDR
#define UART_PPTR 0xfff01000
#define WDT_PPTR 0xfff02000
#define ARM_MP_PPTR1 0xfff03000
#define ARM_MP_PPTR2 0xfff04000
#define ARM_MP_PPTR3 0xfff05000
#define ARM_MP_PRIV_TIMER_PPTR (ARM_MP_PPTR1 + 0x600 )
#define ARM_MP_GLOBAL_TIMER_PPTR (ARM_MP_PPTR1 + 0x200 )
#define GIC_PL390_CONTROLLER_PPTR (ARM_MP_PPTR3)
#define GIC_PL390_DISTRIBUTOR_PPTR (ARM_MP_PPTR2)
#define ARM_SCU_PADDR 0x31000000
/* All devices */
#define ARM_MP_PADDR (ARM_SCU_PADDR) /* 2 pages */
/* addresses from Linux device tree */
#define GPIO0_PADDR 0x30200000 /* 0x10000 */
#define GPIO1_PADDR 0x30210000
#define GPIO2_PADDR 0x30220000
#define GPIO3_PADDR 0x30230000
#define GPIO4_PADDR 0x30240000
#define GPIO5_PADDR 0x30250000
#define GPIO6_PADDR 0x30260000
#define WDOG0_PADDR 0x30280000
#define WDOG1_PADDR 0x30290000
#define WDOG2_PADDR 0x302a0000
#define WDOG3_PADDR 0x302b0000
#define IOMUXC_LPSR_PADDR 0x302c0000
#define GPT0_PADDR 0x302d0000
#define GPT1_PADDR 0x302e0000
#define GPT2_PADDR 0x302f0000
#define GPT3_PADDR 0x30300000
#define IOMUXC_PADDR 0x30330000
#define GPR_PADDR 0x30340000
#define OCOTP_PADDR 0x30350000
#define ANATOP_PADDR 0x30360000
#define SNVS_PADDR 0x30370000
#define CLKS_PADDR 0x30380000
#define SRC_PADDR 0x30390000
#define PWM0_PADDR 0x30660000
#define PWM1_PADDR 0x30670000
#define PWM2_PADDR 0x30680000
#define PWM3_PADDR 0x30690000
#define UART0_PADDR 0x30860000
#define UART1_PADDR 0x30890000
#define UART2_PADDR 0x30880000
#define UART3_PADDR 0x30a60000
#define UART4_PADDR 0x30a70000
#define UART5_PADDR 0x30a80000
#define UART6_PADDR 0x30a90000
#define I2C0_PADDR 0x30a20000
#define I2C1_PADDR 0x30a30000
#define I2C2_PADDR 0x30a40000
#define I2C3_PADDR 0x30a50000
#define USBOTG0_PADDR 0x30b10000 /* 0x200 */
#define USBOTG1_PADDR 0x30b20000 /* 0x200 */
#define USBH_PADDR 0x30b30000 /* 0x200 */
/* addresses are not page-aligned */
#define USDHC0_PADDR 0x30b40000 /* 0x10000 */
#define USDHC1_PADDR 0x30b50000
#define USDHC2_PADDR 0x30b60000
#define FEC0_PADDR 0x30be0000
#define FEC1_PADDR 0x30bf0000
#endif /* !__PLAT_MACHINE_DEVICES_H */

11
include/plat/imx7/plat/machine/hardware.bf Normal file
View file

@ -0,0 +1,11 @@
--
-- Copyright 2014, General Dynamics C4 Systems
--
-- This software may be distributed and modified according to the terms of
-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
-- See "LICENSE_GPLv2.txt" for details.
--
-- @TAG(GD_GPL)
--
base 32

96
include/plat/imx7/plat/machine/hardware.h Normal file
View file

@ -0,0 +1,96 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_HARDWARE_H
#define __PLAT_MACHINE_HARDWARE_H
#define physBase 0x80000000
#define kernelBase 0xe0000000
#define physMappingOffset (kernelBase - physBase)
#define BASE_OFFSET physMappingOffset
/*
* 0xffe00000 asid id slot (arm/arch/kernel/vspace.h)
* 0xfff00000 devices (plat/machine/devices.h)
* 0xffff0000 vectors (arch/machine/hardware.h)
* 0xffffc000 global page (arch/machine/hardware.h)
* 0xfffff000 kernel stack (arch/machine/hardware.h)
*/
#define PPTR_TOP 0xfff00000
#define PADDR_TOP (PPTR_TOP - BASE_OFFSET)
#ifndef __ASSEMBLER__
#include <types.h>
#include <arch/object/structures.h>
#include <plat/machine.h>
#include <plat/machine/hardware_gen.h>
#include <arch/machine/gic_pl390.h>
static inline void * CONST
ptrFromPAddr(paddr_t paddr)
{
return (void*)(paddr + physMappingOffset);
}
static inline paddr_t CONST
addrFromPPtr(void *pptr)
{
return (paddr_t)pptr - physMappingOffset;
}
#define paddr_to_pptr ptrFromPAddr
#define pptr_to_paddr addrFromPPtr
static inline region_t CONST
paddr_to_pptr_reg(p_region_t p_reg)
{
return (region_t) {
p_reg.start + physMappingOffset, p_reg.end + physMappingOffset
};
}
static inline p_region_t CONST
pptr_to_paddr_reg(region_t reg)
{
return (p_region_t) {
reg.start - physMappingOffset, reg.end - physMappingOffset
};
}
int get_num_avail_p_regs(void);
p_region_t get_avail_p_reg(word_t i);
int get_num_dev_p_regs(void);
p_region_t get_dev_p_reg(word_t i);
void map_kernel_devices(void);
bool_t CONST isReservedIRQ(irq_t irq);
void handleReservedIRQ(irq_t irq);
static inline void
plat_cleanInvalidateL2Range(paddr_t start, paddr_t end) {}
static inline void
plat_cleanL2Range(paddr_t start, paddr_t end) {}
static inline void
plat_invalidateL2Range(paddr_t start, paddr_t end) {}
void initL2Cache(void);
void initTimer(void);
void resetTimer(void);
#endif /* !__ASSEMBLER__ */
#endif /* !__PLAT_MACHINE_HARDWARE_H */

26
include/plat/imx7/plat/machine/io.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_IO_H
#define __PLAT_IO_H
#include <types.h>
#if defined DEBUG || defined RELEASE_PRINTF
void imx7_uart_putchar(char c);
void putDebugChar(unsigned char c);
unsigned char getDebugChar(void);
#define kernel_putchar(c) imx7_uart_putchar(c)
#else /* !DEBUG */
#define kernel_putchar(c) ((void)(0))
#endif /* DEBUG */
#endif /* !__PLAT_IO_H */

15
include/plat/pc99/plat/machine/io.h
View file

@ -21,21 +21,6 @@ uint8_t in8(uint16_t port);
uint16_t in16(uint16_t port);
uint32_t in32(uint16_t port);
/* these versions are linked to physical addresses */
static inline void PHYS_CODE
out8_phys(uint16_t port, uint8_t value)
{
asm volatile("outb %[value], %[port]" :: [port] "d"(port), [value] "a"(value));
}
static inline uint8_t PHYS_CODE
in8_phys(uint16_t port)
{
uint8_t value;
asm volatile("inb %[port], %[value]" : [value] "=a"(value) : [port] "d" (port));
return value;
}
#if defined DEBUG || defined RELEASE_PRINTF
void serial_init(uint16_t port);

94
include/plat/tk1/autoconf.h Normal file
View file

@ -0,0 +1,94 @@
/*
* Automatically generated C config: don't edit
* Project Configuration
* Mon Mar 14 15:34:46 2016
*/
#define AUTOCONF_INCLUDED
#define CONFIG_LIB_SEL4_SIMPLE 1
#define CONFIG_IRQ_REPORTING 1
#define CONFIG_HAVE_ARCH_TIMER 1
#define CONFIG_HAVE_CACHE 1
#define CONFIG_LIB_SEL4_DEBUG 1
#define CONFIG_LIB_ELF 1
#define CONFIG_USER_DEBUG_BUILD 1
#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1
#define CONFIG_HAVE_LIB_SEL4 1
#define CONFIG_LIB_SEL4_VKA 1
#define CONFIG_HAVE_CRT 1
#define CONFIG_TESTPRINTER_HALT_ON_TEST_FAILURE 1
#define CONFIG_TIMER_TICK_MS 2
#define CONFIG_KERNEL_CFLAGS ""
#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1
#define CONFIG_COLOUR_PRINTING 1
#define CONFIG_IMAGE_ELF 1
#define CONFIG_HAVE_LIBC 1
#define CONFIG_USER_COMPILER ""
#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1
#define CONFIG_WORD_SIZE 32
#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199
#define CONFIG_APP_TESTS 1
#define CONFIG_MAX_NUM_TRACE_POINTS 0
#define CONFIG_SEL4UTILS_STACK_SIZE 65536
#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1
#define CONFIG_PLAT_TK1 1
#define CONFIG_FASTPATH 1
#define CONFIG_ARM_CORTEX_A15 1
#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0
#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 16
#define CONFIG_DOMAIN_SCHEDULE ""
#define CONFIG_LIB_SEL4 1
#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
#define CONFIG_LIB_SEL4_UTILS 1
#define CONFIG_LIB_SEL4_VSPACE 1
#define CONFIG_LIB_PLATSUPPORT 1
#define CONFIG_LIB_SEL4_ALLOCMAN 1
#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
#define CONFIG_LIB_SEL4_TEST 1
#define CONFIG_LIB_ELFLOADER 1
#define CONFIG_HAVE_LIB_SEL4_VSPACE 1
#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 167
#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0
#define CONFIG_CROSS_COMPILER_PREFIX "arm-none-eabi-"
#define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1
#define CONFIG_LIB_SEL4_MUSLC_SYS 1
#define CONFIG_HAVE_LIB_SEL4_TEST 1
#define CONFIG_LIB_MUSL_C 1
#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100
#define CONFIG_ARCH_ARM_V7A 1
#define CONFIG_USER_CFLAGS ""
#define CONFIG_HAVE_LIB_SEL4_DEBUG 1
#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1
#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1
#define CONFIG_DEBUG_BUILD 1
#define CONFIG_LIB_UTILS 1
#define CONFIG_OPTIMISATION_O2 1
#define CONFIG_HAVE_LIB_CPIO 1
#define CONFIG_HAVE_LIB_SEL4_VKA 1
#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1
#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1
#define CONFIG_USER_EXTRA_CFLAGS ""
#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
#define CONFIG_ARCH_ARM 1
#define CONFIG_HAVE_LIB_ELF 1
#define CONFIG_HAVE_LIB_PLATSUPPORT 1
#define CONFIG_ARM_MONITOR_MODE 1
#define CONFIG_NUM_DOMAINS 1
#define CONFIG_USER_DEBUG_INFO 1
#define CONFIG_HAVE_LIB_UTILS 1
#define CONFIG_USER_OPTIMISATION_O2 1
#define CONFIG_LIB_CPIO 1
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
#define CONFIG_ROOT_CNODE_SIZE_BITS 12
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_TESTPRINTER_REGEX ".*"
#define CONFIG_APP_SEL4TEST 1
#define CONFIG_HAVE_LIB_SEL4_UTILS 1
#define CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR 1
#define CONFIG_KERNEL_COMPILER ""
#define CONFIG_TIME_SLICE 5
#define CONFIG_ARCH_AARCH32 1
#define CONFIG_KERNEL_EXTRA_CPPFLAGS ""
#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128
#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1
#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576
#define CONFIG_ARM_MONITOR_HOOK 1

11
include/plat/tk1/plat/Makefile Normal file
View file

@ -0,0 +1,11 @@
#
# Copyright 2016, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile

226
include/plat/tk1/plat/machine.h Normal file
View file

@ -0,0 +1,226 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_H
#define __PLAT_MACHINE_H
#include <arch/machine/gic_pl390.h>
#define N_INTERRUPTS 192
enum IRQConstants {
INTERRUPT_SGI_0 = 0,
INTERRUPT_SGI_1 = 1,
INTERRUPT_SGI_2 = 2,
INTERRUPT_SGI_3 = 3,
INTERRUPT_SGI_4 = 4,
INTERRUPT_SGI_5 = 5,
INTERRUPT_SGI_6 = 6,
INTERRUPT_SGI_7 = 7,
INTERRUPT_SGI_8 = 8,
INTERRUPT_SGI_9 = 9,
INTERRUPT_SGI_10 = 10,
INTERRUPT_SGI_11 = 11,
INTERRUPT_SGI_12 = 12,
INTERRUPT_SGI_13 = 13,
INTERRUPT_SGI_14 = 14,
INTERRUPT_SGI_15 = 15,
INTERRUPT_PPI_0 = 16,
INTERRUPT_PPI_1 = 17,
INTERRUPT_PPI_2 = 18,
INTERRUPT_PPI_3 = 19,
INTERRUPT_PPI_4 = 20,
INTERRUPT_PPI_5 = 21,
INTERRUPT_PPI_6 = 22,
INTERRUPT_PPI_7 = 23,
INTERRUPT_PPI_8 = 24,
INTERRUPT_PPI_9 = 25,
INTERRUPT_PPI_10 = 26,
INTERRUPT_PPI_11 = 27,
INTERRUPT_PPI_12 = 28,
INTERRUPT_PPI_13 = 29,
INTERRUPT_PPI_14 = 30,
INTERRUPT_PPI_15 = 31,
INTERRUPT_TMR2 = 32,
INTERRUPT_TMR1 = 33,
INTERRUPT_RTC = 34,
INTERRUPT_CEC = 35,
INTERRUPT_SHR_SEM_INBOX_FULL = 36,
INTERRUPT_SHR_SEM_INBOX_EMPTY = 37,
INTERRUPT_SHR_SEM_OUTBOX_FULL = 38,
INTERRUPT_SHR_SEM_OUTBOX_EMPTY = 39,
INTERRUPT_VDE_UCQ = 40,
INTERRUPT_VDE_SYNC_TOKEN = 41,
INTERRUPT_VDE_BSEV = 42,
INTERRUPT_VDE_BSEA = 43,
INTERRUPT_VDE_SXE = 44,
INTERRUPT_SATA_RX_STAT = 45,
INTERRUPT_SDMMC1 = 46,
INTERRUPT_SDMMC2 = 47,
// RESERVED = 48,
INTERRUPT_VDE = 49,
INTERRUPT_AVP_UCQ = 50,
INTERRUPT_SDMMC3 = 51,
INTERRUPT_USB = 52,
INTERRUPT_KEYPAD = 53,
INTERRUPT_USB2 = 54,
// RESERVED = 55,
INTERRUPT_SATA_CTL = 56,
// RESERVED = 57,
INTERRUPT_VCP = 58,
INTERRUPT_APB_DMA_CPU = 59,
INTERRUPT_AHB_DMA_CPU = 60,
INTERRUPT_ARB_SEM_GNT_CPU = 61,
INTERRUPT_OWR = 62,
INTERRUPT_SDMMC4 = 63,
INTERRUPT_GPIO1 = 64,
INTERRUPT_GPIO2 = 65,
INTERRUPT_GPIO3 = 66,
INTERRUPT_GPIO4 = 67,
INTERRUPT_UARTA = 68,
INTERRUPT_UARTB = 69,
INTERRUPT_I2C = 70,
INTERRUPT_USB3_HOST = 71,
INTERRUPT_USB3_HOST_SMI = 72,
INTERRUPT_TMR3 = 73,
INTERRUPT_TMR4 = 74,
INTERRUPT_USB3_HOST_PME = 75,
INTERRUPT_USB3_DEV_HOST = 76,
INTERRUPT_ACTMON = 77,
INTERRUPT_UARTC = 78,
INTERRUPT_HSI = 79,
INTERRUPT_THERMAL = 80,
INTERRUPT_XUSB_PADCTL = 81,
INTERRUPT_TSEC = 82,
INTERRUPT_EDP = 83,
INTERRUPT_VFIR = 84,
INTERRUPT_I2C5 = 85,
INTERRUPT_STAT_MON = 86,
INTERRUPT_GPIO5 = 87,
INTERRUPT_USB3_DEV_SMI = 88,
INTERRUPT_USB3_DEV_PME = 89,
INTERRUPT_SE = 90,
INTERRUPT_SPI1 = 91,
INTERRUPT_APB_DMA_COP = 92,
INTERRUPT_AHB_DMA_COP = 93,
INTERRUPT_CLDVFS = 94,
INTERRUPT_I2C6 = 95,
INTERRUPT_HOST1X_SYNCPT_COP = 96,
INTERRUPT_HOST1X_SYNCPT_CPU = 97,
INTERRUPT_HOST1X_GEN_COP = 98,
INTERRUPT_HOST1X_GEN_CPU = 99,
INTERRUPT_MSENC = 100,
INTERRUPT_VI = 101,
INTERRUPT_ISPB = 102,
INTERRUPT_ISP = 103,
INTERRUPT_VIC = 104,
INTERRUPT_DISPLAY = 105,
INTERRUPT_DISPLAYB = 106,
INTERRUPT_HDMI = 107,
INTERRUPT_SOR = 108,
INTERRUPT_MC = 109,
INTERRUPT_EMC = 110,
INTERRUPT_SPI6 = 111,
// RESERVED = 112,
INTERRUPT_HDA = 113,
INTERRUPT_SPI2 = 114,
INTERRUPT_SPI3 = 115,
INTERRUPT_I2C2 = 116,
// RESERVED = 117,
INTERRUPT_PMU_EXT = 118,
INTERRUPT_GPIO6 = 119,
// RESERVED = 120,
INTERRUPT_GPIO7 = 121,
INTERRUPT_UARTD = 122,
// RESERVED = 123,
INTERRUPT_I2C3 = 124,
// RESERVED = 125,
// RESERVED = 126,
INTERRUPT_SW = 127,
INTERRUPT_SNOR = 128,
INTERRUPT_USB3 = 129,
INTERRUPT_PCIE_INT = 130,
INTERRUPT_PCIE_MSI = 131,
INTERRUPT_PCIE_WAKE = 132,
INTERRUPT_AVP_CACHE = 133,
// RESERVED = 134,
INTERRUPT_AUDIO_CLUSTER = 135,
INTERRUPT_APB_DMA_CH0 = 136,
INTERRUPT_APB_DMA_CH1 = 137,
INTERRUPT_APB_DMA_CH2 = 138,
INTERRUPT_APB_DMA_CH3 = 139,
INTERRUPT_APB_DMA_CH4 = 140,
INTERRUPT_APB_DMA_CH5 = 141,
INTERRUPT_APB_DMA_CH6 = 142,
INTERRUPT_APB_DMA_CH7 = 143,
INTERRUPT_APB_DMA_CH8 = 144,
INTERRUPT_APB_DMA_CH9 = 145,
INTERRUPT_APB_DMA_CH10 = 146,
INTERRUPT_APB_DMA_CH11 = 147,
INTERRUPT_APB_DMA_CH12 = 148,
INTERRUPT_APB_DMA_CH13 = 149,
INTERRUPT_APB_DMA_CH14 = 150,
INTERRUPT_APB_DMA_CH15 = 151,
INTERRUPT_I2C4 = 152,
INTERRUPT_TMR5 = 153,
INTERRUPT_HIER_GROUP1_COP = 154,
INTERRUPT_WDT_CPU = 155,
INTERRUPT_WDT_AVP = 156,
INTERRUPT_GPIO8 = 157,
INTERRUPT_CAR = 158,
INTERRUPT_HIER_GROUP1_CPU = 159,
INTERRUPT_APB_DMA_CH16 = 160,
INTERRUPT_APB_DMA_CH17 = 161,
INTERRUPT_APB_DMA_CH18 = 162,
INTERRUPT_APB_DMA_CH19 = 163,
INTERRUPT_APB_DMA_CH20 = 164,
INTERRUPT_APB_DMA_CH21 = 165,
INTERRUPT_APB_DMA_CH22 = 166,
INTERRUPT_APB_DMA_CH23 = 167,
INTERRUPT_APB_DMA_CH24 = 168,
INTERRUPT_APB_DMA_CH25 = 169,
INTERRUPT_APB_DMA_CH26 = 170,
INTERRUPT_APB_DMA_CH27 = 171,
INTERRUPT_APB_DMA_CH28 = 172,
INTERRUPT_APB_DMA_CH29 = 173,
INTERRUPT_APB_DMA_CH30 = 174,
INTERRUPT_APB_DMA_CH31 = 175,
INTERRUPT_CPU0_PMU = 176,
INTERRUPT_CPU1_PMU = 177,
INTERRUPT_CPU2_PMU = 178,
INTERRUPT_CPU3_PMU = 179,
INTERRUPT_SDMMC1_SYS = 180,
INTERRUPT_SDMMC2_SYS = 181,
INTERRUPT_SDMMC3_SYS = 182,
INTERRUPT_SDMMC4_SYS = 183,
INTERRUPT_TMR6 = 184,
INTERRUPT_TMR7 = 185,
INTERRUPT_TMR8 = 186,
INTERRUPT_TMR9 = 187,
INTERRUPT_TMR0 = 188,
INTERRUPT_GPU = 189,
INTERRUPT_GPU_NONSTALL = 190,
ARDPAUX = 191,
maxIRQ = 192
} platform_interrupt_t;
#define INTERRUPT_S_PGPT INTERRUPT_PPI_13
#define INTERRUPT_NS_PGPT INTERRUPT_PPI_14
#define INTERRUPT_VGPT INTERRUPT_PPI_11
#define INTERRUPT_HGPT INTERRUPT_PPI_10
/* the kernel runs in secure supervisor mode by default */
#define KERNEL_TIMER_IRQ INTERRUPT_S_PGPT
enum irqNumbers {
irqInvalid = 255
};
#endif /* ! __PLAT_MACHINE_H */

13
include/plat/tk1/plat/machine/Makefile Normal file
View file

@ -0,0 +1,13 @@
#
# Copyright 2016, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
DIRECTORIES += plat/machine
BF_SOURCES += plat/machine/hardware.bf

17
include/plat/tk1/plat/machine/debug_helpers.h Normal file
View file

@ -0,0 +1,17 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_DEBUG_HELPERS_H
#define __PLAT_MACHINE_DEBUG_HELPERS_H
#include <plat/machine/io.h>
#endif

108
include/plat/tk1/plat/machine/devices.h Normal file
View file

@ -0,0 +1,108 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_DEVICES_H
#define __PLAT_MACHINE_DEVICES_H
/* These devices are used by the seL4 kernel. */
#define UARTA_PPTR 0xfff01000
#define UARTB_PPTR 0xfff01040
#define UARTC_PPTR 0xfff01200
#define UARTD_PPTR 0xfff01300
#define GIC_DISTRIBUTOR_PPTR 0xfff03000
#define GIC_CONTROLLER_PPTR 0xfff04000
#define GIC_PL390_CONTROLLER_PPTR GIC_CONTROLLER_PPTR
#define GIC_PL390_DISTRIBUTOR_PPTR GIC_DISTRIBUTOR_PPTR
#define GIC_DISTRIBUTOR_PADDR GICD_PADDR
#define GIC_CONTROLLER0_PADDR GICI_PADDR
/*
* many of the device regions are not 4K page aligned, so some regions may contain more than
* one devices. it is the user's responsibilty to figure out how to use these regions
* */
#define ARM_PERIPHBASE (0x50040000) /* 128 KB */
#define GICD_PADDR (ARM_PERIPHBASE + 0x1000) /* interrupt distributor */
#define GICI_PADDR (ARM_PERIPHBASE + 0x2000) /* GIC CPU interface */
#define VGICI_REQ_PADDR (ARM_PERIPHBASE + 0x4000) /* hyp view for requesting CPU */
#define VGICI_ALL_PADDR (ARM_PERIPHBASE + 0x5000) /* hyp view for all CPUs */
#define VGICI_VM_PADDR (ARM_PERIPHBASE + 0x6000) /* hyp view for VM view */
#define GRAPH_HOST_PADDR (0x54000000) /* 16 MB */
#define GPU_PADDR (0x57000000) /* 144 MB */
#define UP_TAG_PADDR (0x60000000) /* 4 KB */
#define RSEM_PADDR (0x60001000) /* 4 KB */
#define ASEM_PADDR (0x60002000) /* 4 KB */
#define ARB_PRI_PADDR (0x60003000) /* 4 KB */
#define ICTLR_PADDR (0x60004000) /* 4 KB, includes several */
#define TMR_PADDR (0x60005000) /* 4 Kb, 1 KB */
#define CLK_RESET_PADDR (0x60006000) /* 4 KB */
#define FLOW_CTRL_PADDR (0x60007000) /* 4 KB */
#define AHB_DMA_PADDR (0x60008000) /* 8 KB */
#define AHB_DMA_CH_PADDR (0x60009000) /* 4 KB 4 channels, 32 bytes */
#define APB_DMA_PADDR (0x60020000) /* 16 KB */
#define APB_DMA_CH_PADDR (0x60021000) /* 4KB 32 channels, 64 bytes */
#define SYS_REGS_PADDR (0x6000c000) /* 768 bytes + 2 KB */
#define GPIO_PADDR (0x6000d000) /* 8 GPIOs, 265 bytes each */
#define VCP_PADDR (0x6000e000) /* 4 KB */
#define VPUCQ_PADDR (0x60010000) /* 256 Bytes */
#define BSEA_PADDR (0x60011000) /* 4 KB */
#define IPATCH_PADDR (0x6001d000) /* 4 KB offset 0xc00, 1 KB */
#define VDE_FRAMEID_PADDR (0x60030000) /* 16 KB, multiple */
#define MISC_PINMUX_PADDR (0x70000000) /* 16 KB */
#define UARTA_SYNC_PADDR (0x70006000) /* 12 KB, multiple */
#define SYNC_NOR_PADDR (0x70009000) /* 4 KB */
#define PWM_PADDR (0x7000a000) /* 4 KB, 256 bytes */
#define MIPIHSI_PADDR (0x7000b000) /* 4 KB */
#define I2C_I2C4_PADDR (0x7000c000) /* 4 KB */
#define I2C5_SPI2B_6_PADDR (0x7000d000) /* 4 KB */
#define RTC_KFUSE_PADDR (0x7000e000) /* 4 KB */
#define LA_PADDR (0x70010000) /* 8 KB */
#define SE_PADDR (0x70012000) /* 8 KB */
#define TSENSOR_PADDR (0x70014000) /* 4 KB */
#define CEC_PADDR (0x70015000) /* 4 KB */
#define ATOMICS_PADDR (0x70016000) /* 8 KB */
#define MC_PADDR (0x70019000) /* 4 KB */
#define EMC_PADDR (0x7001b000) /* 4 KB */
#define SATA_PADDR (0x70020000) /* 64 KB */
#define HDA_PADDR (0x70030000) /* 64 KB */
#define MIOBFM_PADDR (0x70200000) /* 64 KB */
#define AUDIO_PADDR (0x70300000) /* 64 KB */
#define XUSB_HOST_PADDR (0x70090000) /* 40 KB */
#define XUSB_DEV_PADDR (0x700d0000) /* 40 KB */
#define DDS_PADDR (0x700a0000) /* 8KB 4608 bytes */
#define SDMMC_1_PADDR (0x700b0000) /* 4KB 512 bytes */
#define SDMMC_1B_4_PADDR (0x700b1000) /* 60KB 512 bytes each */
#define SPEEDO_PADDR (0x700c0000) /* 32 KB */
#define SPEEDO_PMON_PADDR (0x700c8000) /* 32 KB */
#define SYSCTR0_PADDR (0x700f0000) /* 64 KB */
#define SYSCTR1_PADDR (0x70100000) /* 64 KB */
#define DP2_PADDR (0x700e0000) /* 256 Bytes */
#define APB2JTAG_PADDR (0x700e1000) /* 512 Bytes */
#define SOC_THERM_PADDR (0x700e2000) /* 4 KB */
#define MIPI_CAL_PADDR (0x700e3000) /* 265 Bytes */
#define DVFS_PADDR (0x70110000) /* 1 KB */
#define CLUSTER_CLK_PADDR (0x70040000) /* 256 KB */
#define CSITE_PADDR (0x70800000) /* 2 MB */
#define PPCS_PADDR (0x7c000000) /* 64 KB */
#define TZRAM_PADDR (0x7c010000) /* 64 KB */
#define USB_PADDR (0x7d000000) /* 8 KB region, 6 KB */
#define USB2_PADDR (0x7d004000) /* 8 KB region, 6 KB */
#define USB3_PADDR (0x7d008000) /* 8 KB region, 6 KB */
#define UARTA_PADDR 0x70006000
#endif

12
include/plat/tk1/plat/machine/hardware.bf Normal file
View file

@ -0,0 +1,12 @@
--
-- Copyright 2016, General Dynamics C4 Systems
--
-- This software may be distributed and modified according to the terms of
-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
-- See "LICENSE_GPLv2.txt" for details.
--
-- @TAG(GD_GPL)
--
base 32

87
include/plat/tk1/plat/machine/hardware.h Normal file
View file

@ -0,0 +1,87 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_MACHINE_HARDWARE_H
#define __PLAT_MACHINE_HARDWARE_H
#define physBase 0x80000000
#define kernelBase 0xe0000000
#define physMappingOffset (kernelBase - physBase)
#define BASE_OFFSET physMappingOffset
#define PPTR_TOP 0xfff00000
#define PADDR_TOP (PPTR_TOP - BASE_OFFSET)
#ifndef __ASSEMBLER__
#include <types.h>
#include <arch/object/structures.h>
#include <plat/machine.h>
#include <plat/machine/hardware_gen.h>
static inline void* CONST
ptrFromPAddr(paddr_t paddr)
{
return (void*)(paddr + physMappingOffset);
}
static inline paddr_t CONST
addrFromPPtr(void* pptr)
{
return (paddr_t)pptr - physMappingOffset;
}
#define paddr_to_pptr ptrFromPAddr
#define pptr_to_paddr addrFromPPtr
static inline region_t CONST
paddr_to_pptr_reg(p_region_t p_reg)
{
return (region_t) {
p_reg.start + physMappingOffset, p_reg.end + physMappingOffset
};
}
static inline p_region_t CONST
pptr_to_paddr_reg(region_t reg)
{
return (p_region_t) {
reg.start - physMappingOffset, reg.end - physMappingOffset
};
}
int get_num_avail_p_regs(void);
p_region_t get_avail_p_reg(word_t i);
int get_num_dev_p_regs(void);
p_region_t get_dev_p_reg(word_t i);
void map_kernel_devices(void);
bool_t CONST isReservedIRQ(irq_t irq);
void handleReservedIRQ(irq_t irq);
/** MODIFIES: [*] */
void resetTimer(void);
/** MODIFIES: [*] */
void initTimer(void);
/* L2 cache control */
/** MODIFIES: [*] */
void initL2Cache(void);
/** MODIFIES: [*] */
static inline void plat_cleanL2Range(paddr_t start, paddr_t end) {}
/** MODIFIES: [*] */
static inline void plat_invalidateL2Range(paddr_t start, paddr_t end) {}
/** MODIFIES: [*] */
static inline void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end) {}
#endif /* !__ASSEMBLER__ */
#endif

26
include/plat/tk1/plat/machine/io.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#ifndef __PLAT_IO_H
#define __PLAT_IO_H
#include <types.h>
#if defined DEBUG || defined RELEASE_PRINTF
void tk1_uart_putchar(char c);
void putDebugChar(unsigned char c);
unsigned char getDebugChar(void);
#define kernel_putchar(c) tk1_uart_putchar(c)
#else /* !DEBUG */
#define kernel_putchar(c) ((void)(0))
#endif
#endif

56
libsel4/include/sel4/bootinfo.h
View file

@ -12,61 +12,7 @@
#define __LIBSEL4_BOOTINFO_H
#include <sel4/types.h>
/* caps with fixed slot potitions in the root CNode */
enum {
seL4_CapNull = 0, /* null cap */
seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
seL4_CapIRQControl = 4, /* global IRQ controller cap */
seL4_CapASIDControl = 5, /* global ASID controller cap */
seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
seL4_CapIOPort = 7, /* global IO port cap (null cap if not supported) */
seL4_CapIOSpace = 8, /* global IO space cap (null cap if no IOMMU support) */
seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
seL4_CapDomain = 11, /* global domain controller cap */
seL4_NumInitialCaps = 12
};
/* Legacy code will have assumptions on the vspace root being a Page Directory
* type, so for now we define one to the other */
#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
/* types */
typedef struct {
seL4_Word start; /* first CNode slot position OF region */
seL4_Word end; /* first CNode slot position AFTER region */
} seL4_SlotRegion;
typedef struct {
seL4_Word basePaddr; /* base physical address of device region */
seL4_Uint32 frameSizeBits; /* size (2^n bytes) of a device-region frame */
seL4_SlotRegion frames; /* device-region frame caps */
} seL4_DeviceRegion;
typedef struct {
seL4_Word nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
seL4_Uint32 numNodes; /* number of seL4 nodes (1 if uniprocessor) */
seL4_Uint32 numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
seL4_IPCBuffer* ipcBuffer; /* pointer to initial thread's IPC buffer */
seL4_SlotRegion empty; /* empty slots (null caps) */
seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
seL4_SlotRegion userImageFrames; /* userland-image frame caps */
seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
seL4_Word untypedPaddrList [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each untyped cap */
seL4_Uint8 untypedSizeBitsList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each untyped cap */
seL4_Uint8 initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
seL4_Uint32 numDeviceRegions; /* number of device regions */
seL4_DeviceRegion deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
seL4_Uint32 initThreadDomain; /* Initial thread's domain ID */
} seL4_BootInfo;
/* function declarations */
#include <sel4/bootinfo_types.h>
void seL4_InitBootInfo(seL4_BootInfo* bi);
seL4_BootInfo* seL4_GetBootInfo(void);

69
libsel4/include/sel4/bootinfo_types.h Normal file
View file

@ -0,0 +1,69 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_BOOTINFO_TYPES_H
#define __LIBSEL4_BOOTINFO_TYPES_H
/* caps with fixed slot potitions in the root CNode */
enum {
seL4_CapNull = 0, /* null cap */
seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
seL4_CapIRQControl = 4, /* global IRQ controller cap */
seL4_CapASIDControl = 5, /* global ASID controller cap */
seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
seL4_CapIOPort = 7, /* global IO port cap (null cap if not supported) */
seL4_CapIOSpace = 8, /* global IO space cap (null cap if no IOMMU support) */
seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
seL4_CapDomain = 11, /* global domain controller cap */
seL4_NumInitialCaps = 12
};
/* Legacy code will have assumptions on the vspace root being a Page Directory
* type, so for now we define one to the other */
#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
/* types */
typedef seL4_Word seL4_SlotPos;
typedef struct {
seL4_SlotPos start; /* first CNode slot position OF region */
seL4_SlotPos end; /* first CNode slot position AFTER region */
} seL4_SlotRegion;
typedef struct {
seL4_Word basePaddr; /* base physical address of device region */
seL4_Word frameSizeBits; /* size (2^n bytes) of a device-region frame */
seL4_SlotRegion frames; /* device-region frame caps */
} seL4_DeviceRegion;
typedef struct {
seL4_NodeId nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
seL4_Word numNodes; /* number of seL4 nodes (1 if uniprocessor) */
seL4_Word numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
seL4_IPCBuffer* ipcBuffer; /* pointer to initial thread's IPC buffer */
seL4_SlotRegion empty; /* empty slots (null caps) */
seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
seL4_SlotRegion userImageFrames; /* userland-image frame caps */
seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
seL4_PAddr untypedPaddrList [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each untyped cap */
seL4_Uint8 untypedSizeBitsList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each untyped cap */
seL4_Uint8 initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
seL4_Word numDeviceRegions; /* number of device regions */
seL4_DeviceRegion deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
seL4_Domain initThreadDomain; /* Initial thread's domain ID */
} seL4_BootInfo;
#endif // __LIBSEL4_BOOTINFO_TYPES_H

3
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/types.h
View file

@ -15,6 +15,9 @@
typedef seL4_Uint32 seL4_Word;
typedef seL4_Word seL4_CPtr;
typedef seL4_Word seL4_NodeId;
typedef seL4_Word seL4_PAddr;
typedef seL4_Word seL4_Domain;
typedef struct seL4_UserContext_ {
/* frame registers */

4
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/types.h
View file

@ -14,6 +14,10 @@
#include <autoconf.h>
typedef seL4_Uint32 seL4_Word;
typedef seL4_Word seL4_NodeId;
typedef seL4_Word seL4_PAddr;
typedef seL4_Word seL4_Domain;
typedef seL4_Word seL4_CPtr;
/* User context as used by seL4_TCB_ReadRegisters / seL4_TCB_WriteRegisters */

6
manual/parts/api.tex
View file

@ -98,6 +98,7 @@
\newcommand{\messageinforetdesc}{A \texttt{seL4\_MessageInfo\_t} structure as described in \autoref{sec:messageinfo}.}
\newcommand{\noret}{This method does not return anything.}
\newcommand{\errorenumdesc}{A return value of \texttt{0} indicates success. A non-zero value indicates that an error occurred. See \autoref{sec:errors} for a description of the message register and tag contents upon error.}
\newcommand{\pagegetaddresstdesc}{struct that contains \texttt{seL4\_Word paddr}, which holds the physical address of the page, and \texttt{int error}. See \autoref{sec:errors} for a description of the message register and tag contents upon error.}
\newcommand{\domcapdesc}{Capability allowing domain configuration.}
\newcommand{\domargdesc}{The thread's new domain.}
@ -312,7 +313,10 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request.
\label{sec:kobj_api_arm}
\inputapidoc{arm_asidcontrol_makepool}
\inputapidoc{arm_asidpool_assign}
\inputapidoc{arm_page_flushcaches}
\inputapidoc{arm_page_cleandata}
\inputapidoc{arm_page_invalidatedata}
\inputapidoc{arm_page_cleaninvalidatedata}
\inputapidoc{arm_page_unifyinstruction}
\inputapidoc{arm_page_map}
\inputapidoc{arm_page_remap}
\inputapidoc{arm_page_unmap}

23
manual/parts/api/arm_page_cleandata.tex Normal file
View file

@ -0,0 +1,23 @@
%
% Copyright 2016, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%
\apidoc
{arm_page_cleandata}
{ARM Page - Clean Data}
{Cleans the data cache out to RAM. The start and end are relative to the page being serviced.}
{static inline int seL4\_ARM\_Page\_Clean\_Data}
{
\param{seL4\_ARM\_Page}{\_service}{The page whose contents will be flushed.}
\param{seL4\_Word}{start\_offset}{The offset, relative to the start of the page inclusive.}
\param{seL4\_Word}{end\_offset}{The offset, relative to the start of the page exclusive.}
}
{\errorenumdesc}
{See \autoref{ch:vspace}}

23
manual/parts/api/arm_page_cleaninvalidatedata.tex Normal file
View file

@ -0,0 +1,23 @@
%
% Copyright 2016, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%
\apidoc
{arm_page_cleaninvalidatedata}
{ARM Page - Clean and Invalidate Data}
{Clean and invalidates the cache range within the given page. The range will be flushed out to RAM. The start and end are relative to the page being serviced.}
{static inline int seL4\_ARM\_Page\_CleanInvalidate\_Data}
{
\param{seL4\_ARM\_Page}{\_service}{The page whose contents will be flushed.}
\param{seL4\_Word}{start\_offset}{The offset, relative to the start of the page inclusive.}
\param{seL4\_Word}{end\_offset}{The offset, relative to the start of the page exclusive.}
}
{\errorenumdesc}
{See \autoref{ch:vspace}}

20
manual/parts/api/arm_page_flushcaches.tex
View file

@ -1,20 +0,0 @@
%
% Copyright 2014, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%
\apidoc
{arm_page_flushcaches}
{ARM Page - Flush Caches}
{Flush a cache range}
{static inline int seL4\_ARM\_Page\_FlushCaches}
{
\param{seL4\_ARM\_Page}{\_service}{The page whose contents will be flushed.}
}
{\errorenumdesc}
{See \autoref{ch:vspace}}

2
manual/parts/api/arm_page_getaddress.tex
View file

@ -16,5 +16,5 @@
{
\param{seL4\_ARM\_Page}{\_service}{Capability to the page to lookup.}
}
{A seL4\_ARM\_Page\_GetAddress\_t structure as described in TODO}
{A seL4\_ARM\_Page\_GetAddress\_t \pagegetaddresstdesc}
{See \autoref{ch:vspace}}

26
manual/parts/api/arm_page_invalidatedata.tex Normal file
View file

@ -0,0 +1,26 @@
%
% Copyright 2016, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%
\apidoc
{arm_page_invalidatedata}
{ARM Page - Invalidate Data}
{Invalidates the cache range within the given page. The start and end are relative to the page being serviced
and should be aligned to a cache line boundary where possible.
An additional clean is performed on the outer cache lines if the start and end are
not aligned, to clean out the bytes between the requested and the cache line boundary.}
{static inline int seL4\_ARM\_Page\_Invalidate\_Data}
{
\param{seL4\_ARM\_Page}{\_service}{The page whose contents will be flushed.}
\param{seL4\_Word}{start\_offset}{The offset, relative to the start of the page inclusive.}
\param{seL4\_Word}{end\_offset}{The offset, relative to the start of the page exclusive.}
}
{\errorenumdesc}
{See \autoref{ch:vspace}}

26
manual/parts/api/arm_page_unifyinstruction.tex Normal file
View file

@ -0,0 +1,26 @@
%
% Copyright 2016, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%
\apidoc
{arm_page_unifyinstruction}
{ARM Page - Unify Instruction Cache}
{Unify Instruction Cache. Cleans data lines to point of unification, invalidate
corresponding instruction lines to point of unification, then invalidates branch
predictors. The start and end are relative to the page being
serviced.}
{static inline int seL4\_ARM\_Page\_Unify\_Instruction}
{
\param{seL4\_ARM\_Page}{\_service}{The page whose contents will be flushed.}
\param{seL4\_Word}{start\_offset}{The offset, relative to the start of the page inclusive.}
\param{seL4\_Word}{end\_offset}{The offset, relative to the start of the page exclusive.}
}
{\errorenumdesc}
{See \autoref{ch:vspace}}

2
manual/parts/api/ia32_page_getaddress.tex
View file

@ -16,5 +16,5 @@
{
\param{seL4\_IA32\_Page}{\_service}{Capability to the page to lookup.}
}
{A seL4\_IA32\_Page\_GetAddress\_t structure as described in TODO}
{A \texttt{seL4\_IA32\_Page\_GetAddress\_t} \pagegetaddresstdesc}
{See \autoref{ch:vspace}}

30
src/arch/arm/32/kernel/vspace.c
View file

@ -565,8 +565,8 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
cap_t pd_cap;
vptr_t pt_vptr;
pptr_t pt_pptr;
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
pptr_t pd_pptr;
/* create PD obj and cap */
@ -585,7 +585,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
pd_pptr /* capPDBasePtr */
);
slot_pos_before = ndks_boot.slot_pos_cur;
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pd_cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pd_cap);
/* create all PT objs and caps necessary to cover userland image */
@ -605,7 +605,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->ui_paging_caps = (slot_region_t) {
ndks_boot.bi_frame->userImagePaging = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
@ -615,22 +615,22 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
BOOT_CODE bool_t
create_device_frames(cap_t root_cnode_cap)
{
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
vm_page_size_t frame_size;
region_t dev_reg;
bi_dev_reg_t bi_dev_reg;
seL4_DeviceRegion bi_dev_reg;
cap_t frame_cap;
word_t i;
pptr_t f;
ndks_boot.bi_frame->num_dev_regs = get_num_dev_p_regs();
if (ndks_boot.bi_frame->num_dev_regs > CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS) {
ndks_boot.bi_frame->numDeviceRegions = get_num_dev_p_regs();
if (ndks_boot.bi_frame->numDeviceRegions > CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS) {
printf("Kernel init: Too many device regions for boot info\n");
ndks_boot.bi_frame->num_dev_regs = CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS;
ndks_boot.bi_frame->numDeviceRegions = CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS;
}
for (i = 0; i < ndks_boot.bi_frame->num_dev_regs; i++) {
for (i = 0; i < ndks_boot.bi_frame->numDeviceRegions; i++) {
/* write the frame caps of this device region into the root CNode and update the bootinfo */
dev_reg = paddr_to_pptr_reg(get_dev_p_reg(i));
/* use 1M frames if possible, otherwise use 4K frames */
@ -654,12 +654,12 @@ create_device_frames(cap_t root_cnode_cap)
slot_pos_after = ndks_boot.slot_pos_cur;
/* add device-region entry to bootinfo */
bi_dev_reg.base_paddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frame_size_bits = pageBitsForSize(frame_size);
bi_dev_reg.frame_caps = (slot_region_t) {
bi_dev_reg.basePaddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frameSizeBits = pageBitsForSize(frame_size);
bi_dev_reg.frames = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
ndks_boot.bi_frame->dev_reg_list[i] = bi_dev_reg;
ndks_boot.bi_frame->deviceRegions[i] = bi_dev_reg;
}
return true;

3
src/arch/arm/armv/armv7-a/machine_asm.S
View file

@ -59,6 +59,9 @@ BEGIN_FUNC(lockTLBEntry)
add r3, r3, #1
mov r2, #0
orr r2, r2, r3, lsl #28
#elif defined(ARM_CORTEX_A7)
/* CORTEX A7 does not support TLB lockdown */
bx lr
#else
# error Undefined CPU for TLB lockdown
#endif

7
src/arch/arm/kernel/boot.c
View file

@ -136,10 +136,9 @@ init_irqs(cap_t root_cnode_cap)
}
/* provide the IRQ control cap */
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IRQ_CTRL), cap_irq_control_cap_new());
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
}
/* This and only this function initialises the CPU. It does NOT initialise any kernel state. */
BOOT_CODE static void
@ -268,7 +267,7 @@ try_init_kernel(
if (!create_frames_ret.success) {
return false;
}
ndks_boot.bi_frame->ui_frame_caps = create_frames_ret.region;
ndks_boot.bi_frame->userImageFrames = create_frames_ret.region;
/* create/initialise the initial thread's ASID pool */
it_ap_cap = create_it_asid_pool(root_cnode_cap);
@ -316,7 +315,7 @@ try_init_kernel(
}
/* no shared-frame caps (ARM has no multikernel support) */
ndks_boot.bi_frame->sh_frame_caps = S_REG_EMPTY;
ndks_boot.bi_frame->sharedFrames = S_REG_EMPTY;
/* finalise the bootinfo frame */
bi_finalise();

2
src/arch/arm/machine/Makefile
View file

@ -26,7 +26,7 @@ endif
endif
ifeq ($(CPU), cortex-a15)
ifeq ($(CPU), $(filter $(CPU), cortex-a15 cortex-a7))
# A15 uses the gic_pl400 which is an extention of pl390
ARCH_C_SOURCES += machine/gic_pl390.c
endif

10
src/arch/x86/32/kernel/vspace.c
View file

@ -439,8 +439,8 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
cap_t vspace_cap;
vptr_t vptr;
pptr_t pptr;
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
slot_pos_before = ndks_boot.slot_pos_cur;
if (PDPT_BITS == 0) {
@ -457,7 +457,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
if (!provide_cap(root_cnode_cap, pd_cap)) {
return cap_null_cap_new();
}
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pd_cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pd_cap);
vspace_cap = pd_cap;
} else {
cap_t pdpt_cap;
@ -505,7 +505,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
/* now that PDs exist we can copy the global mappings */
copyGlobalMappings((vspace_root_t*)pdpt_pptr);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pdpt_cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pdpt_cap);
vspace_cap = pdpt_cap;
}
@ -527,7 +527,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->ui_paging_caps = (slot_region_t) {
ndks_boot.bi_frame->userImagePaging = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};

28
src/arch/x86/kernel/boot.c
View file

@ -59,7 +59,7 @@ init_irqs(cap_t root_cnode_cap)
}
Arch_irqStateInit();
/* provide the IRQ control cap */
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IRQ_CTRL), cap_irq_control_cap_new());
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
}
BOOT_CODE static bool_t
@ -68,11 +68,11 @@ create_device_frames(
dev_p_regs_t* dev_p_regs
)
{
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
vm_page_size_t frame_size;
region_t dev_reg;
bi_dev_reg_t bi_dev_reg;
seL4_DeviceRegion bi_dev_reg;
cap_t frame_cap;
uint32_t i;
pptr_t f;
@ -101,15 +101,15 @@ create_device_frames(
slot_pos_after = ndks_boot.slot_pos_cur;
/* add device-region entry to bootinfo */
bi_dev_reg.base_paddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frame_size_bits = pageBitsForSize(frame_size);
bi_dev_reg.frame_caps = (slot_region_t) {
bi_dev_reg.basePaddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frameSizeBits = pageBitsForSize(frame_size);
bi_dev_reg.frames = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
ndks_boot.bi_frame->dev_reg_list[i] = bi_dev_reg;
ndks_boot.bi_frame->deviceRegions[i] = bi_dev_reg;
}
ndks_boot.bi_frame->num_dev_regs = dev_p_regs->count;
ndks_boot.bi_frame->numDeviceRegions = dev_p_regs->count;
return true;
}
@ -219,7 +219,7 @@ init_sys_state(
/* create the IO port cap */
write_slot(
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IO_PORT),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIOPort),
cap_io_port_cap_new(
0, /* first port */
NUM_IO_PORTS - 1 /* last port */
@ -276,7 +276,7 @@ init_sys_state(
if (!create_frames_ret.success) {
return false;
}
ndks_boot.bi_frame->ui_frame_caps = create_frames_ret.region;
ndks_boot.bi_frame->userImageFrames = create_frames_ret.region;
/* create the initial thread's ASID pool */
it_ap_cap = create_it_asid_pool(root_cnode_cap);
@ -318,12 +318,12 @@ init_sys_state(
}
/* write number of IOMMU PT levels into bootinfo */
ndks_boot.bi_frame->num_iopt_levels = x86KSnumIOPTLevels;
ndks_boot.bi_frame->numIOPTLevels = x86KSnumIOPTLevels;
/* write IOSpace master cap */
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IO_SPACE), master_iospace_cap());
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIOSpace), master_iospace_cap());
} else {
ndks_boot.bi_frame->num_iopt_levels = -1;
ndks_boot.bi_frame->numIOPTLevels = -1;
}
/* convert the remaining free memory into UT objects and provide the caps */

8
src/fastpath/fastpath.c
View file

@ -86,9 +86,9 @@ fastpath_call(word_t cptr, word_t msgInfo)
slowpath(SysCall);
}
/* Ensure that the endpoint has standard non-diminishing rights. */
if (unlikely(!cap_endpoint_cap_get_capCanGrant(ep_cap) ||
thread_state_ptr_get_blockingIPCDiminishCaps(&dest->tcbState))) {
/* Ensure that the endpoint has has grant rights so that we can
* create the reply cap */
if (unlikely(!cap_endpoint_cap_get_capCanGrant(ep_cap))) {
slowpath(SysCall);
}
@ -273,8 +273,6 @@ fastpath_reply_recv(word_t cptr, word_t msgInfo)
/* Set thread state to BlockedOnReceive */
thread_state_ptr_mset_blockingObject_tsType(
&ksCurThread->tcbState, (word_t)ep_ptr, ThreadState_BlockedOnReceive);
thread_state_ptr_set_blockingIPCDiminish_np(
&ksCurThread->tcbState, ! cap_endpoint_cap_get_capCanSend(ep_cap));
/* Place the thread in the endpoint queue */
endpointTail = TCB_PTR(endpoint_ptr_get_epQueue_tail(ep_ptr));

64
src/kernel/boot.c
View file

@ -131,7 +131,7 @@ write_slot(slot_ptr_t slot_ptr, cap_t cap)
*/
compile_assert(root_cnode_size_valid,
CONFIG_ROOT_CNODE_SIZE_BITS < 32 - seL4_SlotBits &&
(1U << CONFIG_ROOT_CNODE_SIZE_BITS) >= BI_CAP_DYN_START)
(1U << CONFIG_ROOT_CNODE_SIZE_BITS) >= seL4_NumInitialCaps)
BOOT_CODE cap_t
create_root_cnode(void)
@ -158,7 +158,7 @@ create_root_cnode(void)
);
/* write the root CNode cap into the root CNode */
write_slot(SLOT_PTR(pptr, BI_CAP_IT_CNODE), cap);
write_slot(SLOT_PTR(pptr, seL4_CapInitThreadCNode), cap);
return cap;
}
@ -200,7 +200,7 @@ create_domain_cap(cap_t root_cnode_cap)
}
cap = cap_domain_cap_new();
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_DOM), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapDomain), cap);
}
@ -220,7 +220,7 @@ create_ipcbuf_frame(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr)
/* create a cap of it and write it into the root CNode */
cap = create_mapped_it_frame_cap(pd_cap, pptr, vptr, IT_ASID, false, false);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), cap);
return cap;
}
@ -237,7 +237,7 @@ create_bi_frame_cap(
/* create a cap of it and write it into the root CNode */
cap = create_mapped_it_frame_cap(pd_cap, pptr, vptr, IT_ASID, false, false);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_BI_FRAME), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapBootInfoFrame), cap);
}
BOOT_CODE pptr_t
@ -259,14 +259,14 @@ allocate_bi_frame(
/* initialise bootinfo-related global state */
ndks_boot.bi_frame = BI_PTR(pptr);
ndks_boot.slot_pos_cur = BI_CAP_DYN_START;
ndks_boot.slot_pos_cur = seL4_NumInitialCaps;
BI_PTR(pptr)->node_id = node_id;
BI_PTR(pptr)->num_nodes = num_nodes;
BI_PTR(pptr)->num_iopt_levels = 0;
BI_PTR(pptr)->ipcbuf_vptr = ipcbuf_vptr;
BI_PTR(pptr)->it_cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS;
BI_PTR(pptr)->it_domain = ksDomSchedule[ksDomScheduleIdx].domain;
BI_PTR(pptr)->nodeID = node_id;
BI_PTR(pptr)->numNodes = num_nodes;
BI_PTR(pptr)->numIOPTLevels = 0;
BI_PTR(pptr)->ipcBuffer = (seL4_IPCBuffer *) ipcbuf_vptr;
BI_PTR(pptr)->initThreadCNodeSizeBits = CONFIG_ROOT_CNODE_SIZE_BITS;
BI_PTR(pptr)->initThreadDomain = ksDomSchedule[ksDomScheduleIdx].domain;
return pptr;
}
@ -294,8 +294,8 @@ create_frames_of_region(
{
pptr_t f;
cap_t frame_cap;
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
slot_pos_before = ndks_boot.slot_pos_cur;
@ -314,7 +314,7 @@ create_frames_of_region(
slot_pos_after = ndks_boot.slot_pos_cur;
return (create_frames_of_region_ret_t) {
(slot_region_t) { slot_pos_before, slot_pos_after }, true
(seL4_SlotRegion) { slot_pos_before, slot_pos_after }, true
};
}
@ -332,11 +332,11 @@ create_it_asid_pool(cap_t root_cnode_cap)
}
memzero(ASID_POOL_PTR(ap_pptr), 1 << seL4_ASIDPoolBits);
ap_cap = cap_asid_pool_cap_new(IT_ASID >> asidLowBits, ap_pptr);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_ASID_POOL), ap_cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadASIDPool), ap_cap);
/* create ASID control cap */
write_slot(
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_ASID_CTRL),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapASIDControl),
cap_asid_control_cap_new()
);
@ -385,7 +385,7 @@ create_initial_thread(
Arch_initContext(&tcb->tcbArch.tcbContext);
/* derive a copy of the IPC buffer cap for inserting */
dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), ipcbuf_cap);
dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), ipcbuf_cap);
if (dc_ret.status != EXCEPTION_NONE) {
printf("Failed to derive copy of IPC Buffer\n");
return false;
@ -394,17 +394,17 @@ create_initial_thread(
/* initialise TCB (corresponds directly to abstract specification) */
cteInsert(
root_cnode_cap,
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_CNODE),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadCNode),
SLOT_PTR(pptr, tcbCTable)
);
cteInsert(
it_pd_cap,
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace),
SLOT_PTR(pptr, tcbVTable)
);
cteInsert(
dc_ret.cap,
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer),
SLOT_PTR(pptr, tcbBuffer)
);
tcb->tcbIPCBuffer = ipcbuf_vptr;
@ -423,7 +423,7 @@ create_initial_thread(
/* create initial thread's TCB cap */
cap = cap_thread_cap_new(TCB_REF(tcb));
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_TCB), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadTCB), cap);
#ifdef DEBUG
setThreadName(tcb, "rootserver");
@ -437,14 +437,14 @@ provide_untyped_cap(
cap_t root_cnode_cap,
pptr_t pptr,
word_t size_bits,
slot_pos_t first_untyped_slot
seL4_SlotPos first_untyped_slot
)
{
bool_t ret;
word_t i = ndks_boot.slot_pos_cur - first_untyped_slot;
if (i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS) {
ndks_boot.bi_frame->ut_obj_paddr_list[i] = pptr_to_paddr((void*)pptr);
ndks_boot.bi_frame->ut_obj_size_bits_list[i] = size_bits;
ndks_boot.bi_frame->untypedPaddrList[i] = pptr_to_paddr((void*)pptr);
ndks_boot.bi_frame->untypedSizeBitsList[i] = size_bits;
ret = provide_cap(root_cnode_cap, cap_untyped_cap_new(0, size_bits, pptr));
} else {
printf("Kernel init: Too many untyped regions for boot info\n");
@ -465,7 +465,7 @@ BOOT_CODE static bool_t
create_untypeds_for_region(
cap_t root_cnode_cap,
region_t reg,
slot_pos_t first_untyped_slot
seL4_SlotPos first_untyped_slot
)
{
word_t align_bits;
@ -495,8 +495,8 @@ create_untypeds_for_region(
BOOT_CODE bool_t
create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
{
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
word_t i;
region_t reg;
@ -517,7 +517,7 @@ create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->ut_obj_caps = (slot_region_t) {
ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
return true;
@ -526,9 +526,9 @@ create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
BOOT_CODE void
bi_finalise(void)
{
slot_pos_t slot_pos_start = ndks_boot.slot_pos_cur;
slot_pos_t slot_pos_end = ndks_boot.slot_pos_max;
ndks_boot.bi_frame->null_caps = (slot_region_t) {
seL4_SlotPos slot_pos_start = ndks_boot.slot_pos_cur;
seL4_SlotPos slot_pos_end = ndks_boot.slot_pos_max;
ndks_boot.bi_frame->empty = (seL4_SlotRegion) {
slot_pos_start, slot_pos_end
};
}

20
src/kernel/thread.c
View file

@ -25,7 +25,7 @@
static seL4_MessageInfo_t
transferCaps(seL4_MessageInfo_t info, extra_caps_t caps,
endpoint_t *endpoint, tcb_t *receiver,
word_t *receiveBuffer, bool_t diminish);
word_t *receiveBuffer);
static inline bool_t PURE
isBlocked(const tcb_t *thread)
@ -110,7 +110,7 @@ restart(tcb_t *target)
void
doIPCTransfer(tcb_t *sender, endpoint_t *endpoint, word_t badge,
bool_t grant, tcb_t *receiver, bool_t diminish)
bool_t grant, tcb_t *receiver)
{
void *receiveBuffer, *sendBuffer;
@ -119,7 +119,7 @@ doIPCTransfer(tcb_t *sender, endpoint_t *endpoint, word_t badge,
if (likely(!fault_get_faultType(sender->tcbFault) != fault_null_fault)) {
sendBuffer = lookupIPCBuffer(false, sender);
doNormalTransfer(sender, sendBuffer, endpoint, badge, grant,
receiver, receiveBuffer, diminish);
receiver, receiveBuffer);
} else {
doFaultTransfer(badge, sender, receiver, receiveBuffer);
}
@ -132,7 +132,7 @@ doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot)
ThreadState_BlockedOnReply);
if (likely(fault_get_faultType(receiver->tcbFault) == fault_null_fault)) {
doIPCTransfer(sender, NULL, 0, true, receiver, false);
doIPCTransfer(sender, NULL, 0, true, receiver);
/** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
cteDeleteOne(slot);
setThreadState(receiver, ThreadState_Running);
@ -156,7 +156,7 @@ doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot)
void
doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint,
word_t badge, bool_t canGrant, tcb_t *receiver,
word_t *receiveBuffer, bool_t diminish)
word_t *receiveBuffer)
{
word_t msgTransferred;
seL4_MessageInfo_t tag;
@ -179,7 +179,7 @@ doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint,
msgTransferred = copyMRs(sender, sendBuffer, receiver, receiveBuffer,
seL4_MessageInfo_get_length(tag));
tag = transferCaps(tag, caps, endpoint, receiver, receiveBuffer, diminish);
tag = transferCaps(tag, caps, endpoint, receiver, receiveBuffer);
tag = seL4_MessageInfo_set_length(tag, msgTransferred);
setRegister(receiver, msgInfoRegister, wordFromMessageInfo(tag));
@ -204,7 +204,7 @@ doFaultTransfer(word_t badge, tcb_t *sender, tcb_t *receiver,
static seL4_MessageInfo_t
transferCaps(seL4_MessageInfo_t info, extra_caps_t caps,
endpoint_t *endpoint, tcb_t *receiver,
word_t *receiveBuffer, bool_t diminish)
word_t *receiveBuffer)
{
word_t i;
cte_t* destSlot;
@ -239,11 +239,7 @@ transferCaps(seL4_MessageInfo_t info, extra_caps_t caps,
break;
}
if (diminish) {
dc_ret = deriveCap(slot, maskCapRights(noWrite, cap));
} else {
dc_ret = deriveCap(slot, cap);
}
dc_ret = deriveCap(slot, cap);
if (dc_ret.status != EXCEPTION_NONE) {
break;

15
src/object/endpoint.c
View file

@ -71,7 +71,6 @@ sendIPC(bool_t blocking, bool_t do_call, word_t badge,
case EPState_Recv: {
tcb_queue_t queue;
tcb_t *dest;
bool_t diminish;
/* Get the head of the endpoint queue. */
queue = ep_ptr_get_queue(epptr);
@ -89,16 +88,14 @@ sendIPC(bool_t blocking, bool_t do_call, word_t badge,
}
/* Do the transfer */
diminish =
thread_state_get_blockingIPCDiminishCaps(dest->tcbState);
doIPCTransfer(thread, epptr, badge, canGrant, dest, diminish);
doIPCTransfer(thread, epptr, badge, canGrant, dest);
setThreadState(dest, ThreadState_Running);
attemptSwitchTo(dest);
if (do_call ||
fault_ptr_get_faultType(&thread->tcbFault) != fault_null_fault) {
if (canGrant && !diminish) {
if (canGrant) {
setupCallerCap(thread, dest);
} else {
setThreadState(thread, ThreadState_Inactive);
@ -114,14 +111,12 @@ void
receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
{
endpoint_t *epptr;
bool_t diminish;
notification_t *ntfnPtr;
/* Haskell error "receiveIPC: invalid cap" */
assert(cap_get_capType(cap) == cap_endpoint_cap);
epptr = EP_PTR(cap_endpoint_cap_get_capEPPtr(cap));
diminish = !cap_endpoint_cap_get_capCanSend(cap);
/* Check for anything waiting in the notification */
ntfnPtr = thread->tcbBoundNotification;
@ -139,8 +134,6 @@ receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
ThreadState_BlockedOnReceive);
thread_state_ptr_set_blockingObject(
&thread->tcbState, EP_REF(epptr));
thread_state_ptr_set_blockingIPCDiminishCaps(
&thread->tcbState, diminish);
scheduleTCB(thread);
@ -184,13 +177,13 @@ receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
/* Do the transfer */
doIPCTransfer(sender, epptr, badge,
canGrant, thread, diminish);
canGrant, thread);
do_call = thread_state_ptr_get_blockingIPCIsCall(&sender->tcbState);
if (do_call ||
fault_get_faultType(sender->tcbFault) != fault_null_fault) {
if (canGrant && !diminish) {
if (canGrant) {
setupCallerCap(sender, thread);
} else {
setThreadState(sender, ThreadState_Inactive);

11
src/plat/imx7/Makefile Normal file
View file

@ -0,0 +1,11 @@
#
# Copyright 2014, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
include ${SOURCE_ROOT}/src/plat/${PLAT}/machine/Makefile

84
src/plat/imx7/linker.lds Normal file
View file

@ -0,0 +1,84 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
ENTRY(_start)
/* WARNING: constants also defined in plat/machine/hardware.h */
KERNEL_BASE = 0xe0000000;
PHYS_BASE = 0x80000000;
KERNEL_OFFSET = KERNEL_BASE - PHYS_BASE;
SECTIONS
{
. = KERNEL_BASE;
.boot . : AT(ADDR(.boot) - KERNEL_OFFSET)
{
*(.boot.text)
*(.boot.rodata)
*(.boot.data)
. = ALIGN(64K);
}
ki_boot_end = .;
.text . : AT(ADDR(.text) - KERNEL_OFFSET)
{
/* Sit inside a large frame */
. = ALIGN(64K);
*(.vectors)
/* Fastpath code */
*(.vectors.fastpath_call)
*(.vectors.fastpath_reply_recv)
*(.vectors.text)
/* Anything else that should be in the vectors page. */
*(.vectors.*)
/* Hopefully all that fits into 4K! */
/* Standard kernel */
*(.text)
}
.rodata . : AT(ADDR(.rodata) - KERNEL_OFFSET)
{
*(.rodata)
*(.rodata.*)
}
.data . : AT(ADDR(.data) - KERNEL_OFFSET)
{
*(.data)
}
.bss . : AT(ADDR(.bss) - KERNEL_OFFSET)
{
*(.bss)
/* 4k breakpoint stack */
_breakpoint_stack_bottom = .;
. = . + 4K;
_breakpoint_stack_top = .;
/* large data such as the globals frame and global PD */
*(.bss.aligned)
}
. = ALIGN(4K);
ki_end = .;
/DISCARD/ :
{
*(.note.gnu.build-id)
*(.comment)
}
}

20
src/plat/imx7/machine/Makefile Normal file
View file

@ -0,0 +1,20 @@
#
# Copyright 2014, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
DIRECTORIES += src/plat/${PLAT}/machine
PLAT_C_SOURCES += machine/hardware.c
ifdef DEBUG
PLAT_C_SOURCES += machine/io.c
endif
ifdef RELEASE_PRINTF
PLAT_C_SOURCES += machine/io.c
endif

243
src/plat/imx7/machine/hardware.c Normal file
View file

@ -0,0 +1,243 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#include <types.h>
#include <machine/io.h>
#include <kernel/vspace.h>
#include <arch/machine.h>
#include <arch/kernel/vspace.h>
#include <plat/machine.h>
#include <arch/linker.h>
#include <plat/machine/devices.h>
#include <plat/machine/hardware.h>
/* Available physical memory regions on platform (RAM) */
/* NOTE: Regions are not allowed to be adjacent! */
const p_region_t BOOT_RODATA avail_p_regs[] = {
/* 1 GiB */
#if CONFIG_MAX_NUM_TRACE_POINTS > 0
#warning "NOTE: logging is currently untested on iMX7 Sabre"
/* 1MB stolen for logging */
{ /* .start = */ 0x80000000, /* .end = */ 0x9fd00000 }
#else
{ /* .start = */ 0x80000000, /* .end = */ 0xc0000000 }
#endif /* CONFIG_MAX_NUM_TRACE_POINTS > 0 */
};
BOOT_CODE int
get_num_avail_p_regs(void)
{
return sizeof(avail_p_regs) / sizeof(p_region_t);
}
BOOT_CODE p_region_t
get_avail_p_reg(word_t i)
{
return avail_p_regs[i];
}
const p_region_t BOOT_RODATA dev_p_regs[] = {
{ GPIO0_PADDR, GPIO0_PADDR + 0x10000 },
{ GPIO1_PADDR, GPIO1_PADDR + 0x10000 },
{ GPIO2_PADDR, GPIO2_PADDR + 0x10000 },
{ GPIO3_PADDR, GPIO3_PADDR + 0x10000 },
{ GPIO4_PADDR, GPIO4_PADDR + 0x10000 },
{ GPIO5_PADDR, GPIO5_PADDR + 0x10000 },
{ GPIO6_PADDR, GPIO6_PADDR + 0x10000 },
{ WDOG0_PADDR, WDOG0_PADDR + 0x10000 },
{ WDOG1_PADDR, WDOG1_PADDR + 0x10000 },
{ WDOG2_PADDR, WDOG2_PADDR + 0x10000 },
{ WDOG3_PADDR, WDOG3_PADDR + 0x10000 },
{ IOMUXC_LPSR_PADDR, IOMUXC_LPSR_PADDR + 0x10000 },
{ GPT0_PADDR, GPT0_PADDR + 0x10000 },
{ GPT1_PADDR, GPT1_PADDR + 0x10000 },
{ GPT2_PADDR, GPT2_PADDR + 0x10000 },
{ GPT3_PADDR, GPT3_PADDR + 0x10000 },
{ IOMUXC_PADDR, IOMUXC_PADDR + 0x10000 },
{ GPR_PADDR, GPR_PADDR + 0x10000 },
{ OCOTP_PADDR, OCOTP_PADDR + 0x10000 },
{ ANATOP_PADDR, ANATOP_PADDR + 0x10000 },
{ CLKS_PADDR, CLKS_PADDR + 0x10000 },
{ SRC_PADDR, SRC_PADDR + 0x10000 },
{ PWM0_PADDR, PWM0_PADDR + 0x10000 },
{ PWM1_PADDR, PWM1_PADDR + 0x10000 },
{ PWM2_PADDR, PWM2_PADDR + 0x10000 },
{ PWM3_PADDR, PWM3_PADDR + 0x10000 },
{ UART1_PADDR, UART1_PADDR + 0x10000 },
{ UART2_PADDR, UART2_PADDR + 0x10000 },
{ UART3_PADDR, UART3_PADDR + 0x10000 },
{ UART4_PADDR, UART4_PADDR + 0x10000 },
{ UART5_PADDR, UART5_PADDR + 0x10000 },
{ UART6_PADDR, UART6_PADDR + 0x10000 },
{ I2C0_PADDR, I2C0_PADDR + 0x10000 },
{ I2C1_PADDR, I2C1_PADDR + 0x10000 },
{ I2C2_PADDR, I2C2_PADDR + 0x10000 },
{ I2C3_PADDR, I2C2_PADDR + 0x10000 },
{ USBOTG0_PADDR, USBOTG0_PADDR + 0x1000 },
{ USBOTG1_PADDR, USBOTG1_PADDR + 0x1000 },
{ USBH_PADDR, USBH_PADDR + 0x1000 },
{ USDHC0_PADDR, USDHC0_PADDR + 0x10000 },
{ USDHC1_PADDR, USDHC1_PADDR + 0x10000 },
{ USDHC2_PADDR, USDHC2_PADDR + 0x10000 },
{ FEC0_PADDR, FEC0_PADDR + 0x10000 },
{ FEC1_PADDR, FEC1_PADDR + 0x10000 },
};
BOOT_CODE int
get_num_dev_p_regs(void)
{
return sizeof(dev_p_regs) / sizeof(p_region_t);
}
BOOT_CODE p_region_t
get_dev_p_reg(word_t i)
{
return dev_p_regs[i];
}
/* Determine if the given IRQ should be reserved by the kernel. */
bool_t CONST
isReservedIRQ(irq_t irq)
{
return irq == KERNEL_TIMER_IRQ;
}
/* Handle a platform-reserved IRQ. */
void
handleReservedIRQ(irq_t irq)
{
printf("Received reserved IRQ: %d\n", (int)irq);
}
BOOT_CODE void
map_kernel_devices(void)
{
/* map kernel device: GIC distributor and private timers */
map_kernel_frame(
ARM_MP_PADDR,
ARM_MP_PPTR1,
VMKernelOnly,
vm_attributes_new(
true, /* armExecuteNever */
false, /* armParityEnabled */
false /* armPageCacheable */
)
);
/* map kernel device: GIC controller */
map_kernel_frame(
ARM_MP_PADDR + BIT(PAGE_BITS),
ARM_MP_PPTR2,
VMKernelOnly,
vm_attributes_new(
true, /* armExecuteNever */
false, /* armParityEnabled */
false /* armPageCacheable */
)
);
/* map kernel device: GIC controller */
map_kernel_frame(
ARM_MP_PADDR + BIT(PAGE_BITS) * 2,
ARM_MP_PPTR3,
VMKernelOnly,
vm_attributes_new(
true, /* armExecuteNever */
false, /* armParityEnabled */
false /* armPageCacheable */
)
);
#if defined DEBUG || defined RELEASE_PRINTF
/* map kernel device: UART */
map_kernel_frame(
UART_PADDR,
UART_PPTR,
VMKernelOnly,
vm_attributes_new(
true, /* armExecuteNever */
false, /* armParityEnabled */
false /* armPageCacheable */
)
);
#endif /* DEBUG */
}
/* co-processor code to read and write GPT */
static void
write_cntp_ctl(uint32_t v)
{
asm volatile ("mcr p15, 0, %0, c14, c2, 1" ::"r"(v));
}
static void
write_cntp_tval(uint32_t v)
{
asm volatile ("mcr p15, 0, %0, c14, c2, 0" :: "r"(v));
}
static uint32_t
read_cntfrq(void)
{
uint32_t val;
asm volatile ("mrc p15, 0, %0, c14, c0, 0" : "=r"(val));
return val;
}
/* default 8 MHz */
#define GPT_DEFAULT_FREQ 0x7a1200
#define GPT_DEFAULT_FREQ_MHZ 8ull
static uint32_t gpt_cntp_tval = 0;
/* we use the count-down timer of the GPT as the kernel preemption timer */
void
initTimer(void)
{
uint32_t freq = read_cntfrq();
uint64_t tval = 0;
if (freq != GPT_DEFAULT_FREQ) {
printf("Default timer has a different frequency %x\n", freq);
}
tval = (uint64_t)CONFIG_TIMER_TICK_MS * (freq / 1000);
if (tval > 0xffffffff) {
printf("timer interval value out of range \n");
halt();
}
gpt_cntp_tval = (uint32_t)tval;
/* write the value */
write_cntp_tval(gpt_cntp_tval);
/* enable the timer */
write_cntp_ctl(0x1);
}
/* need to reload the count-down value */
void
resetTimer(void)
{
write_cntp_tval(gpt_cntp_tval);
}
/* Cortex-A7 uses an integrated L2 cache controller */
void
initL2Cache(void)
{
}

62
src/plat/imx7/machine/io.c Normal file
View file

@ -0,0 +1,62 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#include <stdint.h>
#include <util.h>
#include <machine/io.h>
#include <plat/machine/devices.h>
#if defined DEBUG || defined RELEASE_PRINTF
#define URXD 0x00 /* UART Receiver Register */
#define UTXD 0x40 /* UART Transmitter Register */
#define UCR1 0x80 /* UART Control Register 1 */
#define UCR2 0x84 /* UART Control Register 2 */
#define UCR3 0x88 /* UART Control Register 3 */
#define UCR4 0x8c /* UART Control Register 4 */
#define UFCR 0x90 /* UART FIFO Control Register */
#define USR1 0x94 /* UART Status Register 1 */
#define USR2 0x98 /* UART Status Register 2 */
#define UESC 0x9c /* UART Escape Character Register */
#define UTIM 0xa0 /* UART Escape Timer Register */
#define UBIR 0xa4 /* UART BRM Incremental Register */
#define UBMR 0xa8 /* UART BRM Modulator Register */
#define UBRC 0xac /* UART Baud Rate Counter Register */
#define ONEMS 0xb0 /* UART One Millisecond Register */
#define UTS 0xb4 /* UART Test Register */
#define UART_REG(x) ((volatile uint32_t *)(UART_PPTR + (x)))
#define UART_SR2_TXFIFO_EMPTY 14
#define UART_SR2_RXFIFO_RDR 0
void
imx7_uart_putchar(char c)
{
putDebugChar(c);
if (c == '\n') {
putDebugChar('\r');
}
}
void putDebugChar(unsigned char c)
{
while (!(*UART_REG(USR2) & BIT(UART_SR2_TXFIFO_EMPTY)));
*UART_REG(UTXD) = c;
}
unsigned char getDebugChar(void)
{
while (!(*UART_REG(USR2) & BIT(UART_SR2_RXFIFO_RDR)));
return *UART_REG(URXD);
}
#endif /* DEBUG */

22
src/plat/pc99/machine/pit.c
View file

@ -19,31 +19,31 @@
/* Count frequency in Hz */
#define PIT_HZ 1193180
PHYS_CODE void
BOOT_CODE void
pit_init(void)
{
uint16_t divisor = (PIT_HZ * PIT_WRAPAROUND_MS) / 1000;
out8_phys(PIT_MODE, 0x34); /* Set mode 2 and wait for divisor bytes */
out8_phys(PIT_CH0, divisor & 0xff); /* Set low byte of divisor */
out8_phys(PIT_CH0, divisor >> 8); /* Set high byte of divisor */
out8(PIT_MODE, 0x34); /* Set mode 2 and wait for divisor bytes */
out8(PIT_CH0, divisor & 0xff); /* Set low byte of divisor */
out8(PIT_CH0, divisor >> 8); /* Set high byte of divisor */
}
PHYS_CODE void
BOOT_CODE void
pit_wait_wraparound(void)
{
uint16_t count;
uint16_t count_old;
out8_phys(PIT_MODE, 0x00);
count = in8_phys(PIT_CH0);
count |= (in8_phys(PIT_CH0) << 8);
out8(PIT_MODE, 0x00);
count = in8(PIT_CH0);
count |= (in8(PIT_CH0) << 8);
count_old = count;
while (count <= count_old) {
count_old = count;
out8_phys(PIT_MODE, 0x00);
count = in8_phys(PIT_CH0);
count |= (in8_phys(PIT_CH0) << 8);
out8(PIT_MODE, 0x00);
count = in8(PIT_CH0);
count |= (in8(PIT_CH0) << 8);
}
}

11
src/plat/tk1/Makefile Normal file
View file

@ -0,0 +1,11 @@
#
# Copyright 2016, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
include ${SOURCE_ROOT}/src/plat/$(PLAT)/machine/Makefile

84
src/plat/tk1/linker.lds Normal file
View file

@ -0,0 +1,84 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
ENTRY(_start)
/* WARNING: constants also defined in plat/machine/hardware.h */
KERNEL_BASE = 0xe0000000;
PHYS_BASE = 0x80000000;
KERNEL_OFFSET = KERNEL_BASE - PHYS_BASE;
SECTIONS
{
. = KERNEL_BASE;
.boot . : AT(ADDR(.boot) - KERNEL_OFFSET)
{
*(.boot.text)
*(.boot.rodata)
*(.boot.data)
. = ALIGN(64K);
}
ki_boot_end = .;
.text . : AT(ADDR(.text) - KERNEL_OFFSET)
{
/* Sit inside a large frame */
. = ALIGN(64K);
*(.vectors)
/* Fastpath code */
*(.vectors.fastpath_call)
*(.vectors.fastpath_reply_recv)
*(.vectors.text)
/* Anything else that should be in the vectors page. */
*(.vectors.*)
/* Hopefully all that fits into 4K! */
/* Standard kernel */
*(.text)
}
.rodata . : AT(ADDR(.rodata) - KERNEL_OFFSET)
{
*(.rodata)
*(.rodata.*)
}
.data . : AT(ADDR(.data) - KERNEL_OFFSET)
{
*(.data)
}
.bss . : AT(ADDR(.bss) - KERNEL_OFFSET)
{
*(.bss)
/* 4k breakpoint stack */
_breakpoint_stack_bottom = .;
. = . + 4K;
_breakpoint_stack_top = .;
/* large data such as the globals frame and global PD */
*(.bss.aligned)
}
. = ALIGN(4K);
ki_end = .;
/DISCARD/ :
{
*(.note.gnu.build-id)
*(.comment)
}
}

21
src/plat/tk1/machine/Makefile Normal file
View file

@ -0,0 +1,21 @@
#
# Copyright 2016, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
DIRECTORIES += src/plat/$(PLAT)/machine
PLAT_C_SOURCES += machine/hardware.c \
machine/l2cache.c
ifdef DEBUG
PLAT_C_SOURCES += machine/io.c
endif
ifdef RELEASE_PRINTF
PLAT_C_SOURCES += machine/io.c
endif

231
src/plat/tk1/machine/hardware.c Normal file
View file

@ -0,0 +1,231 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#include <types.h>
#include <machine/io.h>
#include <kernel/vspace.h>
#include <arch/machine.h>
#include <arch/kernel/vspace.h>
#include <plat/machine.h>
#include <arch/linker.h>
#include <plat/machine/devices.h>
#include <plat/machine/hardware.h>
/* Available physical memory regions on platform (RAM minus kernel image). */
/* NOTE: Regions are not allowed to be adjacent! */
const p_region_t BOOT_RODATA avail_p_regs[] = {
{ .start = 0x80000000, .end = 0xf0000000 }
};
BOOT_CODE int get_num_avail_p_regs(void)
{
return sizeof(avail_p_regs) / sizeof(p_region_t);
}
BOOT_CODE p_region_t get_avail_p_reg(word_t i)
{
return avail_p_regs[i];
}
#define SECTION_BITS 20
#define PAGE_SIZE (1 << PAGE_BITS)
#define SECTION_SIZE (1 << SECTION_BITS)
const p_region_t BOOT_RODATA dev_p_regs[] = {
{ GRAPH_HOST_PADDR, GRAPH_HOST_PADDR + (SECTION_SIZE * 16) }, /* 16 MB */
{ GPU_PADDR, GPU_PADDR + (SECTION_SIZE * 144) }, /* 144 MB */
{ UP_TAG_PADDR, UP_TAG_PADDR + PAGE_SIZE }, /* 4 KB */
{ RSEM_PADDR, RSEM_PADDR + PAGE_SIZE }, /* 4 KB */
{ ASEM_PADDR, ASEM_PADDR + PAGE_SIZE }, /* 4 KB */
{ ARB_PRI_PADDR, ARB_PRI_PADDR + PAGE_SIZE }, /* 4 KB */
{ ICTLR_PADDR, ICTLR_PADDR + PAGE_SIZE }, /* 4 KB, includes several */
{ TMR_PADDR, TMR_PADDR + PAGE_SIZE }, /* 4 Kb, 1 KB */
{ CLK_RESET_PADDR, CLK_RESET_PADDR + PAGE_SIZE }, /* 4 KB */
{ FLOW_CTRL_PADDR, FLOW_CTRL_PADDR + PAGE_SIZE }, /* 4 KB */
{ AHB_DMA_PADDR, AHB_DMA_PADDR + (PAGE_SIZE * 2) }, /* 8 KB */
{ AHB_DMA_CH_PADDR, AHB_DMA_CH_PADDR + PAGE_SIZE }, /* 4 KB 4 channels, 32 bytes */
{ APB_DMA_PADDR, APB_DMA_PADDR + (PAGE_SIZE * 4) }, /* 16 KB */
{ APB_DMA_CH_PADDR, APB_DMA_CH_PADDR + PAGE_SIZE }, /* 4KB 32 channels, 64 bytes */
{ SYS_REGS_PADDR, SYS_REGS_PADDR + PAGE_SIZE }, /* 768 bytes + 2 KB */
{ GPIO_PADDR, GPIO_PADDR + PAGE_SIZE }, /* 8 GPIOs, 265 bytes each */
{ VCP_PADDR, VCP_PADDR + PAGE_SIZE }, /* 4 KB */
{ VPUCQ_PADDR, VPUCQ_PADDR + PAGE_SIZE }, /* 256 Bytes */
{ BSEA_PADDR, BSEA_PADDR + PAGE_SIZE }, /* 4 KB */
{ IPATCH_PADDR, IPATCH_PADDR + PAGE_SIZE }, /* 4 KB offset 0xc00, 1 KB */
{ VDE_FRAMEID_PADDR, VDE_FRAMEID_PADDR + (PAGE_SIZE * 4) }, /* 16 KB, multiple */
{ MISC_PINMUX_PADDR, MISC_PINMUX_PADDR + (PAGE_SIZE * 4) }, /* 16 KB */
{ UARTA_SYNC_PADDR, UARTA_SYNC_PADDR + (PAGE_SIZE * 3 ) }, /* 12 KB, multiple */
{ SYNC_NOR_PADDR, SYNC_NOR_PADDR + PAGE_SIZE }, /* 4 KB */
{ PWM_PADDR, PWM_PADDR + PAGE_SIZE }, /* 4 KB, 256 bytes */
{ MIPIHSI_PADDR, MIPIHSI_PADDR + PAGE_SIZE }, /* 4 KB */
{ I2C_I2C4_PADDR, I2C_I2C4_PADDR + PAGE_SIZE }, /* 4 KB */
{ I2C5_SPI2B_6_PADDR, I2C5_SPI2B_6_PADDR + PAGE_SIZE }, /* 4 KB */
{ RTC_KFUSE_PADDR, RTC_KFUSE_PADDR + PAGE_SIZE }, /* 4 KB */
{ LA_PADDR, LA_PADDR + (PAGE_SIZE * 2) }, /* 8 KB */
{ SE_PADDR, SE_PADDR + (PAGE_SIZE * 2) }, /* 8 KB */
{ TSENSOR_PADDR, TSENSOR_PADDR + PAGE_SIZE }, /* 4 KB */
{ CEC_PADDR, CEC_PADDR + PAGE_SIZE }, /* 4 KB */
{ ATOMICS_PADDR, ATOMICS_PADDR + (PAGE_SIZE * 2) }, /* 8 KB */
{ MC_PADDR, MC_PADDR + PAGE_SIZE }, /* 4 KB */
{ EMC_PADDR, EMC_PADDR + PAGE_SIZE }, /* 4 KB */
{ SATA_PADDR, SATA_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ HDA_PADDR, HDA_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ MIOBFM_PADDR, MIOBFM_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ AUDIO_PADDR, AUDIO_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ XUSB_HOST_PADDR, XUSB_HOST_PADDR + (PAGE_SIZE * 10) }, /* 40 KB */
{ XUSB_DEV_PADDR, XUSB_DEV_PADDR + (PAGE_SIZE * 10) }, /* 40 KB */
{ DDS_PADDR, DDS_PADDR + (PAGE_SIZE * 2) }, /* 8KB 4608 bytes */
{ SDMMC_1_PADDR, SDMMC_1_PADDR + PAGE_SIZE }, /* 4KB 512 bytes */
{ SDMMC_1B_4_PADDR, SDMMC_1B_4_PADDR + (PAGE_SIZE * 15) }, /* 60KB 512 bytes each */
{ SPEEDO_PADDR, SPEEDO_PADDR + (PAGE_SIZE * 8) }, /* 32 KB */
{ SPEEDO_PMON_PADDR, SPEEDO_PMON_PADDR + (PAGE_SIZE * 8) }, /* 32 KB */
{ SYSCTR0_PADDR, SYSCTR0_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ SYSCTR1_PADDR, SYSCTR1_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ DP2_PADDR, DP2_PADDR + PAGE_SIZE }, /* 4 KB 256 Bytes */
{ APB2JTAG_PADDR, APB2JTAG_PADDR + PAGE_SIZE }, /* 4 Kb 512 Bytes */
{ SOC_THERM_PADDR, SOC_THERM_PADDR + PAGE_SIZE }, /* 4 KB */
{ MIPI_CAL_PADDR, MIPI_CAL_PADDR + PAGE_SIZE }, /* 4 KB 265 Bytes */
{ DVFS_PADDR, DVFS_PADDR + PAGE_SIZE }, /* 4 KB 1 KB */
{ CLUSTER_CLK_PADDR, CLUSTER_CLK_PADDR + (PAGE_SIZE * 64) }, /* 256 KB */
{ CSITE_PADDR, CSITE_PADDR + (SECTION_SIZE * 2) }, /* 2 MB */
{ PPCS_PADDR, PPCS_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ TZRAM_PADDR, TZRAM_PADDR + (PAGE_SIZE * 16) }, /* 64 KB */
{ USB_PADDR, USB_PADDR + (PAGE_SIZE * 2) }, /* 8 KB region, 6 KB */
{ USB2_PADDR, USB2_PADDR + (PAGE_SIZE * 2) }, /* 8 KB region, 6 KB */
{ USB3_PADDR, USB3_PADDR + (PAGE_SIZE * 2) }, /* 8 KB region, 6 KB */
};
BOOT_CODE int get_num_dev_p_regs(void)
{
return sizeof(dev_p_regs) / sizeof(p_region_t);
}
BOOT_CODE p_region_t get_dev_p_reg(word_t i)
{
return dev_p_regs[i];
}
/* Determine if the given IRQ should be reserved by the kernel. */
bool_t CONST
isReservedIRQ(irq_t irq)
{
return irq == KERNEL_TIMER_IRQ;
}
/* Handle a platform-reserved IRQ. */
void
handleReservedIRQ(irq_t irq)
{
printf("Received reserved IRQ: %d\n", (int)irq);
}
BOOT_CODE void
map_kernel_devices(void)
{
/* map kernel device: GIC */
map_kernel_frame(
GIC_CONTROLLER0_PADDR,
GIC_CONTROLLER_PPTR,
VMKernelOnly,
vm_attributes_new(
true, /* armExecuteNever */
false, /* armParityEnabled */
false /* armPageCacheable */
)
);
map_kernel_frame(
GIC_DISTRIBUTOR_PADDR,
GIC_DISTRIBUTOR_PPTR,
VMKernelOnly,
vm_attributes_new(
true, /* armExecuteNever */
false, /* armParityEnabled */
false /* armPageCacheable */
)
);
#if defined DEBUG || defined RELEASE_PRINTF
/* map kernel device: UART */
map_kernel_frame(
UARTA_PADDR,
UARTA_PPTR,
VMKernelOnly,
vm_attributes_new(
true, /* armExecuteNever */
false, /* armParityEnabled */
false /* armPageCacheable */
)
);
#endif
}
/* co-processor code to read and write GPT */
static void
write_cntp_ctl(uint32_t v)
{
asm volatile ("mcr p15, 0, %0, c14, c2, 1" ::"r"(v));
}
static void
write_cntp_tval(uint32_t v)
{
asm volatile ("mcr p15, 0, %0, c14, c2, 0" :: "r"(v));
}
static uint32_t
read_cntfrq(void)
{
uint32_t val;
asm volatile ("mrc p15, 0, %0, c14, c0, 0" : "=r"(val));
return val;
}
#define GPT_DEFAULT_HZ 12000000
static uint32_t gpt_cntp_tval = 0;
/**
DONT_TRANSLATE
*/
void
resetTimer(void)
{
write_cntp_tval(gpt_cntp_tval);
}
/**
DONT_TRANSLATE
*/
/* we use the physical count-down timer of the GPT as the kernel preemption timer */
BOOT_CODE void
initTimer(void)
{
uint32_t freq = read_cntfrq();
uint64_t tval = 0;
if (freq != GPT_DEFAULT_HZ) {
printf("Default timer has a different frequency %x\n", freq);
}
tval = (uint64_t)CONFIG_TIMER_TICK_MS * (freq / 1000);
if (tval > 0xffffffff) {
printf("timer interval value out of range \n");
halt();
}
gpt_cntp_tval = (uint32_t)tval;
/* write the value */
write_cntp_tval(gpt_cntp_tval);
/* enable the timer */
write_cntp_ctl(0x1);
}

48
src/plat/tk1/machine/io.c Normal file
View file

@ -0,0 +1,48 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#include <stdint.h>
#include <util.h>
#include <machine/io.h>
#include <plat/machine/devices.h>
#if defined DEBUG || defined RELEASE_PRINTF
#define UTHR 0x0
#define ULSR 0x14
#define ULSR_THRE (1 << 5)
#define UART_REG(x) ((volatile uint32_t *)(UARTD_PPTR + (x)))
void
tk1_uart_putchar(char c)
{
while ((*UART_REG(ULSR) & ULSR_THRE) == 0);
*UART_REG(UTHR) = (c & 0xff);
if (c == '\n') {
tk1_uart_putchar('\r');
}
}
void putDebugChar(unsigned char c)
{
while ((*UART_REG(ULSR) & ULSR_THRE) == 0);
*UART_REG(UTHR) = c;
}
unsigned char getDebugChar(void)
{
return 0;
}
#endif

18
src/plat/tk1/machine/l2cache.c Normal file
View file

@ -0,0 +1,18 @@
/*
* Copyright 2016, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*/
#include <arch/machine.h>
void
initL2Cache(void)
{
}