Okay, then let's begin.

Welcome to the second edition of formal methods and software engineering.

Today we will first return to our mutex semaphore example for a bit.

Last time we already established a few properties that such a semaphore implementation is supposed

to satisfy, that we want to hold in a model of semaphore implementation.

One that we, I think, mentioned but didn't talk too much about was that there might be

some crude protocol implemented that just gives out the token, the semaphore, to each

process in a certain order.

It's not possible for some processes to take the token twice and do something in the critical

section more than once before some other process has taken the token.

This property is called no-strict sequencing, so our mutex shouldn't enforce that the processes

gain access in a specific order.

Now we can think about how we could model this statement in natural language and then

how to translate it into a logical formula.

How would you model this?

What would be a natural language expression that captures this property in a more formal

way than it's written here?

Probably with respect to models and transition systems.

How could we quantify over paths, describe a path that, or describe all the paths that

are satisfying this property?

I think I have an example of an allowed path here.

This might help, actually.

This is exactly the situation that we want to have and we don't want to disallow.

First of all, what kind of quantification of a path should we employ?

Do we demand something of every path or do we demand something of just some path?

No idea?

Is it clear what the idea behind this is?

Not clear?

So let's say we have a system that has a semaphore and we only have two processes.

So either the semaphore is zero, it's one, or it's two.

Depending on whether it's one or two, the process one or process two can enter the critical

section.

Now, it's always the case that the next value of the semaphore is semaphore plus one.

This is just, well, modulo, no syntactic modulo, but just hand-waving modulo usage of critical

section.

So this protocol would just enforce that after the first process has entered the critical

section, the second needs to enter the critical section before process one may enter it again.

So this is a very stupid protocol, but we want to make sure that we don't have formalized

our system in such a way that things like this might happen.

So it might be a bigger system and we want to just ensure that we didn't make a mistake

like this.

So the answer is more or less already on the board, right?

So I have an allowed path, so there must be a path that somehow fits in this scheme.

So it's an existential quantification of a path.

So I need to ensure that among all the paths that I have, there is at least one that this

proves that this is enforced, so that has process one in the critical section, leaving

it again and entering it again before process two has entered it.

So in natural language, it would be like there exists a path

such that what?

Think about how to continue this sentence.