A forum for Spin users
You are not logged in.
Pages: 1
Greetings again,
similar to my last post about creating Promela models based on sequential C-Code (http://spinroot.com/fluxbb/viewtopic.php?id=1593), i am now trying to transform another typical occurance in C-Code: Passing of values and pointers to another function. I know that Promela does not support types like pointers, structs and double-values, but since there exists the possibility to use c_code{} statements, I want to try to deliver as many information as possible from the C-Code to the resulting Promela model using Modex.
I took the following toy example for my little experiment:
void foo_a ( int *in_a ) {
(*in_a)++;
}
void foo_b ( double *in_b ) {
(*in_b)*=3.2;
}
void main () {
int a;
double b;
a = 1;
b = 1.5;
foo_a(&a);
foo_b(&b);
}
Now, using a specifically designed test harness, I transformed this code into the following Promela model:
// Generated by MODEX Version 2.8 - 1 September 2015
// Wed May 11 16:09:07 CEST 2016 from para.prx
c_state "double b" "Local p_main"
c_state "double * in_b" "Local p_foo_b"
c_state "int * in_a" "Local p_foo_a"
proctype p_foo_a ( chan callback )
{
c_code { Pp_foo_a->in_a = &(Pp_main->a); };
c_code [Pp_foo_a->in_a] { (*Pp_foo_a->in_a)++; };
callback!1;
}
proctype p_foo_b ( chan callback )
{
c_code { Pp_foo_b->in_b = &(Pp_main->b); };
c_code [Pp_foo_b->in_b] { (*Pp_foo_b->in_b)*=3.2; };
callback!1;
}
active proctype p_main ( )
{
chan wait = [0] of { bit };
int bb;
int a;
c_code { Pp_main->a=1; };
c_code { Pp_main->b=1.5; };
run p_foo_a(wait);wait?1;
run p_foo_b(wait);wait?1;
c_code { Pp_main->bb = (int)Pp_main->b; };
assert(false)
}
As you can see, I transformed each function into one proctype and used a rendezvous-point ("wait" and "callback") to determine the execution order. Both former functions get a pointer from a variable of the main process, which content is altered and should also be different once both processes "foo_a" and "foo_b" are complete. By using the c_code{} statement in the beginning of both processes, I imagined that the local pointer variable is now pointing to the wished location.
The last assert is meant to create an error trace, which make me look at the final value of the local variables before the execution terminates. The values of both variables according to this trace are:
local vars proc 0 (p_main):
chan wait (=1): len 0:
int bb: 1
int a: 1
("bb" is meant to contain the rounded value of "b" after the operations, since values of state-variables are not printed out in the error trace")
The results shows that my little experiment has failed, but I am not sure why. Neither Modex nor Spin did report an error during the transformation, so I am guessing that referring to local variables of other processes is legit when done in c_code{}-statements...
Does someone have an explanation what exactly is happening here?
So long,
Max
Offline
I had to trace this down, which means that I have to agree that things aren't obvious here.
The correct way to refer to a local object in another proctype is to use the remote referencing syntax that Promela supports. You cannot do it as in your example. When you use the syntax Pp_main->a inside a proctype named X, the code is going to assume that X is itself main (because that's what Modex generated code will guarantee).
You can bypass the rule that you shouldn't refer to locals in other proctypes (which breaks partial order reduction assumptions) but then you'd have to do it with code as generated from the remote referencing syntax.
This was difficult to trace down -- but the c_code stuff can hide all the wrinkles. Yes, there should have been a syntax error, but to be able to do that Spin would have to learn to parse the code inside c_code blocks, and it tries not to do that (to avoid having to implement a full parser for C itself -- which Modex can do, but not Spin!)
Thanks for the great example of what can go wrong!
Offline
Thanks for the detailed answer!
I think I understand the basic problem here, although I am not sure what you mean by the following:
[quote] You can bypass the rule that you shouldn't refer to locals in other proctypes (which breaks partial order reduction assumptions) but then you'd have to do it with code as generated from the remote referencing syntax.[/quote]
By "code" do you mean the generated Promela code from Modex or the generated C-Code from Spin?
And by "remote referencing syntax" you mean the type of statements like "Pp_proc_name->var = ... "?
Although I don't want to miss the possibility of using partial order reduction in my final model, I am curious how this bypassing of the stated rule would look like if you would apply it to the example above. Is this possible here or would i have to dig into the verifier file or the sources of Modex or Spin?
In the meantime, I tried to solve the same problem with inline-blocks for each function instead of "main", which should be the calling process (basically the same idea I had in the last topic). Some things get easier this way, although I have to do some alterations of the generated model code to get all the references of the variables right. The following model code is the result of this:
// Generated by MODEX Version 2.8 - 1 September 2015
// Thu May 12 10:00:58 CEST 2016 from para_inline.prx
c_state "double b" "Local p_main"
c_state "double * in_b" "Local p_main"
c_state "int * in_a" "Local p_main"
inline foo_a ( )
{
c_code { Pp_main->in_a = &(Pp_main->a); };
c_code [Pp_main->in_a] { (*Pp_main->in_a)++; };
}
inline foo_b ( )
{
c_code { Pp_main->in_b = &(Pp_main->b); };
c_code [Pp_main->in_b] { (*Pp_main->in_b)*=3.2; };
}
active proctype p_main ( )
{
int bb;
int a;
c_code { Pp_main->a=1; };
c_code { Pp_main->b=1.5; };
foo_a();
foo_b();
c_code { Pp_main->bb = (int)Pp_main->b; };
assert(false)
}
local vars proc 0 (p_main):
int bb: 4
int a: 2
Now the model works just like the C-Code, since all the variables are now in the scope of the main-process and can be correctly referred to. However, this creates new types of problems, since Modex extracts all functions in such a way that they are meant to be put into proctypes and not inlines. When changing all the references after the extraction, all local variables of all functions are now within one main process, which can lead to all kinds of conflicts (two variables with the same name, multiple identical labels).
Additionally, Spin has its own way of dealing with these kind of conflicts: I altered the example a little and inserted two local variables "tmp_a" and "tmp_b" in each of the functions. With my method shown above, I want add both variables to the scope of my main process and continue to refer to them through "Pp_main->tmp_a" and "Pp_main->tmp_b". Sadly, this results in an error when compiling the verifier that the structure "Pp_main" has no member named "tmp_a" or "tmp_b", and after looking into the genereated header pan.h, I found out what happened:
#define Pp_main ((P0 *)this)
typedef struct P0 { /* p_main */
unsigned _pid : 8; /* 0..255 */
unsigned _t : 2; /* proctype */
unsigned _p : 5; /* state */
#ifdef HAS_PRIORITY
unsigned _priority : 8; /* 0..255 */
#endif
int bb;
int a;
int _1_1_tmp_a;
int _1_2_tmp_b;
/* XXX p=< p_main >, s=<p_main>, buf=<p_main > r->s->name=< int * in_a >XXX */
int * in_a ;
/* XXX p=< p_main >, s=<p_main>, buf=<p_main > r->s->name=< double * in_b >XXX */
double * in_b ;
/* XXX p=< p_main >, s=<p_main>, buf=<p_main > r->s->name=< double b >XXX */
double b ;
} P0;
Since both locals appear now in the same proctype, Spin automatically renames them to avoid name conflicts. But to be able to use them the way I want, I would need the correct names of the variables in the model before the verifier is generated...
Therefore I am currently not sure in which of these two methods I should invest more time in, since both lead to different kinds of errors that may or may not be solveable by solely using Modex.
Sorry about the long post, but I am currently working full-time on this, and I try a lot of different things to get the kind of models I need. Any input to this is thus very much appreciated
So long,
Max
Offline
by 'code' i meant generated code from spin (for remote variable references) -- it is not supported in modex
for remote referencing i meant the Promela syntax (see manpages)
the renaming of variables is to enforce scope rules (you can turn that off with a spin option if you don't want it, and have no conflicts of the same variable name appearing in nested scopes)
Offline
Pages: 1