Skip to content

How does MMIO memory fit into the memory model, and can reference point to it? #411

Description

@chorman0773

This question is intended to replace #33 and #265, and ask the general question of whether or not we can have a type, either user-defined or language-provided, that, when wrapped in a shared reference, guarantees that no accesses are introduced at the operational semantics level that are not part of the original program (and thus, if volatile accesses only are used, an implementation won't introduce any speculative reads).
If such a type can exist, the second question is what is the operational semantics of retagging as a shared reference to such a type.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-dereferenceableTopic: when exactly does a reference need to point to regular dereferenceable memory?

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions