russell@unturf.com
0a580b313d
Authors: russell@unturf.com · brackishbert@gmail.com · foxhop.net · TimeHexOn.com Patches, unit tests, benchmarks, whitepaper, and outreach briefs. Public domain — no copyright claimed. Use freely.
214 lines
6.9 KiB
ReStructuredText
214 lines
6.9 KiB
ReStructuredText
Formal Complexity Model
|
||
========================
|
||
|
||
.. contents:: :local:
|
||
|
||
Definitions
|
||
-----------
|
||
|
||
Let G = (V, E) be a directed graph with |V| = n vertices and |E| = m edges.
|
||
|
||
A **CWE-407 graph traversal defect** occurs when a function f satisfies all of the following:
|
||
|
||
1. f is called inside a loop that iterates O(n) times (one call per vertex or edge)
|
||
2. f accepts a collection L as an argument (or closes over L)
|
||
3. f performs a membership test ``x ∈ L`` where ``x`` is a graph node or edge identifier
|
||
4. L is represented as a list/array/vector such that ``x ∈ L`` costs O(|L|)
|
||
5. |L| grows with the traversal: |L| = O(n) at the point of the i-th call
|
||
|
||
Under these conditions, the total cost of all membership tests is:
|
||
|
||
.. math::
|
||
|
||
\sum_{i=0}^{n-1} O(i) = O\!\left(\frac{n(n-1)}{2}\right) = O(n^2)
|
||
|
||
where the defective code achieves O(n²) and the achievable lower bound is O(n).
|
||
|
||
The Quadratic Proof
|
||
--------------------
|
||
|
||
**Theorem:** Any DFS or BFS graph traversal algorithm that maintains ``visited`` or ``onStack``
|
||
state as a list and performs a linear scan for membership has worst-case time complexity O(V²).
|
||
|
||
**Proof:**
|
||
|
||
Consider a Tarjan SCC traversal on a graph G = (V, E). The algorithm visits each vertex once.
|
||
For each vertex v visited, it performs one membership test on the ``stack`` structure:
|
||
|
||
- At the time of the i-th test, the stack contains at most i−1 elements
|
||
- The membership test on a list costs O(i)
|
||
- Summing over all vertices: T(n) = Σᵢ₌₁ⁿ O(i) = O(n(n+1)/2) = O(n²)
|
||
|
||
This result is tight: the ``starWithBackEdges(n)`` topology (one hub connected to n spokes,
|
||
each spoke with a back-edge to the hub) achieves exactly n(n+1)/2 − 1 comparisons in the
|
||
defective implementation. This is confirmed by unit test operation counts in
|
||
``tests/unit/GraphUtilsDefectTest.java``. ∎
|
||
|
||
The O(1) Membership Bound
|
||
--------------------------
|
||
|
||
**Theorem:** Hash table membership tests are O(1) amortized.
|
||
|
||
**Proof sketch:** A hash table with load factor α < 1 stores n elements in a table of size
|
||
⌈n/α⌉. Under a uniform hash function, the expected number of comparisons for a membership
|
||
test (with chaining) is:
|
||
|
||
.. math::
|
||
|
||
E[\text{comparisons}] = 1 + \frac{\alpha}{2} = O(1)
|
||
|
||
as α is bounded by a constant (typically 0.75). Rehashing occurs at most O(log n) times
|
||
over n insertions, each rehash costs O(n), giving amortized O(1) per insertion. Since
|
||
membership tests do not trigger rehashing, they are O(1) worst-case after construction. ∎
|
||
|
||
For the specific use case of CWE-407 graph traversal fixes, the load factor argument is
|
||
conservative: the visited set is used write-heavy (one insert per vertex, one read per edge),
|
||
and the hash keys are object references or integer node IDs — both hash in O(1) time with no
|
||
collision risk from adversarial inputs, since the key space is controlled by the traversal.
|
||
|
||
Canonical Fix Complexity
|
||
-------------------------
|
||
|
||
After replacing the list with a hash set for visited/onStack state:
|
||
|
||
- DFS traversal: each vertex visited once, O(1) membership test per vertex → **O(V)**
|
||
- BFS traversal: each vertex enqueued once, O(1) set-membership check → **O(V + E)**
|
||
- Tarjan SCC: each vertex pushed/popped once, O(1) onStack test → **O(V + E)**
|
||
- Cycle detection: one O(1) set-insert per vertex → **O(V)**
|
||
|
||
All patched implementations achieve the theoretically optimal O(V + E) for connected-graph
|
||
traversal.
|
||
|
||
Exact Operation Counts (Measured)
|
||
-----------------------------------
|
||
|
||
The following operation counts are from unit tests that instrument comparison/insertion
|
||
counters directly (not wall-clock timing), verifying the formulas precisely:
|
||
|
||
.. list-table::
|
||
:header-rows: 1
|
||
:widths: 15 20 30 20 20
|
||
|
||
* - Defect
|
||
- V / N
|
||
- Defective formula
|
||
- Fixed formula
|
||
- Formula name
|
||
* - javac-0001
|
||
- V nodes
|
||
- V*(V+1)/2 - 1
|
||
- V - 1
|
||
- ``starWithBackEdges(V)``
|
||
* - javac-0002a
|
||
- N type vars
|
||
- N*(N+1)/2
|
||
- N
|
||
- ``queryAll(N)``
|
||
* - javac-0002b
|
||
- V nodes, K calls
|
||
- K*V
|
||
- V + (K-1)
|
||
- ``closureFixed K on chain(V)``
|
||
* - javac-0003
|
||
- V modules
|
||
- V*(V-1)/2
|
||
- V
|
||
- ``linearChain(V)``
|
||
* - javac-0004
|
||
- M deps
|
||
- M*(M-1)/2
|
||
- M
|
||
- ``addUnique(M)``
|
||
* - javac-0005
|
||
- B bounds
|
||
- B*(B+1)
|
||
- B
|
||
- ``isEquiv forward vs reversed(B)``
|
||
|
||
The formulas are exact, not asymptotic. The unit tests verify equality, not inequality, at
|
||
each sample point.
|
||
|
||
Balanced BST vs Hash Table
|
||
---------------------------
|
||
|
||
Several fix patterns use balanced BST sets (``Data.Set`` in Haskell, ``gb_sets`` in Erlang,
|
||
``TreeSet`` in Java) rather than hash sets. These give O(log n) membership rather than O(1).
|
||
This is still a strict improvement over O(n) for all n ≥ 2, but is suboptimal compared to
|
||
a hash set. The tradeoff:
|
||
|
||
- **Hash set (O(1)):** requires ``Hash`` + ``Eq`` trait bounds; no element ordering
|
||
- **BST set (O(log n)):** requires only ``Ord``; provides sorted iteration
|
||
- **List (O(n)):** requires only ``Eq``; provides insertion-order iteration
|
||
|
||
For the visited/onStack use case, the ordering provided by BST sets is never needed — hash
|
||
sets are always the correct fix. In languages where hash sets require an additional trait
|
||
bound not already on the node type (e.g., Haskell ``Hashable``), BST sets with ``Ord`` are
|
||
an acceptable intermediate fix.
|
||
|
||
Four Canonical Fix Patterns
|
||
-----------------------------
|
||
|
||
**Python:**
|
||
|
||
.. code-block:: python
|
||
|
||
# Before
|
||
visited = []
|
||
if node in visited: ...
|
||
|
||
# After
|
||
visited = set()
|
||
if node in visited: ...
|
||
|
||
**Java:**
|
||
|
||
.. code-block:: java
|
||
|
||
// Before
|
||
List<Node> visited = new ArrayList<>();
|
||
if (visited.contains(node)) ...
|
||
|
||
// After
|
||
Set<Node> visited = new HashSet<>();
|
||
if (!visited.add(node)) ... // add() returns false if already present
|
||
|
||
**Haskell:**
|
||
|
||
.. code-block:: haskell
|
||
|
||
-- Before (O(n))
|
||
if v `elem` visited then ...
|
||
|
||
-- After with Data.Set (O(log n))
|
||
if Set.member v visited then ...
|
||
|
||
-- After with Data.HashMap (O(1))
|
||
if HashMap.member v visited then ...
|
||
|
||
**Erlang:**
|
||
|
||
.. code-block:: erlang
|
||
|
||
%% Before (O(n))
|
||
case lists:member(V, Visited) of ...
|
||
|
||
%% After with gb_sets (O(log n))
|
||
case gb_sets:is_member(V, Visited) of ...
|
||
|
||
%% After with maps (O(1))
|
||
case maps:is_key(V, Visited) of ...
|
||
|
||
Semantic Preservation
|
||
----------------------
|
||
|
||
The fix is semantically identical to the original in all confirmed defect sites because:
|
||
|
||
1. The visited/onStack set **never contains duplicates by construction** — elements are added
|
||
exactly once and never added if already present
|
||
2. Therefore, set membership returns the identical boolean as list membership for all inputs
|
||
that occur in practice
|
||
3. The patch changes only the **representation** of the set, not the **semantics** of membership
|
||
|
||
This is proven by the unit tests: for all tested inputs, the patched and original implementations
|
||
produce identical output (same SCCs, same topological orders, same cycle-detection results).
|
||
Only performance differs.
|