Thread joining and completion obligations

This follows concurrency/thread.rs::join_thread and join_thread_exclusive. It mutates the join status before waiting and leaves the completion synchronization and return-place write as ordered obligations. The source's actual callback and pointer write remain external actions; this module cannot silently complete them.

structure Miri.Concurrency.JoinReturn : Type

A join's opaque MIR scalar and destination place, preserved for the interpreter callback that eventually writes the return value.

• scalarToken : Nat
• placeToken : Nat

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqJoinReturn : DecidableEq JoinReturn

Equations

• Miri.Concurrency.instDecidableEqJoinReturn = Miri.Concurrency.instDecidableEqJoinReturn.decEq

def Miri.Concurrency.instDecidableEqJoinReturn.decEq (x✝ x✝¹ : JoinReturn) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Concurrency.instReprJoinReturn.repr : JoinReturn → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprJoinReturn : Repr JoinReturn

Equations

• Miri.Concurrency.instReprJoinReturn = { reprPrec := Miri.Concurrency.instReprJoinReturn.repr }

inductive Miri.Concurrency.JoinHandler : Type

• none : JoinHandler
• vectorClocks : JoinHandler

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqJoinHandler : DecidableEq JoinHandler

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprJoinHandler : Repr JoinHandler

Equations

• Miri.Concurrency.instReprJoinHandler = { reprPrec := Miri.Concurrency.instReprJoinHandler.repr }

def Miri.Concurrency.instReprJoinHandler.repr : JoinHandler → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.JoinError : Type

• thread (error : ThreadError) : JoinError
• detachedThreadUb (thread : ThreadId) : JoinError
• alreadyJoinedExclusiveUb (thread : ThreadId) : JoinError
• selfJoinUb (thread : ThreadId) : JoinError
• exclusiveJoinHasOtherWaiter (thread : ThreadId) : JoinError
• callbackUnblockedWithTimeout : JoinError
• callbackTokenMismatch (expected actual : Nat) : JoinError
• callbackTargetMismatch (expected actual : ThreadId) : JoinError
• callbackReasonMismatch (expected actual : BlockReason) : JoinError
• wrongHandler : JoinError

@[instance_reducible]

instance Miri.Concurrency.instReprJoinError : Repr JoinError

Equations

• Miri.Concurrency.instReprJoinError = { reprPrec := Miri.Concurrency.instReprJoinError.repr }

def Miri.Concurrency.instReprJoinError.repr : JoinError → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.JoinCompletionError : Type

• handlerMismatch : JoinCompletionError
• callbackUnblockedWithTimeout : JoinCompletionError
• globalStateRequired : JoinCompletionError
• globalState (error : GlobalStateError) : JoinCompletionError

def Miri.Concurrency.instReprJoinCompletionError.repr : JoinCompletionError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprJoinCompletionError : Repr JoinCompletionError

Equations

• Miri.Concurrency.instReprJoinCompletionError = { reprPrec := Miri.Concurrency.instReprJoinCompletionError.repr }

structure Miri.Concurrency.JoinCompletionObligation : Type

join_thread's after_join work, in source order. The selected handler must run before the interpreter writes the scalar to the destination.

• joiner : ThreadId
• joinee : ThreadId
• callbackToken : Nat
• returnValue : JoinReturn
• handler : JoinHandler

@[instance_reducible]

instance Miri.Concurrency.instReprJoinCompletionObligation : Repr JoinCompletionObligation

Equations

• Miri.Concurrency.instReprJoinCompletionObligation = { reprPrec := Miri.Concurrency.instReprJoinCompletionObligation.repr }

def Miri.Concurrency.instReprJoinCompletionObligation.repr : JoinCompletionObligation → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.JoinPlan : Type

• completedImmediately (manager : ThreadManager) (completion : JoinCompletionObligation) : JoinPlan
• waiting (manager : ThreadManager) (callback : JoinCompletionObligation) : JoinPlan

@[instance_reducible]

instance Miri.Concurrency.instReprJoinPlan : Repr JoinPlan

Equations

• Miri.Concurrency.instReprJoinPlan = { reprPrec := Miri.Concurrency.instReprJoinPlan.repr }

def Miri.Concurrency.instReprJoinPlan.repr : JoinPlan → Nat → Std.Format

Equations

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

def Miri.Concurrency.JoinPlan.manager : JoinPlan → ThreadManager

Equations

• (Miri.Concurrency.JoinPlan.completedImmediately a a_1).manager = a
• (Miri.Concurrency.JoinPlan.waiting a a_1).manager = a

def Miri.Concurrency.ThreadManager.prepareJoin (manager : ThreadManager) (joinee : ThreadId) (returnValue : JoinReturn) (handler : JoinHandler) (callbackToken : Nat) : Except JoinError JoinPlan

Prepare the ordinary Miri join. The active thread is the joiner. The caller supplies the callback token allocated by its interpreter layer.

Equations

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

def Miri.Concurrency.ThreadManager.prepareJoinExclusive (manager : ThreadManager) (joinee : ThreadId) (returnValue : JoinReturn) (handler : JoinHandler) (callbackToken : Nat) : Except JoinError JoinPlan

Miri's exclusive join checks the existing Joined status, self-join, and absence of other waiters before taking the ordinary path.

Equations

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

def Miri.Concurrency.ThreadManager.afterJoinUnblock (callback : JoinCompletionObligation) (unblock : UnblockCallbackObligation) : Except JoinError JoinCompletionObligation

Apply the join completion callback after an actual Ready unblock. The callback does not claim synchronization or write success; it produces a continuation requiring those effects in the exact source order.

Equations

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

def Miri.Concurrency.completeVectorClockJoin (state : GlobalState) (threads : ThreadManager) (completion : JoinCompletionObligation) : Except JoinCompletionError (GlobalState × JoinReturn)

Equations

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