A forum for Spin users
You are not logged in.
Pages: 1
Yes, as spinroot already indicated, it is possible to store these changes in a hidden array using embedded C code.
But I do not yet understand what you want to do with these values "at the end of the execution".
If you only need a trace of the changed values, it is easier to filter the output of SPIN, e.g., using a tool like grep, awk, etc.
What are you doing is OK.
Due to the rather large state vector of the model (5916 bytes), VECTORSZ should be set to a value higher than 5916.
SPIN reports what is happening: the pan verifier is running "out of memory".
Given the large state vector (5916 bytes) and the number of states stored (359829) this is not surprising.
Without any compression, SPIN would have needed more than 2GB (i.e., 359829 * 5916 bytes) to store these states.
SPIN also proposes some fixes to tackle the verification more effictively.
You could first try the -DCOLLAPSE option which offers good compression with a bearable verification time penalty.
Additionally you could reserve more memory for SPIN (e.g., -DMEMLIM=4096 to give SPIN 4GB of memory).
Personally, I would first try some bitstate runs with -DBITSTATE.
Although this verification mode may not be exhaustive, it is very fast and has a more than reasonable coverage.
What version of SPIN are you using?
(use "spin -v" to find out the version of SPIN)
At my side, SPIN 6.1.0 parses the above model without any problems.
I used the following (standard) commands to verify the example:
spin -a dekker.prom
gcc -o pan pan.c
./pan -a
And pan reports that the LTL property is not valid.
The atomic construct can be used to make SPIN treat a sequence of statements as a single atomic instruction. The sequence of statements will execute as one indivisible unit, non-interleaved with any other process.
Suppose e1 is an boolean expression and s2 and s3 are Promela statements that are always executable (e.g., assignments, as in your example). Now consider
atomic { e1; s2; s3; }
If e1 is executable (i.e., the expression evaluates to non-zero), SPIN will execute the sequence e1; s2; s3; as a single transition. On the other hand,
e1; atomic { s2; s3; }
will be different. After the expression e1 has been taken, any other process can continue. When this process is scheduled
again, the atomic clause will be executed. However, due to the execution of the other process(es), e1 might not longer be true. The original atomic sequence has thus been splitted into two atomic sequences: e1, and atomic {s2; s3}.
You first have to install Apple's Xcode (Tools). As part of this installation, several command line utilities (e.g., gcc, make, yacc, lex) will get installed.
The latest version of Xcode can be downloaded from [url]http://developer.apple.com[/url]/ (you might need to register first). Your Mac OS X Install DVD also contains a version of Xcode (although it doesn't get installed by default).
When the following ltl clause is added to a Promela model:
ltl { <>[] (_nr_pr == 1) }SPIN 6.0.1 (i.e., spin -a) issues the following error message:
ltl ltl_0: <> ([] ((nr_pr==1)))
spin: _spin_nvr.tmp:3, Error: undeclared variable: nr_pr saw 'operator: =='The leading _ of _nr_pr seems to be lost.
When the parentheses around _nr_pr == 1 are removed, SPIN gets even more confused and regards _nr_pr as a constant. The following never claim is then generated:
$ cat _spin_nvr.tmp
never ltl_0 { /* !((328==1)) */
accept_init:
T0_init:
if
:: (! (((328==1)))) -> goto accept_all
fi;
accept_all:
skip
}jiong, I guess it might work in that way.
But it is not very elegant and straightforward, IMO.
A solution with "user processes with provided clauses" has some disadvantages:
* You need a scheduler process which sets the pending[] elements and which makes sure that the handler process with the highest priority get scheduled first. In case a lower priority interrupt process gets interrupted, the scheduler process should also make sure that this lower priority interrupt process will finish, before the user process can continue. This scheduler process might be a complex thing, and IMO, SPIN should take care of this scheduling;
* All local variables that may trigger an interrupt procedure have to be made global as the scheduler process has to see them;
* The provided clause prevents SPIN partial order reduction algorithm. This might be expensive in terms of the number of states;
* (minor) Each handler will gets its own process. This might not increase the number of states, but it will increase the size of the state vector.
A (simple?) extension to the Promela language (i.e., a resume/return statement) would make modelling interrupts so much easier...
Hi spinroot,
Your solution with the provided-clause surely works.
And for a single user process it is quite elegant.
But what if there are more user processes running?
And how to deal with a priority-based interrupt mechanism?
In a recent project, I had to model two concurrent processes that both had local interrupt mechanisms. The interrupt mechanism was also priority based: a lower interrupt could be interrupted by a higher interrupt. The only way to model it elegantly was to use a nested unless-clause and manually keeping track of the return addresses. A special construct like resume (or return) would have been very helpful.
jiong: Yes, your POLL_INTERRUPT solution is an explicit implementation of Promela's unless statement.
And yes, if the body is more complicated (with if-clauses and/or do-loops), the instrumented body also gets more complicated. But essentially you should explicitly identify the state of each statement (using a ret-value and optionally a label) within the body and jump back to the correct statement.
I agree with you that (more) support for interrupt handling would be great.
Perhaps it would not even be that hard to implement. For example, a 'resume' (or 'return') statement could be added to Promela. This statement could then only be used within an unless-clause and would resume execution of the code at the state in the body that was interrupted.
Each time when SPIN would take an unless transition, it should save the outgoing state (i.e., the return address) within the body. As unless-clauses may be nested, the implementation in SPIN should keep a stack of "return addresses" (for each process). Although this may seem "expensive" with respect to the size of the state vector, this is not really the case. Due to the static nature of the unless-clauses the maximum depth of the return stack is known at compile-time.
When I need to model an interrupt in Promela, I usually encode return addresses by hand.
Your example would then become something like this:
int a = 0;
bool pending = false;
active proctype test()
{
byte ret = 0;
{
skip;
l0: atomic { a++; ret=1; }
l1: atomic { a++; ret=2; }
l2: atomic { a++; ret=3; }
} unless {
pending -> pending = false;
if
:: ret==0 -> goto l0
:: ret==1 -> goto l1
:: ret==2 -> goto l2
:: else
fi
}
assert(a == 3);
}
active proctype controller()
{
do
:: pending = true;
:: pending = pending;
od;
}It is a bit tedious, but not as ugly as the separate unless construct for each statement.
To minimize the extra code clutter at the end of the unless (i.e., the if-clause), you could use a CPP macro for the calculation of the return address. And even the statements of the body could probably be encoded in a CPP macro to hide the labels and the saving of the return addresses.
You could even make this work for a priority level interrupt mechanism, i.e., with a nested unless.
Pages: 1