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.