Parameterized Verification through View Abstraction | Experiments

Parameterized Verification through View Abstraction

Experiments

Burns' mutual exclusion

Burns' code Burns' diagram

Burns' algorithm implements a mutual exclusion protocol and can be modeled as a parameterized system where the processes are arranged in a linear topology. Each process can communicate with and distinguish its neighbors on its right or its left.

The local state of a process ranges over state {1, ..., 6} where 6 represents the critical section. Transitions are guarded with conditions on the states of the neighbors, on the right, the left or both and is enabled if the guard is not violated.

Initially, all processes are in state 1. A bad configuration is detected if 2 processes or more are in the critical section, ie if the array contains at least 2 processes in state 6.

The transitions are depicted in the following state diagram. i is the the current process, j is another process and j its state.

Dijsktra's mutual exclusion

Dijkstra's code

Dijsktra's algorithm implements a mutual exclusion protocol and can be modeled as a parameterized system where the processes are arranged in a linear topology. Each process can communicate with its neighbors and check their status.

The algorithm is described in code listing on the right. It makes use of a pointer, i.e. a variable ranging over process indices. We model this pointer by a local boolean variable p for each process state. p is true iff the pointer points to this current process. When the pointer changes, this information must be passed onto all other processes, which we model as a broadcast transition. Concretely, upon pointer assignment, the current process sets its local variable p to true and simultaneously sets p to false in all other processes.

We denote the state of process as St (resp. Sf) when the process is in state S and the pointer p is true (resp. false). The state S of a process ranges over {1, ..., 6} where 6 represents the critical section. Initially, one process is in state 1t and all other processes are in state 1f. A bad configuration is detected when 2 or more processes are in the critical section, ie when their state is either 6t or 6f.

Dijkstra's diagram

Szymanski's mutual exclusion

Szymanski's algorithm implements a mutual exclusion protocol and can be modeled as a parameterized system where the processes are arranged in a linear topology. Each process can communicate with and distinguish its neighbors on its right and its left.

Szymanski's code

A state process can be modeled as ranging over {0, ..., 11} where the critical section is 9 and 10. Initially, all processes are in state 0. The transitions are depicted in the following state diagram.

Szymanski's diagram

Gribomont-Zenner's mutual exclusion

This algorithm could be seen as a version of Szymanski's algorithm, with transitions that are finer grained in the sense that tests and assignments are split over different atomic transitions. In this model, the local state of a process ranges over state [1-13] where 1 is the initial state and 12 represents the critical section. Configurations not satisfying mutual exclusion are those where at least two processes are at state12.

Gribomont-Zenner's diagram

Bakery mutual exclusion

Bakery's diagram

This case study describes a simplified version of the original Bakery algorithm. In this version, processes have states that range over [1-3], where 1 is the initial state. A process gets a ticket with a value strictly higher than the ticket value of any process in the queue (transition 12). A process accesses the critical section if it has a ticket with the lowest value among the existing tickets (transition 23). Finally, a process leaves the critical section, freeing its ticket (transition 31). Mutual exclusion violation corresponds to configurations where more than one process is in state3.

Parosh's mutual exclusion

This protocol ensures mutual exclusion between processes. Each process has five local states 0, 1, 2, 3, 4 and is initially in state 0. A process in the critical section is at state 4. The set of bad configurations contains exactly configurations with at least two occurrences of state 4.

Almost downward-closed example

Processes move from state 0 to 1, and then 2. Once the first process is in state 2, it closes the door on the processes which are still in 0. They can no longer leave state 0 until the door is opened again (when no process is in state 2 or 3). Moreover, a process is allowed to cross from state 3 to 4 only if there is at least one process still in state 2 (i.e., the door is still closed on the processes in state 0). This prevents a process to first reach state 4 along with a process to its left starting to move from 0 all the way to state 4 (thus violating mutual exclusion). From the set of processes which have left state 0 (and which are now in state 1 or 2), the leftmost process has the highest priority and it is encoded in the global condition: a process may move from 2 to 3 only if all processes on its left are in state 0.

Critical section guarded by a lock

We can model the critical section problem by read and write access to a resource shared by multiple processes. There is no particular topology so we will model it as an instance of a parametrized system with multisets. More precisely, as a Petri Net. As the petri net of a concurrent program, described at that level of granularity, can quickly grow in size, we choose a short example: The processes repeatedly grab the lock, increment a counter and release the lock. A bad configuration is detected when 2 or more processes are having access to the shared variable simultaneously while one is writing.

The shared variable counter is associated with two places, Readcounter and Writecounter. The tokens of a place in the petri net represent the count of process in a given state, or the available resources. A process places a token in Readcounter (resp. Writecounter) if it is currently accessing the variable counter for reading (resp. writing). We model read and write accesses to shared variables with two transitions, denoted by the dotted rectangle in the following figure. There is a place L associated with a lock. Intuitively, if L contains a token, the lock is free, otherwise it is busy. This ensures that only one process can hold the lock at a time. Note that L is a global variable and that we omit the input places used to balance out the number of tokens in the net.

Initially, the lock is free and the processes are in the initial state init. The petri contains then one token in L and the others in init. A bad situation is detected when the petri net contains 2 or more tokens in Writecounter or when there is one (or more) token in Readcounter and one (or more) token in Writecounter.

Critical Section

Agreement protocol on a Ring

Agreement Ring

Interacting peers are organized in a circular pipeline and are given a number. The protocol in place is to ensure that every participant in the ring knows which number in the maximum among the values of the ring members. We model this protocol as an instance of the framework on rings. Each participant in the ring can communicate with its adjacent neighbors. We assume the ring oriented and a member can send messages to its (immediate) successor and receive messages from its predecessor. The reception is usually blocking while the sending is not. However, we will model this communication as a rendez-vous.

Initially, all process are in a dormant state. One of the process will wake up first. This is the one which initializes the protocol (denoted in the pseudocode as P0). Every process sends the max between its own value and the value its received from its predecessor (the biggest value it has seen so far). Note that the protocol doesn't not terminate when P0 receives the biggest value in the ring. It must indeed communicate this value to the others. Each will receive it from its predecessor and only pass it along to its successor (after recording it). The protocol terminates when the predecessor of P0 receives the biggest value and avoids the re-sending. A bad configuration is detected if one of the participant is in its final state (6 or 17) but has not seen the biggest value go by. We depict the protocol using the following pseudocode. The channel between Pi-1 and Pi is called values[n]. A message in the channel will contain the number the sender sent.

Agreement Ring

Light Control

This algorithm implements a simple solution to the light system of an office room. An arbitrary number of people may get in or out of the room. Initially, the light is off and everyone is outside the room. The first person to enter the room turns the light on and the last person to exit the room turns it off. A bad configuration is detected when the light is on, but there is noone in the room, or when the light is off while there are still people in the room.

We model this algorithm with a Petri Net with Inhibitor arcs. There are 2 places associated with the on and off status of the light. And there are 2 places associated with the fact that a person is inside or outside the room. An extra place exiting is used to check the person who wishes to exit is the last one in the room. Initially, there is a token in the off place, and all the other tokens in the outside place. For readibility, we represent the transitions piecewise as follows.

Light Control

Priority Allocator

A ferry transports one car at a time from one side of the river to the other side. At the departure, there are 2 queues of cars: One with high priority, one without priority. If there are cars in the high priority lane, the ferry must load them first. If not, it can load a car from the lane with no priority, not even with a first-come-first-served basis.

Initially, the cars must choose their respective lane, but are not allowed to board the ferry, which is not loaded. A bad configuration is detected when the ferry has loaded a car from the no-priority lane while there are still cars in the high-priority lane.

We model this situation with a Petri Net with Inhibitor arcs. There are 2 places associated with the high and low priority lanes. And there are 2 places associated with the fact that a car has been granted access on the ferry. There is an initialization phase that models how the car get attributed a priority.

Priority Allocator

Simple Barrier and Barrier with Counters

Simple Barrier

A barrier is a tool to ensure synchronization between threads and allows a programmer to impose restriction for an asynchronous multi-threaded program. A process arriving at the barrier must stop at this point and cannot proceed until all other processes reach this barrier.

The following model represents a barrier with a pivot. The first thread at the barrier will take the role of a pivot and all other processes wait as long as there is a pivot. When all processes have arrived at the barrier, the pivot can then proceed, which in turn releases all the waiting processes.

A process can be in state before B, wait W, pivot P or after A. Initially, all processes are in state B and a bad configuration is detected when there is a process in state A, while there is still a process in state B.

The following invariant can be derived:

  1. a pivot P can coexist with a process in state B and/or W, or is alone, i.e. the set of configurations {PB*W*},
  2. a process after the barrier can only coexist with other process after the barrier or still waiting, i.e. the set of configurations {W*A+}, and
  3. initially, all processes were before the barrier, i.e. B*.
Simple Barrier diagram

It is also possible to model it with a linear topology (see paper ...). In that case, we can consider a non-atomic version, which would not check the state of the other processes all at once. A typically implementation uses an atomic counter as follows.

Barrier with Counters - code

List with Counter Automata

List with Counter Automata

Consider the following single-threaded program. It scans a list starting from the pointer L and must end when it finds a marker P, placed prior to the start of the program. In this case, the parameter for this parametrized system if the length of the list. The program risks a segmentation fault is the marker P is not found. Our analysis retain the presence of the marker information in a context (and would forget it without context).