0:05

Welcome again. In this lecture,

Â I will show how we can formulate the correctness of

Â Peterson's Mutual Exclusion Algorithm using modal formulas,

Â and I will show how we can use the tools to prove these formulas.

Â So, I'll quickly go to Peterson's Mutual Exclusion Algorithm again,

Â but I already presented this in one of the previous lectures.

Â So we have two processes,

Â they both have a critical region and in each critical region,

Â only one process can be at the same time.

Â And by doing an "enter" action,

Â a process enters this critical region.

Â By doing a "leave" action,

Â a process leave this critical region.

Â And we have a "wish" action,

Â and "wish" action is being used to

Â indicate the desire of a process to enter the critical region.

Â And these are the three actions that we will look at.

Â So, if you go to the Wikipedia page,

Â then we see that there are three requirements on Peterson's Mutual Exclusion Algorithm.

Â The first one is mutual exclusion,

Â two processes cannot be in the critical region at the same time.

Â The second one says that if a process wishes to enter the critical region,

Â then a process will actually get into the critical region,

Â not necessarily the process that wishes to enter but there is

Â some form of progress in entering the critical region.

Â And the third property says that when a process wishes to enter the critical region,

Â then it will not be bypassed infinitely often by another process,

Â so it will get â€” gets its turn and in this particular protocol,

Â it will actually have to wait only once.

Â So the question is â€” how can we formulate this as modal formulas?

Â So let's look at the first formula,

Â the first property and what's good strategy is to first formulate a requirement in text,

Â such that humans can understand it;

Â then reformulate it in terms of actions;

Â and only as a third step,

Â formulate this as a modal formula.

Â So first, we formulate it in terms of actions,

Â and what mutual exclusion essentially says is that we cannot have

Â two and consecutive "enters" between - without a "leave" in between.

Â So that's all we have to check.

Â So we already saw this property in one of our earlier lectures, namely,

Â between an A and a B - a C must happen and that's

Â exactly the formulation that we will use.

Â So, what we say in our modal formula is that if two

Â happens - so if an arbitrary number of C actions,

Â then if we do an "enter" followed by a sequence of actions not being a "leave",

Â followed by an "enter",

Â then we can do two "enters" without a leave in between.

Â Then we end up in a state where false must hold or in other words,

Â we end up in a state that cannot â€” that is not reachable.

Â So this says that two "enters" without a "leave" is not possible.

Â So this expresses exactly the mutual exclusion property.

Â Let's go to the second property,

Â so the progress property.

Â So what's the progress property said was that if a process does a "wish" action,

Â then a process can enter the critical region within a finite number of steps,

Â and how do we formulate this as a modal formula?

Â Well, we write this maximum fixed-point operator,

Â with a parameter B,

Â and a parameter B indicates that a process is in the critical region.

Â So initially, no process is in critical region and you set it to false,

Â and whenever a process doesn't enter,

Â we set this boolean B to true.

Â Whenever a process doesn't leave,

Â we set the boolean B to false.

Â And whenever something else then enter and a leave happens,

Â we do not do anything at all,

Â so we do not change the value of this parameter B.

Â And then, see these parts - if we do a "wish" action,

Â then if no process is in the critical region,

Â we want that there will be an "enter" within a finite number of steps.

Â So, this is the typical pattern that we used for that,

Â with its minimal fixed-point Y had this true-true at the end.

Â So let's go to the third property,

Â the property of bounded waiting.

Â So, if a process wishes to enter the critical region,

Â then we will see that it is not too often bypassed.

Â So in terms of actions,

Â if a wish(id) happens then we will only see a limited number of enter(id)

Â prime actions for id-prime being different than id before we see this enter(id ).

Â So, formulated as a modal formula,

Â whenever a wish(id) action happens,

Â what we want is that we want to see only a finite number of enter(id) prime action,

Â so this is indicated with this minimal fixed-point operator X.

Â And this box modality and for all other actions, other than enters,

Â it does not matter how often they happen because that's of no concern currently,

Â and we once that we ultimately end up in a state where we can only do "enter actions".

Â In the particular, where we can only do the enter(id) action,

Â so instead enter(id) will ultimately happen.

Â So what we can do now,

Â is check that these formulas hold by looking at the tools,

Â and then you can see how you can use the tools to check such formulas.

Â So,

Â we've seen that all these formulas hold and I have now a somewhat disconcerting exercise,

Â namely, an exercise putting some doubt on

Â the usefulness of the modal formulas that we had until now.

Â So what we know is that the algorithm of Peterson,

Â as we found it on Wikipedia,

Â has a small flaw in it.

Â And actually, the progress formula that he

Â formulated is not really capturing what we had in mind,

Â and the question is why?

Â And in order to help you,

Â I put the stage page with actions which enter and leave here,

Â reduce small or weak trace equivalents.

Â So, what you've seen is that, actually,

Â this flawed version of Peterson's Mutual Exclusion Protocol requires a "wish" action from

Â the other process in order for the current process to enter its critical region.

Â So what we would like to do is to strengthen our progress formula by saying

Â that we have progress without

Â the other process cooperating and formulas largely the same,

Â so this is completely copied from the progress formula,

Â and here at the end,

Â we say that we want to get into

Â the critical regions by doing actions different from "enter" and different from "wish".

Â And by replacing the true in the diagram's

Â true-true by every action different from "wish",

Â we indicate that we want to do this "enter" action,

Â and you are forced to do the enter(id) action at some point.

Â Okay, now that we see,

Â we showed that we can

Â formulate the requirements of Peterson's Mutual Exclusion Algorithm as modal formulas.

Â I think I implicitly showed that formulating requirements in

Â modal logic is extremely tedious and it

Â requires quite a lot of experience and skill to exactly formulate what you would like to.

Â But fortunately, and I think this is quite important,

Â even if you formulate only partly correct modal formulas,

Â you will find quite some flaws and bugs and problems in the description of particles,

Â and in any case,

Â you will learn a lot by playing with these modal formulas about the systems.

Â In the next lecture,

Â I will use boolean equation systems as a means to

Â actually prove a modal formula on a transition system.

Â