Pinned shims/cpu_affinity.rs and the FreeBSD cpuset_getaffinity arm. Masks use target c_ulong chunks, not host endianness or pointer width.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.CpuAffinity.Mask : Type

Equations

• Miri.Interpreter.CpuAffinity.Mask = Vector UInt8 128

def Miri.Interpreter.CpuAffinity.maximumCpus : Nat

Equations

• Miri.Interpreter.CpuAffinity.maximumCpus = 1024

def Miri.Interpreter.CpuAffinity.set (chunkSize : Nat) (endian : ABI.Endian) (mask : Mask) (cpu : Nat) : Except StepError Mask

Source set ignores out-of-range CPUs before querying chunk layout.

Equations

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

def Miri.Interpreter.CpuAffinity.initial (chunkSize : Nat) (endian : ABI.Endian) (cpuCount : UInt32) : Except StepError Mask

Equations

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

def Miri.Interpreter.CpuAffinity.fromBytes (chunkSize : Nat) (endian : ABI.Endian) (cpuCount : UInt32) (bytes : ByteArray) : Except StepError (Option Mask)

Equations

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

structure Miri.Interpreter.CpuAffinity.Hooks (P S MD : Type) : Type

• os : String
• endian : ABI.Endian
• cpuCount : UInt32
• chunkSize : M S Nat
• readU32 : OpTy P → M S UInt32
• readI32 : OpTy P → M S Int32
• readI64 : OpTy P → M S Int64
• readUsize : OpTy P → M S UInt64
• readPointer : OpTy P → M S (Memory.Pointer (Option P))
• isNull : Memory.Pointer (Option P) → M S Bool
• masks : M S (Option (Array (Concurrency.ThreadId × Mask)))
• putMasks : Array (Concurrency.ThreadId × Mask) → M S Unit
• active : M S Concurrency.ThreadId
• linuxTid : UInt32 → M S (Option Concurrency.ThreadId)
• readBytes : Memory.Pointer (Option P) → UInt64 → M S ByteArray
• writeBytes : Memory.Pointer (Option P) → ByteArray → M S Unit
• writeZero : MD → M S Unit
• errnoNegOne : String → MD → M S Unit
• libcI32 : String → M S Int32

def Miri.Interpreter.CpuAffinity.getAffinity {P S MD : Type} (h : Hooks P S MD) (pid size mask : OpTy P) (dest : MD) : M S Unit

Equations

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

def Miri.Interpreter.CpuAffinity.setAffinity {P S MD : Type} (h : Hooks P S MD) (pid size mask : OpTy P) (dest : MD) : M S Unit

Equations

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

def Miri.Interpreter.CpuAffinity.freeBsdGetAffinity {P S MD : Type} (h : Hooks P S MD) (level which id size mask : OpTy P) (dest : MD) : M S Unit

Source FreeBSD legacy shim, including unused libc queries and null-pointer precedence over unsupported level/which values.

Equations

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