Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-06 01:52:40 -0700 (Tue, 06 Sep 2005)
Revision: 1952
Log message:

      Bits of the model for the group communication library in Promela.
      

Changes by: dnoblet (dnoblet at unknown.email)
Date: 2005-09-07 16:59:32 -0700 (Wed, 07 Sep 2005)
Revision: 1953
Log message:

      Modifications have been made to incorporate a new version of the view change protocol where the new view is decided upon in three stages as opposed to two.
      

Changes by: dnoblet (dnoblet at unknown.email)
Date: 2005-09-07 17:19:53 -0700 (Wed, 07 Sep 2005)
Revision: 1954
Log message:

      Minor fix to module name so the model checker won't complain.
      

Changes by: dnoblet (dnoblet at unknown.email)
Date: 2005-09-09 13:50:28 -0700 (Fri, 09 Sep 2005)
Revision: 1955
Log message:

      Forgot to reset certain variables when a process that has initiated a view change detects that another process with higher priority has also initiated a view change.
      

Changes by: dnoblet (dnoblet at unknown.email)
Date: 2005-09-09 22:53:59 -0700 (Fri, 09 Sep 2005)
Revision: 1956
Log message:

      Some edits (somewhat incomplete) were done to enable the compilation of acks from initiate view change and new view messages on the fly.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-12 11:28:42 -0700 (Mon, 12 Sep 2005)
Revision: 1957
Log message:

      Spin models contains 80% of the new protocol description.
      This is my last commit before migrating the repository to subversion.
      

Changes by: dnoblet (dnoblet at unknown.email)
Date: 2005-09-13 12:32:50 -0700 (Tue, 13 Sep 2005)
Revision: 1971
Log message:

      The model has been fixed again so it should be able to run through TLC.
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-13 18:20:33 -0700 (Tue, 13 Sep 2005)
Revision: 1981
Log message:

      Added local sequence numbers. Sequence number reset still needs to be handled properly though.
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-14 12:18:22 -0700 (Wed, 14 Sep 2005)
Revision: 1996
Log message:

      Now a process will properly initiate its own view change if it detects that the initiator of the current view change has died.
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-14 18:26:13 -0700 (Wed, 14 Sep 2005)
Revision: 2005
Log message:

      Fixed bug where join requests would be sent too often. Also fixed bug where a duplicate view change would be initiated if a node doesn't respond to an initiate view change message.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-15 00:36:41 -0700 (Thu, 15 Sep 2005)
Revision: 2021
Log message:

      This is the spin model that should be similar to the TLA model we have.
      
      I just ran it in verification mode and it finished in about 5-7 minutes.
      
      [crt@dhcp-133-187 spin]$ ./gcomm.spin
      Depth=     336 States=   1e+06 Transitions= 4.5289e+07 Memory= 178.852
      (Spin Version 4.2.5 -- 2 April 2005)
              + Partial Order Reduction
      
      Full statespace search for:
              never claim             - (none specified)
              assertion violations    +
              cycle checks            - (disabled by -DSAFETY)
              invalid end states      +
      
      State-vector 176 byte, depth reached 336, errors: 0
      1.40245e+06 states, stored
      6.48361e+07 states, matched
      6.62386e+07 transitions (= stored+matched)
             7 atomic steps
      hash conflicts: 7.85311e+07 (resolved)
      
      Stats on memory usage (in Megabytes):
      263.660 equivalent memory usage for states (stored*(State-vector + overhead))
      247.803 actual memory usage for states (compression: 93.99%)
              State-vector as stored = 165 byte + 12 byte overhead
      2.097   memory used for hash table (-w19)
      0.320   memory used for DFS stack (-m10000)
      0.436   memory lost to fragmentation
      249.816 total actual memory usage
      
      unreached in proctype node_active
              line 741, state 933, "-end-"
              (336 of 933 states)
      unreached in proctype :init:
              (0 of 12 states)
      
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-15 18:40:29 -0700 (Thu, 15 Sep 2005)
Revision: 2024
Log message:

      Fixed a couple of bugs related to failure detection.
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-16 02:22:05 -0700 (Fri, 16 Sep 2005)
Revision: 2025
Log message:

      I made some edits to get the model into a form that can be verified by TLC. 
      
      It runs through the model checker (with two processes) in about 10 minutes.
      
      [dnoblet@flywheel:~/tla]> java -Xms1024M -Xmx1024M -cp /cs/prl/dump/tla/ tlc.TLC -workers 8 -difftrace ViewChange.tla
      TLC Version 2.0 of August 18, 2005
      Model-checking
      Parsing file ViewChange.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/Naturals.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/FiniteSets.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/Sequences.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/TLC.tla
      Semantic processing of module Naturals
      Semantic processing of module Sequences
      Semantic processing of module FiniteSets
      Semantic processing of module TLC
      Semantic processing of module ViewChange
      Finished computing initial states: 2 distinct states generated.
      Progress(52): 524929 states generated, 150760 distinct states found, 11240 states left on queue.
      Progress(115): 4306979 states generated, 1128915 distinct states found, 18165 states left on queue.
      Model checking completed. No error has been found.
        Estimates of the probability that TLC did not check all reachable states
        because two distinct states had the same fingerprint:
          calculated (optimistic):  2.5112817216065095E-7
          based on the actual fingerprints:  6.347960939726746E-7
      4915297 states generated, 1271251 distinct states found, 0 states left on queue.
      The depth of the complete state graph search is 147.
      
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-16 11:48:23 -0700 (Fri, 16 Sep 2005)
Revision: 2028
Log message:

      Just a couple of minor fixes to get rid of some warnings.
      
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-16 11:53:19 -0700 (Fri, 16 Sep 2005)
Revision: 2029
Log message:

      A few more fixes in the spin model

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-18 23:21:08 -0700 (Sun, 18 Sep 2005)
Revision: 2031
Log message:

      Fixed local sequence number reset conditions.
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-19 11:10:37 -0700 (Mon, 19 Sep 2005)
Revision: 7717
Log message:

      Added PostponedJoins to keep track of nodes that were unable to be incorporated into the current view change.
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-19 15:25:53 -0700 (Mon, 19 Sep 2005)
Revision: 7723
Log message:

      Small fix to prevent a case where the dection of a failure could be forgotten.
      
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-19 18:58:21 -0700 (Mon, 19 Sep 2005)
Revision: 7768
Log message:

      Version without fancy reset of local sequence numbers

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-20 13:44:56 -0700 (Tue, 20 Sep 2005)
Revision: 7769
Log message:

      A non terminating version of the reset and replace lseqn "policy".
      
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-20 17:20:41 -0700 (Tue, 20 Sep 2005)
Revision: 7770
Log message:

      A version of the model that finishes fast for 2 nodes and buffer size 5.
      
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-20 21:05:46 -0700 (Tue, 20 Sep 2005)
Revision: 7771
Log message:

      Made some edits to the sequence number reset mechanism.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-21 01:25:21 -0700 (Wed, 21 Sep 2005)
Revision: 7772
Log message:

      This model is almost perfect... 
      
      I do get a small discrepancy in the total number of states if I start 
      with different initial states. I can't really explain it but it might be 
      just an artifact of spin's way of displaying the number of states.
      
      Also, this model finds a counter-example for buffer size 5 and 2 processes
      but it seems to work fine for 2 processes with buffer size of 6.
      
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-21 17:28:04 -0700 (Wed, 21 Sep 2005)
Revision: 7774
Log message:

      A working model. For 2 nodes and buffer size of 5 it works fine.
      Next I need to put in an optimization on detecting failures
      and try to run it for 3 nodes.
      
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-21 17:37:06 -0700 (Wed, 21 Sep 2005)
Revision: 7775
Log message:

      Now failure detection while waiting for acks acts more like a timeout; all nodes that have not responded to a request at the time of failure detection are suspected dead.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-21 23:14:48 -0700 (Wed, 21 Sep 2005)
Revision: 7776
Log message:

      This model includes the optimization for detecting failures
      
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-23 13:56:39 -0700 (Fri, 23 Sep 2005)
Revision: 7780
Log message:

      Added OMakefile for TLA models
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-28 17:46:50 -0700 (Wed, 28 Sep 2005)
Revision: 7792
Log message:

      Added the spin model for the "catching-up" phase in the view change 
      protocol.
      
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-29 02:12:09 -0700 (Thu, 29 Sep 2005)
Revision: 7796
Log message:

      Added the TLA model for the "catching-up" phase of the view change protocol.
      
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-29 18:01:20 -0700 (Thu, 29 Sep 2005)
Revision: 7803
Log message:

      More changes to the model. 
      
      

Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-29 18:18:25 -0700 (Thu, 29 Sep 2005)
Revision: 7804
Log message:

      Added support for detecting old replies that we have timed out on.