"cached=false" or "cached=true" should be attribute on the memory region, not the mapping

Open
#471 3 comments 1 reaction 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
48/100
Issue type
Feature
Clarity
Mostly clear
Activity status
Quiet
Tech stack
rust

Research direction

Start by locating the memory-region and mapping APIs, then trace how the cached attribute is represented on AArch64. Compare the existing cached and uncached mapping paths and determine whether the attribute should be named cached or device. Done means a memory region cannot be mapped with inconsistent memory attributes, with the relevant behavior covered by tests.

Written by the indexing model from the issue text.

Description

needs-discussion

We've discussed this internally before, but on AArch64 and maybe other architectures, mapping the same memory as both cached and uncached creates weird cache coherence issues.

We've often seen students try to do both cached and uncached on the same memory region when mapping: instead we should be always using the same memory attribute for both.

We can enforce this by making it an attribute of the memory region itself.

(alternatively, call it "device" not "cached", because at least on AArch64 it goes from NORMAL to DEVICE_nGnRnE, and we ignore features of e.g. x86 where you can have write-through or write-combining caches)

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.