TAPAAL

Can you help me understand the fischer-example?

Asked by Asger Gitz-Johansen

Hi,

I am trying to do some verification engine comparisons by using the fischer mutex protocol as a test set, and I saw that TAPAAL already comes with an example implementation of the protocol. However, the example is a bit difficult to understand with all the arcs going back and forth and the provided queries seem to just check that the critical section is not ever reachable (I might misunderstand this). Can you help me write a reachability/safety query that checks wether or not two processes can be in the critical section at once (shouldn't be reachable), and one to check that any critical section is reachable?

 - I have tried the query "EF Protocol.CS > 1", and that does seem to fail.
 - but the query "EF Protocol.CS = 1" also fails, which seems to indicate that the critical section is not reachable at all.

Also, how would I "scale" the example to have more than the two mutex processes already defined?

Question information

Language:
English Edit question
Status:
Solved
For:
TAPAAL Edit question
Assignee:
No assignee Edit question
Solved by:
Jiri Srba
Solved:
Last query:
Last reply:
Revision history for this message
Jiri Srba (srba) said : 		#1

To check if a process can be in a critical section, make the query:

EF (Protocol.CS = 1 or Protocol.CS_ = 1)

To check the mutual exclusion query is:

AG (Protocol.CS <= 1 and Protocol.CS_ <= 1 and (Protocol.CS <= 0 or Protocol.CS_ <= 0))
if you want to negate it (returns true if mutual exclusion is violated), then ask the query:

EF (Protocol.CS > 1 or Protocol.CS_ > 1 or (Protocol.CS >0 and Protocol.CS_ >0))

The TAPN model of Fisher's protocol that we modelled in TAPAAL is described in this paper:

http://www.it.uu.se/research/docs/fm/apv/tools/tpns/files/bqo.pdf

Finally, the example is scaled by allowing for larger and larger number of extra tokens in the query. The transition GenerateProcesses generates the extra tokens representing processes. You can also remove the GenerateProcesses transition and add the tokens directly to the place A, this will have the same effect.

Revision history for this message
Asger Gitz-Johansen (sillydan) said : 		#2

Thanks!

The way that the problem is modelled is very confusing but from the paper, the sentence: "The places marked with † represent that the value of the shared variable is the index of the process modeled by the token in that place." cleared a lot up for me.

Just to confirm if I understand correctly: Protocol.CS > 0 should never be reachable, because that would mean that some process has reached the critical section with the shared variable v not being assigned to i - which would make the mutex not very mutex-y.

In a similar vein:
 - EF Protocol.B != 0 and Protocol.B_ != 0 shouldn't be reachable, because then the value of v is ambiguous again
 - EF Protocol.A_ != 0 and Protocol.udf != 0 shouldn't be reachable either, because then the value of v is ambiguous (both undefined and i at the same time)

The actual TPN provided in TAPAAL is quite different than the one depicted in the paper. Is there a specific reason for this?

Revision history for this message
Best Jiri Srba (srba) said : 		#3

The two places CS and CS_ both represent the critical section; they are duplicit because they also represent the value of a boolean variable. So in short, the number of processes in the critical sections the sum of the tokens in the places CS and CS_ .

The net is different because it aims to make a single net for a scalable number of processes (but using the additional number of tokens feature in the query dialog). Alternatively, one could make multiple nets for different number of processes.

Revision history for this message
Asger Gitz-Johansen (sillydan) said : 		#4

Thanks Jiri Srba, that solved my question.