Entire pinned shims/windows/sync.rs. Pinned source implements InitOnce and address waits, not SRW/CriticalSection/ConditionVariable aliases.

@[reducible, inline]

abbrev Miri.Interpreter.WindowsSync.M (σ α : Type) : Type

Equations

• Miri.Interpreter.WindowsSync.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.WindowsSync.Constant : Type

• trueValue : Constant
• falseValue : Constant
• initFailed : Constant
• infinite : Constant
• invalidParameter : Constant
• timeout : Constant

@[instance_reducible]

instance Miri.Interpreter.WindowsSync.instDecidableEqConstant : DecidableEq Constant

Equations

• Miri.Interpreter.WindowsSync.instDecidableEqConstant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.WindowsSync.instReprConstant : Repr Constant

Equations

• Miri.Interpreter.WindowsSync.instReprConstant = { reprPrec := Miri.Interpreter.WindowsSync.instReprConstant.repr }

def Miri.Interpreter.WindowsSync.instReprConstant.repr : Constant → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.WindowsSync.Payload (R : Type) : Type

• initOnce {R : Type} (ref : R) : Payload R
• futex {R : Type} (ref : R) : Payload R

structure Miri.Interpreter.WindowsSync.Hooks (S R : Type) : Type

• once : Concurrency.InitOnce.Hooks S R Int32 (MPlaceTy Memory.Provenance)
• metadata : Concurrency.SyncObject.Hooks S (Payload R)
• constant32 : Constant → M S UInt32
• constantBool : Constant → M S Int32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• readU32 : OpTy Memory.Provenance → M S UInt32
• readUsize : OpTy Memory.Provenance → M S UInt64
• derefInitOnce : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• readInitPointerFieldZero : MPlaceTy Memory.Provenance → M S UInt64
• derefPendingBool : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• newFutex : M S R
• monotonicDeadlineMillis : UInt32 → M S Concurrency.ThreadDeadline
• seqCstFence : M S Unit
• readAtomicAcquire : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S (Memory.Scalar Memory.Provenance)
• readScalar : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S (Memory.Scalar Memory.Provenance)
• lastError : Constant → M S Unit

def Miri.Interpreter.WindowsSync.initOnceData {S R : Type} (h : Hooks S R) (op : OpTy Memory.Provenance) : M S R

Equations

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

def Miri.Interpreter.WindowsSync.tryBegin {S R : Type} (h : Hooks S R) (ref : R) (pending dest : MPlaceTy Memory.Provenance) : M S Bool

Equations

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

def Miri.Interpreter.WindowsSync.beginInitialize {S R : Type} (h : Hooks S R) (op flags pending context : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsSync.complete {S R : Type} (h : Hooks S R) (op flags context : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.WindowsSync.waitOnAddress {S R : Type} (h : Hooks S R) (pointer compare size timeout : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsSync.wakeByAddress {S R : Type} (h : Hooks S R) (pointer : OpTy Memory.Provenance) (all : Bool) : M S Unit

Equations

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