Proven performance guarantees in Time Sensitive Networking and Deterministic Networking
Event details
| Date | 06.02.2019 |
| Hour | 11:00 › 13:00 |
| Speaker | Ehsan Mohammadpour |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. Patrick Thiran
Thesis advisor: Prof. Jean-Yves Le Boudec
Co-examiner: Prof. Viktor Kuncak
Abstract
Time-Sensitive Networking (TSN) and Deterministic Networking (DetNet) define mechanisms for zero packet loss and bounded end-to-end latency. A known technique to compute these bounds is network calculus. Classical network calculus provides pessimistic bounds in feed-forward networks with per-class queuing due to the effect of multiplexing: burstiness of competing flows are accounted multiple times in the bound calculations. To address this issue, Pay-Multiplexing-Only-Once (PMOO) property was introduced to improve the latency bound by accounting the burstiness of competing flows once in the feed-forward networks. However, it does not apply to non-feed-forward networks with circular dependency due to burstiness cascade: individual flows may see their burstiness increase due to sharing one queue, that in turn causes burstiness of the downstream flows. In order to avoid this problem, the interleaved regulator was introduced to perform reshaping for the flows leading to have fresh flows at every hop. Interleaved regulators aggregate flows in one queue, while reshaping the packet at the head of the queue based on its flows regulation policy. Accordingly, latency and backlog bounds in any FIFO-based networks are obtained. Due to criticality of TSN/DetNet applications, it is necessary to certify the obtained bounds. Isabelle/HOL is a semi-automatic software framework to certify the theorems based on a trusted kernel, user-defined syntax and proof rules. This report also describes a research plan based on the three selected papers. To this end, rigorous theorems to compute latency and backlog bounds by using interleaved regulators in TSN/DetNet, a routing algorithm for TSN/DetNet flows, certification of the theorem with the Isabelle/HOL, and a TSN/DetNet simulator will be reported.
Background papers
A Theory of Traffic Regulators for Deterministic Networks with Application to Interleaved Regulators, by Prof J-Y., Le Boudec
Improving Performance Bounds in Feed-Forward Networks by Paying Multiplexing Only Once, by J.B., Schmitt et al.
Certifying Network Calculus in a Proof Assistant, by E. Mabille et al.
Exam president: Prof. Patrick Thiran
Thesis advisor: Prof. Jean-Yves Le Boudec
Co-examiner: Prof. Viktor Kuncak
Abstract
Time-Sensitive Networking (TSN) and Deterministic Networking (DetNet) define mechanisms for zero packet loss and bounded end-to-end latency. A known technique to compute these bounds is network calculus. Classical network calculus provides pessimistic bounds in feed-forward networks with per-class queuing due to the effect of multiplexing: burstiness of competing flows are accounted multiple times in the bound calculations. To address this issue, Pay-Multiplexing-Only-Once (PMOO) property was introduced to improve the latency bound by accounting the burstiness of competing flows once in the feed-forward networks. However, it does not apply to non-feed-forward networks with circular dependency due to burstiness cascade: individual flows may see their burstiness increase due to sharing one queue, that in turn causes burstiness of the downstream flows. In order to avoid this problem, the interleaved regulator was introduced to perform reshaping for the flows leading to have fresh flows at every hop. Interleaved regulators aggregate flows in one queue, while reshaping the packet at the head of the queue based on its flows regulation policy. Accordingly, latency and backlog bounds in any FIFO-based networks are obtained. Due to criticality of TSN/DetNet applications, it is necessary to certify the obtained bounds. Isabelle/HOL is a semi-automatic software framework to certify the theorems based on a trusted kernel, user-defined syntax and proof rules. This report also describes a research plan based on the three selected papers. To this end, rigorous theorems to compute latency and backlog bounds by using interleaved regulators in TSN/DetNet, a routing algorithm for TSN/DetNet flows, certification of the theorem with the Isabelle/HOL, and a TSN/DetNet simulator will be reported.
Background papers
A Theory of Traffic Regulators for Deterministic Networks with Application to Interleaved Regulators, by Prof J-Y., Le Boudec
Improving Performance Bounds in Feed-Forward Networks by Paying Multiplexing Only Once, by J.B., Schmitt et al.
Certifying Network Calculus in a Proof Assistant, by E. Mabille et al.
Practical information
- General public
- Free
Contact
- EDIC - [email protected]