What is a correct concurrent program and how can it be validated ?

A correct concurrent program must satisfy two classes of property : safety and liveness.

Safety properties assert that nothing "bad" will ever happen during an execution (that is, the program will never enter a "bad" state). Examples of safety property are the respect of mutual exclusion, the denial of placing a new item in a full buffer, the freedom from deadlock, the insurance that all dynamically allocated resources will return to the resource allocator (i.e., the number of dynamic resources remain constant).

Liveness properties assert that something "good" will eventually happen during the execution (that is, the program will eventually enter a "good" state) Examples of liveness property are the absence of livelock, fairness, absence of indefinite postponement or starvation.

Owing to its advantages (such as design clarity, reactive facilities, distribution ability, scaling capabilities,...), concurrent programming is growing more and more in importance, and appears in a wide range of applications, even for applications needing a high degree of safety. However, the application behavior induced by concurrency is intrinsically difficult to validate.

Traditional methods, using specifications or tests, do not give full satisfaction. Specifications are often situated at a too high level of view and thus far from the final details of the source code and/or of the target platform, which can induce huge behavior modifications. Exhaustively testing is a long, tiresome process and it is often very difficult to reproduce the concurrent execution which leads to the error. Moreover testing gives only probabilistic results that depend of the coverage of the implemented tests. These experienced drawbacks, due to the indeterminism inherent to concurrency, push engineers to limit the use of concurrency, and thus unfortunately to limit also the facilities that concurrency provides.

Another approach consists in using the source code as the source formalism and to elaborate from it a model on which properties can be validated. Alike a compiler that builds a syntactic tree which allows to verify the program syntax before generating the code, this method builds a model which allows to verify the semantic of concurrency of the program before running it.

This approach bears also additional advantages. There is not necessary to transcribe the application in a different language for specification, validation or testing purposes, and this avoids transcription errors or semantic loss. The approach is also usable for analyzing the full and final application program after linking all its imported components. This is very important when the checked properties, like absence of deadlock, are global properties which are not decomposable and which cannot be proven by parts.

last update : 20/10/2005