[crt] Bits of the model for the group communication library in Promela._ Tue Sep 13 04:29:42 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-42-725270000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-42-725270000-PDT.html [dnoblet] 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._ Tue Sep 13 04:29:45 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-45-182679000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-45-182679000-PDT.html [dnoblet] Minor fix to module name so the model checker won_t complain._ Tue Sep 13 04:29:46 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-46-286687000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-46-286687000-PDT.html [dnoblet] 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._ Tue Sep 13 04:29:46 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-46-681882000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-46-681882000-PDT.html [dnoblet] Some edits _somewhat incomplete_ were done to enable the compilation of acks from initiate view change and new view messages on the fly._ Tue Sep 13 04:29:47 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-47-119101000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-47-119101000-PDT.html [crt] Spin models contains 80_ of the new protocol description._ Tue Sep 13 04:29:47 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-47-804253000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-04-29-47-804253000-PDT.html [dnoblet] The model has been fixed again so it should be able to run through TLC._ Tue Sep 13 12:32:50 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-12-32-50-605023000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-12-32-50-605023000-PDT.html [dnoblet] Added local sequence numbers. Sequence number reset still needs to be handled properly though._ Tue Sep 13 18:20:39 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-18-20-39-861553000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-13-18-20-39-861553000-PDT.html [dnoblet] Now a process will properly initiate its own view change if it detects that the initiator of the current view change has died._ Wed Sep 14 12:18:23 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-14-12-18-23-357362000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-14-12-18-23-357362000-PDT.html [dnoblet] 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._ Wed Sep 14 18:26:14 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-14-18-26-14-236900000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-14-18-26-14-236900000-PDT.html [crt] This is the spin model that should be similar to the TLA model we have._ Thu Sep 15 00:36:42 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-15-00-36-42-374546000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-15-00-36-42-374546000-PDT.html [dnoblet] Fixed a couple of bugs related to failure detection._ Thu Sep 15 18:40:29 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-15-18-40-29-728085000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-15-18-40-29-728085000-PDT.html [dnoblet] I made some edits to get the model into a form that can be verified by TLC._ Fri Sep 16 02:22:06 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-16-02-22-06-367977000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-16-02-22-06-367977000-PDT.html [dnoblet] Just a couple of minor fixes to get rid of some warnings._ Fri Sep 16 11:48:24 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-16-11-48-24-690947000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-16-11-48-24-690947000-PDT.html [crt] A few more fixes in the spin model_ Fri Sep 16 11:53:20 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-16-11-53-20-425424000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-16-11-53-20-425424000-PDT.html [dnoblet] Fixed local sequence number reset conditions._ Sun Sep 18 23:21:09 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-18-23-21-09-265032000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-18-23-21-09-265032000-PDT.html [dnoblet] Added PostponedJoins to keep track of nodes that were unable to be incorporated into the current view change._ Mon Sep 19 11:10:38 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-19-11-10-38-488103000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-19-11-10-38-488103000-PDT.html [dnoblet] Small fix to prevent a case where the dection of a failure could be forgotten._ Mon Sep 19 15:25:53 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-19-15-25-53-634338000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-19-15-25-53-634338000-PDT.html [crt] Version without fancy reset of local sequence numbers_ Mon Sep 19 18:58:22 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-19-18-58-22-299353000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-19-18-58-22-299353000-PDT.html [crt] A non terminating version of the reset and replace lseqn _policy_._ Tue Sep 20 13:44:57 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-20-13-44-57-957980000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-20-13-44-57-957980000-PDT.html [crt] A version of the model that finishes fast for 2 nodes and buffer size 5._ Tue Sep 20 17:20:42 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-20-17-20-42-704090000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-20-17-20-42-704090000-PDT.html [dnoblet] Made some edits to the sequence number reset mechanism._ Tue Sep 20 21:05:47 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-20-21-05-47-453321000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-20-21-05-47-453321000-PDT.html [crt] This model is almost perfect..._ Wed Sep 21 01:25:23 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-01-25-23-274641000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-01-25-23-274641000-PDT.html [crt] A working model. For 2 nodes and buffer size of 5 it works fine._ Wed Sep 21 17:28:05 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-17-28-05-074610000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-17-28-05-074610000-PDT.html [dnoblet] 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._ Wed Sep 21 17:37:07 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-17-37-07-222901000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-17-37-07-222901000-PDT.html [crt] This model includes the optimization for detecting failures_ Wed Sep 21 23:14:49 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-23-14-49-530256000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-21-23-14-49-530256000-PDT.html [dnoblet] Added OMakefile for TLA models_ Fri Sep 23 13:56:40 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-23-13-56-40-882323000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-23-13-56-40-882323000-PDT.html [crt] Added the spin model for the _catching_up_ phase in the view change_ Wed Sep 28 17:46:51 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-28-17-46-51-223008000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-28-17-46-51-223008000-PDT.html [dnoblet] Added the TLA model for the _catching_up_ phase of the view change protocol._ Thu Sep 29 02:12:10 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-29-02-12-10-008121000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-29-02-12-10-008121000-PDT.html [crt] More changes to the model._ Thu Sep 29 18:01:22 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-29-18-01-22-082899000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-29-18-01-22-082899000-PDT.html [dnoblet] Added support for detecting old replies that we have timed out on._ Thu Sep 29 18:18:25 PDT 2005 http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-29-18-18-25-737599000-PDT.html http://svn.metaprl.org/commitlogs/mojavefs/2005-09/2005-09-29-18-18-25-737599000-PDT.html