Interpreter: Operations fail to update state

[joey-coleman]

[Submitting for @JeremyBryans, who wasn't able to submit for some reason]

I think I’ve got a case where the operation isn’t updating the state as it should, but I may be wrong.

I have different behaviour from two processes, Election and Election2. The traces from each are below, as is the CML source.

From the debug traces, the difference is whether or not the variable myCS is updated. (This variable is debugged on the channel DebugClaim.i.j.claim, where i is the node id, & j is a marker for the position within process Undecided where the debug is taking place. )

myCS is updated by the operation changeClaim(newc), which is called between position 1 and position 2 in the traces below. myCS is updated only in Election2.

If I make the change directly as an assignment within the process things behave as I'd expect.

The top level definitions:

allNodes = {1,...,3}

process AllNodesSet = ||| i in set allNodes @  (Node(i)) 
process ThreeNodes = Node(1) ||| Node(2) ||| Node(3)
process Election = (AllNodesSet [|{|inn,out|}|] MessageStore)  \\ {|inn,out|}
process Election2 = (ThreeNodes [|{|inn,out|}|] MessageStore)  \\ {|inn,out|}

Trace from Election:

[init.1, init.2, init.3, on.1, on.2, on.3, DebugMem.1.1.{2 |-> nil, 3 |-> nil}, DebugMem.2.1.{1 |-> nil, 3 |-> nil}, DebugMem.3.1.{1 |-> nil, 2 |-> nil}, DebugClaim.1.1.mk_CS(<off>, 0), DebugClaim.2.1.mk_CS(<off>, 0), DebugClaim.3.1.mk_CS(<off>, 0), DebugMem.1.2.{2 |-> nil, 3 |-> nil}, DebugMem.2.2.{1 |-> nil, 3 |-> nil}, DebugMem.3.2.{1 |-> nil, 2 |-> nil}, DebugClaim.1.2.mk_CS(<off>, 0), DebugClaim.2.2.mk_CS(<off>, 0), DebugClaim.3.2.mk_CS(<off>, 0)]

Trace from Election2:

[init.1, init.2, init.3, on.1, on.2, on.3, DebugMem.1.1.{2 |-> nil, 3 |-> nil}, DebugMem.2.1.{1 |-> nil, 3 |-> nil}, DebugMem.3.1.{1 |-> nil, 2 |-> nil}, DebugClaim.1.1.mk_CS(<off>, 0), DebugClaim.2.1.mk_CS(<off>, 0), DebugClaim.3.1.mk_CS(<off>, 0), DebugMem.1.2.{2 |-> nil, 3 |-> nil}, DebugMem.2.2.{1 |-> nil, 3 |-> nil}, DebugMem.3.2.{1 |-> nil, 2 |-> nil}, DebugClaim.1.2.mk_CS(<undecided>, 0), DebugClaim.2.2.mk_CS(<undecided>, 0), DebugClaim.3.2.mk_CS(<undecided>, 0), undecided.1, undecided.2, undecided.3]   

The CML source is below.

values 

  debug = false -- true
  debugMem = true -- true
  debugCS = true -- true

 allNodes : set of nat = {1,...,3}

 uls : nat = 10

 n_timeout : nat = 1     -- the timeout value employed by the Nodes

types

 NODE = nat
  inv n == n in set allNodes

 CLAIM = <leader>|<follower>|<undecided>|<off>|<TEST>
 STRENGTH = nat

 CS :: c : CLAIM
        s : STRENGTH

-- The only messages transmitted are CS messages, so MSG can be specialised to them  
 MSG :: src : NODE
        dest : NODE
        cs : CS 

channels
  inn : NODE * NODE * MSG     -- SRC * DEST * MSG
  out : NODE * NODE * MSG     -- DEST * SRC * MSG

  debugStore : map NODE to seq of MSG
  debugKey : NODE
  debugTail, debugStoreI : seq of MSG

process MessageStore =
begin 
 state
  store : map NODE to seq of MSG := {i|->[]|i in set allNodes}

 operations

   RmvHdFrmStore:NODE ==> ()
   RmvHdFrmStore(i) ==
    store := store ++ {i |-> tl(store(i))}
   pre store(i) <> []

-- temp back in  functions

/*      -- implicit helper function; selects an element of a non-empty set  
     select(sn : set of nat) r: nat
     pre sn <> {}
     post r in set sn 
*/       

 actions

  DebugState = i : nat @ 
   if debug then 
    debugStore!store ->
      debugStoreI!(store(i)) -> 
        debugKey!i -> 
          debugTail!(tl(store(i))) -> Skip
   else 
    Skip

   Loop =  
    inn?src?des?m -> store(m.dest) := store(m.dest)^[m]; Skip  
     []
     ([] i in set allNodes @ 
       [store(i) <> []] &  -- there are messages for node i    
          let m = hd(store(i)) in
          out!(m.dest)!(m.src)!m -> 
               RmvHdFrmStore(i);
                 Skip)

   @ while true do Loop
end          

channels 
 on, off,init : nat1

-- test channels
 leading : nat1
 following : nat1
 undecided : nat1

 DebugLeaders : NODE * nat * nat
 DebugHighestStrength : NODE * nat * [STRENGTH] 
 DebugHighestStrengthID : NODE * nat * [NODE]
 DebugIsLeader : NODE *  nat *bool
 DebugMem      : NODE * nat * map NODE to [CS]
 DebugClaim : NODE * nat * CS

 DebugClaimBeforeL : NODE * CS
 DebugClaimAfterL : NODE * CS

 DebugStrength : NODE * STRENGTH

process Node = i : nat1 @

begin 

state

   mem: map NODE to [CS] := { cid |-> nil | cid in set allNodes \ {i} }         
    inv dom mem = allNodes  \ {i} and -- the domain of mem must not include id (the ID of the node)
        dom mem <> {}                  -- must be more than one node in the network  (although this model 
                                       -- should work if there is only one node)

   -- below are summary variables  
   highest_strength : [STRENGTH] := nil                   -- the highest strength of leadership claim node is aware of         

   highest_strength_id : [NODE] := nil                 -- id of node making the leadership claim with the highest strength
                                                      -- this is allowed to be any node id, including id itself

   inv highest_strength_id <> nil => highest_strength_id in set (dom mem union {i}) 

   leaders : nat := 0                                 -- the leader count among my neighbours
   inv leaders <= card dom mem

   myCS : CS := mk_CS(<off>, 0)                                     -- my claim/strength pair

   isleader : bool := false

  -- temp variables s,c created here while maxSet cannot use dcl to create them.

  s : set of nat 
  c : nat

operations

   flushState: () ==> ()
   flushState() ==
    (
     flushMemory();flushSummary()
    )

   flushMemory: () ==> ()
   flushMemory() ==
      (
       mem := { cid |-> nil | cid in set allNodes \ {i} } 
      )

   flushSummary: () ==> ()
   flushSummary() ==
   ( 
     highest_strength := nil; --0;
     highest_strength_id := nil; 
     leaders := 0;                
     myCS := mk_CS(<off>, 0);
     isleader := false
   )

   write: NODE * MSG ==> ()
   write(j,m) ==
   ( 
    mem := mem ++ {j |-> m.cs}
   )     
   pre j in set dom mem
   post mem(j) = m.cs

   update:()==>()
   update() == 
   (  --the leaders count should not increase if mem(c)=nil
     leaders := card{n|n in set dom mem @ mem(n)<>nil and mem(n).c = <leader>};
     highest_strength := maxStrength();                
     highest_strength_id := maxStrengthID()
   )  

--    post isleader or 
--         (leaders > 0 and  mem(highest_strength_id).s = highest_strength)

   -- maxStrengh returns the maximum strength of leadership claim

 maxStrength:() ==> [nat]
   maxStrength() == 
   (
    let leaderNodes = {n|n in set dom mem @ mem(n) <> nil and mem(n).c = <leader>} in
    (    
    if leaderNodes <> {} then 
     let strs = {mem(l).s|l in set leaderNodes} in 
      if strs <> {} 
      then return maxSet(strs) 
      else return nil 
    else return nil   
    )
   )    

  -- return the ID of the leader with the max strength
  -- or nil if no leader claims

    maxStrengthID : () ==> [NODE]
   maxStrengthID() ==  
   (
     let leaderNodes = {n|n in set dom mem @ mem(n) <> nil and mem(n).c = <leader>} in 
     (
      if leaderNodes = {} 
      then return nil 
      else 
        let maxStrIds = {n | n in set leaderNodes @ mem(n).s = highest_strength} in 
        -- return select(maxStrIds) -- select is wrong here; has to pixk the maximum one!!
        return maxSet(maxStrIds)
      )
    )   

    -- update my claim 
   -- note that we can enforce state transitions through the changeClaim operation
   -- since Claim corresponds directly to the states in the ST diagram

   changeClaim: CLAIM ==> ()
   changeClaim(newc) ==
   ( 
--      if myCS.c = newc then      
--       myCS := mk_CS(newc, myCS.s)  
--      else --reset strength -- could differentiate between leader and follower
--       myCS := mk_CS(newc,0)
        myCS.c := newc
    )

/*  pre myCS.c = <off> => newc = <undecided> and
        myCS.c = <undecided> => newc = <leader> or newc = <follower> and
       myCS.c = <leader> => newc = <undecided> and
       myCS.c = <follower> => newc = <undecided>
*/

   changeStrength: nat ==> ()
   changeStrength(n) ==
     myCS := mk_CS(myCS.c,n)

   -- increase the strength of my claim up to the maximum (upper limit of petitions: uls)
    incStrength:()==>()
    incStrength() ==
    (
      if myCS.s < uls                    
      then myCS := mk_CS(myCS.c, myCS.s+1)
      else Skip
    )

   amILeader: () ==> bool
   amILeader() ==  
   (
     return (leaders = 0)  or
            (highest_strength = nil) or  
            (highest_strength <> nil and highest_strength < myCS.s) or 
            (highest_strength <> nil and highest_strength = myCS.s and highest_strength_id < i) 
   )

 maxSet: set of nat ==> nat
   maxSet(sn) ==
    ( 
--    dcl s:nat @   
         s:= sn;
--      (
--      dcl c:nat @ 
        c := select(s); 
        s := s \ {c};
        while (s <> {}) do
         (let n = select(s) in
            (if (n>c) then c:=n else c:=c;
             s := s\{n})
         ); 
       return c
--        )
     )
     pre sn <> {}

 functions

     -- implicit helper function; selects an element of a non-empty set  
     select(sn : set of nat) r: nat
     pre sn <> {}
     post r in set sn 

 actions 

   Listener = ReceiveData;update();Skip

   Debug = pos : nat @ DebugM(pos);DebugRest(pos);DebugMyCS(pos)

   DebugM =  pos : nat @
   if debugMem then
     DebugMem!i!pos!mem -> Skip
   else 
    Skip
   DebugRest = pos : nat @
   if debug then  
    DebugLeaders!i!pos!leaders ->
     DebugHighestStrength!i!pos!highest_strength -> 
      DebugHighestStrengthID!i!pos!highest_strength_id -> 
       DebugIsLeader!i!pos!isleader ->
          Skip
    else
     Skip  

   DebugMyCS = pos : nat @
   if debugCS then  
       DebugClaim!i!pos!myCS ->
          Skip
    else
     Skip      

  -- receive data via "out", writes then repeats until timed out

       ReceiveData = 
       (
        out!i?j?msg -> (mem := mem ++ {j |-> msg.cs}); ReceiveData
       ) [_ n_timeout _> Skip

-- The first version of SendCS produces an exception: it is reported as Bug#268

--    SendCS = (||| t in set dom mem @ [{}] inn!i!t!(mk_MSG(i,t,myCS)) -> Skip) -- insists on sending all messages before it progresses.

-- The second version is temporary.

     SendCS =
      let mycs = myCS in
      ( 
       for all d in set dom mem do
         (
           inn!i!d!(mk_MSG(i,d,mycs)) -> Skip 
         ) 
      )

   Off =  on!i -> (Undecided /_\  off!i -> flushState();Off)  

-- isleader must to be updated separately and directly; otherwise the guards don't work correctly.

   Undecided = Debug(1);
--                   (myCS.c := <undecided>);  
--                 changeClaim(<leader>);   -- the operation fails; I don't know why. 
                 changeClaim(<undecided>); 
                Debug(2);
                  undecided!i -> Debug(3);Listener;
                (isleader := amILeader());
                 Debug(4);
              (
            [isleader] & Leader
               [] 
               [not isleader] & Follower
              )             

   Leader =  changeClaim(<leader>);
                  leading.i-> Debug(1);
                   SendCS; 
                    Listener; 
                     (isleader := amILeader()); 
       --                Debug(2);
            (
             [not isleader] & Undecided  
             []
             [isleader] & incStrength();Leader
            )                    

--    Follower = changeClaim(<follower>);flushMemory(); following.i -> DebugMyCS();SendCS; Listener; -- flushing primary memory; self-declare as a follower
 Follower = changeClaim(<follower>);changeStrength(0); following!i ->
 -- Debug(2);
    SendCS; flushMemory();Listener; -- flushing primary memory; then listen
                (isleader := amILeader());
               --   Debug(2);
              (                                                
               [leaders <> 1] & Undecided 
               []
               [leaders = 1] & Follower                      
              )             

 @ init.i -> flushState();Off

end

process AllNodesSet = ||| i in set allNodes @  (Node(i)) 

process AllNodesType = ||| i : NODE @  (Node(i)) 

process OneNode = Node(1)

process TwoUnconnectedNodes = Node(1) ||| Node(2)

process ThreeNodes = Node(1) ||| Node(2) ||| Node(3)

process TwoProcesses = (TwoUnconnectedNodes [|{|inn,out|}|] MessageStore) \\ {|inn,out|}

process Election = (AllNodesSet [|{|inn,out|}|] MessageStore)  \\ {|inn,out|}

process ElectionType = (AllNodesSet [|{|inn,out|}|] MessageStore)  \\ {|inn,out|}

process Election2 = (ThreeNodes [|{|inn,out|}|] MessageStore)  \\ {|inn,out|}

--===testing area===--
channels 
success, cp1,cp2,cp3,offthree,alloff
chansets 
allEventsExcOff = {|init,on,undecided,leading,following|}
allEvents = {|init,on,undecided,leading,following|} union {|off|}
process Tests = i : nat @
begin 
actions 

RunTest = 
  [i=1] & Init;AllOn;Trace1;Success                      -- success after three tocks
  []
  [i=2] & Init;AllOn;Trace2;Success                      -- success after two tocks [off.3, offthree, tock, tock, success]
  []
  [i=3] & Skip;Success                                   -- immediate success 
  []
  [i=4] & Init;AllOn;Trace1;AllOff;AllOn;Trace4;Success  -- fails: should have [tock, tock, tock, tock, tock, tock, success]
  []
  [i=5] & Init;AllOn;Trace1;Trace5;Success               -- fails
  []
  [i=6] & Trace6;Success

  Init   = init.1 -> init.2 -> init.3 -> Skip
  AllOn  = on.1 -> on.2 -> on.3 -> Skip
  AllOff = off.1 -> off.2 -> off.3 -> Skip
  Success = success -> Skip 

  Trace1 =   undecided.1 -> undecided.2 -> undecided.3 -> 
            leading.1 -> leading.2 -> leading.3 ->              
               leading.3 -> undecided.1 ->  
                  undecided.2 -> 
                   following.1 -> following.2 -> leading.3 -> Skip
  Trace2 = undecided.1 -> undecided.2 -> undecided.3 -> offthree ->
          leading.1 -> leading.2 -> leading.2 -> undecided.1 -> Skip

  Trace4 = undecided.1 -> undecided.2 -> undecided.3 -> off.3 ->
          leading.1 -> leading.2 -> leading.2 -> undecided.1 -> 
            leading.2 -> following.1 -> Skip

Trace6 = Trace1;AllOff;AllOn

  Trace5 = off.3 -> undecided.1 -> undecided.2 -> 
           leading.2 -> following.1 -> leading.2 -> following.1 -> 
             on.3 -> undecided.3 -> leading.2 -> following.1 ->
              leading.2 -> following.1 -> following.3 -> Skip 

 @RunTest
end  

process TestOne = Election [|allEventsExcOff|] Tests(1)    \\ allEventsExcOff
process TestTwo = Election [|allEventsExcOff|] Tests(2)    \\ allEventsExcOff
process TestThree = Election [|allEventsExcOff|] Tests(3)    \\ allEventsExcOff
process TestFour = Election [|allEvents|] Tests(4)    \\ allEvents
process TestFive = Election [|allEvents|] Tests(5)    \\ allEvents

[joey-coleman]

Obvious question: any chance you can provide a minimal example?

[JeremyBryans]

Below; running Version: 0.3.3-SNAPSHOT Build date: 2014 Jul 03 15:24 CEST Git commit description: Dev/0.3.3-117-g1931a74

The call to an operation in process INT does not update the state.

The call to the same operation in process INT2 does.

channels 

 debug : nat * nat

process simple = id : nat @ begin

state 
 s : nat := 0

operations

  add: nat ==> ()
  add(n) == s:= s+n

actions
 P = debug!id!s -> add(3);debug!id!s -> Skip

@ P

end

process INT = ||| i in set {1} @ simple(i)

process INT2 = simple(1) -- ||| simple(2) ||| simple(3)    

[JeremyBryans]

sorry - trying to submit; still very much open!

[lausdahl]

The general issue here is that:

process INT = ||| i in set {1} @ op(i)

generates a context for op as:

ctxt (delayed write) [i=1]

but since this is a replication of 1 then there is not replicated node to handle the "replication" and thus no where to terminate it e.g. writing the changes.

A solution that seems to work is to only use delayed contexts when there is more than one in a replication. If the replication is done only once then there for e.g. [] is no need for a roll back.

Changing the context to be a plain context as:

ctxt [i=1]

seems to do the job. It makes any change that happens to state visible immediately. (this of cause only affects the current construct. If nested then the assignment might still be nested from its parent

||| i in set {1,2,...} @ ||| j in set {1}@ var:=op(i,j)

[richardpaynea55]

Quick question: what are delayed/plain contexts? Is this something that we need to sort out in the model, or an interpreter bug?

Also, the issue appears irrespective of the cardinality of the replication set. So for example:

process INT = ||| i in set {1,2,3} @ op(i)

also has the same issue.

[joey-coleman]

No, this is internal; that was mostly a comment between Kenneth and I, as we try to untangle the problem in the code.

[JeremyBryans]

Ah -- thanks Joey -- it had me baffled ;-)

[joey-coleman]

Still broken in aca6238 — this may be a regression at this point.

[joey-coleman]

This is indeed a regression from fixing something else (related, but not directly connected).

I should also note that the expected behaviour here is only correct because the interleaving operator is used in a process context rather than an action context. If it were in an action context, you would have to give namesets (and you wouldn't be able to use replication, because we don't have indexed namesets).

[lausdahl]

This is fixed in https://github.com/symphonytool/symphony/commit/5814e9804dfffcaf1598719dc7cad12d822b8408

[joey-coleman]

This will appear in development build 81 on the buildserver; it's pending as I post this.