Concrete source synchronization dictionaries selected by the final OS foreign chain. This record owns no state: all identities refer to HostRuntime and allocation-local metadata built by EvalTypedSyncMachine.

structure Miri.Interpreter.ForeignSyncMachine.Objects (S : Type) : Type

• runtime : Concurrency.SyncRuntime.Hooks S Concurrency.TypedSyncRuntime.Ref Int32 Concurrency.TypedSyncRuntime.Dest
• once : Concurrency.InitOnce.Hooks S Concurrency.TypedSyncRuntime.Ref Int32 Concurrency.TypedSyncRuntime.Dest
• pthread : PthreadObjects.Hooks S Concurrency.TypedSyncRuntime.Ref
• metadata : Concurrency.SyncObject.MetadataHooks S TypedSyncMetadata.Payload
• bytes : TypedSyncObjectMachine.Bytes S
• newFutex : EStateM StepError S Concurrency.TypedSyncRuntime.Ref
• newMacFutex : UInt64 → Bool → EStateM StepError S Concurrency.TypedSyncRuntime.Ref
• macSettings : Concurrency.TypedSyncRuntime.Ref → EStateM StepError S (UInt64 × Bool)
• putMacSettings : Concurrency.TypedSyncRuntime.Ref → UInt64 → Bool → EStateM StepError S Unit

def Miri.Interpreter.ForeignSyncMachine.pthread {S Duration : Type} (objects : Objects S) (h : PthreadSync.Hooks S Concurrency.TypedSyncRuntime.Ref Duration) : PthreadSync.Hooks S Concurrency.TypedSyncRuntime.Ref Duration

Equations

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

def Miri.Interpreter.ForeignSyncMachine.windows {S : Type} (objects : Objects S) (h : WindowsSync.Hooks S Concurrency.TypedSyncRuntime.Ref) : WindowsSync.Hooks S Concurrency.TypedSyncRuntime.Ref

Equations

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

def Miri.Interpreter.ForeignSyncMachine.mac {S : Type} (objects : Objects S) (h : MacOsSync.Hooks S Concurrency.TypedSyncRuntime.Ref) : MacOsSync.Hooks S Concurrency.TypedSyncRuntime.Ref

Equations

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

def Miri.Interpreter.ForeignSyncMachine.freeBsd {S : Type} (objects : Objects S) (h : FreeBsdSync.Hooks S Concurrency.TypedSyncRuntime.Ref) : FreeBsdSync.Hooks S Concurrency.TypedSyncRuntime.Ref

Equations

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