What are the messages supported by these examples ?

Operational tool

Quasar works fine and the set of analyzed concurrency solutions may be used as acceptance trials for the present version and as regression tests for future versions.

Concurrency correctness

Quasar has a prime objective to prove concurrent pattern correction. It allows to thoroughly categorize correctness and to check user specified safety and liveness properties.
A primary analysis of the analyzed patterns will often focus on usual practical considerations such as deadlock and starvation. Once the program has been shown to be prone of these defects, additional correctness may be checked with LTL properties.

Java and POSIX concurrency patterns

Quasar has been tuned to analyze concurrent Ada programs since the Ada concurrency semantics is precisely defined (it is an ISO standard) and since ASIS, available as free software, allows to navigate in the syntactic tree of the program.
However Quasar is presently also useful for analyzing the concurrent features present in Java or POSIX. Hints for concurrency patterns in Java and POSIX can be obtained through the different styles of programming exercised in the Ada examples. For example Ada programs using server tasks for implementing the monitor structuring concept show a concurrency semantics close to the Java "synchronized" methods using "wait" and "notify", and they give insights for concurrency programming in Java. The simulation of semaphores with tasks or with protected objects allows to implement programs with POSIX like semaphores and to analyze patterns using them.
Moreover, one of Quasar' future could be to use tools providing for Java the same functionalities that Gnat and ASIS provide today for Ada.

Concurrency complexity comparison

Given a concurrency paradigm (or design pattern) and several theoretical solutions, several implementations of these solutions may exist according to the concurrency features used and according to the programming style. Quasar allows to remove erroneous implementations and to compare the complexity of the remaining correct implementations.
Thus a practitioner may choose the "simpler" implementation, whatever "simple" means for him (smallest size of the generated Petri net, or of the reachability graph ; implementation where entry queues have at most one waiting task ; a given style of programming).
This has a practical impact since it is usually admitted that simpler solutions are easier to document, less prone to coding errors and easier to maintain.

Sensitiveness of concurrency solutions

Quasar allows to show how a slight modification in a concurrent algorithm may destroy its correctness. This may happen when a more efficient solution is sought after. This is also the case when a deadlock free solution that shows starvation is modified in order to obtain a fair solution. Unfortunately in some cases shown in the examples, this may lead to a solution prone to deadlock solution.

Scalability

Quasar allows to compare the complexity of an implementation versus the number of concurrent tasks. Of course this use is limited by the combinatorial explosion of states. However since Quasar behaves relatively well reducing this explosion, this additional attribute should not be ignored.

last update : 10/02/2004