Interpreter: Parallel and map update bug

[richardpaynea55]

There appears to be a bug with the map update expression when called in an operation in a parallel process. Given the model below:

channels
  inA :  nat * nat
  outA :  map nat to nat
  test

process p = 
begin
  state
    a: map nat to nat := {1|->3, 3|->4, 5|-> 9, 7|->8}

  operations
    updateA :  map nat to nat ==> ()
    updateA(newA) == 
      a := a ++ newA

  actions
    PARRACT = ACT1 ||| ACT2
    ACT1 = [] i in set {1,2,3,4,7} @ inA.i?n -> (updateA({i|->n}); outA!a -> Skip)
    ACT2 = test-> (updateA({3|->3});Skip)

  @ PARRACT
end

When attempting to update the map index 1 or 2, the update fails (inA.1.x, inA2.2.x) however any other (inA.3.x, inA.4.x, inA.7.x) updates the map successfully. However, when removing the parallel operator and ACT2, all map updates work perfectly.

Not sure if this is a map or parallel issue.

[joey-coleman]

I suspect that this and #293 are both actually working per the semantics, but i'll dig into this in the next couple of days. Part of what suggests this is that neither this example nor the one in #293 are using namesets — for values to 'escape' their parallel branch, they must be named in the corresponding nameset, otherwise changes just get thrown away.

[richardpaynea55]

No worries - I have a larger example which has some very odd behaviour - tried to trim it down in for this simple example - let me know if you want to use that. The odd thing is really the inconsistency in how the assignments to the map change depending on which domain value is updated...

[joey-coleman]

There is something that's not behaving correctly; I will construct an example for this and #293 shortly.

[joey-coleman]

So, simple model for sanity:

channels
  ping
  pair : nat * nat

process TEST = begin
state
  simple : nat := 0
actions
  TOP = A(1) ||| A(2)
  A   = val x : nat @ pair!x!simple -> simple := x; pair!x!simple -> Skip
@ ping -> TOP ; ping!simple!simple -> Skip
end

This works correctly, giving the traces <ping.0; (pair.1.0,pair.1.1) interleaved with (pair.2.0, pair.2.2); ping.0> (there are four permutations in total).

So I think it may have to do with maps, specifically.

[joey-coleman]

More complex example; this fails. I get the trace:

ping.0, pair.1.0, pair.2.0, pair.2.2, pair.1.1, ping.2

and the last ping.2 should definitely be a ping.0

channels
  ping : nat
  pair : nat * nat

process TEST = begin
state
  simple : map nat to nat := {1 |-> 0}
actions
  TOP = A(1) ||| A(2)
  A   = val x : nat @ 
          pair!x!(simple(1)) ->
          simple(1) := x;
          pair!x!(simple(1)) ->
          Skip
@ ping!(simple(1)) ->
  TOP;
  ping!(simple(1)) ->
  Skip
end

[lausdahl]

This looks like a problem with the DelayedWriteContext and MapValue + SeqValue. Both of these are non-updatable but can actually be updated using a AMapSeqStateDesignator. Where simple(1) returns an updatable value (from the none updatable map) or if the index doesnt exist it adds it and returns it as updatable.

So I think the above example can be reproduced using a seq too.

[joey-coleman]

ok, confirmed bug; I'm assigning it over to @lausdahl :)