def
Miri.Interpreter.ThreadShimMachine.bindMemory
{K U C O X F A Aff : Type}
(h : ThreadMachine.Hooks K U C O X F A Aff)
(place : PlaceHooks Memory.Provenance (ThreadStacks.State K U) C MachineHooks.FrameExtra)
:
ThreadMachine.Hooks K U C O X F A Aff
Install concrete scalar memory writes including source validation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.ThreadShimMachine.bind
{K U C O X F A Aff D B I HostPath : Type}
[DecidableEq K]
(h : ThreadMachine.Hooks K U C O X F A Aff)
(choice : C)
(unitLayout : LocalLayout)
(reuseClock : Option Concurrency.VectorIdx)
(base : MiriShims.Hooks Memory.Provenance (ThreadStacks.State K U) D (MPlaceTy Memory.Provenance) B I HostPath)
:
MiriShims.Hooks Memory.Provenance (ThreadStacks.State K U) D (MPlaceTy Memory.Provenance) B I HostPath
miri_thread_spawn/join use actual typed memory destinations and Rust ABI. The clock-reuse choice is an explicit permitted execution input.
Equations
- One or more equations did not get rendered due to their size.