broken atomic lock when starting multiple cores

Open
#463 2 comments 0 reactions 1 assignee View on GitHub

@midnightveil is already working on this.

Since Jun 17, 2026.

Assessment

This issue has not been assessed yet.

Description

Hello,

Synchronization between cores in SMP mode relies on STLR/LDAR instructions to implement release/acquire semantics on the print_lock flag. These instructions depend on proper cache coherency and on memory being mapped as Normal, Inner Shareable.

Therefore, all cores must have the MMU (and caches) enabled with consistent attributes in order to use locks across cores0

In loader.c:main(), the MMU on logical core 0 is enabled after the secondary cores have already been started.
As a result, core 0 does not participate in the coherency domain when the other cores begin execution. Consequently, updates to the print_lock flag performed by secondary cores are not observed by core 0, leading to an infinite loop.

Workarounds are: Disabling the data cache via SCTLR.C, or using Normal_NC in MAIR for the translation tables

The MMU on core 0 should be enabled before releasing secondary cores.

Originally posted by @bruelc in https://github.com/seL4/microkit/issues/446#issuecomment-4156815830

Dominant language
Rust
Stars
201
Forks
80
Avg merge
1d 4h
Merged PRs (30d)
7

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from seL4/microkit

All issues in seL4/microkit

Similar issues

More Rust issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.