Found and fixed a bug

harmony_model_checker/charm/charm.c

@@ -1497,7 +1497,9 @@ void path_recompute(struct global *global){
  pid = global->oldpid;
  }
  else {
+ // printf("Search for %p\n", (void *) ctx);
  for (pid = 0; pid < global->nprocesses; pid++) {
+ // printf("%d: %p\n", pid, (void *) global->processes[pid]);
  if (global->processes[pid] == ctx) {
  break;
  }
@@ -1508,6 +1510,9 @@ void path_recompute(struct global *global){
  printf("PID %p %u %u\n", (void *) ctx, pid, global->nprocesses);
  panic("bad pid");
  }
+ else {
+ // printf("Found %d\n", pid);
+ }
  assert(pid < global->nprocesses);
 
  macro->tid = pid;
@@ -1527,6 +1532,8 @@ void path_recompute(struct global *global){
  );
  assert(global->processes[pid] == e->after || e->after == 0);
 
+ // printf("Set %d to %p\n", pid, (void *) e->after);
+
  // Copy thread state
  macro->nprocesses = global->nprocesses;
  macro->processes = copy(global->processes, global->nprocesses * sizeof(hvalue_t));
@@ -3701,6 +3708,8 @@ int exec_model_checker(int argc, char **argv){
 
  printf("* Phase 3: analysis\n");
 
+ bool computed_components = false;
+
  // If no failures were detected (yet), determine strongly connected components
  // and look for non-terminating states.
  if (global->failures == NULL) {
@@ -3710,6 +3719,7 @@ int exec_model_checker(int argc, char **argv){
  }
  double now = gettime();
  tarjan(global);
+ computed_components = true;
 
  // Compute shortest path to initial state for each node.
  shortest_path(global);
@@ -3931,7 +3941,10 @@ int exec_model_checker(int argc, char **argv){
  struct node *node = global->graph.nodes[i];
  assert(node->id == i);
  fprintf(df, "\nNode %d:\n", node->id);
- fprintf(df, " component: %d\n", node->u.ph2.component);
+ if (computed_components) {
+ fprintf(df, " component: %d\n", node->u.ph2.component);
+ }
+ fprintf(df, " len to parent: %d\n", node->u.ph2.len);
  if (node->u.ph2.u.to_parent != NULL) {
  fprintf(df, " ancestors:");
  for (struct node *n = node->u.ph2.u.to_parent->src;; n = n->u.ph2.u.to_parent->src) {
@@ -3942,7 +3955,21 @@ int exec_model_checker(int argc, char **argv){
  }
  fprintf(df, "\n");
  }
- fprintf(df, " vars: %s\n", value_string(node_state(node)->vars));
+ struct state *state = node_state(node);
+ fprintf(df, " vars: %s\n", value_string(state->vars));
+ fprintf(df, " contexts:\n");
+ for (unsigned int i = 0; i < state->bagsize; i++) {
+ fprintf(df, " %"PRI_HVAL": %u\n", state_contexts(state)[i], multiplicities(state)[i]);
+ }
+ if (state->stopbag != VALUE_DICT) {
+ fprintf(df, " stopbag:\n");
+ unsigned int size;
+ hvalue_t *vals = value_get(state->stopbag, &size);
+ size /= 2 * sizeof(hvalue_t);
+ for (unsigned int i = 0; i < size; i++) {
+ fprintf(df, " %"PRI_HVAL": %d\n", vals[2*i], (int) VALUE_FROM_INT(vals[2*i+1]));;
+ }
+ }
  // fprintf(df, " len: %u %u\n", node->len, node->steps);
  if (node->failed) {
  fprintf(df, " failed\n");
@@ -4058,7 +4085,9 @@ int exec_model_checker(int argc, char **argv){
  }
  fprintf(out, " {\n");
  fprintf(out, " \"idx\": %d,\n", node->id);
- fprintf(out, " \"component\": %d,\n", node->u.ph2.component);
+ if (computed_components) {
+ fprintf(out, " \"component\": %d,\n", node->u.ph2.component);
+ }
 #ifdef notdef
  if (node->parent != NULL) {
  fprintf(out, " \"parent\": %d,\n", node->parent->id);

harmony_model_checker/charm/ops.c

@@ -1375,11 +1375,26 @@ void op_Go(
  ctx_push(copy, result);
  copy->stopped = false;
  // TODO. Check success of context_add
- context_add(state, value_put_context(&step->engine, copy));
+ hvalue_t context = value_put_context(&step->engine, copy);
+ context_add(state, context);
 #ifdef HEAP_ALLOC
  free(buffer);
 #endif
  step->ctx->pc++;
+
+ if (step->keep_callstack) {
+ // Find the process
+ unsigned int pid;
+ for (pid = 0; pid < global->nprocesses; pid++) {
+ if (global->processes[pid] == ctx) {
+ global->processes[pid] = context;
+ break;
+ }
+ }
+ if (pid >= global->nprocesses) {
+ panic("op_Go: can't find process");
+ }
+ }
 }
 
 void op_Finally(const void *env, struct state *state, struct step *step, struct global *global){
@@ -2147,6 +2162,7 @@ void op_Spawn(
  global->processes = realloc(global->processes, (global->nprocesses + 1) * sizeof(hvalue_t));
  global->callstacks = realloc(global->callstacks, (global->nprocesses + 1) * sizeof(struct callstack *));
  global->processes[global->nprocesses] = context;
+ // printf("Add %d %p\n", global->nprocesses, (void *) context);
  struct callstack *cs = new_alloc(struct callstack);
  cs->pc = pc;
  cs->arg = arg;

harmony_model_checker/charm/value.c

@@ -1747,9 +1747,11 @@ void context_remove(struct state *state, hvalue_t ctx){
  (char *) &state_contexts(state)[state->bagsize + 1] + i + 1,
  state->bagsize - i);
  }
- break;
+ return;
  }
  }
+ // TODO. this can happen with invariant contexts
+ // panic("context_remove: can't find context");
 }
 
 // Add context 'ctx' to the state's context bag. May fail if there are too

runall.py

@@ -17,7 +17,7 @@
  { "args": "code/naiveTurn.hny", "issue": "Non-terminating state", "nstates": 28 },
  { "args": "code/Peterson.hny", "issue": "No issues", "nstates": 104 },
  { "args": "code/PetersonBroken.hny", "issue": "Safety violation", "nstates": 126 },
- { "args": "code/PetersonInductive.hny", "issue": "No Issues", "nstates": 4 },
+ { "args": "code/PetersonInductive.hny", "issue": "No issues", "nstates": 104 },
  { "args": "code/csonebit.hny", "issue": "Active busy waiting", "nstates": 73 },
  { "args": "code/PetersonMethod.hny", "issue": "No issues", "nstates": 104 },
  { "args": "code/hanoi.hny", "issue": "Safety violation", "nstates": 28 },
@@ -29,7 +29,7 @@
  { "args": "-msynch=synchS code/UpLock.hny", "issue": "No issues", "nstates": 58 },
  { "args": "code/spinlock.hny", "issue": "No issues", "nstates": 473 },
  { "args": "code/xy.hny", "issue": "Safety violation", "nstates": 19 },
- { "args": "code/atm.hny", "issue": "Safety violation", "nstates": 128 },
+ { "args": "code/atm.hny", "issue": "Invariant violation", "nstates": 1832 },
  { "args": "code/queuedemo.hny", "issue": "No issues", "nstates": 80 },
  { "args": "code/setobjtest.hny", "issue": "No issues", "nstates": 217 },
  { "args": "-msetobj=linkedlist code/setobjtest.hny", "issue": "No issues", "nstates": 9495 },
@@ -44,7 +44,7 @@
  { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 },
  { "args": "-B queue4.hfa -m queue=queueconc code/qtestpar.hny", "issue": "No issues", "nstates": 66530 },
  { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 },
- { "args": "-B queue4.hfa -m queue=queueMS code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 },
+ { "args": "-B queue4.hfa -m queue=queueMS code/qtestpar.hny", "issue": "No issues", "nstates": 99816 },
  { "args": "-mqueue=queuebroken code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 },
  { "args": "code/RWtest.hny", "issue": "No issues", "nstates": 135 },
  { "args": "-mRW=RWsbs code/RWtest.hny", "issue": "No issues", "nstates": 1757 },
@@ -84,7 +84,7 @@
  { "args": "-msynch=synchS code/trap6.hny", "issue": "No issues", "nstates": 554 },
  { "args": "code/hw.hny", "issue": "No issues", "nstates": 23864 },
  { "args": "code/abptest.hny", "issue": "No issues", "nstates": 2778 },
- { "args": "code/leader.hny", "issue": "Safety violation", "nstates": 117 },
+ { "args": "code/leader.hny", "issue": "No issues", "nstates": 33005 },
  { "args": "-mstack=stack1 code/stacktest.hny", "issue": "No issues", "nstates": 2 },
  { "args": "-mstack=stack2 code/stacktest.hny", "issue": "No issues", "nstates": 2 },
  { "args": "-mstack=stack3 code/stacktest.hny", "issue": "No issues", "nstates": 2 },
@@ -106,8 +106,9 @@
  if t["issue"] != hco["issue"]:
  print("Different issue (was %s)??? Aborting further tests" % t["issue"])
  break
- if min(t["nstates"], hco["nstates"]) / max(t["nstates"], hco["nstates"]) < .9:
+ if t["issue"] != "Safety violation" and min(t["nstates"], hco["nstates"]) / max(t["nstates"], hco["nstates"]) < .9:
  print("#states very different (was %d)??? Aborting further tests" % t["nstates"])
+ break
  else:
  print("Error code %d, aborting further tests" % cp.returncode)
  print("Output: ", cp.stdout)