def
Miri.Interpreter.FreeBsdSyncMachine.bindTime
{K U Host System TZ Timestamp R : Type}
(time : TimeShims.Hooks (MachineHooks.State K U) Host System TZ Timestamp)
(deadline : DeadlineMachine.Hooks K U Host System)
(base : FreeBsdSync.Hooks (MachineHooks.State K U) R)
:
FreeBsdSync.Hooks (MachineHooks.State K U) R
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.FreeBsdSyncMachine.bindReads
{K U R : Type}
[DecidableEq K]
(access : PlaceMachine.AccessConfig K U)
(base : FreeBsdSync.Hooks (MachineHooks.State K U) R)
:
FreeBsdSync.Hooks (MachineHooks.State K U) R
Regular _umtx_time metadata reads use actual physical scalar reads. The Acquire load and SeqCst fence remain separate required atomic-engine effects.
Equations
- One or more equations did not get rendered due to their size.