145
2005-04-01 18:05:20 +0200
Value passing over channels
2006-11-06 12:31:50 +0100
1
1
1
Unclassified
UPPAAL
Engine
unspecified
All
All
ASSIGNED
P2
enhancement
---
1
behrmann
marius
adavid
kgl
m.amann
oldest_to_newest
397
0
behrmann
2005-04-01 18:05:20 +0200
The modeling language should be extended with value passing over channels. Such
an extension of the language was designed a year or two ago. Plans for an
implementation should be made. I assign this to Marius, as he was involved in
the initial design.
401
1
marius
2005-04-06 19:11:05 +0200
Yes, I will allocate some of my freetime to this after hard-deadline has passed.
422
2
marius
2005-05-03 15:46:19 +0200
SYNTAX: VALUE PASSING DECLARATIONS
I propose to extend the syntax for (channel) variable initializer to include
the type of values to be passed through channel:
Initializer:
Expression /* ordinary variable initializer */
| '{' FieldInitList '}' /* struct variable initializer */
| '{' TypeList '}' ArrayDecl /* value types and size of channel queue */
| '{' TypeList '}' ; /* just value types, assume size=0, i.e. handshake */
ArrayDecl: '[' Expression ']' ;
The above yelds the following backward compatible sentences:
chan a = { int, int[5,10] } [5];
chan b = { int, int[5,10] }; // assume default [0] for handshake
chan c[4] = { int, int[5,10] } [5]; // array of channels
Now, if you are C-person it looks OK, but if you are Promela-person
you would expect some more syntactical sugar like:
chan a = [5] of { int, int[5,10] };
I can massage the bison grammar for one of those forms,
please make up your mind here (are we C or Promela oriented?).
SYNTAX: VALUE PASSING EXPRESSIONS
I propose to extend syntax for synchronization expressions to the following:
SyncExpr:
Expression '!' ArgList
| Expression '?' Arglist ;
ArgList: /* empty */
| Expression /* single value */
| ArgList ',' Expression ; /* several values */
Which would yeld the following sentenced on edge synchronization:
a ! x, y
a ? i, j
where x, y, i and j are expressions of compatible types with a initializer.
SEMANTICS OF VALUE PASSING
Expressions on sending and receiving transitions should be side-effect-free.
Upon synchronization(s) of "a!x,y" and "a?i,j" the following should happen:
1) Evaluate the sending expressions (x,y) and the receiving expressions (i,j).
2) the receiving expressions may yeld either right-value (reference to
variable) or left-value (constant or reference to expression computed value):
2.1) check the types of corresponding expressions
2.2) compare all receiving lvalue expressions with corresponding shouting
values like guards (i==x && j==y in case i and j are lvalue expressions) and
discard the receiving transition if this "guard" is not satisfied.
2.3) execute assignments on rvalue expressions to corresponding sending
expressions (i=x, j=y in case i and j are rvalue expressions).
Similarly to Promela, I propose to have a default function "template"
for converting rvalue expression to lvalue which is defined for all
available types, in C++ I would express this as:
template <type EXPR>
EXPR lval(EXPR value) { return value; };
Note that it is not necessary as we may require user to use his own defined
function to do the same thing.
QUEUED SYNCHRONIZATION SEMANTICS
This is future work. I guess queueing will contribute to the size of
symbolic state and to the whole state space as it becomes asynchronous.
Although, it is good to have syntax denoting queue size for later use
when it is implemented in engine if at all.
NOTES
I already have pretty-printer working to the syntax above, will commit
changes when type-checker is done, so please send your comments.
925
3
marius
2006-02-23 16:25:44 +0100
Gerd (and Kim?) asked to have conditions on receiving synchronization, hence
some ideas on that:
1) sending part: a ! x, y, z
receiving part: a ? #1>5, i==#2, j=#3, k=#1+#3
where #1 denotes the first variable value in structure that is passed
via channel, i.e. x, #2 means value of y and #3 is z.
semantics of such synchronization would be:
synchronize only if (x>5) and (i==y) then execute j=z, k=x+z
perhaps it makes sense to separate conditions from assignments by ";", or
require conditions not to be mixed with
This would allow conditions to be added to existing guards
(transition filter) and assignments to updates (expensive successor filter),
hence simpler(?) and more efficient(?) implementation.
2) sending part: a ! x, y, z
receiving part: a ? f
where f is a function with a signature:
boolean f(typeof(x), typeof(y), typeof(z))
semantics would be: execute f with x,y,z as parameters and fire
the transition only if function returns true.
it looks more powerfull but could probably be executed only in successor
filter with additional (expensive) state-copy.
There seems to be a potential problem with side-effects in broadcast
synchronizations where reveiver could potentially modify the value that is being
sent (like a!x,y with a?x=#2,y=#1).
Additional static analysis on variables would be needed or we could allow only
local values to be transmitted or reveived.
any comments?
1047
4
marius
2006-04-07 17:03:44 +0200
From interview with Alexandre ;-)
Parenthesis around parameters are wanted, and (optionally) conditions could be placed after assignment, like in Ruby.
Syntax:
sending part: a! (x, y)
receiving part: a? (&i, &j) if (i>5 && i+j+k<10)
Semantics:
i=x, j=y, and synchronization is taken only if (i>5 && i+j+k<10) is true.
Implementation:
1) during parsing (or just before model-checking) rewrite the receiving part to the following: a? (&i, &j) if (#1 > 5 && #1 + #2 + k < 10)
where #1 and #2 are the references to the first and the second value sent (to be received), k is just another variable.
2) now the conditional part can be checked (in transition filter) just after guard evaluation: if true proceed with successor computation, otherwise discard.
3) value assignments executed in successor filter before assignment.
Benefits: cosier syntax, memory save on state size (due to removed reduntant global communication variables) and increased performance (due to avoiding redundant expensive state copy).