Signal Ownership and Effects¶

For step-by-step instructions on running and reading the analysis, see how-to/audit-signal-ownership.md. For the normative classification table, see reference/assurance.md.

Signal ownership analysis answers a question that static variable listings cannot: can two writers for the same output signal be simultaneously active in a single scan cycle, and if so, do they write the same value? This document explains why that question matters, how the ownership analysis approaches it, and what each outcome classification means in practice.

Why "who writes this variable?" is not enough¶

In a simple sequential program a signal has exactly one assignment site, and asking "who writes it?" gives you the full picture. In an SSFC with multiple lifecycle blocks the picture is more complex. A single output signal can be written from:

Multiple states, each in their DU (during) block
EN (entry) or EX (exit) blocks
OutputRule sections — priority-ordered conditional assignments that can span states
Parent lifecycle blocks that read child component outputs

STATE Heating
  EN:
    heater_command := WARM_UP;
  DU:
    heater_command := pid.output;
  EX:
    heater_command := OFF;
END_STATE

If Cooling.DU also writes heater_command, we have at least two writers. But knowing that two writers exist does not tell us whether they can conflict. They might belong to mutually exclusive states, in which case no conflict is possible. Or they might both become active during the same scan — for example, during a transition between states — in which case the question of what each one writes becomes safety-critical.

Simply enumerating WriteSites and listing the states associated with each does not answer the reachability question. the analysis goes further.

Lifecycle co-activation: what can happen in one scan¶

The SSFC execution model allows several lifecycle blocks to fire in a single scan. The most important cases are:

Transition scan (A → B): when state A transitions to state B, the following can all be True in the same scan: - A.EX — A's exit block fires because A is leaving - B.EN — B's entry block fires because B is being entered - B.DU — B's during block fires in the same scan as entry

Entry scan (any state A): in the first scan that A is active: - A.EN and A.DU always co-occur

This means two WriteSites whose conditions appear to be "different phases" can nevertheless both be active simultaneously. A signal written in A.EX and also in B.EN has two writers that are both active during an A→B transition.

Two WriteSites are called co-activatable if their activation conditions — state marking, lifecycle phase, and any guard expressions — can both be True simultaneously in some reachable scan configuration. The ownership analysis checks co-activatability for every pair of WriteSites for each output signal. The check is not a simulation; it is a formal query over the marking graph of the SSFC.

OwnershipClass: what each classification means¶

The result of the ownership analysis for a given signal is one of five classes.

SINGLE_WRITER¶

Exactly one WriteSite writes to this signal. The co-activation question does not arise; there is no second writer to conflict with.

EXCLUSIVE_MULTI_WRITER¶

Multiple WriteSites exist, but every pair has been proved mutually exclusive. The marking graph contains no reachable configuration in which both could be active in the same scan. This is not an assumption or a heuristic — it is a formal result derived from the SSFC's reachability structure. See the section on why this classification is safe for the reasoning.

COMPATIBLE_MULTI_WRITER¶

Some WriteSite pairs are co-activatable — the marking graph does admit configurations where both are active. However, for every such pair, the analysis has proved that both writers write the same value: either the write expressions are syntactically identical, or Z3 has established their equivalence. No observable conflict occurs because both writers agree on what to write.

CONFLICTING¶

At least one co-activatable pair writes different or unknown values. This is a design finding: a genuine write conflict exists that the analysis cannot resolve. The signal is written by two simultaneously active sites that disagree on the value to write.

This classification requires action. Options typically include restructuring the lifecycle logic so that the conflicting sites become mutually exclusive, or consolidating the writes into an OutputRule with an explicit priority order.

UNKNOWN¶

The analysis could not determine whether a particular pair of WriteSites is mutually exclusive. The solver reached a resource limit, encountered an encoding gap, or the state dependencies were too complex for the current analysis depth. UNKNOWN is conservative: it does not claim that a conflict exists. It means the analysis could not rule one out.

The epistemic distinction between CONFLICTING and UNKNOWN¶

This distinction matters for pipeline configuration:

CONFLICTING means co-activation is established and the values differ. The analysis has found a definite problem.
UNKNOWN means co-activation was neither proved nor disproved. The analysis has hit a limit.

A pipeline that only gates on conflict_free() will pass a signal classified UNKNOWN. A pipeline that requires both conflict_free() and analysis_complete() will flag UNKNOWN signals for manual review or deeper analysis. These gates serve different purposes and should be chosen deliberately.

Transitive component effects¶

A WriteSite that names a state as the writing location captures direct assignments in that state's lifecycle block. But an SSFC can also influence outputs indirectly through wired child components.

STATE Heating
  DU:
    WIRING
      pid(enable := Heating.X, setpoint := target_temp);
    END_WIRING

    heater_command := pid.output;
END_STATE

STATE Cooling
  DU:
    WIRING
      pid(enable := NOT Heating.X, setpoint := cool_temp);
    END_WIRING
END_STATE

Here heater_command is a direct assignment in Heating.DU. But pid.output depends on pid.enable, which is set differently by Heating.DU and Cooling.DU. The chain that connects a state to an output through a child component is called a ComponentEffect:

state activation
  → WIRING binding (S.X)
  → child instance input
  → child instance output
  → parent output assignment

ComponentEffects appear in the ownership report as transitive effects alongside direct WriteSites. They explain why a given state influences a signal indirectly, through the child component boundary. This makes the full dependency graph visible even when the assignment in the parent lifecycle block looks unconditional.

When to use conflict_free() vs analysis_complete()¶

The ownership analysis result object exposes three predicates for use in validation pipelines and acceptance tests.

conflict_free() — True when no signal in the analysed SSFC carries a CONFLICTING classification. This is the primary safety gate for write conflicts: it asserts that no pair of simultaneously active WriteSites disagrees on the value written. Most safety-relevant pipelines should check this.

analysis_complete() — True when no signal carries an UNKNOWN classification. UNKNOWN signals represent a gap in the analysis, not a confirmed conflict, but they leave open the possibility of an undetected conflict. Pipelines that require high confidence should check both conflict_free() and analysis_complete().

is_clean() — True when conflict_free() holds and no policy violations are present. This is the strictest gate and implies complete analysis under the active policy. Use it when both conflict freedom and policy conformance must be certified together.

EXCLUSIVE_MULTI_WRITER: why it is safe¶

The EXCLUSIVE_MULTI_WRITER classification can seem counterintuitive at first: if there are multiple writers, surely that is risky? The classification is architecturally sound for the following reason.

The mutual exclusion proof covers all reachable scan-cycle configurations of the SSFC. The ownership analysis does not check a sample of execution paths; it examines the full marking graph and verifies that no reachable marking exists in which both writers could be simultaneously active. This includes all transition sequences, parallel-region interleavings, and multi-step reachability.

A human reviewer can rely on this proof without needing to simulate execution scenarios or enumerate state sequences manually. The SSFC structure guarantees that if the marking graph has no configuration activating both writers, then no program execution — regardless of inputs or timing — will produce such a configuration.

The proof obligation is discharged once, statically, and the classification reflects the result. EXCLUSIVE_MULTI_WRITER is not a weaker form of SINGLE_WRITER; it is a formally equivalent safety guarantee achieved by a different structural argument.

What the analysis does not cover¶

Three boundaries are intentional approximations in the ownership analysis.

Intra-component analysis of child FBs. The ownership analysis treats child function block outputs as opaque at the WIRING boundary. If a child FB computes its output through complex internal logic, the analysis records the chain up to the child's output pin but does not trace into the child's implementation. Full inter-component analysis would require access to child internals and is outside the scope of the ownership analysis. Engineers who need guarantees about child FB behaviour should analyse those components separately under their own contracts.

Quantitative value range analysis. The ownership analysis checks whether two co-activatable writers produce the same value — by syntactic equality or Z3 equivalence of write expressions. It does not check whether they produce values in the same range. A pair of writers that both write pid.output would be classified COMPATIBLE_MULTI_WRITER even if pid.output could in principle span a wide range. Range and numerical safety properties are handled by the numerical representation analysis, not by ownership classification.

Sub-scan ordering of writes. All lifecycle blocks that fire in a given scan are treated as atomic with respect to each other. The analysis does not reason about sub-scan ordering: it asks "can both fire in the same scan?" and "what do they write?", but not "which fires first within that scan?". This is consistent with the LoLa execution model, where the observable state is the value present after the scan completes.