Skip to content

Add 32-bit MCS support#336

Open
dlom wants to merge 1 commit into
seL4:mainfrom
dlom:mold/32bit-mcs
Open

Add 32-bit MCS support#336
dlom wants to merge 1 commit into
seL4:mainfrom
dlom:mold/32bit-mcs

Conversation

@dlom
Copy link
Copy Markdown

@dlom dlom commented Apr 2, 2026

Add aarch32/riscv32 MCS worlds. Fix timeout fault consumed field (split high/low on 32-bit) and tcb_configure calls. Exclude spawn examples from MCS.

Verified by: make run-fast-tests

Add aarch32/riscv32 MCS worlds. Fix timeout fault consumed field
(split high/low on 32-bit) and tcb_configure calls. Exclude spawn
examples from MCS.

Verified by: `make run-fast-tests`

Signed-off-by: Mark Old <mold@redhat.com>
@dlom dlom requested a review from nspin as a code owner April 2, 2026 10:24
Comment on lines +64 to +87
sel4::sel4_cfg_if! {
if #[sel4_cfg(KERNEL_MCS)] {
child_tcb
.tcb_configure(
child_cnode,
sel4::CNodeCapData::new(0, sel4::WORD_SIZE - child_cnode_size_bits),
child_vspace,
ipc_buffer_addr as sel4::Word,
ipc_buffer_cap,
)
.unwrap();
} else {
child_tcb
.tcb_configure(
sel4::init_thread::slot::NULL.cptr(),
child_cnode,
sel4::CNodeCapData::new(0, sel4::WORD_SIZE - child_cnode_size_bits),
child_vspace,
ipc_buffer_addr as sel4::Word,
ipc_buffer_cap,
)
.unwrap();
}
}
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In hacking/nix/scope/world/instances/default.nix, you disabled this test for MCS. Is this change incomplete? If so, maybe we should leave this test with just non-MCS support.

Comment on lines +47 to +66
sel4::sel4_cfg_if! {
if #[sel4_cfg(KERNEL_MCS)] {
secondary_thread_tcb.tcb_configure(
sel4::init_thread::slot::CNODE.cap(),
sel4::CNodeCapData::new(0, 0),
sel4::init_thread::slot::VSPACE.cap(),
SECONDARY_THREAD_IPC_BUFFER_FRAME.ptr() as sel4::Word,
SECONDARY_THREAD_IPC_BUFFER_FRAME.cap(bootinfo),
)?;
} else {
secondary_thread_tcb.tcb_configure(
sel4::init_thread::slot::NULL.cptr(),
sel4::init_thread::slot::CNODE.cap(),
sel4::CNodeCapData::new(0, 0),
sel4::init_thread::slot::VSPACE.cap(),
SECONDARY_THREAD_IPC_BUFFER_FRAME.ptr() as sel4::Word,
SECONDARY_THREAD_IPC_BUFFER_FRAME.cap(bootinfo),
)?;
}
}
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(See above)

@nspin
Copy link
Copy Markdown
Member

nspin commented Apr 28, 2026

Thanks for this, and apologies for the delayed review.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants