LARA

• P: Propose
• R: ProposeResponse (i.e. Promise)
• A: Accept
• L: Learn
• C: Chosen value

maysam@nslrack52:~/secondRun/pastryNode2$ ~/analyzeLog.sh

NODE_NUM 3

DIR_PREFIX /home/maysam/secondRun/pastryNode

duration: 25

LIVE_CNT is 0

awk: (FILENAME=- FNR=2) fatal: division by zero attempted awk: (FILENAME=- FNR=2) fatal: division by zero attempted awk: fatal: division by zero attempted QUERY_CNT is 16

AVOID_CNT is 2

FALSE_AVOID_CNT is 1

_1STEP_RUN_CNT is 15

_1STEP_AVOID_CNT is 0

0

180:1221237931.799641 07 [TRACE::Paxos::propose::(demux)] Firing Transition downcall propose [ guards : (true) ] void propose(mace::string const & key, mace::string const & value, registration_uid_t rid)

267:REPRODUCE case 2

334:REPRODUCE case 3

423:REPRODUCE case 5

567:REPRODUCE case 6

684:REPRODUCE case 7

754:REPRODUCE case 10

1

171:REPRODUCE case 4

238:REPRODUCE case 9

1078:1221237945.811295 07 [TRACE::Paxos::propose::(demux)] Firing Transition downcall propose [ guards : (true) ] void propose(mace::string const & key, mace::string const & value, registration_uid_t rid)

1162:REPRODUCE case 12

1248:REPRODUCE case 13

2

816:REPRODUCE case 14 =⇒ It is avoided

Bug is Reported here

depths of 11, 3419 in 6

depths of 12, 7111 in 16

depths of 13, 12242 in 40

depths of 14, 19061 in 73

depths of 15, 27726 in 116

depths of 16, 38328 in 172

depths of 17, 51130 in 242

depths of 18, 66616 in 330

depths of 19, 85838 in 443

    void PaxosService::printState(std::ostream& __out) const {
      __out << "state=" << getStateName(state) << std::endl;
      //__out << "prepared=";  mace::printState(__out, &(prepared), (prepared));
      //__out << "accepted=";  mace::printState(__out, &(accepted), (accepted));
      //__out << "proposals=";  mace::printState(__out, &(proposals), (proposals));
      //__out << "learnedValues=";  mace::printState(__out, &(learnedValues), (learnedValues));
      __out << "chosenValues=";  mace::printState(__out, &(chosenValues), (chosenValues));
      __out << "chosenValue=";  mace::printState(__out, &(chosenValue), (chosenValue));
      //__out << "__snapshots_logicalclock=";  mace::printState(__out, &(__snapshots_logicalclock), (__snapshots_logicalclock));
      __out << std::endl;
      if(_printLower) {
        _m.printState(__out);
        _mu.printState(__out);
        _t.printState(__out);
      }
      return;
    }

#Definitely set this one!

MACE_PRINT_HOSTNAME_ONLY = 1

#For more verbosity use higher numbers. But the default is very verbose on replay.

#MACE_LOG_LEVEL = 1

#Control network and node errors

#USE_UDP_REORDER = 1

#USE_UDP_ERRORS = 1

#USE_NET_ERRORS=1 # specifically TCP errors

#SIM_NODE_FAILURE=1

#Whether the search should use best-first or not – turning on is less tested, but can be faster at the expense of more memory

USE_BEST_FIRST = 0

MACE_PORT=5377 #10201 #Just some random port number

max_num_steps=20000 #How many steps before the path is considered dead

#Controlls how often status is printed out – the path number is masked with this number, and if it's 0 prints path status

#search_print_mask=0

#search_print_mask=15

#search_print_mask=255

search_print_mask=4095

#When set to 1, prints the serch prefix to a file (prefixN.path) for each path found which leads to a live state

PRINT_SEARCH_PREFIX=0

#Controls search features. Recommended to leave these on.

#USE_RANDOM_WALKS=1

USE_GUSTO=1

USE_STATE_HASHES=1

#NUM_RANDOM_PATHS=60 # The number of paths to attempt at a prefix length before declaring a prefix dead.

#When set, the model checker will stop after exploring this number of paths.

MAX_PATHS=200000000

#MAX_PATHS=200

#MAX_PATHS=50000

#MAX_PATHS=1000000

#The divergence monitor will signal errors when transitions take

#longer than divergence_timeout. A kind of deadlock detector.

RUN_DIVERGENCE_MONITOR = 1

divergence_assert = 1 # causes a divergence to end the execution, as opposed to allowing it to continue to see if the transition will complete.

divergence_timeout = 30 # how long is considered too long to run a single transition

#Which test to run

#CHECKED_SERVICE=Pastry

#CHECKED_SERVICE=Chord

#CHECKED_SERVICE=RandTree

CHECKED_SERVICE=Paxos

#num_nodes=100 #number of nodes to create

queue_size=100000 #commonly used to pass into the SimulatedTCP service for buffer size (in # messages) before dropping them.

#You can also set service-specific parameters here:

#MaceTransport

#messageCount = 16

#messageSize = 1600

#useRTS = 1

#CHECKED_SERVICE=MaceTransport

#Trace options

#TRACE_ALL=1

#TRACE_SUBST=ERROR

#TRACE_SUBST=::forward::(demux) ::deliver::(demux) ::requestFlushedNotification ::expire ::maceInit ::route (downcall) (upcall) (routine) (timer) Propert Quantification SimulatorUDPService logThread monitor Simulator SimulateEventEnd SimulateEventBegin NumberGen getReadyNodes SimNetwork SimScheduler SimApplication SimTransportApp

#TRACE_SIMULATOR=1

#TRACE_STATE=1

#Parameters for using the replay run – the name of the file to provide the sequence

#RANDOM_REPLAY_FILE=- # a '-' means it will read the file from standard input. mdb uses this for live-replays.

#RANDOM_REPLAY_FILE=error1.path

#RANDOM_REPLAY_FILE=error2.path

#LAST_NAIL_REPLAY_FILE=error1.path # the path to search around. run-modelchecker uses this internally

#Parameters for using the state space search: Search depth and an optional sequence to start with.

SEARCH_DEPTH=11 # controls the bounded search depth increment. Is both the starting depth and the depth increment

#RANDOM_UTIL_PREFIX_FILE=prefix1.path # start the search after executing the path in prefix1.path

#RANDOM_UTIL_PREFIX_SEARCH=1 2 1 2 1 0 1 3 1 0 2 2 2 0 0 # Can also specify the path here. Advanced use only

#RANDOM_UTIL_START_SEARCH=1 1 3 0 0 1 1 1 2 0 2 1 0 0 0 # Can be used to skip ahead in the search. Advanced use only

#There are a variety of other configuration options for advanced users. See the code for these.

#Added by Maysam Yabandeh

#nodeIP(0)=nslrack52

#nodeIP(1)=nslrack04

#nodeIP(2)=nslrack06

#nodeIP(3)=nslrack07

#nodeIP(4)=nslrack08

#myNodeId=0

MAX_DEAD_PATHS=1000

#FIRST_PATH_TO_BUG_IS_ENOUGH=1

#I_USE_ONLY_LOCAL_PROPERTIES=1

DONT_EXIT=1

#LET_MODELCHECKER_FINISH_HIS_JOB=1

#child_size=5

#DEBUGGER_MODE=1

FIX_ISSAFE_INIT_BUG=1

#BACKUP_BUG_STATE=1

#START_APPLICATION_FROM_INITIAL_SCENARIO=1

FIX_ORIGINAL_ID_BUG=1

INIT_NETWORK=1

######LIVENESS_RETURN_VALUE_DOES_NOT_MATTER=1

MAX_LIVENESS_PENALTY=10

#

1STEP_CHECK=1

######PROBABILISTIC_ACTION_SELECTION=1

#

SERIAL_SEARCH=1

#SUPER_SERIAL_SEARCH=1

EXECUTION_STEERING=1

RUN_PARALLEL_MODELCHECKER=1

CONSIDER_ES_ACTION_CONSEQUENCES=1

#

#never enable CONSIDER_ES_ACTION_CONSEQUENCES && SUPER_SERIAL_SEARCH, the code is not update for both of them to be enabled

bandwidthLimit=1000000

REPRODUCE_MODE=1

num_nodes=3 #number of nodes to create

nodeIP(1)=10.0.0.5

nodeIP(0)=10.0.0.1

nodeIP(2)=10.0.0.9

myNodeId=2