Source constructors for typed synchronization state, static-initializer sanity flags and MacOsFutex settings. No function registry is requested.

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncFactories.M (K U A : Type) : Type

Equations

• Miri.Interpreter.TypedSyncFactories.M = Miri.Interpreter.TypedSyncMachine.M

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncFactories.Views (U : Type) : Type

Equations

• Miri.Interpreter.TypedSyncFactories.Views = Miri.Interpreter.TypedSyncMachine.Views

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncFactories.State (K U : Type) : Type

Equations

• Miri.Interpreter.TypedSyncFactories.State = Miri.Interpreter.TypedSyncMachine.State

def Miri.Interpreter.TypedSyncFactories.sanity {U K : Type} (v : Views U) (kind : PthreadObjects.Kind) : M K U Bool

Equations

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

def Miri.Interpreter.TypedSyncFactories.putSanity {U K : Type} (v : Views U) (kind : PthreadObjects.Kind) (value : Bool) : M K U Unit

Equations

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

structure Miri.Interpreter.TypedSyncFactories.PthreadMemory (S : Type) : Type

• os : String
• deref : OpTy Memory.Provenance → PthreadObjects.Kind → EStateM StepError S Concurrency.TypedSyncRuntime.Dest
• initializer : String → EStateM StepError S Concurrency.TypedSyncRuntime.Dest
• readBytes : Concurrency.TypedSyncRuntime.Dest → ABI.Size → EStateM StepError S ByteArray
• readInitByte : Concurrency.TypedSyncRuntime.Dest → ABI.Size → EStateM StepError S UInt8

def Miri.Interpreter.TypedSyncFactories.pthread {U K : Type} (v : Views U) (e : TypedSyncMachine.Effects (State K U)) (metadata : Concurrency.SyncObject.MetadataHooks (State K U) TypedSyncMetadata.Payload) (bytes : TypedSyncObjectMachine.Bytes (State K U)) (memory : PthreadMemory (State K U)) : PthreadObjects.Hooks (State K U) Concurrency.TypedSyncRuntime.Ref

Equations

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

def Miri.Interpreter.TypedSyncFactories.newMacFutex {U K : Type} (v : Views U) (size : UInt64) (shared : Bool) : M K U Concurrency.TypedSyncRuntime.Ref

Equations

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

def Miri.Interpreter.TypedSyncFactories.macSettings {U K : Type} (v : Views U) (ref : Concurrency.TypedSyncRuntime.Ref) : M K U (UInt64 × Bool)

Equations

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

def Miri.Interpreter.TypedSyncFactories.putMacSettings {U K : Type} (v : Views U) (ref : Concurrency.TypedSyncRuntime.Ref) (size : UInt64) (shared : Bool) : M K U Unit

Equations

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