Proof - i

Loading...

En provenance du cours de EIT Digital

Quantitative Formal Modeling and Worst-Case Performance Analysis

36 notes

EIT Digital

Quantitative Formal Modeling and Worst-Case Performance Analysis

36 notes

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.

À partir de la leçon

Performance analysis

In this module/week you will learn to exploit the structure of single-rate dataflow graphs to perform worst-case analysis of performance metrics like throughput, latency and buffering. After this week, you know how to calculate the maximum cycle mean of a dataflow graph, how to construct a periodic schedule for it, how to optimize this schedule for latency analysis, and how to determine the size of buffers with back-pressure such that the worst-case analysis remains valid. If you understood the material of the previous module/week, the proofs presented in this week will give you a deeper understanding of the mathematical underpinning of these methods.

Throughput is bounded by 1/MCM8:35

The throughput bound is tight5:05

Rencontrer les enseignants

Dr.ir. Pieter Cuijpers
Assistant Professor
Mathematics and Computer Science
Anne Remke
Prof. dr.
Computer Science

[MUSIC]

Okay, so we have worst case response times defined, and

we know that the worst case response time of a production arrow is related to

the worst case response times of previous production arrows in the graph.

And we still need to prove that N over PN in the limit

is going to get bigger than one over the maximum cycle mean,

or the through put requirement that we already had on the input of the graph.

Now, the next step is to look at paths in the graph.

I mean, we know one previous that we can relate it to one previous actor but

now we want to go a little bit longer.

We want to look at multiple steps in the graph.

What do I mean by that?

Well, suppose that we want

to calculate for this production arrow P2

the worst case time at which four tokens have come out.

Then we can use our formula to derive that we are certain that this is actually

before the time, at which consumption has taken place here plus two or

better this Q and then two before.

So this is before the time at which the worst case response time of

Q for two tokens plus the two seconds of the worst case response time of the actor.

And that, if we look at that problem we can just go back in the graph,

again and we can look at this one or

at that one and that one and that one, right?

So we have to take maximum and we know that this is

smaller than the maximum of many possibilities.

Well, first one was P1 and there is one token in the way in-between here.

So that is P1 of two- one is one + of course this

two + also this one, so that's + three.

And it's smaller than the input, P input of 1,

so the worst case time at which one token comes out of the input,

and it's smaller than.

Well, what would this be?

It would be the same as this F, right?

Because, tokens fire at the same time so F of well,- four,

so that would be F of- 2, which is interesting, + 3.

This is also plus 3, of course or we can go up all the way here.

And see that it's R2 of 1, because this is actually an empty,

but first, so R2 of 2, sorry, + 3.

Well, and then we have to look, again,

we can see that the input, well we cannot do anything about that.

If we reach back to the input then

we have to use our assumptions that we know something about the input.

But, we can also look at this F- 2,

which means it is the first time at which- 2 tokens have been produced by F.

And well, that is actually impossible so

that would be give you the empty set and the supreme M over the empty set

if we consider only positive numbers would be zero so this is actually zero

which means that it gives us + 3.

And now we see that by going back in the graph,

you eventually either get to the input or

you get to a point where the term that refers back to

a worst case production time becomes zero.

So what we are looking for is long path inter graph up to the point in

time where we are below zero, regarding the number of tokens for

which we want to calculate the worst case production time.

That means that we just have to take paths back into the graph until the number of

tokens that occur in the buffers along that pass has dropped below zero.

Right?

And over all of those paths we have to take the maximum.

So what does that look like in a formula?

It looks like this.

We say PN is smaller than the maximum of well,

we start by taking all paths that end in P.

But all paths that end in P, that may be too many.

We are sure that we only want paths in which the number of tokens on the path,

and I've used some sloppy notation maybe and wrote I of X but

that's actually of course the sum for all the buffers in the past.

And the past is just defined in the same way as I defined the cycle

back in week two all the buffers in the past, and

then you add up the initial number of tokens in that buffer.

If all the tokens on a pass, they need to be bigger than N,

otherwise we are not going to consider the pass.

And the nice thing is you also know that it can be smaller than N + I,

where I is the maximum for

all buffers in the graph, so B and B of Iota B.

Why is that?

Well, while we were going back in the graph, we asked new buffers to a path,

And we want to get a number of buffers in a path bigger than N,

but once it's bigger than N, we want to stop.

And, well, how much do we add?

Well, every time we take a step back in the graph,

we add the number of tokens that is in a buffer.

So we can only overshoot N by the amount of tokens that is in the buffer, right?

If you are just before N and

we add that amount, then we overshoot N by a little bit, but

the most we can overshoot N by is by the maximum number of tokens in the buffer.

So we know that the path that we are interested in

has a number of tokens that lies between N and N + I.

Or, we have a path that starts at the input and

ends in P and has a number of tokens that is less than N.

Those paths are also interesting.

If we know those paths, if we have all those paths,

then we can start looking at the total production time on these paths.

And now there's something interesting going on.

If a path X is long enough, then, the total production time,

sigma A N X of tau A.

Well, you can actually provide that as

the number of tokens on that path.

Right.

So, that's delta

X x the sum of tau A for A in X.

So, it's a bit scribbly divided by your tau X, right?

We can multiply and divide by your tax without any cost.

And this is the cycle mean of the path.

So this is smaller than the maximum cycle mean of the graph.

This is smaller than iota X x the maximum cycle mean.

Which means that this term can be replaced by iota X x the maximum cycle mean.

Well, almost, because it could be that there is also

a part that is not in a cycle.

And that part, well it can only finitely long because since we have a finite graph,

you can only have a finitely long path before you have to cycle in the path.

Suppose that that finitely long path can at most have a time

L as execution time then will be something like MCM + L.

Now let's clean that up, or at least let's clean up the part up here.

And then we get this formula.

So definitions of iota etc., they stay the same.

But we know that the worst-case response time is smaller than the maximum,

and then we can lead back the paths that start from some input.

P input at N- the number of tokens in the path,

+ the number of tokens in the path, x the MCM.

Plus a little bit extra for

the possibility of, well, having a piece of a path that does not cycle.

And this you can add up for all paths in X with still the conditions.

So I didn't write it down but the iota x bigger than N and

smaller than N + I should still be there.

All right, so if you look at this formula in more detail, then you can see that

actually this part of the formula, and that's the important part because that's

the part we are taking the maximum over, does not depend on the path at all.

It only depends on the number of tokens in the paths, right?

So let's call that number of tokens K.

Then we can clean up this formula a lot.

And what we get.

Is this.

We get a formula that does not depend on the path,

it only depends on the worst case arrival basically of

tokens on the input and on the maximum cycle mean.

And we enter it over K smaller than N + I, so it also depends on N and plus I.

[COUGH].

Now from here, the only thing that we still have

to do is show that N ÷ P, N is for limit of course,

for N going to infinity, has the properties that we want.

And well, I would advise that you first check whether you can

follow the derivation of this formula.

And then in the next video we're going to finally finish off this proof.

Explorer notre catalogue

Rejoignez-nous gratuitement et obtenez des recommendations, des mises à jour et des offres personnalisées.

Coursera propose un accès universel à la meilleure formation au monde, en partenariat avec des universités et des organisations du plus haut niveau, pour proposer des cours en ligne.

© 2018 Coursera Inc. Tous droits réservés.

Télécharger dans l'App Store

Disponible sur Google Play