Quantitative Formal Modeling and Worst-Case Performance Analysis
Welcome to "Quantitative Formal Modeling and Worst-Case Performance Analysis," an intellectually stimulating course designed to hone your abstract thinking skills in the realm of theoretical computer science. This course invites you to dive deep into the world of token production and consumption, a foundational approach to system behaviour. Master the art of mathematically formalizing these concepts through prefix orders and counting functions. Get hands-on with Petri-nets, explore the nuances of timing, and delve into the scheduling intricacies of token systems.
Monthly Subscription Starting at AED 99 + VAT
- Level Foundation
- Duration 17 hours
- Course by EIT Digital
-
Offered by
About
Welcome to Quantitative Formal Modeling and Worst-Case Performance Analysis. In this course, you will learn about modeling and solving performance problems in a fashion popular in theoretical computer science, and generally train your abstract thinking skills. After finishing this course, you have learned to think about the behavior of systems in terms of token production and consumption, and you are able to formalize this thinking mathematically in terms of prefix orders and counting functions. You have learned about Petri-nets, about timing, and about scheduling of token consumption/production systems, and for the special class of Petri-nets known as single-rate dataflow graphs, you will know how to perform a worst-case analysis of basic performance metrics, like throughput, latency and buffering. Disclaimer: As you will notice, there is an abundance of small examples in this course, but at first sight there are not many industrial size systems being discussed. The reason for this is two-fold. Firstly, it is not my intention to teach you performance analysis skills up to the level of what you will need in industry. Rather, I would like to teach you to think about modeling and performance analysis in general and abstract terms, because that is what you will need to do whenever you encounter any performance analysis problem in the future. After all, abstract thinking is the most revered skill required for any academic-level job in any engineering discipline, and if you are able to phrase your problems mathematically, it will become easier for you to spot mistakes, to communicate your ideas with others, and you have already made a big step towards actually solving the problem. Secondly, although dataflow techniques are applicable and being used in industry, the subclass of single-rate dataflow is too restrictive to be of practical use in large modeling examples. The analysis principles of other dataflow techniques, however, are all based on single-rate dataflow. So this course is a good primer for any more advanced course on the topic. This course is part of the university course on Quantitative Evaluation of Embedded Systems (QEES) as given in the Embedded Systems master curriculum of the EIT-Digital university, and of the Dutch 3TU consortium consisting of TU/e (Eindhoven), TUD (Delft) and UT (Twente). The course material is exactly the same as the first three weeks of QEES, but the examination of QEES is at a slightly higher level of difficulty, which cannot (yet) be obtained in an online course.Modules
Introduction
-
1
Videos
-
1
Readings
1
Videos
- Introduction
1
Readings
- Some suggested reading material
Drawing consumption/production models
-
6
Videos
-
1
Readings
-
2
Assignment
2
Assignment
- Basic modeling ideas
- Modeling Warehouse 13
6
Videos
- A single picture tells more than a thousand words
- Consumption and production of tokens
- Modeling an intensive care unit
- Modeling a wireless LAN radio
- Modeling and refining an industrial robot
- Pick your own system
1
Readings
- Always ask yourself...
Petri-nets and dataflow graphs
-
2
Videos
-
1
Assignment
1
Assignment
- Modeling features
2
Videos
- Classes of Petri-nets
- Causality, choice and concurrency (modeling patterns)
Refinement
-
2
Videos
-
1
Readings
-
2
Assignment
2
Assignment
- Definition of refinement
- Which is a refinement of which?
2
Videos
- Refinement of consumption/production systems
- Interpreting pictures for performance analysis
1
Readings
- The refinement of the robot.
A peer-reviewed modeling assignment
-
1
Videos
-
1
Readings
-
1
PeerReview
1
Peer Review
- Draw your own model
1
Videos
- Draw your own model
1
Readings
- Tooling
Warning: prepare for some set theory!
-
1
Videos
-
1
Readings
1
Videos
- Warning: prepare for some set theory!
1
Readings
- Flags and Fitch style proofs
Syntax and semantics
-
1
Videos
1
Videos
- Syntax and semantics
Formalizing pictures as bipartite graphs
-
2
Videos
-
1
Assignment
1
Assignment
- Bipartite graphs
2
Videos
- The basics
- Extensions
Formalizing behaviors as a prefix orders
-
3
Videos
-
1
Readings
3
Videos
- Prefix orders
- Exercise on prefix orders
- Proof that flows form a prefix order
1
Readings
- Slides of the proof
Formalizing interpretations as functions
-
2
Videos
-
2
Assignment
2
Assignment
- Thinking about observation functions
- Isomorphism
2
Videos
- Formalizing interpretations as functions
- Counting is order preserving
Formalizing the Petri-nets interpretation
-
2
Videos
-
1
Readings
-
1
Assignment
1
Assignment
- Summarize!
2
Videos
- Formalizing the Petri-net interpretation
- Proof that the number of tokens in a single-rate dataflow cycle is constant
1
Readings
- Slides of the proof
Formalizing time and scheduling
-
3
Videos
-
2
Readings
-
1
Assignment
1
Assignment
- Formalizing performance properties
3
Videos
- Formalizing timing
- Formalizing eager scheduling
- Formalizing periodic scheduling
2
Readings
- Exercise: Formalize best-case response times
- About the next quiz.
Running example
-
1
Videos
1
Videos
- Running example
Throughput and the maximum cycle mean
-
12
Videos
-
2
Readings
-
2
Assignment
2
Assignment
- Summarize!
- Calculating the MCM and worst-case throughput
12
Videos
- Throughput is bounded by 1/MCM
- Proof - a
- Proof - b
- Proof - c
- Proof - d
- Proof - e
- Proof - f
- Proof - g
- Proof - h
- Proof - i
- Proof - j
- The throughput bound is tight
2
Readings
- Slides of the proof
- Alternative proof in synchronization and linearity
Periodic scheduling
-
1
Videos
-
1
Assignment
1
Assignment
- Calculate some periodic schedules
1
Videos
- Periodic scheduling of a dataflow graph
Latency analysis
-
5
Videos
-
1
Assignment
1
Assignment
- Calculating optimal periodic schedules and their latencies
5
Videos
- Latency analysis of a periodic schedule
- Latency analysis of an eager schedule
- The formal definition of latency
- The boot-up time of a dataflow graph
- Optimizing latency estimates w.r.t. boot-up time
Buffering
-
1
Videos
-
1
Assignment
1
Assignment
- Calculating suitable buffer sizes
1
Videos
- Buffering and backpressure
One final example
-
1
Videos
-
5
Readings
1
Videos
- One final example
5
Readings
- 2015 Assignment on dataflow modeling.
- Additional dataflow exercises
- Example of an exam at masters level (without solutions)
- Another example of an exam (with solutions)
- Material created by fellow students
Auto Summary
Dive into Quantitative Formal Modeling and Worst-Case Performance Analysis, an IT & Computer Science course led by Coursera. Enhance your abstract thinking skills and learn to model and solve performance issues through mathematical formalization, focusing on Petri-nets, timing, and scheduling. Ideal for foundation-level learners, the course spans 1020 minutes and is part of the prestigious QEES curriculum from top Dutch universities. Available with a Starter subscription, it's perfect for those aiming to grasp theoretical computer science concepts.
Dr.ir. Pieter Cuijpers
Anne Remke