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
36 changes: 26 additions & 10 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 @@ -1274,17 +1275,32 @@ def build_system(
for pd in system.protection_domains:
for sysirq in pd.irqs:
cap_address = system_cap_address_mask | cap_slot
system_invocations.append(
Sel4IrqControlGetTrigger(
kernel_config.arch,
IRQ_CONTROL_CAP_ADDRESS,
sysirq.irq,
sysirq.trigger.value,
root_cnode_cap,
cap_address,
kernel_config.cap_address_bits
# If we are in UP mode, use GetTrigger, in SMP use GetTriggerCore
if kernel_config.num_cpus > 1:
system_invocations.append(
Sel4IrqControlGetTriggerCore(
kernel_config.arch,
IRQ_CONTROL_CAP_ADDRESS,
sysirq.irq,
sysirq.trigger.value,
root_cnode_cap,
cap_address,
kernel_config.cap_address_bits,
pd.cpu_affinity
)
)
else:
system_invocations.append(
Sel4IrqControlGetTrigger(
kernel_config.arch,
IRQ_CONTROL_CAP_ADDRESS,
sysirq.irq,
sysirq.trigger.value,
root_cnode_cap,
cap_address,
kernel_config.cap_address_bits,
)
)
)

cap_slot += 1
cap_address_names[cap_address] = f"IRQ Handler: irq={sysirq.irq:d}"
Expand Down
69 changes: 51 additions & 18 deletions tool/microkit/sel4.py
Original file line number Diff line number Diff line change
Expand Up @@ -754,22 +754,24 @@ 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 +795,8 @@ 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 +807,8 @@ 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 +824,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 +1094,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 +1118,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 Expand Up @@ -1564,4 +1597,4 @@ def arch_get_page_sizes(arch: KernelArch) -> [int]:
if arch == KernelArch.AARCH64 or arch == KernelArch.RISCV64 or arch == KernelArch.X86_64:
return [0x1000, 0x200_000]
else:
raise Exception(f"Unexpected kernel architecture: {arch}")
raise Exception(f"Unexpected kernel architecture: {arch}")
10 changes: 6 additions & 4 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 Expand Up @@ -516,4 +518,4 @@ def xml2system(filename: Path, plat_desc: PlatformDescription) -> SystemDescript
memory_regions=memory_regions,
protection_domains=protection_domains,
channels=channels,
)
)