2 posts tagged with "protocol"

This week in Leios development, the team focused on simulation analysis and formal methods. Key accomplishments include detailed analyses of both Haskell and Rust simulations, initial work on a protocol dashboard, and advancements in formal methods through trace verification in Agda.

Cross-simulation analysis​

• Completed a comprehensive analysis of simulations at tag leios-2025w09:
  • Refactored the ELT workflow to improve simulation data processing
  • Modified the Rust simulator to generate fixed-size input blocks (IBs) for comparison with Haskell
  • Partially resolved discrepancies in congestion metrics between simulators
  • Developed detailed analyses of:
    • IB generation to receipt elapsed time
    • Time-in-flight over node-to-node links
  • Identified the dual role of network bandwidth and CPU bottlenecks in high throughput congestion.

Protocol dashboard initiative​

• Initiated the design of an interactive protocol dashboard with planned features:
  • Protocol parameter configuration
  • Stake distribution settings
  • Performance visualization:
    • Block arrival efficiency
    • Transaction duplication
    • Leios operation rewards
    • Resource utilization
  • Security metrics visualization:
    • Quorum failure analysis
    • Certificate forgery detection
    • Adversarial block tracking.

Rust simulation​

• Enhanced parallel message handling capabilities:
  • Implemented parallel mini-protocol message transmission
  • Added even bandwidth distribution between mini-protocols
  • Introduced the simulate-transactions configuration option
  • Updated simulation output for better Haskell compatibility
  • Improved block visualization for scenarios with high IB counts.

Formal methods​

• Commenced trace verifier development in Agda:
  • Added decidability to Short Leios protocol relational specification
  • Implemented a proof-by-computation approach for execution traces
  • Applied the successful methodology from Streamlet formalization.

This week in Leios development, CPS-0018 for transaction throughput was approved, along with improved Docker support for simulations and analysis of cross-simulation results. The team also examined input block (IB) production rates and their impact on network performance.

Protocol development​

• CPS-0018 'Greater transaction throughput' officially approved:
  • Merged into Cardano Foundation's CIP/CPS repository
  • Documents urgency of higher transaction throughput
  • Defines goals for the Leios initiative
  • Identifies key open questions and use cases.

Cross-simulation analysis​

• Conducted a comprehensive analysis of IB production rates ranging from 1 IB/s to 100 IB/s:
  • Developed an ELT workflow for data processing via MongoDB
  • Created an R Jupyter notebook for analysis and visualization
  • Identified and addressed three significant bugs (#207, #208, #209)
• Key findings from the Haskell simulation:
  • Network congestion emerges at high IB production rates
  • Both average propagation time and slow propagation tail increase
  • A critical threshold of ~40 IBs/s was identified, beyond which network congestion severely impacts block reception
• Comparison of PeerNet and Haskell simulations:
  • Both exhibit qualitatively similar block propagation distributions
  • Both demonstrate protocol breakdown under high block production rates
  • Differences in resolution and configuration prevent exact comparison.

Infrastructure improvements​

• Added comprehensive Docker support for both simulations:
  • Optimized multi-stage Docker files for Haskell and Rust
  • Simplified deployment process
  • Enabled easy configuration via volume mounts and parameters
  • Documented usage in README.md.

Rust simulation​

• Enhanced Rust simulation capabilities:
  • Implemented bandwidth usage tracking
  • Added configurable bandwidth limits per connection
  • Fixed issues identified in cross-simulation comparisons
  • Started updating visualizations for improved clarity.

Haskell simulation​

• Enhanced IB sortition handling for IB/slot < 1
• Began integrating block expiration and diffusion-halt proposal
• Implemented ideal timing calculations for diffusion:
  • Added uniform block behavior configuration
  • Identified relay mini-protocol complexities:
    • Variable latency (3-4) for block transfer
    • Latency depends on traffic conditions and request handling.

Formal methods​

• Moved formal specification to a dedicated repository
• Established a conformance testing framework:
  • Enabled testing between Short Leios implementations
  • Documented the test suite execution process
• Initiated a survey of network models across IO consensus projects.