Skip to content

Add support to concurrency #313

Description

@danielsn

RMC does not currently support verification of concurrent code. RMC may spuriously miss bugs that occur when shared data-structures are modified.

Likelihood:

An issue for any concurrent code customers want to verify.

Mitigation:

  • Document the limitation.
  • Raise a warning if RMC encounters code which uses concurrency

Path to soundness:

  • Either document this as not supported,
  • or add support.

Activity

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions