07-EFT.WP.Core.Threads v1.0 | Chapter 4 — Timing, Consistency, and Failure Semantics

Home ／ Docs-Technical WhitePaper ／ 07-EFT.WP.Core.Threads v1.0

Chapter 4 — Timing, Consistency, and Failure Semantics

I. Scope and Objectives

• Unify the clock system and time bases: tau_mono (monotonic clock) and ts (UTC); define mapping, drift, and calibration rules.
• Formalize the hb (happens-before) relation and visibility boundaries; specify delivery semantics and the interface contract for compensating transactions.
• Provide composite upper bounds for timeout, retry, and jitter; define metrics and governance for reordering, duplication, and deduplication windows.
• Deliver postulates P74-, minimal equations S74-, the operational flow Mx-3, and alignment with implementation interfaces I70-4/I70-7/I70-8/I70-9.

II. Clock System and Mapping (tau_mono ↔ ts)

1. Baseline mapping and drift
   • S74-1: ts(t) approx tau_mono(t) + offset + skew * ( tau_mono(t) - tau0 ), with |offset| <= eps_off, |skew| <= eps_skew.
   • P74-1 (Timing consistency): all evaluations of timeouts, retries, and jitter must be measured on tau_mono; auditing and external events are recorded in ts.
2. Synchronization and re-calibration
   • Trigger: when |ts_obs - ts(tau_mono)| > eps_resync or cumulative drift exceeds threshold.
   • Action: update offset/skew, record eid_sync, and attach calibration evidence in Trace.
3. Arrival-time calibration (cross-volume anchor)
   • S74-2 (dual-form in parallel)
     T_arr = ( 1 / c_ref ) * ( ∫ n_eff d ell )；T_arr = ( ∫ ( n_eff / c_ref ) d ell )。
     Discrepancy report: delta_form = | ( 1 / c_ref ) * ( ∫ n_eff d ell ) - ( ∫ ( n_eff / c_ref ) d ell ) |。
   • P74-2 (Alignment rule): when T_arr is used to calibrate ts, the path gamma(ell) and the measure d ell must be explicit, and the manifest must record both formulations and delta_form.

III. Causality and Visibility: the hb Relation

1. Core definition
   • hb is a strict partial order: irreflexive, antisymmetric, transitive (we use its transitive closure in this volume).
   • Generation rules:
     1. Program order within a thread: if u -> v, then hb(u,v).
     2. Send–receive edge: if send(msg) -> recv(msg), then hb(send,recv).
     3. Synchronization: if release(x) -> acquire(x), then hb(release,acquire).
     4. Lifecycle: spawn(child) -> start(child), done(child) -> join(child).
2. Visibility boundary
   • P74-3 (Commit boundary): only writes that cross an hb edge are visible to successors; non-crossing effects remain local.
   • P74-4 (Compensation first): if an hb-consistent history cannot be provided to external observers, publish compensating events compensate(eid_parent) (see §V).

IV. Composite Bounds for Timeout, Retry, and Jitter

1. Time budget and upper bounds
   • S74-3: W_retry <= timeout * ( retries + 1 ) + J_total, where J_total = ∑ J_i。
   • S74-4 (Success probability, independent drops): p_ok = 1 - ( p_drop )^( retries + 1 )。
   • P74-5 (Budget closure): deadline must satisfy deadline >= W_retry + margin; otherwise requests must not be issued or must be degraded.
2. Budget decomposition
   budget_total = W_q_in + w(proc) + W_q_out + W_net; SLO-facing target: P99(budget_total) <= SLO.

V. Delivery Semantics and Compensating Transactions

1. Semantic tiers
   • sem="at_most_once": no retry, minimal latency, highest loss risk.
   • sem="at_least_once": duplicates allowed; requires idempotent idemp_key with a deduplication window.
   • sem="exactly_once*": approximate once-only via idempotent storage and dedup tables.
2. Compensation and SAGA
   • P74-6 (Reversible pairs): every external side-effect op_i must provide op_i^{-1} or declare non-reversibility and an isolation strategy.
   • Minimal sequence: do1 -> do2 -> commit_k -> ...; if do_j fails and cannot continue, trigger compensation in reverse: do_{j-1}^{-1} -> ... -> do1^{-1}。
   • Audit: record the hb chain of eid_flow and eid_comp and the final ruling.

VI. Reordering, Duplication, and the Deduplication Window

1. Reorder bound and watermarks
   • Define reordering span: span_reorder = max( ts_recv - ts_send ) (bounded per-idemp_key stream).
     S74-5: span_reorder <= J_net + eps_off + |skew| * Delta_t_window。
   • Watermark progression: watermark(t) = min_observed_ts_up_to(t) to decide the “definitely late” threshold.
2. Dedup table and window
   • Structure: dedup_table = {(idemp_key) -> ts_last}。
   • Rule: if tau_mono_now - ts_last <= Delta_t_dedup then drop duplicate else accept and update ts_last。
   • P74-7 (Explicit window): Delta_t_dedup must be declared, coordinated with span_reorder and ttl: Delta_t_dedup >= span_reorder, ttl >= Delta_t_dedup.

VII. Failure Model and Semantic Adjudication

1. Failure classes
   Crash-stop (process), omission (lost packet/ACK), partition (network split), timing (timeout/jitter anomaly).
2. Adjudication
   • P74-8 (Partition precedence): when a partition conflicts with the SLA_window, prioritize idempotence and consistency; degrade or switch to read-only if necessary.
   • P74-9 (Cancellation propagation): cancel_token propagates across hb edges; upon cancel, no new external side-effects may be initiated.

VIII. Transaction Boundaries, Idempotence, and Approximate Once Semantics

1. Idempotence contract
   Definition: f(x; idemp_key) = f(x; idemp_key) (identity).
   P74-10: any externally visible write must be guarded by an idemp_key or an idempotent storage layer.
2. Outbox/Inbox patterns
   • Outbox: business mutation and message persistence in the same transaction; an async forwarder delivers.
   • Inbox: consumer first writes idempotently, then applies business mutation; afterward writes an acknowledgment bit.
3. Approximate once
   S74-6 (Minimal sufficient conditions, engineering): atomic( write(idemp_key, state) ) ∧ dedup(Delta_t_dedup) ∧ ack(ordered)。

IX. Consistency Levels and Read Views

• Read levels
  read_local (thread-local), read_committed (across hb commit boundary), read_linearizable* (requires total-order arbitration and quorum clocks).
  Asterisk denotes engineering approximations subject to eps_off/eps_skew and arbitration latency.
• View construction
  P74-11 (Monotone views): consecutive reads by the same consumer on the same key must be monotone; enforce via version stamps or monotone watermarks.

X. Observability and SLIs (Timing and Semantic Dimensions)

• Core metric families
  TS.sli.latency_ms{P50,P95,P99}, TS.sli.timeout_rate, TS.sli.retry_rate, TS.sli.reorder_span_ms, TS.sli.dup_rate, TS.sli.compensate_rate。
• Audit invariants
  S74-7: within a window, verify check_dim( L - lambda * W ) = 0; anomalies trigger re-estimation of lambda/mu and eps_skew/eps_off.

XI. Interface Bindings (I70 Alignment Summary)

• Timing and tracing: with_timeout(timeout), trace_span(name, ...), trace_link(span, eid)。
• Retry and idempotence: retry(policy), ensure_idempotent(fn, key_fn, window=Delta_t_dedup)。
• Binding to data specs: bind_to_parameters, bind_to_equations, enforce_arrival_time_convention (for T_arr alignment).
• P74-12 (Interface constraints): retry policies must be declared jointly with with_timeout and satisfy S74-3; the ensure_idempotent window must equal Delta_t_dedup.

XII. Contracts and Test Matrix (Configured via I70-8)

1. Required tests
   • hb guarantees: visibility tests for spawn/start, release/acquire, send/recv edges.
   • Timeout composition: given timeout/retries/J_total, verify the upper bound on W_retry and the success probability p_ok.
   • Reordering and dedup: construct extreme span_reorder scenarios and verify Delta_t_dedup neither misses nor overkills.
   • Compensating transactions: under partial-failure timelines, compensate applies in reverse order and external state rolls back consistently.
2. Assertion samples
   assert_thread_contract(G,[ {"type":"hb_edges","edges":["send->recv","release->acquire"]}, {"type":"timeout_retry","W_retry_le":budget}, {"type":"dedup","window":Delta_t_dedup}, {"type":"saga","compensate_order":"LIFO"} ])。

XIII. Operational Flow Mx-3 (Timing and Semantics Closure)

• Choose time base and initial offset/skew; enable tau_mono timing and ts auditing.
• If cross-domain calibration is involved, compute T_arr (both forms), apply alignment, and record delta_form.
• Configure timeout/retries for critical paths; decompose the budget per S74-3 and set alert thresholds.
• Mark idempotent keys for external side-effects, configure Delta_t_dedup, and implement Outbox/Inbox.
• Exercise the test matrix to trigger hb, reordering, duplication, and compensation cases; refine policies until all pass.
• Post-deploy, continuously collect TS.sli.*; when reorder_span_ms or dup_rate exceeds thresholds, tune Delta_t_dedup and retry strategies dynamically.

XIV. Exit Criteria and Deliverables

• Pass P74-, S74-, and the full Mx-3 validation; persist TS.sli.* metrics and meet declared SLOs.
• Deliverables include: clock mapping and calibration records, hb proof sketch, timeout/retry strategy cards, Delta_t_dedup and compensation inventories, and the assert_thread_contract report.