Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 45 additions & 1 deletion build_sdk.py
Original file line number Diff line number Diff line change
Expand Up @@ -307,6 +307,20 @@ class ConfigInfo:
},
examples = {}
),
BoardInfo(
name="odroidc4_2_cores",
arch=BoardArch.AARCH64,
gcc_flags="GCC_CPU=cortex-a55",
loader_link_address=0x20000000,
kernel_options = {
"KernelPlatform": "odroidc4",
"KernelIsMCS": True,
"KernelArmVtimerUpdateVOffset": False,
"KernelIRQReporting": False,
"KernelMaxNumNodes": 2,
},
examples = {}
),
BoardInfo(
name="rpi3b",
arch=BoardArch.AARCH64,
Expand Down Expand Up @@ -361,6 +375,21 @@ class ConfigInfo:
"hello": Path("example/maaxboard/hello")
}
),
BoardInfo(
name="maaxboard_2_cores",
arch=BoardArch.AARCH64,
gcc_flags="GCC_CPU=cortex-a53",
loader_link_address=0x50000000,
kernel_options = {
"KernelPlatform": "maaxboard",
"KernelIsMCS": True,
"KernelArmExportPCNTUser": True,
"KernelMaxNumNodes": 2,
},
examples = {
"hello": Path("example/maaxboard/hello")
}
),
# For RISC-V the link address for the Microkit loader is dependent on the
# previous loader. Currently for RISC-V platforms we use OpenSBI which
# is placed at the start of memory and since we use FW_PAYLOAD, it places
Expand Down Expand Up @@ -489,12 +518,27 @@ class ConfigInfo:
name="benchmark",
debug=False,
kernel_options = {
"KernelDebugBuild": False,
"KernelDebugBuild": True,
"KernelVerificationBuild": False,
"KernelPrinting": True,
"KernelBenchmarks": "track_utilisation",
"KernelArmExportPMUUser": True,
# Enable signal fastpath for sDDF benchmarking
"KernelSignalFastpath": True,
},
),
ConfigInfo(
name="profile",
debug=False,
kernel_options = {
"KernelDebugBuild": True,
"KernelVerificationBuild": False,
"KernelPrinting": True,
"KernelBenchmarks": "track_utilisation",
"KernelArmExportPMUUser": True,
# Enable signal fastpath for sDDF benchmarking
"KernelSignalFastpath": True,
"ProfilerEnable": True,
},
),
)
Expand Down
6 changes: 6 additions & 0 deletions libmicrokit/include/microkit.h
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,12 @@ microkit_msginfo_get_label(microkit_msginfo msginfo)
return seL4_MessageInfo_get_label(msginfo);
}

static inline uint64_t
microkit_msginfo_get_count(microkit_msginfo msginfo)
{
return seL4_MessageInfo_get_length(msginfo);
}

static void
microkit_mr_set(uint8_t mr, uint64_t value)
{
Expand Down
4 changes: 2 additions & 2 deletions loader/src/aarch64/loader.c
Original file line number Diff line number Diff line change
Expand Up @@ -208,7 +208,7 @@ putc(uint8_t ch)
while ((*UART_REG(UART_STATUS) & UART_TX_FULL));
*UART_REG(UART_WFIFO) = ch;
}
#elif defined(BOARD_odroidc4)
#elif defined(BOARD_odroidc4) || defined(BOARD_odroidc4_2_cores)
#define UART_BASE 0xff803000
#define UART_WFIFO 0x0
#define UART_STATUS 0xC
Expand Down Expand Up @@ -288,7 +288,7 @@ putc(uint8_t ch)

*((volatile uint32_t *)(UART_BASE + R_UART_TX_RX_FIFO)) = ch;
}
#elif defined(BOARD_maaxboard)
#elif defined(BOARD_maaxboard) || defined(BOARD_maaxboard_2_cores)
#define UART_BASE 0x30860000
#define STAT 0x98
#define TRANSMIT 0x40
Expand Down
2 changes: 1 addition & 1 deletion monitor/src/main.c
Original file line number Diff line number Diff line change
Expand Up @@ -532,7 +532,7 @@ monitor(void)
puts(pd_names[badge]);
puts("\n");
} else {
fail("unknown/invalid badge\n");
puts("unknown/invalid badge\n");
}

seL4_UserContext regs;
Expand Down
6 changes: 4 additions & 2 deletions tool/microkit/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@
Sel4CnodeCopy,
Sel4UntypedRetype,
Sel4IrqControlGetTrigger,
Sel4IrqControlGetTriggerCore,
Sel4IrqHandlerSetNotification,
Sel4SchedControlConfigureFlags,
Sel4ArmVcpuSetTcb,
Expand Down Expand Up @@ -1275,14 +1276,15 @@ def build_system(
for sysirq in pd.irqs:
cap_address = system_cap_address_mask | cap_slot
system_invocations.append(
Sel4IrqControlGetTrigger(
Sel4IrqControlGetTriggerCore(
kernel_config.arch,
IRQ_CONTROL_CAP_ADDRESS,
sysirq.irq,
sysirq.trigger.value,
root_cnode_cap,
cap_address,
kernel_config.cap_address_bits
kernel_config.cap_address_bits,
pd.cpu_affinity
)
)

Expand Down
71 changes: 54 additions & 17 deletions tool/microkit/sel4.py
Original file line number Diff line number Diff line change
Expand Up @@ -754,22 +754,26 @@ class Sel4Label(IntEnum):
ARMVCPUAckVPPI = 56
# ARM IRQ
ARMIRQIssueIRQHandlerTrigger = 57
ARMIRQIssueIRQHandlerTriggerCore = 58

# RISC-V Page Table
RISCVPageTableMap = 58
RISCVPageTableUnmap = 59
RISCVPageTableMap = 59
RISCVPageTableUnmap = 60
# RISC-V Page
RISCVPageMap = 60
RISCVPageUnmap = 61
RISCVPageGetAddress = 62
RISCVPageMap = 61
RISCVPageUnmap = 62
RISCVPageGetAddress = 63
# RISC-V ASID
RISCVASIDControlMakePool = 63
RISCVASIDPoolAssign = 64
RISCVASIDControlMakePool = 64
RISCVASIDPoolAssign = 65
# RISC-V IRQ
RISCVIRQIssueIRQHandlerTrigger = 65
RISCVIRQIssueIRQHandlerTrigger = 66
RISCVIRQIssueIRQHandlerTriggerCore = 67

# RISC-V VCPU
RISCVVCPUSetTCB = 66
RISCVVCPUReadReg = 67
RISCVVCPUWriteReg = 68
RISCVVCPUSetTCB = 68
RISCVVCPUReadReg = 69
RISCVVCPUWriteReg = 70

def get_id(self, kernel_config: KernelConfig) -> int:
if kernel_config.arch == KernelArch.AARCH64:
Expand All @@ -793,7 +797,9 @@ def get_id(self, kernel_config: KernelConfig) -> int:
# respective kernel config. This has some duplication (the first 4 invocations are always the same).
AARCH64_LABELS = {
# ARM IRQ
Sel4Label.ARMIRQIssueIRQHandlerTrigger: 52
Sel4Label.ARMIRQIssueIRQHandlerTrigger: 52,
Sel4Label.ARMIRQIssueIRQHandlerTriggerCore: 53

}

AARCH64_HYP_LABELS = {
Expand All @@ -804,7 +810,9 @@ def get_id(self, kernel_config: KernelConfig) -> int:
Sel4Label.ARMVCPUWriteReg: 55,
Sel4Label.ARMVCPUAckVPPI: 56,
# ARM IRQ
Sel4Label.ARMIRQIssueIRQHandlerTrigger: 57
Sel4Label.ARMIRQIssueIRQHandlerTrigger: 57,
Sel4Label.ARMIRQIssueIRQHandlerTriggerCore: 58

}

RISCV_LABELS = {
Expand All @@ -820,10 +828,11 @@ def get_id(self, kernel_config: KernelConfig) -> int:
Sel4Label.RISCVASIDPoolAssign: 42,
# RISC-V IRQ
Sel4Label.RISCVIRQIssueIRQHandlerTrigger: 43,
Sel4Label.RISCVIRQIssueIRQHandlerTriggerCore: 44,
# RISC-V VCPU
Sel4Label.RISCVVCPUSetTCB: 44,
Sel4Label.RISCVVCPUReadReg: 45,
Sel4Label.RISCVVCPUWriteReg: 46,
Sel4Label.RISCVVCPUSetTCB: 45,
Sel4Label.RISCVVCPUReadReg: 46,
Sel4Label.RISCVVCPUWriteReg: 47,
}

"""
Expand Down Expand Up @@ -1089,7 +1098,7 @@ def __init__(self, arch: KernelArch, asid_pool: int, vspace: int):
@dataclass
class Sel4IrqControlGetTrigger(Sel4Invocation):
_object_type = "IRQ Control"
_method_name = "Get"
_method_name = "GetTrigger"
_extra_caps = ("dest_root", )
irq_control: int
irq: int
Expand All @@ -1113,6 +1122,34 @@ def __init__(self, arch: KernelArch, irq_control: int, irq: int, trigger: int, d
self.dest_index = dest_index
self.dest_depth = dest_depth

@dataclass
class Sel4IrqControlGetTriggerCore(Sel4Invocation):
_object_type = "IRQ Control"
_method_name = "GetTriggerCore"
_extra_caps = ("dest_root", )
irq_control: int
irq: int
trigger: int
dest_root: int
dest_index: int
dest_depth: int
target: int

def __init__(self, arch: KernelArch, irq_control: int, irq: int, trigger: int, dest_root: int, dest_index: int, dest_depth: int, target: int):
if arch == KernelArch.AARCH64:
self.label = Sel4Label.ARMIRQIssueIRQHandlerTriggerCore
elif arch == KernelArch.RISCV64 or arch == KernelArch.RISCV32:
self.label = Sel4Label.RISCVIRQIssueIRQHandlerTriggerCore
else:
raise Exception(f"Unexpected kernel architecture: {arch}")

self.irq_control = irq_control
self.irq = irq
self.trigger = trigger
self.dest_root = dest_root
self.dest_index = dest_index
self.dest_depth = dest_depth
self.target = target

@dataclass
class Sel4IrqHandlerSetNotification(Sel4Invocation):
Expand Down
8 changes: 5 additions & 3 deletions tool/microkit/sysxml.py
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ class SysIrq:
irq: int
id_: int
trigger: str
target: int


@dataclass(frozen=True, eq=True)
Expand Down Expand Up @@ -217,9 +218,9 @@ def __init__(
all_irqs = set()
for pd in self.protection_domains:
for sysirq in pd.irqs:
if sysirq.irq in all_irqs:
if (sysirq.irq, sysirq.target) in all_irqs:
raise UserError(f"duplicate irq: {sysirq.irq} in protection domain: '{pd.name}' @ {pd.element._loc_str}") # type: ignore
all_irqs.add(sysirq.irq)
all_irqs.add((sysirq.irq, sysirq.target))

# Ensure no duplicate channel identifiers
ch_ids: Dict[str, Set[int]] = {pd_name: set() for pd_name in self.pd_by_name}
Expand Down Expand Up @@ -362,7 +363,8 @@ def xml2pd(pd_xml: ET.Element, plat_desc: PlatformDescription, is_child: bool=Fa
trigger = Sel4ArmIrqTrigger.Edge
else:
raise UserError(f"Invalid IRQ trigger '{trigger_str}': {child._loc_str}")
irqs.append(SysIrq(irq, irq_id, trigger))
target = cpu
irqs.append(SysIrq(irq, irq_id, trigger, target))
elif child.tag == "setvar":
_check_attrs(child, ("symbol", "region_paddr"))
symbol = checked_lookup(child, "symbol")
Expand Down