Core Concepts¶

Understanding the key concepts behind UPIR's architecture.

Overview¶

UPIR combines three powerful techniques:

Formal Verification - Prove correctness using SMT solvers
Program Synthesis - Generate code from specifications
Reinforcement Learning - Optimize from production data

The UPIR Workflow¶

graph LR
    A[Specification] --> B[Architecture]
    B --> C[Verification]
    C --> D{Valid?}
    D -->|Yes| E[Synthesis]
    D -->|No| F[Fix Architecture]
    F --> C
    E --> G[Deployment]
    G --> H[Metrics]
    H --> I[Learning]
    I --> J[Optimized Architecture]
    J --> C

Specify requirements using temporal logic
Verify architecture satisfies requirements
Synthesize implementation code
Deploy and collect metrics
Learn to optimize architecture
Iterate for continuous improvement

Formal Specification¶

Temporal Properties¶

UPIR uses Linear Temporal Logic (LTL) to express properties that must hold over time.

Operators¶

ALWAYS (□): Property holds at all times
Example: □ data_consistent - Data is always consistent
EVENTUALLY (◇): Property eventually holds
Example: ◇ task_complete - Task eventually completes
WITHIN (◇_{≤t}): Property holds within time bound
Example: ◇_{≤100ms} respond - Response within 100ms
UNTIL (U): P holds until Q becomes true
Example: processing U complete - Keep processing until complete

Example¶

from upir.core.temporal import TemporalOperator, TemporalProperty

# Safety property: Data consistency must always hold
safety = TemporalProperty(
    operator=TemporalOperator.ALWAYS,
    predicate="data_consistent"
)

# Liveness property: All events eventually processed
liveness = TemporalProperty(
    operator=TemporalOperator.EVENTUALLY,
    predicate="all_events_processed",
    time_bound=60000  # within 60 seconds
)

# Performance property: Low latency response
performance = TemporalProperty(
    operator=TemporalOperator.WITHIN,
    predicate="respond",
    time_bound=100  # within 100ms
)

Constraints¶

Hard constraints on resources and performance:

constraints = {
    "latency_p99": {"max": 100.0},      # Max p99 latency
    "latency_p50": {"max": 50.0},       # Max median latency
    "monthly_cost": {"max": 5000.0},    # Max monthly cost
    "throughput_qps": {"min": 10000.0}, # Min queries per second
    "availability": {"min": 0.999}      # Min 99.9% uptime
}

Architecture¶

Components¶

A component is a building block of your system:

component = {
    "id": "unique_id",
    "name": "Human-readable name",
    "type": "component_type",  # e.g., "database", "api_gateway"
    "latency_ms": 50.0,        # Component latency
    "cost_monthly": 500.0,     # Monthly cost in USD
    "config": {                # Component-specific config
        "key": "value"
    }
}

Connections¶

Connections define how components communicate:

connection = {
    "from": "component_a",
    "to": "component_b",
    "latency_ms": 5.0  # Network latency
}

Architecture Example¶

from upir.core.architecture import Architecture

architecture = Architecture(
    components=[
        {"id": "api", "type": "api_gateway", "latency_ms": 10},
        {"id": "db", "type": "database", "latency_ms": 50}
    ],
    connections=[
        {"from": "api", "to": "db", "latency_ms": 5}
    ]
)

Verification¶

UPIR uses Z3, a state-of-the-art SMT (Satisfiability Modulo Theories) solver, to verify that architectures satisfy specifications.

How It Works¶

Encode specification as SMT formulas
Translate temporal properties to first-order logic
Solve using Z3's constraint solver
Cache proven properties for incremental verification

Verification Results¶

from upir.verification.verifier import Verifier
from upir.verification.solver import VerificationStatus

verifier = Verifier()
results = verifier.verify_specification(upir)

# Possible statuses:
# - VerificationStatus.PROVED: All properties verified
# - VerificationStatus.FAILED: Counterexample found
# - VerificationStatus.UNKNOWN: Solver timeout or incomplete

Incremental Verification¶

UPIR caches proofs to speed up repeated verification:

# First verification: ~100ms
results1 = verifier.verify_specification(upir)

# Modify architecture slightly
upir.architecture.components[0]["latency_ms"] = 11

# Second verification: ~10ms (cached proofs reused)
results2 = verifier.verify_specification(upir)

Synthesis¶

UPIR uses CEGIS (Counterexample-Guided Inductive Synthesis) to generate implementation code from specifications.

How CEGIS Works¶

Sketch: Start with a program template with "holes"
Synthesize: Fill holes to satisfy specification
Verify: Check if synthesis is correct
Counterexample: If incorrect, use counterexample to refine
Iterate: Repeat until correct or max iterations

Synthesis Example¶

from upir.synthesis.cegis import Synthesizer

synthesizer = Synthesizer(max_iterations=10)

# Generate sketch from specification
sketch = synthesizer.generate_sketch(spec)

# Synthesize implementation
result = synthesizer.synthesize(upir, sketch)

if result.status.value == "SUCCESS":
    print(f"Generated code:\n{result.implementation}")
    print(f"Iterations: {result.iterations}")

Sketch Templates¶

Sketches define the structure with holes (??) to be filled:

def process_??_streaming(events):
    # Configure ??_framework
    pipeline = beam.Pipeline(options=??)

    # Read from ??_source
    events = pipeline | beam.io.ReadFromPubSub(??)

    # Transform with ??_logic
    processed = events | beam.Map(??)

    # Write to ??_sink
    processed | beam.io.WriteToBigQuery(??)

    return pipeline.run()

Learning & Optimization¶

UPIR uses PPO (Proximal Policy Optimization), a reinforcement learning algorithm, to optimize architectures from production metrics.

How It Works¶

Observe: Collect production metrics (latency, cost, throughput)
Reward: Compute reward based on performance
Policy: Neural network maps architecture to action probabilities
Update: Adjust architecture to maximize reward
Iterate: Repeat over many episodes

Learning Example¶

from upir.learning.learner import ArchitectureLearner

learner = ArchitectureLearner(upir)

# Simulate production metrics
metrics = {
    "latency_p99": 85.0,
    "monthly_cost": 4500.0,
    "throughput_qps": 12000.0
}

# Learn to optimize
optimized_upir = learner.learn(metrics, episodes=100)

print(f"Original cost: ${upir.architecture.total_cost}")
print(f"Optimized cost: ${optimized_upir.architecture.total_cost}")

Reward Function¶

The reward balances multiple objectives:

reward = (
    throughput_bonus  # Higher throughput = better
    - latency_penalty  # Lower latency = better
    - cost_penalty     # Lower cost = better
    + correctness_bonus  # Meets all requirements = big bonus
)

Pattern Management¶

UPIR can extract, store, and reuse proven architectural patterns.

Pattern Extraction¶

from upir.patterns.extractor import PatternExtractor

extractor = PatternExtractor()
pattern = extractor.extract(upir)

print(f"Pattern: {pattern.name}")
print(f"Success rate: {pattern.success_rate:.2%}")

Pattern Library¶

from upir.patterns.library import PatternLibrary

library = PatternLibrary()

# Add pattern to library
library.add_pattern(pattern)

# Find matching patterns
matches = library.match_architecture(upir, threshold=0.8)

for pattern, similarity in matches:
    print(f"{pattern.name}: {similarity:.2%} similar")

Built-in Patterns¶

UPIR includes 10 common distributed system patterns:

Streaming ETL - Real-time data pipelines
Batch Processing - Large-scale batch jobs
Request-Response API - Synchronous request handling
Event-Driven Microservices - Asynchronous event processing
Lambda Architecture - Batch + streaming hybrid
Kappa Architecture - Pure streaming architecture
CQRS - Command Query Responsibility Segregation
Event Sourcing - Event-driven state management
Pub/Sub Fanout - Message broadcasting
MapReduce - Distributed data processing

UPIR Instance¶

The UPIR class ties everything together:

from upir import UPIR

upir = UPIR(
    specification=spec,  # FormalSpecification
    architecture=arch    # Architecture
)

# Access components
upir.specification.properties  # List of temporal properties
upir.architecture.components   # List of components

# Compute metrics
total_latency = upir.architecture.total_latency_ms
total_cost = upir.architecture.total_cost

# Validate
is_valid = upir.validate()  # Basic validation

# Serialize
upir_json = upir.to_json()
upir_loaded = UPIR.from_json(upir_json)

Next Steps¶

Now that you understand the core concepts:

Formal Specifications Guide - Deep dive into specifications
Verification Guide - Learn SMT solving
Synthesis Guide - Master CEGIS
Learning Guide - Understand PPO optimization
Pattern Guide - Use pattern library