Case study : Peterson Example

Presentation :

Quasar is now able to check more complex properties than deadlock using the Linear Time Temporal Logic (LTL). As LTL manipulation is error prone, and as referencing the state of a program using the source code is not easy, we add templates to facilitate its use by non LTL experts.

This example is the implementation of the mutual exclusion by the Peterson method. Two tasks are trying to access a critical section, and call a procedure (Peterson.Enter) to ensure that the mutual exclusion is respected. The Peterson.Enter procedure uses Two global variables. A table that contain state of the task (if they are candidate or not to enter in critical section) and a Priority variable defining which task has the priority. Then the Peterson.Enter wait on a condition until the critical section is free.

Our problem is define this condition. We have three idea, but we are not sure that they respect some properties, like any task which is candidate to enter in the critical section will access it, or that there is only one task in critical section at any time, ...

not(Candidate(X) and (Priority = X))
Candidate(Other) and (Priority = Other)
Candidate(Other) or  (Priority = Other)

With Quasar, we are able to prove that the only valid proposition is the second one.

Major Ada language components added :

• Global Variables (only at main level of a package/main procedure)

Downloads :

Source code /

Pictures :

Select the property to check	Statistics of the analysis

last update : 20/10/2005