Presentation Script

Parameterized Verification of Systems with Precise (0,1)-Counter

A control flow automaton, or as an abbreviation a cfa, is just an automaton that describes

We have a program that initialize x with 0 at the label start, then goes to the label loop
where it increments x until it reaches 3 then goes out from the loop to the exit label. The
corresponding cfa is this, we begin the program in the start node, we go from the start
node to the loop node by assigning x to 0 and while x is less than 3 we increment x and
when x is equal to 3 we go to exit node. I’m going to show you now the execution of this
program to demonstrate how the cfa works and I will keep track of the value of x in what
we call the controller.

Before entering the label start in the program, the value of x is still undefined. When we
enter the start label now the value of x is 0, in the cfa this translates to being currently
in the state start and taking the edge x assigned to 0.

And thus we go from the label start to the label loop in the program and same thing in
the cfa we go from label start to the label loop, and since x is now less than 3 we will
execute this edge right here and we will increment x once so now x equals to one and
we return to the loop node in the cfa. We increment again and we get x equals 2, and
increment one final time and we get x equals 3 at the moment. Now in the program since
x is equal to 3 we go from label loop to label exit and the same in the cfa we cannot take
this edge because x is not less than 3 anymore and we take this label because x equals 3,
and we go to the exit node.

The problem now is that this code could be executed in parallel with many processes not
just one, and for example we can have a process that is executing at the moment the

1
start instruction and another process has already finished and went to the exit label. To
solve this problem we will not use just one CFA but we will use a CFA for each process
that execute this program. Also since the controller represents the changes made to the
value x, it defines also a program that we can represent with a CFA that represents how
x changes.

For instance take the same program as before but now executed with two processes instead
of one. We have a cfa of the controller that represents the changes of x, we have one cfa
that describes the flow of the process 1, and we have an identical cfa that describes the
flow of the process 2. At the beginning x is still undefined and we haven’t started the
program yet. P1 now executes the start label and now x = 0 and goes to the loop node.
Now process P2 also executes the start label and x still equals to 0 and goes to the loop
node. P1 now takes this transition and increments x by 1 so x is now equal to 1. P1 does
this again and x is now equals to 2. And now P2 is the one that increments and goes to
exit, and after that P1 goes also to exit.

As just a quick observation, of course it is very not effective to draw a cfa for each process
in terms of space, large distributed systems constitute of millions and even billions of
processes. So we lighten the notation a bit and since all the cfas are the same we can just
draw a single cfa and just say that there is for instance in this example two processes in
the state start, we represent that by 2 tokens in the start node. When P1 goes to loop
we now have 1 process in start state and 1 process in loop state, when P2 goes to loop
we have 2 tokens in the loop state meaning there are two processes in state loop.

The only loss of precision in this presentation is that for example when P1 goes to the
exit in this example, in this representation you will only know that there is a process in
the loop state and a process in the exit state and you will not know which one of which
is in each state. In this case we have anonymized processes and we care only about the
number of processes in some state and not which process is in this state. These types of
systems are called parametrized systems.

A configuration is written as a pair (c, v) where c is the current location of the controller
and v is a vector of states of the cfa such that v(q) is the number of processes in state q.
For instance in this example the controller is in state c0 and we have 0 processes in state
start and state exit, 2 processes in state loop. If 1 process goes from loop to exit we have
now the controller goes to state c1 , and we have no process in state start, 1 in state loop
and one in state exit. And now P2 goes to exit and now we have the controller stays in
the same state c1 , zero processes in states start and loop and state exit has two processes.
We model the changes of configurations with this arrow right here.

And now we formally define what a counter system, or as an abbreviation we say CS,
is. Just a cfa for the controller, we add it to track the modifications of some shared

2
variable or to model a pipeline of communication or anything else. The idea is that the
processes execute the same program and there are some other external things that change
accordingly that we model with one CFA that we call the controller CFA, one cfa of the
processes that hold some tokens, the tokens in some state of the cfa represent the number
of processes currently in this state. Also the total number of processes stays constant,
meaning that if your algorithm adds processes using for example fork or something or
kills processes and you want to verify some properties then this paper is not for you.

Now when you’re writing programs, and in particular parallel or distributed ones, there are
so many things that you could do. For example you can write a program where processes
communicate with each other, you can write a program that writes and reads a shared
variable, you can write a program where all the processes are completely independent.
There are many types of programs. We take an example of lossy broadcast programs.
A lossy broadcast is a program where one process can broadcast a message a, meaning
it sends a message a to all the other processes including itself and the controller, and
also processes can receive messages that have been sent. When we write an exclamation
mark some letter a we mean that the message a has been broadcasted, and we write the
interrogation mark a we mean that a process heard the message a. The term lossy comes
from the fact that we are working with distributed systems and it is possible to not receive
a message even if it was sent to you, this is a common problem in distributed systems.

So for instance there is a cfa for the controller, and a cfa for the processes. The controller
is currently in state c1 , and there are initially two processes in state q1 and one process
in state q2 . The entering edges here in state q1 and q2 means that those are the states
processes can be initially, for example in the initial configuration you cannot have a process
in state q3 .

At the beginning one process in state q1 will broadcast the message a. After that processes
in state q1 and the controller in state c1 may or may not receive the message a. Suppose
for instance that the controller receives the message a, and only one of the two processes
receives the message a, so the controller goes to state c2 and one process in q1 goes to q2
because they have received the message a, and one process in state q1 will not move to
state q2 because it didn’t receive the message as it was lost. Now the controller in state c2
will broadcast the message c and we suppose that the two processes in state q2 will both
receive the message c without loss and one of them will go to the state q1 and the other
to the state q3 . And finally the controller in state c2 will broadcast b and we suppose that
one of the two processes in q1 will receive the message and the other will lose it and the
process in q3 will also not receive the message, so at the end we get this configuration.

The paper deals also with many other types of programs but I will not be able to talk
about them deeply like I did with the lossy broadcast but I’m going to give the general

3
idea of these programs. First, programs with internal transitions: these programs are
just like the example I’ve given you in the beginning of the presentation where transitions
are just assignments or comparisons. The lossy broadcast programs are what I’ve defined
in the last slides where we broadcast and receive messages. Synchronization programs
are programs such that if two processes are in the same state and one of them executes
an instruction then the other process will also execute this instruction. We have also
ASM, asynchronous memory, which is you have a shared variable and instructions you
can do are either read this shared variable or write on this shared variable. Disjunctive
guards programs are programs where you have instructions like if there exists a process in
this state q then the process in state p executes this transition. Until now in my studies
these types of programs cover most of things I’ve done during my studies when working
in parallel and distributed systems except from the programs where you need to create
and kill some processes, so I think that getting results of decidability of these types of
programs is very interesting.

And now after all this talking I’m finally able to define to you the Cardinality Reachability
Problem. I’ve defined to you before the PMCP problem and told you that we want to see
if a program verifies a property for any number of processes, and I told you that we will
deal with just some properties and not all of them. And now the Cardinality Reachability
Problem, as an abbreviation CRP, is a subproblem of the PMCP problem where we check
these properties. First property is this: for all the possible initial configurations, meaning
that we don’t deal with just a fixed number of processes but we want this to be true for
all the number of processes we start with, can the controller CFA reach some state c. We
want to check if there is an execution that ends with the controller being in state c. We
want also to check if a state c of the controller is unreachable, meaning in all possible
executions in all possible scenarios the controller is never in state c. We want also to
check some properties about the number of processes in some state: we want to check if
from any initial configuration there is always a reachable configuration in some execution
from the initial configuration where the state q has more than a processes currently. We
want also to check conversely if there is always a configuration where the state q has
no processes at some point. Finally we can do a finite conjunction or disjunction of the
above properties. For example we can say something like: can we always, regardless of
the initial configuration, reach a configuration where state p has 0 processes and state q
has more than two processes?

Examples of that: for instance the mutual exclusion problem that I’ve spoken about in
the first slide. You have a critical section that you will represent with a node in the cfa.
You will always, regardless of the initial configuration, want to not reach a configuration
where there are more than two processes in this state, you want these configurations to
be unreachable. Also for the safety properties, meaning that nothing bad happens, can

4
be modeled as the bad node should always in all possible scenarios be empty.

Now I’m going to speak about the paper’s main contributions. Before the paper, the
types of programs I’ve spoken about were already dealt with in prior years. CRP is not
something new, it was studied for decades now and many decidability results have been
established. But until this paper, the verification results of CRP were dependent on the
type of program: we already know that the CRP is decidable for lossy broadcast, we
already know that the CRP is decidable for asynchronous memory systems and so on.
But a person in general when writing a program wants for example in one instruction to
send a message to the others, in the next instruction of the same program to read or write
a shared variable, in the next instruction to wait until some other process goes to some
state and so on. We didn’t have decidability results for these programs that combine all
these primitives, we had only decidability results for programs that use for instance only
lossy broadcast primitives, or completely only read or write on a shared variable and so
on. So the paper’s main goal is to unify the verification of these protocols. Also the
problem we had before is that techniques for decidability results of these programs were
different and there was no common technique. So the goal of the paper was to unify all
these programs, all these protocols and find one technique for all of them. To do so the
paper proves that all these programs verify a property that we will call full compatibility,
and instead of working with every type alone we will find decidability results for fully
compatible systems in general, using what we will call (0, 1) abstraction. So I still need
to define to you what a (0, 1) abstraction means and also what full compatibility means.

First, before defining these two terms, I’m going to give the intuition, that is not at
all hard to grasp, that led us to introduce them, and this is the key observation why
the theorems of the paper work. And since the only non trivial type of program I have
explained deeply in this presentation is the lossy broadcast one, my example will be on
lossy broadcast programs. Suppose we have this property that we want to check: a
configuration where states q and r have each more than one process and state p is empty.
This is our bad configuration, and we want for every initial configuration a configuration
where this property is always false, so if there is an initial configuration that leads to
a configuration where this is true then this configuration is bad. Suppose this scenario:
we start with one process in the initial state p, p broadcasts a message a and receives
it and goes to state q. Suppose another scenario: again we start with one process in
state p, and now we broadcast the message b, p receives b and goes to state r. Suppose
another example: we start now with three processes in state p. We know that an initial
configuration with only one token led us to one process to exist in state q, we choose one
process to mimic this execution in the smaller system. This process broadcasts a message
a and receives it and goes to q, in this scenario we suppose that the two other processes
did not receive the message and stayed at the same state p.