0.1 Concurrent processes: basic issues  (Page 3/3)

Race Condition

A race condition is when some possible interleaving of threads results in an undesired computation result.

Typically, a race condition is an oversight by the programmer who did not realize the interleaving was possible.Race conditions are notoriously hard to debug and test for because they can well occur in highly unlikely situations.

More generally, these and other issues are categorized as being either safety or liveness issues.

• Safety properties are those that say ``bad things never happen''.Examples are the lack of deadlock, the lack of livelock, and the lack of race conditions.For a particular program, a safety property might be that inventory levels never become negative, or that customers can'tcut ahead in line.
• Liveness properties are those that say ``good things eventually happen''.An example is fairness. For a particular program, a liveness property might be thateach customer is served, or that after each program error, an error message is printed.Typically, liveness issues can't be detected by looking at a program at a particular moment, but instead requireconsidering an entire (infinite) trace.

In this module, we will concentrate on the four issues of deadlock, livelock, race conditions, and fairness.We will see how to write and automatedly detect these problems in some concurrent programs, using the tools Promela and SPIN . We will also learn how to formally specify more intricate propertiesusing temporal logic .

Avoiding and detecting problems with concurrency

There are known programming techniques to avoid certain problems such as deadlock and some kinds of race conditions.Some of these techniquesnotably locks and semaphoresare so common that they are often embedded into programming languages.While the details of such techniques are outside the scope of this module,it is important to recognize that although they greatly help writing concurrent problems, they don't mean that concurrency problemscan't arise.

Given concurrent code, how can we determine if it behaves as expected? Certainly we can test it on various inputs, but we can never tryevery possible input. Neither can we test every possible interleaving on every possible input. As always, testing can reveal errors, but itcan't demonstrate the lack of errors.

Since concurrency problems can lead to programs that don't terminate, it's clear that detecting concurrency problems can't be any easierthan the Halting Problem , which is itself unsolvable. So we can't write a checker which takes a concurrent program asinput and always determines whether it's free of (say) deadlock.

But just as we can study individual programs and conclude whether or not they will halt,for many real-world concurrent programs, we can determine whether or not they are susceptible to deadlock. For example, communications protocolsgenerally have a finite number of options and are amenable to automated checking.Thus automated tools (such as SPIN) are valuable aid in catching and eliminating real-world bugs.