Lecture

Designing Provably Performant Networked Systems

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture by the instructor focuses on the design of networked systems with robust performance, emphasizing the need for real-time applications and parallel computation. The presentation covers the challenges of heuristics in network design, the importance of proving system properties before deployment, and the use of formal verification to gain insights into system performance. Case studies on congestion control algorithms like Copa and BBR are discussed, along with the exploration of delay jitter issues and the complexity of real-world network behaviors. The lecture concludes with a look at future research directions, including modularizing proofs and automatically synthesizing performant system designs.

Official source

Related concepts (32)

Parallel computing

Parallel computing is a type of computation in which many calculations or processes are carried out simultaneously. Large problems can often be divided into smaller ones, which can then be solved at the same time. There are several different forms of parallel computing: bit-level, instruction-level, data, and task parallelism. Parallelism has long been employed in high-performance computing, but has gained broader interest due to the physical constraints preventing frequency scaling.

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Heuristic

A heuristic (hjʊˈrɪstɪk; ), or heuristic technique, is any approach to problem solving or self-discovery that employs a practical method that is not guaranteed to be optimal, perfect, or rational, but is nevertheless sufficient for reaching an immediate, short-term goal or approximation. Where finding an optimal solution is impossible or impractical, heuristic methods can be used to speed up the process of finding a satisfactory solution. Heuristics can be mental shortcuts that ease the cognitive load of making a decision.

Social heuristics

Social heuristics are simple decision making strategies that guide people's behavior and decisions in the social environment when time, information, or cognitive resources are scarce. Social environments tend to be characterised by complexity and uncertainty, and in order to simplify the decision-making process, people may use heuristics, which are decision making strategies that involve ignoring some information or relying on simple rules of thumb.

Formal methods

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Related lectures (33)

Stainless Verification System Tutorial

Introduces Stainless, an open-source tool for verifying Scala programs, covering language, modeling, verification tips, and inner workings.

Timing and Performance Analysis: Model Checking

Covers timing and performance analysis using model checking and multiple objective scheduling.

Software Correctness: Testing and Verification

Explores software correctness through testing, verification, property-based fuzzing, and dynamic information flow control.

Dependable Architectures and Software

Explores dependable architectures, error detection, fault-tolerant structures, and software reliability through examples like the Patriot Missile failure and ABB dual controller.

Property-Based Testing: QuickChick