[MUSIC] In this lecture we will model Peterson's mutual exclusion algorithms as an example of the application of what we have seen until now. Peterson's mutual exclusion algorithm is used when you have more processes running on all the same computer. So, here there's one process, process zero. Here is another process, and it can be that these process have spacial areas, where only one process can be at the same time. So, in this red area it could be that one process is accessing a printer and here this [INAUDIBLE] area, where other process is could access the printer, and what you do not want to have is that both processes access the printer at exactly the same time. So, this is what's called a critical region, and that is an area where only one process can be at the same time. And now the question is, how can we guarantee that each process can only be there on its own without the other process being there? And that is the purpose of Peterson's mutual exclusion algorithm. So, what we have is an enter action, and this enter action indicates that a process enters the critical region. And we have a leave action, and that also indicates that a process leaves the critical region. And in this way we can see how many processes are in the critical region. If you look at Wikipedia and this is the page from May 17 in 2015, we find this description of Peterson's mutual exclusion algorithm. So, in the beginning, we see a block of its three variables, flag 0, flag 1. And turn, flag 0 and flag 1 contain Booleans, and they are accessible by both processes. And turn contains an integer also accessible by both processes. And we see the two other blocks, which are quite similar, and that are the behaviors of the two processes to enter these critical sections. How can we model this? Well, we can do this as follows. Here we have the two processes, and we have these three variables, and these three variables can be accessed by both processes. So, we model them also as separate processes. So, actually, we model five separate parallel processes. So, if we take the variable term, we model this as the following process. It just to process turn with as local variable, a natural number n. You can set this variable using the set turn action to any value, so you choose an n prime from the natural numbers. You do the set_turn in that n prime, and then replace the n by the n prime. And you can reach the current value of the variable by doing a get_turn action. And in the same way, we model the flags, these are two processes, flag 0 and flag 1. So, we model them with the process flag with as first variable in identifier, indicating which process, it is indicating so either 0 or 1. And the Boolean, which is the Boolean which is contained in this flag variable. And completely similarly to turn, we can set the Boolean by a set flag and then we set it to the Boolean b prime, and we can read the Boolean by the action get_flag. Then we can look at the behavior of the full process, so this is the full process taken from this Wikipedia page, and this is the model as we will use it. So, what we wrote down is a process with an identifier, so this is both the process of this model process 0 and process 1 depending on the value of id. [COUGH] We have this set_flag action and there set the flag indicated to the id, so assume that id is 0 to true. We set the turn to the other id, so if id is zero we set the turn to 1 so that is the second action here. Then we have here appear at the left a busy way loop which says we weight until flag 1 is false or true is 0, and we can mold it with two actions with choice in between. So, we do a get_flag of the other id, and check where it falls or we do a get_turn and check route equal to id, and if that is the case, we can enter the critical region. So, entering the critical region is done here with the enter action. Then you leave the critical region, and at the end, you set the flag of the current process again to false. And just to figure out what will happen when you try to enter and leave the critical section again, the process is recursive so at the end we call process id again just to let the process repeat. So, now we have a description of all five components and we can describe the whole system by just putting them in parallel like this, and here you see the five parallel components. And if you compare that to the original description then you can see this process for turn with the parameter 0, and for this purpose more importantly, we have the flag 0 which is initialized to false. And we have a flag 1 which is initialized to true, so if we have processes in parallel we want to let them communicate. So, we put the communication operator in front of it, and take care that the correct actions communicate to that communication actions. We allow all the actions that we want to see, so the enters, and the leaves, and the results of the communications, and the height of the results of the communications, and we only leave enter and leave visible because that are the only actions we are really interested in. The rest is into an old part of the internal workings of the protocol. And then we generate a state space, and this is what we get, mode low branching bisimulation. So, we generate full state space produces mode low branching bisimulation, and well, you may still be somewhat disappointed by the fact that the behavior is not as straightforward as you might expect. But if we start to inspect this behavior, then we can see that mutual exclusion is actually guaranteed. Namely, here we see a state where a process of 1 is in a critical region. Here we a state where process 1 is in the critical region between an enter and a leave. And this is a third state, process 1 is in critical region. And if we do the same for process 0, we see here the case of process 0 is in the critical region. Here, another state and there's even a third state, and that's due to the symmetry in the whole thing. And that's here where also process 0 is in a critical region. And very importantly, we see that there is no state where both process 1 and process 0 are in the critical region, and this is the primary goal of Peterson's mutual exclusion algorithm. So, we see it works correctly, but what we can do is that we reduce this behavior a little bit more because this is still complex, and we might get more insight if he also reduces further using weak trace equivalents. And then we get this picture and I must admit that I was a little surprised when I saw this. And I do not know whether you share my surprise, but if you look at behavior at initial state that is the green state then what we see is that we can do an enter 0 followed by a leave for 0, and that's nice so we process 0 enter the critical region. And then it leaves the critical region again and after that it cannot enter the critical region for a second time and this is what we expect that processes can enter and will if the other process does not have a desire to enter the critical region. Here it must be the case that after process 0 enters the critical region process 1 must enter the critical region. And the question is what's actually going on here? So, this is the crucial place, and what we see is that initialization of Peterson's mutual exclusion algorithm is actually wrong. And it's only due to this picture that I started to realize that the true here, should be false. And if we generate the transition system after we replace the true by false, so in the initial, in a parallel composition of the process we've replaced true of process 1 by false as indicated here. We can get this. Transition system mode low weak trace equivalents, and what you can see here in initial state is that process 0 can enter the critical region or process 1 can enter the critical region. And then if process 0 has entered the critical region it must leave it before either 0 or 1 can enter it again. And I think that you agree with me that this is actually the desired behavior of a mutual exclusion protocol. There are more correctness criteria for Peterson's mutual exclusion algorithm and one is the questions of bounded waiting, and that means the following. Namely, if a process indicates that it would like to enter the critical region then it can only be over hold by the other process a limited number of times, so it is guaranteed that it will access the critical region within a finite number of steps, and that is what this text says. So, what do we do? We take the process, we add a new action which to indicate the wish to enter the critical region. And you do this in a multi-action, so whenever the process sets the flag id to true, it also performs the wish action indicating that it wishes to enter the critical region. And what happens if we generated a whole states base, and we reuse it mode low weak trace reduction, then we see that the total behavior of the system is this. And if we take the initial state and that's, this is the initial state, we see that there is a desire if we go to this state, to enter from process 0 to enter the behavior. So, we have process 0 that wishes to entertain the correct region. We see that process 0 enters the critical region, and then if you go back to the initial state leaves the critical region and this is a typical sequence of actions namely of this enter and leave sequence. If you go to the upper state again, then it's also possible that process 1 in parallel indicates that it also would like to enter the critical region. And then, we go to this state. And our two possibilities here, either that process 0 enters the critical region like this, or process 1 enters the critical region. But if process 1 enters the critical region and it has left critical region, you see that after that process 0 must enter the critical region. And if process 1 in any case again that it wishes to enter the critical region then we see here that process 0 has now priority, and will first enter it. So, what we see is that process 0 is only overtaken once, but not more than once and that means that the property of bounded waiting is indeed guaranteed by this protocol. And one of the experiments that we can do is that we take the first actions, namely, the first set turn and the first set flag. And we can ask ourselves, is it really necessary that they happen in that sequence, or can we reverse that sequence? So, here we have the process. You see here set_flag and set_turn, and if we now change their position, we get a new process. We can generate the states base, this is the states base. The question is, is it safe to exchange these two? Let's go to a second exercise, if the protocol introduced the true variable to guarantee bounded waiting. What you can do is remove this term variable from the protocol and then generate the state's base. And this is the states base that we get, mode low weak trace reduction. And the question is, is it this case that the turn variable is needed? So, what did we do? We took Peterson's mutual exclusion algorithm just as an example, and we took the description on the Wikipedia page, and we modelled it and we analyzed it. We came to the conclusion that it was wrong, and on the one hand I was surprised. I didn't didn't expect this standard protocol to be incorrect, but it's completely in line with my own experience whenever I start modeling protocols, I will find mistakes in them. We also looked at the property of bounded waiting, and we showed that that property was guaranteed in this protocol. So, this brings us to the end of the second MOOC namely, how we can model process behavior. I think you saw that the, this is quite an effective tool which you probably also show that the transition systems that we generated could become very complex indeed. So, if they become more complex we need other tools namely, model logics to investigate these transition systems. And this will be the topic of the next MOOC namely, how can we formulate requirements by model formulas, how can we check them? Thank you for watching, hope to see you again in the next MOOC. [MUSIC]