Metadata wrappers from pinned concurrency/sync.rs:18–62,302–446. Registry payloads are typed by the caller: mismatched dynamic types must return none, causing replacement just as dyn SyncObj::downcast_ref does in source.

@[reducible, inline]

abbrev Miri.Concurrency.SyncObject.M (σ α : Type) : Type

Equations

• Miri.Concurrency.SyncObject.M = EStateM Miri.Interpreter.StepError

inductive Miri.Concurrency.SyncObject.AccessKind : Type

• read : AccessKind
• write : AccessKind
• deallocation : AccessKind

@[instance_reducible]

instance Miri.Concurrency.SyncObject.instDecidableEqAccessKind : DecidableEq AccessKind

Equations

• Miri.Concurrency.SyncObject.instDecidableEqAccessKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.SyncObject.instReprAccessKind : Repr AccessKind

Equations

• Miri.Concurrency.SyncObject.instReprAccessKind = { reprPrec := Miri.Concurrency.SyncObject.instReprAccessKind.repr }

def Miri.Concurrency.SyncObject.instReprAccessKind.repr : AccessKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Miri.Concurrency.SyncObject.Object (S Payload : Type) : Type

• payload : Payload
• onAccess : AccessKind → M S Unit
• deleteOnWrite : Bool

structure Miri.Concurrency.SyncObject.Address : Type

• allocation : Memory.AllocId
• offset : ABI.Size

structure Miri.Concurrency.SyncObject.Info : Type

• liveData : Bool
• mutable : Bool
• size : ABI.Size

structure Miri.Concurrency.SyncObject.Hooks (S T : Type) : Type

• tryResolve : Memory.Pointer (Option Memory.Provenance) → M S (Option Address)
• resolve : Memory.Pointer (Option Memory.Provenance) → M S Address
• info : Memory.AllocId → M S Info
• lookup : Address → M S (Option (Object S T))
• insert : Address → Object S T → M S Unit
• checkAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit
• offset : Interpreter.MPlaceTy Memory.Provenance → ABI.Size → M S (Interpreter.MPlaceTy Memory.Provenance)
• compareExchangeByteRelaxed : Interpreter.MPlaceTy Memory.Provenance → UInt8 → UInt8 → M S (UInt8 × Bool)
• writeZeros : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit
• writeByte : Interpreter.MPlaceTy Memory.Provenance → UInt8 → M S Unit

structure Miri.Concurrency.SyncObject.MetadataHooks (S T : Type) : Type

• tryResolve : Memory.Pointer (Option Memory.Provenance) → M S (Option Address)
• resolve : Memory.Pointer (Option Memory.Provenance) → M S Address
• info : Memory.AllocId → M S Info
• lookup : Address → M S (Option (Object S T))
• insert : Address → Object S T → M S Unit

def Miri.Concurrency.SyncObject.getOrInitMetadata {S T : Type} (h : MetadataHooks S T) (pointer : Memory.Pointer (Option Memory.Provenance)) (new : M S (Object S T)) : M S (Option (Object S T))

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncObject.getOrInit {S T : Type} (h : Hooks S T) (pointer : Memory.Pointer (Option Memory.Provenance)) (new : M S (Object S T)) : M S (Option (Object S T))

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncObject.getImmovableWithStaticInit {S T : Type} (h : Hooks S T) (obj : Interpreter.MPlaceTy Memory.Provenance) (initOffset : ABI.Size) (uninitValue initValue : UInt8) (new : M S (Object S T)) : M S (Object S T)

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncObject.initImmovable {S T : Type} (h : Hooks S T) (obj : Interpreter.MPlaceTy Memory.Provenance) (initOffset : ABI.Size) (initValue : UInt8) (metadata : Object S T) : M S (Option (Object S T))

Equations

• One or more equations did not get rendered due to their size.

structure Miri.Concurrency.SyncObject.AccessHooks (S T : Type) : Type

• entries : Memory.AllocId → M S (Array (ABI.Size × Object S T))

  Complete live registry; access traverses ascending byte offsets, as BTreeMap.

• remove : Memory.AllocId → ABI.Size → M S Unit

def Miri.Concurrency.SyncObject.onMemoryAccess {S T : Type} (h : AccessHooks S T) (allocation : Memory.AllocId) (start size : ABI.Size) (kind : AccessKind) : M S Unit

Equations

• One or more equations did not get rendered due to their size.