Canonical source synchronization runtime on the final pointer/validation/ thread composition. Optional clocks and actual thread stacks share the same machine fields; no synthetic GlobalState is created for disabled tracking.

@[reducible, inline]

abbrev Miri.Interpreter.SyncMachine.User (U : Type) : Type

Equations

• Miri.Interpreter.SyncMachine.User = Miri.Interpreter.ExecutionStateTransport.Inner

@[reducible, inline]

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

Equations

• Miri.Interpreter.SyncMachine.State K U = Miri.Interpreter.MachineHooks.State K (Miri.Interpreter.SyncMachine.User U)

def Miri.Interpreter.SyncMachine.sourceError : Concurrency.SyncError → StepError

Equations

• Miri.Interpreter.SyncMachine.sourceError x✝ = Miri.Interpreter.StepError.invalidProgram (toString "synchronization invariant: " ++ toString (reprStr x✝))

def Miri.Interpreter.SyncMachine.bind {K U B R V D : Type} (selection : State K U → Except StepError (RaceMode.Handler B)) (base : Concurrency.SyncRuntime.Hooks (State K U) R V D) : MachineHooks.M K (User U) (Concurrency.SyncRuntime.Hooks (State K U) R V D)

Select the immutable source backend kind from the canonical machine at the actual binding point. Compiler/configuration leaves and typed object/callback stores remain the supplied source records; clock/thread access is replaced.

Equations

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