Complete pinned concurrency/init_once.rs state transitions and typed callback execution. Rc identity is supplied by the same canonical registry.

@[reducible, inline]

abbrev Miri.Concurrency.InitOnce.M (σ α : Type) : Type

Equations

• Miri.Concurrency.InitOnce.M = EStateM Miri.Interpreter.StepError

inductive Miri.Concurrency.InitOnce.Status : Type

• Uninitialized : Status
• Begun : Status
• Complete : Status

@[instance_reducible]

instance Miri.Concurrency.InitOnce.instDecidableEqStatus : DecidableEq Status

Equations

• Miri.Concurrency.InitOnce.instDecidableEqStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.InitOnce.instReprStatus : Repr Status

Equations

• Miri.Concurrency.InitOnce.instReprStatus = { reprPrec := Miri.Concurrency.InitOnce.instReprStatus.repr }

def Miri.Concurrency.InitOnce.instReprStatus.repr : Status → Nat → Std.Format

Equations

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

structure Miri.Concurrency.InitOnce.State : Type

• status : Status
• waiters : List ThreadId
• clock : VClock

def Miri.Concurrency.InitOnce.instReprState.repr : State → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.InitOnce.instReprState : Repr State

Equations

• Miri.Concurrency.InitOnce.instReprState = { reprPrec := Miri.Concurrency.InitOnce.instReprState.repr }

structure Miri.Concurrency.InitOnce.Hooks (S R V D : Type) : Type

• runtime : SyncRuntime.Hooks S R V D
• get : R → M S State
• put : R → State → M S Unit
• new : M S R

def Miri.Concurrency.InitOnce.begin {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Unit

Equations

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

def Miri.Concurrency.InitOnce.enqueueAndBlock {S R V D : Type} (h : Hooks S R V D) (ref : R) (callback : SyncRuntime.Callback S) (capture : Option (SyncRuntime.UserCapture R D) := none) : M S Unit

Equations

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

def Miri.Concurrency.InitOnce.complete {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Unit

Equations

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

def Miri.Concurrency.InitOnce.fail {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Unit

Equations

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

def Miri.Concurrency.InitOnce.observeCompleted {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Unit

Equations

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