Skip to content

How does the aliasing model interact with the concurrency model? #585

@RalfJung

Description

@RalfJung

Based on discussions I had with @JoJoDeveloping, it seems like there will have to be some sort of interaction between the aliasing model and the concurrency model. We'll have to figure out the details before finalizing decisions here.

One of the ways in which they interact is the "end of a function call" event that deactivates protectors: if that event happens in one thread, while another thread accesses that location, there's the question of -- did the access happen before or after the end of the call? Miri just uses the actual execution order for this, but in a weak memory world, we will likely have to use something like happens-before here or else we may lose some of the optimizations we were hoping for.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-aliasing-modelTopic: Related to the aliasing model (e.g. Stacked/Tree Borrows)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions