Source dyn SyncObj payloads are distinct even when they refer to the same kind of host synchronization state. This sum preserves source downcast identity without closure-valued persistent metadata.

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncMetadata.Ref : Type

Equations

• Miri.Interpreter.TypedSyncMetadata.Ref = Miri.Concurrency.TypedSyncRuntime.Ref

inductive Miri.Interpreter.TypedSyncMetadata.Payload : Type

• pthread (value : PthreadObjects.Payload Ref) : Payload
• windows (value : WindowsSync.Payload Ref) : Payload
• macLock (value : MacOsSync.Unfair Ref) : Payload
• macSemaphore (value : MacOsSync.Semaphore Ref) : Payload
• macFutex (ref : Ref) : Payload
• freeBsdFutex (ref : Ref) : Payload

def Miri.Interpreter.TypedSyncMetadata.guardAccess {m : Type → Type u_1} [Monad m] [MonadExceptOf StepError m] (getObject : Ref → m Concurrency.TypedSyncRuntime.Object) (payload : Payload) : Concurrency.SyncObject.AccessKind → m Unit

Source access guards reconstructed from typed persistent captures. No allocation roots are added: sync.rs VisitProvenance for these Rc states is empty.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.TypedSyncMetadata.guardAccess getObject (Miri.Interpreter.TypedSyncMetadata.Payload.windows (Miri.Interpreter.WindowsSync.Payload.futex ref)) x✝ = pure ()
• Miri.Interpreter.TypedSyncMetadata.guardAccess getObject (Miri.Interpreter.TypedSyncMetadata.Payload.macLock Miri.Interpreter.MacOsSync.Unfair.permanentlyLocked) x✝ = pure ()
• Miri.Interpreter.TypedSyncMetadata.guardAccess getObject (Miri.Interpreter.TypedSyncMetadata.Payload.macFutex ref) x✝ = pure ()
• Miri.Interpreter.TypedSyncMetadata.guardAccess getObject (Miri.Interpreter.TypedSyncMetadata.Payload.freeBsdFutex ref) x✝ = pure ()

def Miri.Interpreter.TypedSyncMetadata.onAccess {S : Type} (h : Concurrency.TypedSyncRuntime.Hooks S) (payload : Payload) (kind : Concurrency.SyncObject.AccessKind) : EStateM StepError S Unit

Equations

• Miri.Interpreter.TypedSyncMetadata.onAccess h payload kind = Miri.Interpreter.TypedSyncMetadata.guardAccess h.get payload kind

def Miri.Interpreter.TypedSyncMetadata.deleteOnWrite : Payload → Bool

Equations

• Miri.Interpreter.TypedSyncMetadata.deleteOnWrite (Miri.Interpreter.TypedSyncMetadata.Payload.pthread value) = true
• Miri.Interpreter.TypedSyncMetadata.deleteOnWrite (Miri.Interpreter.TypedSyncMetadata.Payload.windows (Miri.Interpreter.WindowsSync.Payload.initOnce ref)) = true
• Miri.Interpreter.TypedSyncMetadata.deleteOnWrite (Miri.Interpreter.TypedSyncMetadata.Payload.macLock value) = true
• Miri.Interpreter.TypedSyncMetadata.deleteOnWrite (Miri.Interpreter.TypedSyncMetadata.Payload.macSemaphore value) = true
• Miri.Interpreter.TypedSyncMetadata.deleteOnWrite x✝ = false

def Miri.Interpreter.TypedSyncMetadata.object {S : Type} (h : Concurrency.TypedSyncRuntime.Hooks S) (payload : Payload) : Concurrency.SyncObject.Object S Payload

Equations

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