Synchronization marker bytes use the canonical atomic scalar operations and shared memory state.

def Miri.Interpreter.TypedSyncBytes.bindObjectHooks {K U C P O B : Type} [DecidableEq K] (h : LinuxFutexMachine.ObjectHooks K U C P O B) (choice : C) (u8Layout : LocalLayout) : TypedSyncObjectMachine.Bytes (LinuxFutexMachine.State K U)

Equations

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

def Miri.Interpreter.TypedSyncBytes.bind {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : LinuxFutexMachine.Hooks K U C P O B H Y Z T E) (choice : C) (u8Layout : LocalLayout) : TypedSyncObjectMachine.Bytes (LinuxFutexMachine.State K U)

Equations

• Miri.Interpreter.TypedSyncBytes.bind h choice u8Layout = Miri.Interpreter.TypedSyncBytes.bindObjectHooks (Miri.Interpreter.LinuxFutexMachine.objectHooks h) choice u8Layout

def Miri.Interpreter.TypedSyncBytes.pthreadMemoryFromObjectHooks {K U C P O B : Type} [DecidableEq K] (h : LinuxFutexMachine.ObjectHooks K U C P O B) (choice : C) (os : String) (initializer : String → LinuxFutexMachine.M K U Concurrency.TypedSyncRuntime.Dest) : TypedSyncFactories.PthreadMemory (LinuxFutexMachine.State K U)

Pthread object compiler globals remain required by their exact source names; all operand dereferences and byte reads are the canonical physical operations.

Equations

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

def Miri.Interpreter.TypedSyncBytes.pthreadMemory {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : LinuxFutexMachine.Hooks K U C P O B H Y Z T E) (choice : C) (os : String) (initializer : String → LinuxFutexMachine.M K U Concurrency.TypedSyncRuntime.Dest) : TypedSyncFactories.PthreadMemory (LinuxFutexMachine.State K U)

Equations

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