The actual clock-state boundary used by source synchronization operations. Legacy pure transitions retain GlobalState; canonical runtime transitions carry Option GlobalState. No absent-state implementation constructs a clock. release_clock exposes its source callback point before incrementing the clock.

inductive Miri.Concurrency.SyncClockError : Type

• missingGlobal : SyncClockError
• global (error : GlobalStateError) : SyncClockError

@[instance_reducible]

instance Miri.Concurrency.instReprSyncClockError : Repr SyncClockError

Equations

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

def Miri.Concurrency.instReprSyncClockError.repr : SyncClockError → Nat → Std.Format

Equations

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

class Miri.Concurrency.SyncClockState (G : Type) : Type

• acquire : G → ThreadManager → VClock → Except SyncClockError G
• prepareRelease : G → ThreadManager → Except SyncClockError (VClock × Except SyncClockError G)

  First failure is before the source callback; the nested result is after the callback and retains its effects when clock increment fails.

@[instance_reducible]

instance Miri.Concurrency.instSyncClockStateGlobalState : SyncClockState GlobalState

Equations

• Miri.Concurrency.instSyncClockStateGlobalState = { acquire := Miri.Concurrency.acquireGlobal✝, prepareRelease := Miri.Concurrency.releaseGlobal✝ }

@[instance_reducible]

instance Miri.Concurrency.instSyncClockStateOptionGlobalState : SyncClockState (Option GlobalState)

Equations

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

theorem Miri.Concurrency.absent_acquire (threads : ThreadManager) (clock : VClock) : SyncClockState.acquire none threads clock = Except.error SyncClockError.missingGlobal

An absent clock is a representation error if a VClock operation is requested. Source None-mode skips the operation before reaching this boundary.

theorem Miri.Concurrency.absent_release (threads : ThreadManager) : SyncClockState.prepareRelease none threads = Except.error SyncClockError.missingGlobal